| Naissance | |
|---|---|
| Décès | (à 92 ans) Hudson |
| Sépulture | Cimetière de Princeton(en)  |
| Nationalité | |
| Formation | |
| Activités |
| A travaillé pour | |
|---|---|
| Membre de | |
| Directeur de thèse | |
| Archives conservées par | Bibliothèque de l'Université de Princeton (C0948) Archives de l'École polytechnique fédérale de Zurich(en) (CH-001807-7:Hs 984)[1] |
Thèse de Church,Principe de Church-Turing-Deutsch,Frege–Church ontology(d),propriété de Church-Rosser,Church–Turing theorem(d) |
Alonzo Church (Washington -Hudson) est unmathématicien (logicien)américain à qui l'on doit certains des fondements de l'informatique théorique.
Alonzo Church est né le à Washington. Il est le fils de Samuel Robbins Church, juge auprès de lacour de district de Columbia, et de Mildred Hannah Letterman Parker[2]. Son arrière grand-pèreAlonzo S. Church (en) a été professeur de mathématiques et d'astronomie puis président duFranklin College, l'actuelleUniversité de Géorgie, pendant trente ans[3]. Son grand-père Alonzo Webster Church fut bibliothécaire et bibliographe duSénat des États-Unis et conseiller général pour leChicago & Alton Railroad[4].
Quand le déclin de la vue et de l'audition de son père l'obligent à abandonner son poste, la famille déménage en Virginie[5] où Alonzo Church et son jeune frère Randolph[6] grandissent. L'oncle d'Alonzo (également nommé Alonzo Church) vivant àNewark dans leNew Jersey, apporte une aide financière à la famille et participe à l'éducation des enfants. Un accident avec un pistolet à air comprimé fait perdre un œil à Church[7]. Church poursuit ses études à l'école de Ridgefield, un établissement pour garçon dans leConnecticut[8] réputé pour sa grande rigueur. Il en sort diplômé en 1920[6].
Church s'inscrit à l'université de Princeton, établissement que ses oncles ont également fréquenté. Sa première publication,Uniqueness of the Lorentz Transformation[9], parue en 1924, fut écrite pendant ses études depremier 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[4],[note 1]. De leur union naîtront trois enfants Alonzo Church, Jr. (1929), Mary Ann (1933)[note 2],[10] et Mildred (1938). Il obtient son doctorat en trois ans en 1927 sous la direction d'Oswald Veblen. Dans sa thèse intituléeAlternatives to Zermelo's Assumption, il étudie une logique dans laquelle l'axiome du choix, proposé en 1904 parZermelo, serait faux[11].
Avec son doctorat, il reçoit une bourse de recherche nationale[12] 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 rencontreDavid Hilbert etPaul Bernays, puis à l'Université d'Amsterdam où il rencontreLuitzen Egbertus Jan Brouwer (1928-1929)[12]. Son fils Alonzo Church Junior naît le dans cette même ville[4].
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'uncompendium 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 œuvreA bibliography of symbolic logic[2]. Elle sera publiée par la suite par l'intermédiaire de l'Association for Symbolic Logic dans le premier volume duJournal of Symbolic Logic en 1936[13].
Dans les années 1930, Princeton est un lieu propice aux échanges en logique carJohn von Neumann s'y trouve, ainsi que trois étudiants brillants de Church :Stephen Kleene,John Barkley Rosser etAlan Turing.Kurt Gödel, après plusieurs déplacements à l'Institute for Advanced Study entre 1933 et 1935, y donne plusieurs conférences sur sonthé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[14] en 1936. Church en sera l'un des éditeurs. Il édite quinze volumes entre 1936 et 1950. Il est également lerédacteur en chef de la partieReview duJournal 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 accomplit pour les 44 premiers volumes entre 1936 et 1979.
En 1967, Church décide de quitter Princeton pour rejoindre l'Université de Californie à Los Angeles, car l’université de Princeton n'est plus disposée à accueillir l'équipe duJournal 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 logicienWilliam Craig (en).Alonzo Church est élu membre de laNational Academy of Sciences en 1978[15].
En 1979 Church arrête de rédiger ses critiques dans leJournal of Symbolic Logic.Church est faitdocteurhonoris causa de plusieurs universités, et reçoit undiplôme d'honneur de sonalma mater[16] en 1985. Il est membre correspondant de laBritish Academy et membre de l’Académie américaine des arts et des sciences[15].En 1990, à 87 ans, Church met fin à 63 ans de carrière universitaire en quittant l'UCLA.
Il est connu principalement pour le développement dulambda-calcul, son application à la notion defonction récursive, pour la première démonstration de l'indécidabilité de l'arrêt. Il a aussi dirigé leJournal of Symbolic Logic[17], dont il est l'un des fondateurs en 1936[2].
Church en 1936 publie « An Unsolvable Problem of Elementary Number Theory »[18] (avec l'aide de ses élèvesKleene etRosser) 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 floue — 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[19]. 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 »[20]. 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[21]. 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 sont en fait 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 etTuring démontrent ensuite que lelambda-calcul de Church, lesfonctions générales récursives (modèle dit de Herbrand-Gödel) et lesmachines de Turing ont des capacités équivalentes : les fonctions définissables par chacun de ces trois moyens sont les mêmes.
Cette constatation aboutit à lathèse de Church (appelée aussithè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édé 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.
Parmi ses étudiants à Princeton, il eut des logiciens devenus célèbres, à savoirC. Anthony Anderson,Peter Andrews (en),Martin Davis,Leon Henkin (en),Maurice L'Abbé,John George Kemeny,Stephen Kleene,Michael O. Rabin,Hartley Rogers, Jr (en),J. Barkley Rosser,Dana Scott,Raymond Smullyan etAlan Turing[15].
Ses travaux influencèrent les langages deprogrammation fonctionnelle.
: :
