next up previous contents
Next: La thèse de Church Up: La thèse de Church Previous: La thèse de Church

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 F0 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 F1 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 suivante :

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 à F0, ou F est égale à F1. 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'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'est Post, en 1922, qui est le premier à proposer la ``thèse de Church". Pour lui elle constituait une loi naturelle de l'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'incomplétude. Il est encore le premier à ``réfuter" l'hypothèse du mécanisme avec l'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'incomplétude, Hilbert espérait qu'un formalisme assez puissant allait pouvoir sécuriser formellement les fondements des mathématiques. Russell et Whitehead s'é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'était une définition. Kleene a estimé un temps cette ``définition" inadéquate. C'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'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]).
next up previous contents
Next: La thèse de Church Up: La thèse de Church Previous: La thèse de Church

Bruno Marchal
Thu Apr 1 00:14:24 CEST 1999