Alonzo Church
| 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 | Archives de l'École polytechnique fédérale de Zurich (en) (CH-001807-7:Hs 984)[1] Bibliothèque de l'Université de Princeton (C0948) |
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 un mathématicien (logicien) américain à qui l'on doit certains des fondements de l'informatique théorique.
Biographie
[modifier | modifier le code]Alonzo Church est né le à Washington. Il est le fils de Samuel Robbins Church, juge auprès de la cour de district de Columbia, et de Mildred Hannah Letterman Parker[2]. 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, l'actuelle Université de Géorgie, pendant trente ans[3]. 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[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 le New 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 le Connecticut[8] réputé pour sa grande rigueur. Il en sort diplômé en 1920[6].
Princeton
[modifier | modifier le code]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 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 [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ée Alternatives to Zermelo's Assumption, il étudie une logique dans laquelle l'axiome du choix, proposé en 1904 par Zermelo, 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 rencontre David Hilbert et Paul Bernays, puis à l'Université d'Amsterdam où il rencontre Luitzen 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'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[2]. 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[13].
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[14] en 1936. Church en sera l'un des éditeurs. Il édite quinze 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 accomplit pour les 44 premiers volumes entre 1936 et 1979.
UCLA
[modifier | modifier le code]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[15].
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[16] en 1985. Il est membre correspondant de la British 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.
Travaux
[modifier | modifier le code]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[17], dont il est l'un des fondateurs en 1936[2].
Les débuts de la calculabilité
[modifier | modifier le code]Church en 1936 publie « An Unsolvable Problem of Elementary Number Theory »[18] (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 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.
La thèse de Church
[modifier | modifier le code]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é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.
Influence et étudiants
[modifier | modifier le code]Parmi ses étudiants à Princeton, il eut des logiciens devenus célèbres, à savoir C. 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 et Alan Turing[15].
Ses travaux influencèrent les langages de programmation fonctionnelle.
Publications
[modifier | modifier le code]- 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)[22].
- Alonzo Church, A Bibliography of Symbolic Logic, 1666–1935 (ISBN 978-0-8218-0084-3).
Notes et références
[modifier | modifier le code]Notes
[modifier | modifier le code]- Il rencontra Mary à la suite d'un accident : il fut heurté par un tramway qu'il n'avait pas vu arriver. Mary était alors élève infirmière à l’hôpital où elle lui donna des soins
- Mary Ann deviendra plus tard l'épouse de John West Addison Jr, lui aussi logicien
Références
[modifier | modifier le code]- « http://archivdatenbank-online.ethz.ch/hsa/#/content/195ac2f6479044ef8ff1d609d697be08 » (consulté le )
- (en) John J. O'Connor et Edmund F. Robertson, « Alonzo Church », sur MacTutor, université de St Andrews..
- (en) « Presidents at the University of Georgia 1785-1997 », sur le site de l'Université de Géorgie (consulté le ).
- (en) Ellwood Count Curtis, The descendants of Josiah Churchill (c. 1615-1686) and Elizabeth Foote (1616-1700), vol. 4, L'Université du Wisconsin - Madison, Galactic Press, (présentation en ligne), p. 1880.
- (en) Maria Manzano, Alonzo Church : His Life, His Work and Some of His Miracles : History and Philosophy of Logic, vol. 18, Taylor and Francis, (ISBN 84-7800-627-3), p. 211-232.
- (en) Kenneth T. Jackson, The Scribner Encyclopedia of American Lives, vol. 4, Gale, , 649 p. (ISBN 0-684-80644-4 et 9780684806440, présentation en ligne), p. 90.
- (en) Peter J. Bentley, Digitized : The Science of Computers and how it Shapes Our World, Oxford, OUP Oxford, , 298 p. (ISBN 978-0-19-969379-5 et 0-19-969379-X, lire en ligne), p. 24-26,45,50,88.
- (en) « Ridgefield School for Boys » (consulté le ).
- (en) Alonzo Church, The American Mathematical Monthly : Uniqueness of the Lorentz Transformation, vol. 31 (no 8), , 410 p. (présentation en ligne), p. 376-382.
- (en) « Mary Ann Addison - Obituary 1933-2013 » (consulté le ).
- (en) « Alternatives to Zermelo's Assumption », sur le site de l'American Mathematical Society (consulté le ).
- « Interview d'Alonzo Church par William Aspray », sur The Princeton Mathematics Community, (consulté le ) .
- (en) Alonzo Church, The Journal of Symbolic Logic : A bibliography of symbolic logic, vol. 1, Association for Symbolic Logic, , 156 p. (ISBN 978-0-8218-0084-3 et 0821800841, présentation en ligne), p. 121-216
- Herbert Enderton (en) reprend cette tâche de 1980 à 2002
- H. B. Enderton, « In memoriam: Alonzo Church 1903–1995 », The Bulletin of Symbolic Logic, vol. 1, no 4, , p. 488. (présentation en ligne)
- (en) « Princeton University - Honorary Degrees » (since 1948) sur Princeton.edu
- Françoise Armengaud, « Church Alonzo (1903-1995) », sur Encyclopædia universalis (consulté le ).
- Alonzo Church, « An Unsolvable Problem of Elementary Number Theory », American Journal of Mathematics, vol. 58, no 2, , p. 345–363 (ISSN 0002-9327, DOI 10.2307/2371045, lire en ligne, consulté le ).
- Alonzo Church, « A Set of Postulates for the Foundation of Logic », Annals of Mathematics, vol. 33, no 2, , p. 346–366 (ISSN 0003-486X, DOI 10.2307/1968337, lire en ligne, consulté le )
- (en) Kurt Gödel, On undecidable propositions of formal mathematical systems (Mimeographed lecture notes by S. C. Kleene and J. B. Rosser. Corrected and amplified in Davis, The Undecidable, 1965), , New York, Institute for Advanced Study,
- (en) A. M. Turing, « On Computable Numbers, with an Application to the Entscheidungsproblem », Proceedings of the London Mathematical Society, vol. s2-42, no 1, , p. 230–265 (DOI 10.1112/plms/s2-42.1.230, lire en ligne, consulté le )
- ORRIN FRINK, JR., The calculi of lambda-conversion. By Alonzo Church. (Annals of Mathematics Studies, no. 6.) Princeton, Princeton University Press; London, Humphrey Milford and Oxford University Press, 1941. p. 169-172
Bibliographie
[modifier | modifier le code]- Stephen Kleene, Origins of Recursive Function Theory in Annals of the History of Computing, Vol. 3 No. 1, . 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, no 2. Discute l'émergence du concept de récursivité dans la pensée de Church.
Voir aussi
[modifier | modifier le code]Articles connexes
[modifier | modifier le code]Liens externes
[modifier | modifier le code]
- Ressources relatives à la recherche :
- Notices dans des dictionnaires ou encyclopédies généralistes :
- « Un entretien avec Church sur sa période à Princeton (en anglais) »(Archive.org • Wikiwix • Archive.is • Google • Que faire ?) (consulté le )
