Généralité et histoire

Church voulait définir formellement le concept (pré-théorique, philosophique, intuitif) de fonctions calculables. Une fonction définie sur les nombres naturels et à valeurs dans les nombres naturels, est considérée comme étant calculable, si on peut en principe la calculer, c'est-à-dire s'il existe une règle permettant de la calculer. Cette règle doit être publiquement communicable en un temps fini. Il est important de comprendre que cette ``définition" informelle est non-constructive. On demande que la règle existe en principe. On ne demande pas que la règle soit explicitement donnée. En particulier l'existence de la règle ne doit pas être explicite. Les fonctions sont considérées comme étant des objets mathématiques définis extensionnellement (par leur ensemble de couples). Par exemple la fonction constante $F$₀ qui envoie tout nombre $sur\; 0\; :$

$\{(0,0)\; (1,0)\; (2,0)\; (3,0)\; (4,0),\; (5,0),\; ...\},$

est trivialement calculable. Et, de même, la fonction $F$₁ qui envoie tout $sur\; 1\; :$

$\{(0,1)\; (1,1)\; (2,1)\; (3,1)\; (4,1),\; (5,1),\; ...\},$

est calculable. Donc la fonction $F$ suivante, présentée intensionnellement de la façon suivan$te\; :$

$F(x)=1\; si\; la\; conjecture\; de\; Goldbach\; est\; vraie=0\; sinon.$

est aussi calculable, malgré qu'à partir de cette présentation (ou ``intension" comme on dit dans le domaine) personne ne sait la calculer. $F$ est calculable, car, extensionnellement parlant $F$ est égale à $F$₀, ou $F$ est égale à $F$₁. La règle pour la calculer existe, mais à l'heure actuelle personne ne la connaît. On a déjà rencontré une situation similaire avec la définition du computationnalisme où on exige l'existence du niveau de substitution sans exiger qu'on puisse définir explicitement ce niveau. Pour définir mathématiquement la notion de fonctions calculables, il suffit donc de définir de façon précise ce qu'on entend par règle publiquement communicable en un temps fini. Church parvint à une définition de fonction calculable avec la notion formelle de fonctions lambda-définissables. A présent, on peut démontrer qu'une fonction est lambda-définissable si et seulement si elle est programmable (calculable par un ordinateur). Une version moderne de la thèse de Church est alors donnée $par\; :$

Une fonction de N dans N est calculable ssi elle est programmable.

Conceptuellement cette thèse est très forte: elle entraîne le théorème d'incomplétude de Gödel, ce que j'illustre plus bas, et de nombreux autres phénomènes d'incomplétude. Autrement $dit\; :si\; le\; théorème\; de\; Gödel,\; avait\; été\; faux,\; la\; thèse\; de\; Church\; serait\; elle-même\; fausse.\; Comme\; le\; théorème\; de\; Gödel\; étaient\; tout\; à\; fait\; inattendu\; dans\; la\; communauté\; des\; mathématiciens\; (à\; l\text{'}exception\; des\; précurseurs\; comme\; Post\; et\; Turing,\; mais\; aussi\; Markov),\; on\; peut\; dire\; que\; la\; thèse\; de\; Chuch\; fut\; tout\; autant\; inattendue.\; Historiquement,\; c\text{'}est\; Post,\; en\; 1922,\; qui\; est\; le\; premier\; à\; proposer\; la\; ``thèse\; de\; Church".\; Pour\; lui\; elle\; constituait\; une\; loi\; naturelle\; de\; l\text{'}esprit,\; et\; elle\; devait\; être\; justifiée\; par\; des\; considérations\; psychologiques.\; Il\; est\; aussi\; le\; premier\; à\; dériver\; de\; cette\; thèse\; le\; phénomène\; d\text{'}incomplétude.\; Il\; est\; encore\; le\; premier\; à\; ``réfuter"\; l\text{'}hypothèse\; du\; mécanisme\; avec\; l\text{'}incomplétude\; (comme\; Lucas\; et\; Penrose\; par\; exemple),\; et\; il\; est\; encore\; le\; premier\; à\; réaliser\; que\; cette\; réfutation\; est\; incorrecte\; (à\; la\; différence\; de\; Lucas\; et\; Penrose).\; Le\; travail\; de\; Post\; date\; de\; 1922,\; sera\; proposé\; et\; refusé\; à\; la\; publication\; en\; 1943.\; Il\; sera\; finalement\; publié\; en\; 1965\; après\; sa\; mort\; (en\; 1957),\; par\; Davis\; [Post,\; 1922,Davis,\; 1965].\; Avant\; que\; Gödel\; ne\; démontre\; en\; 1931\; son\; résultat\; d\text{'}incomplétude,\; Hilbert\; espérait\; qu\text{'}un\; formalisme\; assez\; puissant\; allait\; pouvoir\; sécuriser\; formellement\; les\; fondements\; des\; mathématiques.\; Russell\; et\; Whitehead\; s\text{'}était\; attaqué\; à\; cette\; tâche\; avec\; Principia\; Mathematica.\; Le\; théorème\; de\; Gödel\; a\; ruiné\; cet\; espoir.\; La\; thèse\; est\; généralement\; attribuée\; à\; Church,\; mais\; pour\; Church,\; c\text{'}était\; une\; définition.\; Kleene\; a\; estimé\; un\; temps\; cette\; ``définition"\; inadéquate.\; C\text{'}est\; en\; échouant\; dans\; la\; critique\; (voir\; plus\; loin)\; de\; cette\; ``définition"\; que\; Kleene\; a\; créé\; le\; vocable\; ``thèse\; de\; Church"\; et\; qu\text{'}il\; en\; est\; devenu\; un\; des\; grands\; partisans.\; En\; fait\; Kleene\; est\; le\; premier\; à\; réaliser\; la\; nature\; essentiellement\; hypothétique\; de\; cette\; ``définition".\; Il\; devint\; aussi\; le\; premier\; chaleureux\; partisan\; de\; cette\; thèse.\; On\; devrait\; donc\; parler\; plutôt\; de$thèse de Kleene. (voir [Kleene, 1952]).