Alonzo Church

Pour les articles homonymes, voir Alonzo et Church.

Alonzo Church (14 juin 1903 Washington - 11 août 1995 Hudson) est un mathématicien (logicien) américain à qui l'on doit certains des fondements de l'informatique théorique.

Biographie

Alonzo Church est né le 14 juin 1903 à Washington, il est le fils de Samuel Robbins Church juge auprès de la Cour du district de Columbia et de Mildred Hannah Letterman Parker^[1]. Son arrière grand-père Alonzo S. Church (en), a été professeur de mathématiques et d'astronomie puis président du Franklin College actuelle Université de Géorgie pendant trente ans^[2]. Son grand-père Alonzo Webster Church fut bibliothécaire et bibliographe du Sénat des États-Unis et conseiller général pour le Chicago & Alton Railroad^[3].

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^[4] où Alonzo Church et son jeune frère Randolph^[5] grandissent. L'oncle d'Alonzo (également nommé Alonzo Church) vivant à Newark dans le New Jersey, apporte une aide financière utile à la famille et participe à l'éducation des enfants. Un incident de pistolet à air comprimé rend Church aveugle d'un œil^[6]. Church poursuit ses études à l'école préparatoire de Ridgefield, un établissement pour garçon dans le Connecticut^[7] réputé pour sa grande rigueur, il en sort diplômé en 1920^[5].

Princeton

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 universitaire à 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 où sous la direction d'Oswald Veblen il présente sa thèse Alternatives to Zermelo's Assumption où il envisage 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 vient au monde 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é par la suite par l'intermédiaire de l'Association for Symbolic Logic dans le premier volume du Journal of Symbolic Logic (en) en 1936^[12].

Princeton dans les années 1930, 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 nait; 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.

UCLA

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.

Travaux

Il est connu principalement pour le développement du lambda-calcul, son application à la notion de fonction récursive, pour la première démonstration de l'indécidabilité de l'arrêt. Il a aussi dirigé le Journal of Symbolic Logic (en)^[16], dont il est l'un des fondateurs en 1936^[1].

Les débuts de la calculabilité

Les travaux de son équipe (Church, Kleenne et Rosser) précèdent, sur le problème de l'arrêt, le travail d'Alan Turing, qui va d'ailleurs les rejoindre. C'est Church qui, le premier, a l'idée que l'on peut définir le concept de fonction calculable dans un sens très large, cette idée avait déjà été entrevue par Herbrand, mais sa mort prématurée ne lui avait pas permis de la pousser plus loin. Church en a eu l'idée par le lambda-calcul. Church démontre en 1936 l'existence d'un problème insoluble par algorithme, autrement qui ne peut pas être résolu par un calcul mécanisable.

Le thèse de Church

Kleene et Turing démontrent 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. L'équivalence démontrée ensuite qu'un certain nombre de formalisations mathématiques de la notion de traitement par des processus mécaniques ont des aptitudes en tous points semblables confirme l'intuition de Church. Cette constatation aboutit à la thèse de Church (appelée aussi thèse de Church-Turing). Elle s'appelle « thèse » parce qu'il s'agit d'un résultat qui ne peut pas être prouvé, car il affirme l'équivalence entre un concept intuitif, à savoir les fonctions mécaniquement calculables, et un concept formel, à savoir, les diverses définitions des fonctions récursives. Elle s'appelle la « thèse de Church » puisque c'est lui qui en a eu le premier l'idée. Elle s'appelle la « thèse de Church-Turing » puisque les machines de Turing donnent une véritable idée de ce que « mécanique » veut dire.

Influence et étudiants

Parmi ses étudiants à Princeton, il eut des logiciens devenus célèbres, à savoir C. Anthony Anderson (en), 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 et Alan Turing^[14].

Ses travaux influencèrent les langages de programmation fonctionnelle.

Publications

• Alonzo Church, Introduction to Mathematical Logic (ISBN 978-0-691-02906-1)
• Alonzo Church, The Calculi of Lambda-Conversion (ISBN 978-0-691-08394-0)^[17]
• Alonzo Church, A Bibliography of Symbolic Logic, 1666–1935 (ISBN 978-0-8218-0084-3)

Notes et références

Notes

Références

Bibliographie

• Stephen Kleene Origins of Recursive Function Theory in Annals of the History of Computing, Vol. 3 No. 1, janvier 1981. Cet article raconte la période qui a vu à Princeton l'émergence du concept de fonction récursive.
• Wilfried Sieg Step By Recursive Step: Church's Analysis Of Effective Calculability (1997), The Bulletin of Symbolic Logic, vol 3, n^o 2. Discute l'émergence du concept de récursivité dans la pensée de Church.

Voir aussi

Articles connexes

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

Liens externes

• Notices d’autorité : Fichier d’autorité international virtuel • International Standard Name Identifier • Bibliothèque nationale de France • Système universitaire de documentation • Bibliothèque du Congrès • Gemeinsame Normdatei • WorldCat
• Un entretien avec Church sur sa période à Princeton (en anglais)

• Portail de la logique
• Portail de l'informatique théorique