Thèse de Church

La thèse est formulée en disant que des règles formelles de calcul (machines de Turing, les fonctions λ-définissables, les fonctions récursives…) formalisent correctement la notion de méthode effective de calcul, ou de calculabilité[4].

On considère généralement[5] que la notion intuitive de méthode effective de calcul correspond aux caractéristiques suivantes :

1. l'algorithme consiste en un ensemble fini d'instructions simples et précises qui sont décrites avec un nombre limité de symboles ;
2. l'algorithme doit toujours produire le résultat en un nombre fini d'étapes ;
3. l'algorithme peut en principe être suivi par un humain avec seulement du papier et un crayon ;
4. l'exécution de l'algorithme ne requiert pas d'intelligence de l'humain sauf celle qui est nécessaire pour comprendre et exécuter les instructions.

Un exemple d'une telle méthode est l'algorithme d'Euclide pour déterminer le plus grand commun diviseur d'entiers naturels ou celui qui détermine pour un entier n la longueur de la suite de Goodstein qui commence en n.

La thèse de Church est énoncée clairement par Church dans le résumé de la conférence qu'il a donnée à l'American Mathematical Society en 1935[6] :

« ... Gödel a proposé ... une définition du terme fonction récursive dans un sens très général. Dans cet article un sens de fonction récursive très générale sur les entiers positifs, qui est essentiellement celui de Gödel, est adopté. Et il est affirmé que la notion de fonction effectivement calculable sur les entiers positifs devrait être identifiée avec celle de fonction générale récursive puisque toutes les autres notions de calculabilité effective se réduisent à des notions qui sont ou bien équivalentes ou bien plus faibles que la récursivité. »

Dans son article de 1936 Church écrit[7] - [8] :

« Le fait cependant que deux définitions largement différentes et (du point de vue de l'auteur) tout aussi naturelles de la calculabilité effective se révèlent être équivalentes ajoutent de la force aux raisons invoquées ci-dessous de croire qu'elles constituent une caractérisation aussi bien générale que cohérente de sa compréhension intuitive habituelle. »

Dans son article de 1943 Prédicats et quantificateurs récursifs (titre original Recursive Predicates and Quantifiers) Stephen Kleene (repris dans L'Indécidable, titre original The Undecidable) a utilisé le premier la terminologie « thèse » et l'a attribué à Church :

« Ce fait heuristique [les fonctions récursives générales sont effectivement calculables]… a conduit Church à énoncer la thèse suivante »

— [note 22 de Kleene], La même thèse est implicite dans la description des machines de Turing [note 23 de Kleene].

« THÈSE I. Chaque fonction effectivement calculable (chaque prédicat effectivement décidable) est récursive générale [les italiques sont de Kleene] »

« Puisque nous recherchions une définition mathématique précise de l'expression effectivement calculable (effectivement décidable), nous prendrons cette thèse comme sa définition […] »

— Kleene, dans l'indécidable, p. 274

La note 22 de Kleene fait référence à l'article de Church tandis que sa note 23 fait référence à l'article d'Alan Turing. Il continue en notant que

« … la thèse n'est qu'une hypothèse -- une constatation déjà soulignée par Post et par Church »

— [sa note 24, dans L'indécidable, P. 274], Il fait référence à l'article de Post (1936) et aux définitions formelles de l'article de Church Formal definitions in the theory of ordinal numbers, Fund. Math. vol. 28 (1936) pp.11-21 (voir réf. 2, P. 286, de l'indécidable).

Dans son article de 1936 « sur des nombres calculables, avec une application à l'Entscheidungsproblem » (titre original « On Computable Numbers, with an Application to the Entscheidungsproblem ») Turing a formalisé la notion d'algorithme (alors appelée « calculabilité effective »), en introduisant les machines dites maintenant de Turing. Dans cet article il écrit en particulier à la page 239 :

« Une suite calculable γ est déterminée par une description d'une machine qui calcule γ […] et, en fait, n'importe quelle suite calculable est susceptible d'être décrite en termes d'une table [c'est-à-dire d'une machine de Turing]. »

Ce qui est la version de Turing de la thèse de Church, qu'il ne connaissait pas à l'époque.

Church avait démontré lui aussi quelques mois plus tôt l'insolvabilité du problème de la décision dans « une note sur l'Entscheidungsproblem »[7] pour cela il avait utilisé les fonctions récursives et les fonctions λ-définissables pour décrire formellement la calculabilité effective. Les fonctions λ-définissables avait été introduites par Alonzo Church et Stephen Kleene (Church 1932, 1936a, 1941, Kleene 1935) et les fonctions récursives avaient été introduites par Kurt Gödel et Jacques Herbrand (Gödel 1934, Herbrand 1932). Ces deux formalismes décrivent le même ensemble de fonctions, comme cela a été démontré dans le cas des fonctions sur les entiers positifs par Church et Kleene (Church 1936a, Kleene 1936). Après avoir entendu parler de la proposition de Church, Turing a pu rapidement esquisser une démonstration que ses machines de Turing décrivent en fait le même ensemble de fonctions (Turing 1936, 263 et suivantes). Dans un article paru en 1937[λdef 1] il montre l'équivalence des trois modèles : fonctions λ-définissables, machines de Turing[9] et fonctions générales récursives au sens de Herbrand et Gödel. Rosser[10] résume les sentiments des protagonistes : « Une fois l'équivalence de la récursivité générale et de la λ-définissabilité établie, Church, Kleene et moi nous attendions à ce que Gödel nous rejoigne pour supporter la thèse de Church. Gödel avait cependant encore des réserves et ce n'est qu'au moins deux ou trois ans plus tard, après les travaux de Turing, que Gödel devint finalement un adepte (comme le devint aussi Turing). »

Turing écrit[λdef 2] en 1937 : « L'identification des fonctions « effectivement calculables » avec les fonctions calculables [c-à-d. définies par une machine de Turing] est peut-être plus convaincante que l'identification avec les fonctions λ-définissables ou récursives générales. Pour ceux qui adoptent ce point de vue, la démonstration formelle de l'équivalence fournit une justification du calcul de Church et permet de remplacer les 'machines' qui engendrent des fonctions calculables par les λ-définitions qui sont plus commodes. »

On peut définir très formellement des fonctions (par exemple sur les entiers naturels) qui ne sont pas calculables. Elles prennent en général des valeurs tellement grandes que l'on ne peut pas les calculer et par conséquent on ne peut même pas « exprimer » les valeurs qu'elles prennent, car c'est leur définition qui le dit. La plus connue est celle dite du castor affairé. Pour simplifier, il s'agit de la taille du plus grand travail que peut faire une machine de Turing quand on lui donne une ressource limitée par n. Comme sa définition est obtenue comme une limite de ce que pourraient faire les machines de Turing, le nombre qu'elle produit ne peut pas être calculé, ni même sa valeur exacte exprimée, tout au plus les chercheurs arrivent-ils à donner des nombres qui lui sont inférieurs pour les plus petites valeurs de n (2, 3, 4, 5, péniblement 6).

Le nombre Oméga de Chaitin est un nombre réel parfaitement défini qui n'est pas calculable, précisément parce que sa construction dépend des réponses au problème semi-décidable de l'arrêt des machines de Turing.

On ne connaît pas de modèle de calcul plus puissant que les machines de Turing, c'est-à-dire qui serait en mesure de calculer des fonctions non-calculables par une machine de Turing. La thèse de Church physique pourrait être remise en cause par l'hypercalcul, mais les processus physiques utilisés par l'hypercalcul sont extrêmement spéculatifs et probablement à jamais impossibles à mettre en œuvre en pratique.

Inversement, il existe des modèles de calcul plus faibles que les machines de Turing. Par exemple la définition des fonctions récursives primitives propose implicitement un modèle de calcul : essentiellement celui des définitions par récurrence sur un paramètre. Or la fonction d'Ackermann est calculable, mais n'est pas récursive primitive.

Plus généralement, un système formel (comme un langage de programmation) qui ne permet de définir que des fonctions totales (comme Gallina le langage de Coq ou Agda (en)), c'est-à-dire que le calcul de ces fonctions s'arrête quelle que soit l'entrée ne peut pas être candidat à la thèse de Church, autrement dit, il n'est pas Turing-complet. La fonction d'évaluation des fonctions définies dans un système formel ne peut être définie dans ce même système formel. Par exemple, le système du calcul des constructions, bien qu'extrêmement riche et général (on peut pratiquement y formaliser toutes les mathématiques) ne peut pas être candidat à la thèse de Church, car il ne définit que des fonctions normalisantes, c'est-à-dire des fonctions dont le calcul s'arrête pour toute entrée[11].

Les différents modèles de calcul purement mathématiques élaborés pour modéliser la calculabilité ne prennent pas en compte de processus physiques. Comme l'ont montré Robin Gandy[12] , Nachum Dershowitz (en) et Yuri Gurevich (en)[13] les considérations physiques ne sont pas négligeables. Or, d'après le Principe de Church-Turing-Deutsch, tout processus physique fini peut être simulé par un mécanisme physique fini. C'est donc pour cela que l'informatique s'inspire de la physique classique, et utilise des bits et non des qbits (le modèle quantique "rompt le charme de la thèse de Church-Turing étendue"[14]).

En 1982, le physicien Richard Feynman s'est posé la question de savoir si les modèles de calcul pouvaient calculer l'évolution de processus quantiques. Il est parvenu à démontrer que cela était possible, mais de manière inefficace, inapplicable en pratique. Or, la nature est visiblement capable de « calculer » cette évolution de manière efficace. La question se pose donc inévitablement de savoir si les processus quantiques sont en relation avec une autre forme de calculabilité et s'ils remettent en cause la forme physique de la thèse de Church.

Pour explorer cette question, il est nécessaire d'élaborer un modèle de calcul prenant en compte les particularités de la mécanique quantique, et capable de calculer les processus quantiques efficacement. Muni de ce modèle mathématique, on peut alors étudier ses relations avec les modèles classiques de calcul, sur le plan de la calculabilité (ce que les modèles sont capables de calculer ou non), l'universalité (si une machine peut simuler toutes les autres efficacement), et de la complexité (dans quels ordres de temps et de mémoire les problèmes peuvent-ils être calculés).

Les premières tentatives de créer des modèles de calcul quantiques ont eu lieu au début des années 1980 par Paul Benioff[15]. C'était un modèle de machine de Turing réversible, prenant en compte une des particularités majeures de la mécanique quantique : l'unitarité qui implique que les calculs quantiques doivent être réversibles (contrairement aux calculs classiques). C'est-à-dire que, connaissant un résultat et la série d'opérations y ayant mené, un calcul quantique peut toujours être déroulé en arrière jusqu'à retrouver les données initiales[16]. Mais il manquait encore des ingrédients pour aboutir à un véritable modèle de calcul quantique : même si les calculs utilisaient la superposition quantique, les états des bits à chaque étape de calcul étaient dans un état classique « 0 » ou bien « 1 ».

En 1985, David Deutsch propose un véritable modèle de calcul quantique[17], reconnu comme étant le premier véritable modèle de machine de Turing quantique[18]. Dans cet article, Deutsch remarque que les calculateurs quantiques sont capables de produire un résultat que les machines de Turing classiques ne peuvent produire : générer un nombre purement aléatoire. Mais cela ne remet pas en cause la thèse de Church, car la génération d'un nombre aléatoire ne fait pas partie de ce qui est considéré comme un « calcul ».

Ce modèle de calcul a permis d'établir que les machines de Turing quantiques ne permettent pas de résoudre davantage de problèmes que les machines de Turing classiques. Elles sont même, d'un certain point de vue, moins complètes que les machines de Turing classiques car, si on désire utiliser le parallélisme quantique pour calculer plus rapidement certaines propriétés conjointes entre m valeurs binaires, alors il a été démontré en 1991 par Richard Jozsa[19] que seules ${\displaystyle 2^{2^{m}}-2^{m+1}}$ propriétés parmi les ${\displaystyle 2^{2^{m}}}$ propriétés conjointes possibles étaient calculables de cette manière, alors qu'elles le sont toutes avec une machine de Turing classique[20].