La thèse de Church-Turing

La thèse de Church-Turing affirme que toute fonction calculable par une procédure effective est calculable par une machine de Turing, assimilant ainsi l'idée informelle d'un algorithme à un modèle mathématique précis.

Definition

La thèse de Church-Turing est l'affirmation selon laquelle les fonctions intuitivement calculables sont exactement les fonctions calculables par une machine de Turing, ou de manière équivalente par le calcul lambda ou les fonctions récursives générales ; il s'agit d'une thèse plutôt que d'un théorème car la notion intuitive n'est pas formellement définie.

Scope

Ce sujet aborde l'énoncé de la thèse, les preuves convergentes issues de modèles proposés indépendamment, la distinction entre la thèse originale concernant la calculabilité effective et des variantes physiques ou théoriques de la complexité plus fortes, ainsi que le rôle de la thèse comme pont entre l'intuition et la preuve formelle en théorie de la calculabilité.

Core questions

• Que signifie identifier la notion informelle d'algorithme à un modèle formel ?
• Pourquoi la convergence de modèles indépendants est-elle considérée comme une preuve solide de la thèse ?
• La thèse est-elle un théorème mathématique, une définition ou une affirmation empirique ?
• Comment les versions physiques et théoriques de la complexité vont-elles au-delà de l'énoncé original ?

Key theories

Convergence des modèles de calcul

Il a été démontré que les machines de Turing, le calcul lambda de Church et les fonctions récursives de Gödel et Herbrand définissent exactement la même classe de fonctions, et cet accord indépendant constitue la principale preuve avancée pour la thèse.

Statut de thèse, non de théorème

Étant donné que la notion intuitive de procédure effective n'est pas formalisée, l'affirmation ne peut être prouvée ; elle est acceptée comme une identification fondamentale qui permet aux arguments algorithmiques informels de remplacer les constructions formelles de machines de Turing.

Clinical relevance

La thèse autorise la pratique courante de décrire les algorithmes en pseudocode de haut niveau plutôt qu'en tant que machines de Turing, étant donné que toute notion raisonnable de procédure effective est supposée être équivalente à une machine de Turing ; elle encadre également les débats sur la question de savoir si des dispositifs physiques ou quantiques pourraient un jour calculer au-delà de ce qui est calculable par une machine de Turing.

History

En 1936, Church a proposé d'identifier la calculabilité effective à la lambda-définissabilité, et Turing a indépendamment défendu son modèle de machine ; par la suite, Turing, Kleene et d'autres ont prouvé l'équivalence de ces modèles et des fonctions récursives. Gödel, initialement sceptique, en est venu à considérer l'analyse de Turing comme concluante, et l'affirmation combinée est devenue connue sous le nom de thèse de Church-Turing.

Debates

Le calcul physique peut-il dépasser la limite de Turing ?

La thèse originale concerne les procédures effectives, mais des versions physiques plus fortes affirment qu'aucun dispositif physiquement réalisable ne peut calculer des fonctions non calculables par une machine de Turing. Les propositions d'hypercalcul et les implications de la mécanique quantique maintiennent cette affirmation étendue contestée, même si la thèse classique reste essentiellement incontestée.

Key figures

• Alonzo Church
• Alan Turing
• Kurt Gödel
• Stephen Kleene

Seminal works

• church1936
• turing1937

Frequently asked questions

Pourquoi est-ce appelé une thèse plutôt qu'un théorème ?

Elle relie un modèle formel à l'idée informelle d'une procédure effective, et cette idée informelle n'a pas de définition mathématique sur laquelle prouver des choses. La preuve solide est que chaque tentative indépendante de formaliser le calcul a produit la même classe de fonctions, mais ce soutien est conceptuel plutôt qu'une preuve.

Les ordinateurs quantiques réfutent-ils la thèse de Church-Turing ?

Non. Les ordinateurs quantiques peuvent résoudre certains problèmes plus rapidement, mais ils calculent exactement la même classe de fonctions que les machines de Turing, de sorte que la thèse originale sur ce qui est calculable demeure valide. Ils concernent plutôt la version plus forte de la théorie de la complexité, qui s'intéresse à l'efficacité plutôt qu'à la calculabilité.