Church Alonzo

Dans les années 1930, aux États-Unis, Alonzo Church cherche à décrire rigoureusement ce qu’un calcul peut accomplir. Il crée le lambda-calcul : un petit langage formel où une fonction reçoit une entrée et produit un résultat.

Cette idée aide à tracer une frontière majeure : certains problèmes peuvent être résolus par une procédure de calcul, tandis que d’autres ne le peuvent pas. Elle demeure au cœur de l’informatique théorique.

Alonzo Church (Washington, 1903 – Hudson, 1995) est un mathématicien et logicien américain. Dans les années 1930, il introduit le lambda-calcul, un système formel qui décrit la définition d’une fonction et son application à un argument. Ce modèle est devenu une base théorique de la sémantique des langages de programmation fonctionnels.

La thèse de Church-Turing affirme que toute fonction effectivement calculable peut être calculée par une machine de Turing ou, de façon équivalente, définie dans le lambda-calcul. Elle relie ainsi deux modèles fondamentaux du calcul.

En 1936, Church démontre que le problème de la décidabilité de la logique du premier ordre est indécidable : il n’existe pas de procédure générale qui fournisse toujours la décision recherchée. Ce résultat, appelé théorème de Church, est parallèle au théorème d’incomplétude de Gödel. Longtemps professeur à Princeton, puis professeur à l’Université de Californie à Los Angeles, Church a formé de nombreux mathématiciens et logiciens influents.

Considérons une fonction identité, qui rend exactement l’argument reçu. La lettre x désigne sa variable liée et la lettre a désigne l’argument auquel elle est appliquée.

Données :
la fonction identité est $\lambda x\mathrm{.}x\backslash lambda\; x.x$ ;
l’argument choisi est a.

1. On applique la fonction à l’argument : $(\lambda x\mathrm{.}x)a(\backslash lambda\; x.x)\backslash ,a$.

2. On remplace, dans le corps de la fonction, la variable liée x par l’argument a.

3. La réduction donne $(\lambda x\mathrm{.}x)a\to a(\backslash lambda\; x.x)\backslash ,a\; \backslash to\; a$. La figure résume cette substitution en distinguant l’expression initiale, l’opération et le résultat.

Le résultat est donc l’argument a, sans modification. Pour contrôler la règle, on recommence avec un autre argument, nommé b : la même substitution rend b.

Dans l’étude des langages de programmation fonctionnels, le lambda-calcul sert de modèle pour décrire la signification d’une fonction et de son application. On le préfère lorsqu’on veut suivre les substitutions dans une expression.

Pour raisonner sur ce qui est calculable, on peut choisir le lambda-calcul ou la machine de Turing. Le premier met les fonctions au premier plan ; la seconde décrit le calcul à l’aide d’une machine abstraite. La thèse de Church-Turing affirme leur équivalence quant aux fonctions effectivement calculables.

Face à un problème de décision, le bon geste consiste à demander s’il existe une procédure générale qui termine toujours avec une réponse. Le résultat de Church montre que cette exigence échoue pour la décidabilité de la logique du premier ordre.

Alonzo Church et le lambda-calcul. Church est la personne ; le lambda-calcul est le système formel qu’il a créé. Une date ou un poste universitaire concerne Church, tandis qu’une définition ou une application de fonction concerne le lambda-calcul.

Thèse de Church-Turing et théorème de Church. La thèse porte sur les fonctions effectivement calculables et l’équivalence de modèles de calcul. Le théorème de 1936 établit l’indécidabilité d’un problème de logique du premier ordre.

Théorème de Church et théorème d’incomplétude de Gödel. La source les présente comme des résultats parallèles, non comme deux noms du même théorème. Le premier répond à une question de décidabilité ; le second est le résultat associé à Gödel.

Une thèse n’est pas ici un algorithme. La thèse de Church-Turing caractérise ce que signifie « effectivement calculable ». Elle ne fournit pas, à elle seule, une procédure pour résoudre chaque problème particulier. Il faut encore exhiber un calcul dans un modèle formel.

Équivalence ne signifie pas même écriture. Une machine de Turing et une expression du lambda-calcul n’ont pas la même forme. Leur équivalence concerne les fonctions qu’elles peuvent calculer ; il ne faut donc pas chercher une ressemblance visuelle entre leurs descriptions.

Indécidable ne signifie pas que chaque cas est insoluble. Le théorème de Church exclut une procédure générale de décision pour la logique du premier ordre. Pour un cas particulier, il faut étudier les données propres au problème au lieu de conclure automatiquement à l’impossibilité.

La fiche machine de Turing présente l’autre modèle de calcul cité par la thèse de Church-Turing.

La fiche décidabilité et indécidabilité approfondit la frontière entre problèmes dotés d’une procédure générale de décision et problèmes indécidables.

L’article Les théorèmes d'incomplétude de Gödel éclaire le résultat auquel la définition source rapproche le théorème de Church.