Alonzo Church

Church s'inscrit à l'université de Princeton, établissement que ses oncles ont également fréquenté. Sa première publication, Uniqueness of the Lorentz Transformation[8], parue en 1924, fut écrite pendant ses études de premier cycle universitaire. Il obtient sa licence la même année.

Il continue ses études universitaires à Princeton, où il épouse une jeune élève infirmière Mary Julia Kuczinski le 25 août 1925[3] - [note 1]. De leur union naîtront trois enfants Alonzo Church, Jr. (1929), Mary Ann (1933)[note 2] - [9] et Mildred (1938). Il obtient son doctorat en trois ans en 1927 sous la direction d'Oswald Veblen. Dans sa thèse intitulée Alternatives to Zermelo's Assumption, il étudie une logique dans laquelle l'axiome du choix, proposé en 1904 par Zermelo serait faux[10].

Avec son doctorat il reçoit une bourse de recherche nationale[11] qu'il utilise pour voyager. Ainsi, durant l'été 1927 il est instructeur à l'Université de Chicago. Il passe deux ans à l'Université Harvard (1927-1928), puis se rend à l'Université de Göttingen où il rencontre David Hilbert et Paul Bernays puis à l'Université d'Amsterdam où il rencontre Luitzen Egbertus Jan Brouwer (1928-1929)[11]. Son fils Alonzo Church Junior naît le 9 septembre 1929 dans cette même ville[3].

Au terme de sa bourse de recherche, Church retourne à Princeton. Il y devient professeur assistant de 1929 à 1939, puis professeur associé de 1939 à 1947, puis professeur de 1947 à 1967

Vers 1934, Church commence la rédaction d'un compendium dans lequel il rassemble l'ensemble des œuvres disponibles en logique sur la période courant de 1666 à 1935; celles-ci y sont référencées par auteur et par sujet. Il intitule son œuvre A bibliography of symbolic logic[1]. Elle sera publiée par la suite par l'intermédiaire de l'Association for Symbolic Logic dans le premier volume du Journal of Symbolic Logic en 1936[12].

Dans les années 1930, Princeton est un lieu propice aux échanges en logique car John von Neumann s'y trouve, ainsi que trois étudiants brillants de Church, Stephen Kleene, John Barkley Rosser et Alan Turing. Kurt Gödel, après plusieurs déplacements à l'Institute for Advanced Study entre 1933 et 1935, y donne plusieurs conférences sur son théorème d'incomplétude, et s'y installe définitivement vers 1940. L'Association for Symbolic Logic y naît ; il en est nommé le président[13] en 1936. Church en sera l'un des éditeurs. Il édite 15 volumes entre 1936 et 1950. Il est également le rédacteur en chef de la partie Review du Journal of Symbolic Logic dans laquelle il apporte une relecture et une critique analytique des thèses qui lui sont soumises, une tâche qu'il accompli pour les 44 premiers volumes entre 1936 et 1979.

En 1967, Church décide de quitter l'université de Princeton pour rejoindre l'Université de Californie à Los Angeles, car l’université de Princeton n'est plus disposée à accueillir l'équipe du Journal of Symbolic Logic alors que celle de Californie s'engage à la soutenir tant que Church en restera le rédacteur en chef. À la mort de son épouse Mary en 1976, Church partage sa fonction dans le journal avec le logicien William Craig (en). Alonzo Church est élu membre de la National Academy of Sciences en 1978[14].

En 1979 Church arrête de rédiger ses critiques dans le Journal of Symbolic Logic. Church est fait docteur honoris causa de plusieurs universités, et reçoit un diplôme d'honneur de son alma mater[15] en 1985. Il est membre correspondant de la British Academy et membre de l’Académie américaine des arts et des sciences[14]. En 1990 à 87 ans, Church met fin à 63 ans de carrière universitaire en quittant l'UCLA.

Church en 1936 publie « An Unsolvable Problem of Elementary Number Theory »[17] (avec l'aide de ses élèves Kleene et Rosser) sur les fonctions de nombres entiers que l'on peut calculer mécaniquement. C'est à dire les fonctions dont on peut calculer les valeurs par un algorithme en un nombre fini d'étapes. Il les appelle des "fonctions effectivement calculables" . La notion de "mécaniquement calculable" étant intuitive et flou, — puisqu'elle fait appel aux machines présentes et à venir —, il cherche à donner une définition précise de ces fonctions. Il va faire deux propositions.

La première consiste à utiliser le lambda-calcul, qu'il vient d'inventer en 1932[18]. Les fonctions effectivement calculables seront alors les fonctions lambda-définissables, c'est à dire les fonctions que l'on définir grâce au lambda-calcul. La proposition se justifie puisqu'il est clair que les valeurs des fonctions lambda-définissables peuvent être déterminées par un algorithme en un nombre fini d'étapes.

La seconde proposition consiste à utiliser les fonctions que Gödel a définies dans les leçons qu'il a données à Princeton en 1934 et qu'il a appelées "fonctions récursives"[19] . L'intérêt de cette notion avait déjà été entrevu par Herbrand — et communiqué par celui-ci à Gödel — mais la mort prématurée en 1931 du logicien français avait interrompu ses recherches.

Church ne parle pas des travaux de Turing sur les machines qui portent désormais son nom puisqu'ils ne seront publiés qu'en 1937[20]. Mais elles constitueront un troisième moyen de définir les fonctions effectivement calculables.

Dans son article de 1936, Church démontre l'existence d'un problème insoluble par des fonctions effectivement calculables.

Les fonctions étudiées par Church peuvent sembler très particulière puisqu'elles portent sur des variables entières mais il suffit de penser au fonctionnement d'un ordinateur — dont la mémoire n'est constituée que de nombres entiers et dont le processeur ne traitent que des nombres entiers — pour réaliser que ces fonctions en fait sont très générales.

Cette notion est également cruciale en logique puisqu'elle conditionne la possibilité de calculer mécaniquement, — et non par une démonstration, laquelle fait appel à l'imagination —, la vérité d'un théorème.

Kleene et Turing démontrent ensuite que le lambda-calcul de Church, les fonctions générales récursives (modèle dit de Herbrand-Gödel) et les machines de Turing ont des capacités équivalentes : les fonctions définissables par chacun de ces trois moyens sont les mêmes.

Cette constatation aboutit à la thèse de Church (appelée aussi thèse de Church-Turing) : les fonctions calculables mécaniquement sont les fonctions effectivement définissables. Proposition indémontrable — d'où le nom de thèse—puisque s'il est clair que les fonctions lambda définissables, les fonctions récursives de Gödel ou les fonctions définies par une machine de Turing peuvent être calculées par un procès mécanique, le contraire reste improuvable à cause du flou qui entoure la notion de procédé mécanique. Elle s'appelle la « thèse de Church » puisque c'est lui qui en a eu le premier l'idée.

La « thèse de Church » s'appelle encore la « thèse de Church-Turing » puisque les machines de Turing donnent l'idée la plus claire de ce que « mécanique » veut dire.

• Association for Symbolic Logic
• Problème de la décision
• Thèse de Church

• Ressources relatives à la recherche :
  • Persée
  • (en) Digital Bibliography & Library Project
  • (en) Mathematics Genealogy Project
  • (en) Stanford Encyclopedia of Philosophy
• Notices dans des dictionnaires ou encyclopédies généralistes :

  • American National Biography
  • Britannica
  • Brockhaus
  • Hrvatska Enciklopedija
  • Nationalencyklopedin
  • Proleksis enciklopedija
  • Store norske leksikon
  • Universalis
• Notices d'autorité :

  • VIAF
  • ISNI
  • BnF (données)
  • IdRef
  • LCCN
  • GND
  • Italie
  • CiNii
  • Pays-Bas
  • Pologne
  • Israël
  • NUKAT
  • Suède
  • Australie
  • Norvège
  • Croatie
  • Tchéquie
  • WorldCat
• « Un entretien avec Church sur sa période à Princeton (en anglais) »^{(Archive.org • Wikiwix • Archive.is • Google • Que faire ?)} (consulté le 5 août 2017)