La thèse de Church est une thèse concernant la définition de la notion de calculabilité.
Dans une forme dite « physique », elle affirme que la notion physique de la calculabilité, définie comme étant tout traitement systématique réalisable par un processus physique ou mécanique, peut être exprimée par un ensemble de règles de calcul, défini de plusieurs façons dont on a pu démontrer mathématiquement qu'elles sont équivalentes.
Dans sa forme dite « psychologique », elle affirme que la notion intuitive de calculabilité, qui est liée à ce qu'un être humain considère comme effectivement calculable ou non, peut également être exprimée par ces mêmes ensembles de règles de calcul formelles.
Stephen Kleene fut le premier à nommer « thèse de Church » (en 1943 et 1952) ce que ce dernier présentait comme une définition de la calculabilité effective. Elle est également connue sous le nom plus récent de thèse de Church-Turing, terminologie proposée par certains spécialistesvoir Robert I. Soare, article cité. dans les années 1990. Bien que Church soit sans nul doute le premier, au début des années 1930, à avoir pensé pouvoir définir formellement la calculabilité intuitive (par la λ-définissabilité)Attesté pas une lettre de Church à Gödel de 1934, voir Soare, article cité., ce sont cependant l'article d'Alan Turing de 1936 et son modèle mécanique de calculabilité qui ont définitivement emporté l'adhésion, selon Gödel, Kleene et Church lui-même.
Formulation de la thèse
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é.
On considère généralement que la notion intuitive de méthode effective de calcul correspond aux caractéristiques suivantes : l'algorithme consiste en un ensemble fini d'instructions simples et précises qui sont décrites avec un nombre limité de symboles ; l'algorithme doit toujours produire le résultat en un nombre fini d'étapes ; l'algorithme peut en principe être suivi par un humain avec seulement du papier et un crayon ; 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.
Qu'est-ce qu'une thèse ? Une thèse consiste à affirmer, sans le démontrer, qu'une notion intuitive correspond exactement à une notion formelle. Toute démonstration est impossible, il est seulement possible de la falsifier ou d'apporter des arguments en faveur ou en défaveurp. 22. Un autre exemple de thèse consiste à affirmer que la notion intuitive de suite de nombres tirés au hasard correspond aux définitions formelles données par Gregory Chaitin ou Per Martin-Löfp. 3. Les caractéristiques intuitives ne sont pas une formalisation en soi, car elle contient des termes informels comme « instruction simple et précise », ou « intelligence requise pour exécuter les instructions ». On peut en revanche définir formellement ce qu'est un algorithme et pour cela on a le choix entre les diverses règles formelles de calcul citées au début de ce paragraphe. À ce stade, la thèse de Church affirme que les deux notions, intuitive de « méthode effective », et formelle (« règles de calcul », ou « algorithme »), concordent, apportant ainsi une définition rigoureuse du concept de calculabilité.
En effet, au début du , les mathématiciens utilisaient des expressions informelles comme effectivement réalisables. Il était donc important de trouver une formalisation rigoureuse de ce concept. Depuis les années 1940, les mathématiciens utilisent grâce à la thèse de Church une notion bien définie, celle de fonction calculable.
Les différentes formulations de la thèse de Church La thèse a d'abord été formulée pour le lambda-calcul, mais d'autres formalismes ont été proposés pour modéliser les fonctions calculables, par exemple les fonctions récursives, les machines de Turing, les machines de Post et les machines à compteurs. La plus surprenante est probablement celle proposée par Yuri Matiyasevich en résolvant le dixième problème de Hilbert. On peut montrer que toutes ces définitions, bien que fondées sur des idées assez différentes, décrivent exactement le même ensemble de fonctions. Ces systèmes, qui ont le même pouvoir d'expression que l'une quelconque de ces définitions équivalentes, sont dits Turing-équivalents ou Turing-complets.
Le fait que toutes ces tentatives pour formaliser le concept d'algorithme aient conduit à des résultats équivalents est un argument fort pour la thèse de Church.
Histoire
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 1935cité dans Wilfried Sieg, 2005, Church without dogma: axioms for computability, Carnegie Mellon University p. 4 :
Dans son article de 1936 Church écritAlonzo Church: A Note on the Entscheidungsproblem. J. Symb. Log. 1(1): 40-41 (1936)Robert I. Soare: Computability and Incomputability. CiE 2007: 705-715. :
Dans son article de 1943 Prédicats et quantificateurs récursifs (titre original ) Stephen Kleene (repris dans L'Indécidable, titre original ) a utilisé le premier la terminologie « thèse » et l'a attribué à Church :
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
Dans son article de 1936 (titre original ) 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 :
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 » 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 153-163. ; voir aussi Collected Works of A.M. Turing, tome Mathematical Logic. il montre l'équivalence des trois modèles : fonctions λ-définissables, machines de TuringLa terminologie est due à Church. et fonctions générales récursives au sens de Herbrand et Gödel. RosserIn Highlights of the History of the Lambda-Calculus, Annals of the History of Computing vol. 6, n°4, oct 1984. résume les sentiments des protagonistes :
Turing écritdans cet article en 1937 :
Les historiens ont tendance à oublier les travaux de Post, à la même époque, qui publia une première thèse sur la calculabilité en 1920, qu'il prolongea en 1936.Pour une discussion de la contribution dEmil Post, on lira ..
Des fonctions et nombres non calculables
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.
Autres modèles de calcul
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 changement de nom Coq ou ), 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.
Thèse de Church et calcul quantique
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 , et 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").
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.