Une affirmation fondatrice, informelle, selon laquelle toute fonction calculable par une procédure finie et mécanique (un algorithme effectif) peut être calculée par une machine de Turing ; elle identifie la calculabilité au sens intuitif et algorithmique à la calculabilité par Turing.

Principe

Qu'un modèle formel unique (machines de Turing, équivalemment le lambda-calcul, fonctions récursives, etc.) saisit le concept informel de calcul effectif.

Démonstration

Exemple concret : tout algorithme écrit dans un langage de programmation moderne peut être traduit en une procédure équivalente pour une machine de Turing qui, pour une encodage des entrées, reproduit le même comportement en sortie ; l'équivalence se montre en construisant un simulateur de la sémantique du langage sur une machine de Turing universelle.

Mauvaise application

Prétendre que la thèse de Church–Turing est un théorème mathématique prouvé concernant tous les processus physiques, ou l'utiliser pour affirmer des bornes de temps ou d'espace (complexité) plutôt que des résultats de calculabilité ; ou affirmer qu'elle exclut toute hypercalcul sans justification empirique.

Conséquence

Fournit une base acceptée pour la théorie de la calculabilité et pour classer les problèmes en décidables ou indécidables ; justifie l'usage des machines de Turing (ou de modèles équivalents) comme canonique pour discuter de ce qui est calculable en principe.

Inversion

L'inversion affirmerait l'existence d'une procédure effective, décrite intuitivement, qu'aucune machine de Turing ne pourrait mettre en œuvre — c'est‑à‑dire un algorithme faisable hors de la calculabilité de Turing.

Limite

C'est une thèse, non un théorème formel : elle porte sur la définition d'algorithme effectif et ne traite pas des bornes de ressources (temps/espace), du calcul probabiliste ou approximatif, ni de la réalisabilité physique ; les variantes qui concernent des limites physiques (thèses physique de Church–Turing) sont distinctes et empiriques.

Tension sémantique

Tension entre « calculable en principe » (équivalence théorique aux machines de Turing) et « calculable en pratique » (calcul sous contraintes de ressources, physique ou approximatif), et entre une assertion descriptive et une affirmation normative/empirique sur les systèmes physiques.

Synthèse

La thèse de Church–Turing affirme que l'idée informelle d'algorithme effectif est capturée par la calculabilité de Turing : elle organise la théorie de la calculabilité en assimilant les procédures algorithmique intuitives au modèle formel des machines de Turing, tout en laissant ouvertes les questions de ressources et de réalisation physique.