- Alonzo Church est moins connu du grand public qu’Alan Turing, mais c’est un logicien qui a posé les bases logiques de l’informatique avec le λ-calculus et la théorie de la calculabilité
- En 1936, la thèse de Church-Turing a fourni un cadre selon lequel toute fonction effectivement calculable peut être calculée par une machine de Turing ou un système équivalent
- En répondant au Entscheidungsproblem de Hilbert qu’il n’existe pas d’algorithme décisif permettant de trancher tous les énoncés mathématiques, il a clarifié les limites du calcul
- À Princeton, il a encadré Stephen Kleene, J. Barkley Rosser et Alan Turing, et Turing a terminé son doctorat sous sa direction
- Son travail abstrait s’inscrit dans la lignée du calcul qui mène aux compilateurs modernes, aux interpréteurs, à la programmation fonctionnelle, aux applications mobiles et à l’IA
Une influence théorique plus grande que sa notoriété
- Alan Turing est plus souvent cité dans l’histoire populaire de l’informatique et de l’intelligence artificielle via le test de Turing, mais Church a profondément influencé la pensée et les travaux de Turing
- Les travaux de Church constituent une base essentielle pour comprendre ce qu’est le calcul et pour façonner les concepts servant à évaluer l’IA
- Sans ses contributions, notre conception actuelle de l’intelligence artificielle et de ses modes d’évaluation aurait pu être très différente
Vie et orientation académique
- Church était un logicien discret et peu loquace, né le 14 juin 1903 à Washington, D.C.
- Certaines sources indiquent qu’un accident avec un pistolet à air comprimé durant son enfance l’a rendu aveugle d’un œil ou lui a fait perdre partiellement la vue
- Après avoir terminé une preparatory school dans le Connecticut en 1920, il a commencé ses études supérieures à Princeton la même année, puis a achevé son doctorat en 1927
- Après des séjours comme National Research Fellow à Harvard, Göttingen et Amsterdam, il est revenu à Princeton où il a construit une grande partie de son œuvre académique
- Il était connu pour son écriture soignée au tableau et son caractère méticuleux, au point de recouvrir parfois des articles importants de Duco cement pour les préserver
λ-calculus et calculabilité
- La contribution la plus profonde de Church est le λ-calculus, qui a servi de fondement à ce qui deviendrait plus tard l’informatique théorique, avant même que le terme informatique n’existe
- En 1936, Church a formulé la thèse de Church-Turing, concept central de l’informatique théorique
- toute fonction effectivement calculable peut être calculée par une machine de Turing ou un système équivalent
- elle fournit un cadre pour comprendre ce qu’une machine peut théoriquement faire
- elle met aussi en lumière les frontières que les procédures algorithmiques ne peuvent pas franchir
- Cette thèse est un concept fondamental, mais elle laisse aussi place à des débats et à des limites autour de l’interprétation de l’« effective computability », du calcul physique et de la nature de l’intelligence humaine
- Là où Turing proposait la machine de Turing pour traduire des procédures mécaniques en forme logique, Church fournissait la pure abstraction qui sous-tend théoriquement de telles machines
Programmation moderne et pensée fonctionnelle
- L’influence du λ-calculus se voit encore aujourd’hui dans les principes d’écriture des programmes, notamment dans les approches qui mettent l’accent sur la composition, les fonctions d’ordre supérieur et l’immuabilité
- Ce système formel a permis de coder des problèmes mathématiques abstraits et de les résoudre mécaniquement, devenant une base de l’architecture des compilateurs et des interpréteurs modernes
- Pour les programmeurs d’aujourd’hui, le λ-calculus peut évoquer un ensemble de fonctions imbriquées, comme dans certains paradigmes de Lisp, Haskell, Python ou JavaScript
- Son abstraction est à la base de la programmation fonctionnelle, où les fonctions sont traitées comme des first-class citizens
Entscheidungsproblem et les limites du calcul
- Church a aussi apporté d’importantes contributions à d’autres domaines de la logique et de la philosophie, et son travail sur l’Entscheidungsproblem en est un exemple représentatif
- L’Entscheidungsproblem, posé par David Hilbert en 1928, demandait s’il existe un algorithme décisif capable de déterminer la vérité ou la fausseté de n’importe quel énoncé mathématique
- Church a apporté une réponse négative en montrant qu’un tel algorithme n’existe pas, un résultat connu sous le nom de théorème de Church
- Cette découverte a profondément influencé la théorie de la décision et a souligné les limites de ce que le calcul seul peut accomplir
Le centre intellectuel de Princeton et ses élèves
- Church fut un mentor pour plusieurs grands logiciens et informaticiens de son époque
- Sa lignée académique comprend Stephen Kleene, J. Barkley Rosser et Alan Turing
- Turing a terminé son doctorat à Princeton sous la direction de Church
- On rapporte que David Kaplan recommandait aux nouveaux doctorants d’assister aux cours de Church, en disant que, même si ce n’était pas leur domaine d’intérêt, ce serait une expérience qu’ils raconteraient un jour à leurs petits-enfants
- Dans les années 1930, Princeton fut un centre intellectuel majeur du développement de la logique moderne, avec John von Neumann, Kurt Gödel et Church
Un héritage peu visible
- Church n’a pas acquis le même niveau de notoriété publique que Turing, von Neumann ou Gödel
- Son héritage ne se prêtait pas autant à l’imaginaire populaire que les récits héroïques du décryptage en temps de guerre ou la tragédie d’une mort prématurée
- Les milliards de programmes exécutés sur les smartphones d’aujourd’hui peuvent faire remonter leur logique jusqu’aux fonctions abstraites du λ-calculus
- Des applications les plus simples à l’intelligence artificielle, l’ADN invisible du calcul hérite d’une part essentielle de la lignée issue des travaux de Church
- Le génie de Church ne résidait pas dans le spectacle, mais dans des structures rigoureuses et une élégance discrète qui ont changé le monde
1 commentaires
Avis sur Hacker News
J’ai apprécié l’origine du nom lambda expliquée dans Paradigms of Artificial Intelligence Programming (PDF/EPUB : https://github.com/norvig/paip-lisp)
L’histoire raconte qu’Alonzo Church, voulant transformer en chaîne unidimensionnelle le caret placé au-dessus d’une variable liée dans la notation des Principia Mathematica de Russell et Whitehead,
x̂(x + x), l’aurait déplacé devant comme dans^x(x + x); trouvant étrange ce caret vide, il l’aurait remplacé par un lambda majusculeΛx(x + x), puis par un lambda minusculeλx(x + x)pour éviter toute confusion.John McCarthy a été l’étudiant de Church à Princeton, et lorsqu’il a créé Lisp en 1958, les perforatrices de l’époque ne disposant pas de caractères grecs, il a écrit
(lambda (x) (+ x x)), forme qui est restée jusqu’à aujourd’hui.Ainsi, comme le suggère le thème de cet article, Church revient souvent dans les rétrospectives sur Lisp, et il ne peut être considéré comme « oublié » que par des personnes n’ayant presque aucun intérêt pour l’histoire de l’informatique.
Selon Dana Scott, Church lui-même aurait dit que ce choix relevait d’une sélection arbitraire façon « eeny, meeny, miny, moe », et l’explication de type Barendregt aurait également été réfutée lors d’une conférence récente à l’University of Birmingham.
En français, « personne lambda » désigne une personne ordinaire ou anonyme, ce qui semble bien correspondre aux fonctions anonymes ; l’adjectif lambda signifie aussi « quelconque/ordinaire », et il y a l’idée que cette lettre située à peu près au milieu de l’alphabet grec représente quelque chose de moyen.
https://math.stackexchange.com/questions/64468/why-is-lambda...
Il couvre de nombreux sujets de programmation et ouvre aussi à des paradigmes qui peuvent sembler peu familiers à ceux qui ont été peu exposés à la programmation fonctionnelle.
On trouve sur https://en.wikipedia.org/wiki/Lambda_calculus#Origin_of_the_... d’autres éléments laissant entendre que Church avait plutôt choisi arbitrairement une lettre grecque, sans signification particulière.
Je me demande aussi si c’était avant ou après que McCarthy commence Lisp.
« Le calcul lambda de Church et la machine de Turing ont une puissance de calcul équivalente, mais la machine de Turing diffère en ce qu’elle utilise un état mutable. Si, aujourd’hui encore, il existe une fracture entre langages fonctionnels et langages impératifs, c’est à cause de la séparation de Church et de l’état. »
Je connais cette citation depuis longtemps, mais je n’ai jamais réussi à en trouver la source originale.
Édition : cela vient peut-être de cette phrase de Guy Steele : « Il y a des gens qui ne veulent pas mélanger la partie fonctionnelle/lambda-calcul du langage et la partie qui provoque des effets de bord. Ils semblent croire en la séparation de Church et de l’état. »
L’archive originale est ici : https://people.csail.mit.edu/gregs/ll1-discuss-archive-html/...
Les Européens prononcent en général correctement son nom « Nick-louse Veert », tandis que les Américains le massacrent en « Nickel’s Worth ».
Autrement dit, les Européens l’appellent par son nom, et les Américains par sa valeur.
https://en.m.wikiquote.org/wiki/Niklaus_Wirth
Si vous voulez lire un texte vraiment étonnant sur Church, je recommande les souvenirs de Rota.
C’est la première section de https://www34.homepage.villanova.edu/robert.jantzen/princeto...
Parmi les liens connexes, il y a Alonzo Church, 92, Theorist of the Limits of Mathematics (1995) - https://news.ycombinator.com/item?id=12240815 - août 2016, et Gian-Carlo Rota on Alonzo Church (2008) - https://news.ycombinator.com/item?id=9073466 - février 2015.
Le livre entier mérite d’être lu.
Le langage de programmation Alonzo, nommé d’après lui, est presque oublié.
https://dl.acm.org/doi/pdf/10.1145/68127.68139
En particulier, sa philosophie de la logique, dans le prolongement des travaux de Frege et Russell, ainsi que ses théories du sens et de la référence, ont été largement oubliées.
Church a publié de nombreux articles sur ce sujet, mais il est à peine traité dans des endroits comme Wikipédia.
L’entrée de la Stanford Encyclopedia of Philosophy est tout de même un peu meilleure : https://plato.stanford.edu/entries/church/
Cela dit, on m’a dit qu’elle omettait elle aussi une partie de ses travaux majeurs, et j’imagine que c’était trop philosophique pour les mathématiciens et trop technique pour les philosophes.
Ce n’est pas le cœur du sujet, mais j’aimerais qu’on évite un peu d’utiliser des illustrations générées par IA dans les billets de blog.
Il existe de vraies photos de Church dans le domaine public, alors que cette illustration ne lui ressemble pas vraiment et, avec la popularité de l’article, elle apparaît déjà dans les résultats de recherche d’images.
Si l’illustration ne valait même pas plus de cinq minutes de génération, il vaudrait peut-être mieux simplement s’en passer.
Et si l’on tient vraiment à utiliser une image générée par « IA », il faut au minimum l’indiquer en légende.
Je n’étais pas très à l’aise avec l’idée de reprendre une photo en ligne, et cette image était le 7e résultat que j’avais produit pour éviter d’obtenir un faux sosie ; je trouvais qu’elle lui ressemblait dans une certaine mesure.
L’image de JvN était plutôt réussie, mais à l’avenir il sera sans doute préférable d’utiliser des images symboliques plutôt que de faux sosies ayant l’air de portraits.
L’expression « architecte de l’intelligence informatique » me paraît excessive.
Church était certes un logicien remarquable, mais si l’intelligence informatique désigne ici l’IA/ML, sa contribution est pratiquement inexistante.
Par ailleurs, je ne suis même pas sûr que le lambda-calcul soit vraiment des mathématiques ; cela ressemble davantage à une notation ingénieuse.
Les avantages d’une notation sont subjectifs, et il est aussi intéressant de noter que Church ne s’intéressait guère au fait que ses idées aient inspiré la conception de certains langages de programmation.
La STT est aussi souvent assimilée à la logique d’ordre supérieur, car elle permet d’exprimer n’importe quel objet logique à partir de seulement deux types primitifs — les « individus » de base et les valeurs de vérité V/F — ainsi que des types de fonctions
(a --> b).La STT est clairement une invention de Church, elle a fortement influencé les théories modernes des types, ainsi que des langages de programmation dotés de systèmes de types complexes comme Haskell.
Je ne peux pas vraiment le démontrer, mais intuitivement, Turing et ce qu’il symbolise finissent par être valorisés du côté de l’IA, tandis que Church semble représenter l’inverse.
Le premier partait de la pureté, des conditions minimales possibles, d’un calcul abstrait et « pur », tandis que le second s’intéressait à la manière dont nous pouvons réellement penser et semblait davantage préoccupé par l’extension de l’expression et de l’abstraction que par l’implémentation.
Church n’avait pas d’expérience pratique de l’informatique et était plutôt tourné vers l’extension de la théorie mathématique elle-même.
Leur collaboration et leurs échanges de part et d’autre de l’Atlantique ont combiné pratique et théorie pour consolider des notions fondamentales comme la dualité impératif/fonctionnel, la thèse de Church-Turing, ou encore les liens entre le problème de l’arrêt et le théorème de Church.
Les voir comme des rivaux est une erreur, et dire que l’informatique a « deux pères » est approprié pour plusieurs raisons.
D’autant plus si l’on pense à la mort de Turing.
Il ne faut pas non plus oublier que Turing n’était pas indifférent à l’implémentation : il voulait revenir aux réalisations concrètes, mais on ne l’y a pas autorisé.
Il reste une grande tragédie, et une grande question, de savoir ce qui aurait changé si les règles de classification du gouvernement britannique avaient été différentes ; mais dans ce cas, sur notre ligne temporelle, nous aurions peut-être perdu cette collaboration avec Church qui a si bien consolidé la théorie.
J’ai eu la chance de pouvoir rencontrer Alonzo Church et Haskell Curry lors de l’ACM Symposium on LISP and Functional Programming qui s’est tenu à la CMU en août 1982.
Curry était manifestement en mauvaise santé et il est mort environ deux semaines après la conférence, mais Church avait l’air en forme et a vécu encore environ treize ans.
À la réception, Gerry Sussman était très enthousiaste en faisant le tour de la salle pour présenter les deux hommes, et les rencontrer a aussi été un grand moment pour nous.
L’une des grandes contributions de Church a été ses étudiants.
Un nombre étonnant de penseurs remarquables sont sortis du même endroit.