De la crise des fondements jusqu'aux diagrammes de Tromp, un siècle de recherche pour donner une forme à l'idée de calcul.
En 1901, Bertrand Russell trouve un paradoxe qui fissure la théorie naïve des ensembles : « l'ensemble des ensembles qui ne se contiennent pas eux-mêmes ». S'il se contient, il ne devrait pas. S'il ne se contient pas, il devrait. Le projet de fonder toutes les mathématiques sur la logique vacille.
En réponse, David Hilbert formule au congrès international de 1900 un programme : axiomatiser les mathématiques, prouver leur cohérence, leur complétude, et — ambition fatidique — leur décidabilité. C'est l'Entscheidungsproblem (problème de la décision), posé en 1928 : existe-t-il un algorithme qui, donné une formule logique, décide en temps fini si elle est valide ?
À l'époque, personne ne sait définir précisément ce qu'est un « algorithme ». Le λ-calcul naîtra de cette tension.
Alonzo Church (1903–1995), jeune professeur à Princeton, ne croit pas
au programme de Russell tel quel. Trop lourd, trop arbitraire dans ses axiomes.
Il propose à la place un système formel minimal où tout est fonction,
avec deux opérateurs primitifs :
Λ pour quantifier sur les types, λ pour les fonctions
ordinaires.
L'idée géniale : remplacer la notion d'ensemble par celle de fonction. Plus de paradoxe de Russell, parce que les fonctions sont stratifiées. Le système, publié en 1932 sous le titre "A Set of Postulates for the Foundation of Logic", doit servir de fondement aux mathématiques.
L'origine du symbole λ est anecdotique : Church voulait écrire x̂
(« x avec un chapeau »), comme dans Russell, mais l'imprimeur ne savait pas
gérer cet accent. Il a écrit le chapeau à part, ça donnait ∧x,
puis s'est dégradé en λx. Un accident typographique a baptisé
toute une famille de langages.
Deux étudiants de Church, Stephen Kleene et J. Barkley Rosser, découvrent en 1935 que le système initial est inconsistant : on peut y dériver toute formule, vraie comme fausse. Catastrophe pour les fondations.
Mais Church remarque alors un fait crucial. Si on retire la machinerie
logique et qu'on ne garde que l'ossature des fonctions — λx. M
et l'application — ce sous-système, le λ-calcul non typé, reste
parfaitement cohérent comme calcul. Plus une logique, mais un système de
manipulation symbolique. C'est ce qui survivra et fera l'histoire.
Ω = (λx. x x)(λx. x x)Toujours en 1936, Church et Rosser publient un résultat fondamental : la confluence. Si on β-réduit un terme λ par n'importe quel ordre, et qu'on atteint une forme normale, alors on atteint la même forme normale. L'ordre n'a pas d'importance pour le résultat — seulement pour la terminaison.
C'est exactement ce que ta page Tree visualise : les quatre stratégies divergent, parfois s'entrelacent, mais quand elles terminent, elles tombent toujours sur la même feuille. Le théorème est aussi appelé « propriété du diamant » à cause de la forme du diagramme des co-réductions qui se rejoignent.
En avril 1936, Church publie "An Unsolvable Problem of Elementary Number Theory". Verdict pour Hilbert : l'Entscheidungsproblem est indécidable. Aucun algorithme ne peut décider la validité de toute formule logique. La preuve repose sur le λ-calcul.
Quelques semaines plus tard, à Cambridge, un certain Alan Turing, 24 ans, achève sans connaître les travaux de Church son article "On Computable Numbers". Il y définit ce qu'on appelera les machines de Turing et démontre, par un autre chemin, exactement le même résultat.
Turing apprend l'existence du papier de Church juste avant de soumettre le sien. Il ajoute une annexe pour montrer que les deux formalismes — λ-calcul et machines de Turing — sont équivalents : ils calculent exactement la même classe de fonctions. C'est la thèse de Church-Turing : ce qui est intuitivement « calculable » coïncide avec ce que ces deux modèles peuvent faire.
Turing rejoint Church à Princeton fin 1936 pour son doctorat. Deux des mathématiciens les plus importants du XXᵉ siècle, dans le même bureau.
Pendant que Church construit le λ-calcul, Haskell Curry (1900–1982)
développe en parallèle depuis 1929 la logique combinatoire. Son
objectif : se débarrasser complètement des variables liées, source de
bugs subtils (capture, renommage). À la place, trois combinateurs
primitifs : S, K, I.
S = λx.λy.λz. x z (y z)K = λx.λy. xI = λx. xThéorème : tout terme λ peut être traduit en SKI, sans aucune variable. C'est un résultat surprenant — on dirait que les variables sont essentielles, mais elles sont juste un confort syntaxique.
Le langage Haskell (1990) est nommé en l'honneur de Curry. Et son
nom de famille a aussi donné le verbe curry en programmation
fonctionnelle (transformer f(x, y) en f(x)(y)) —
bien que la technique soit en fait due à Schönfinkel, antérieur.
John McCarthy, au MIT, cherche un langage pour ce qu'on appellera bientôt l'intelligence artificielle. Il lit Church, est frappé par la simplicité du λ-calcul, et conçoit en 1958 LISP (LISt Processor) — le premier langage de programmation à incorporer directement le concept :
(lambda (x) (* x x))
Le mot-clé lambda arrive directement de Church. LISP introduit
aussi les fonctions de première classe, le ramasse-miettes, l'évaluation
récursive, et la métaprogrammation par homoïconicité (le code et les
données ont la même représentation). Toutes ces idées sont aujourd'hui
partout — mais en 1958 elles étaient révolutionnaires.
Robin Milner à Édimbourg conçoit en 1973 ML (« Meta Language »). Il y résout un problème ouvert depuis Curry : comment inférer automatiquement les types d'un programme λ ? Le système qu'il développe avec Roger Hindley est devenu la base de tous les langages fonctionnels typés modernes : OCaml, Haskell, Rust (en partie), Elm, F#, Swift.
En parallèle, Gordon Plotkin formalise en 1975 la distinction entre call-by-name et call-by-value — les deux stratégies que ta page Tree visualise côte à côte. Plotkin montre qu'elles ne sont pas équivalentes en présence d'effets de bord ou de divergence.
En 1990, un comité de chercheurs formalise Haskell, l'aboutissement direct de cette lignée : λ-calcul typé, paresseux, pur. Le langage est nommé en hommage à Curry ; et même si peu de gens écrivent du Haskell au quotidien, ses idées (immutabilité, typage fort, effets explicites) ont influencé tous les langages modernes — y compris Rust et TypeScript.
En 1972, Jean-Yves Girard, en France, développe le System F pour démontrer la cohérence de l'arithmétique d'ordre supérieur. Indépendamment, en 1974 à Carnegie Mellon, John Reynolds arrive au même système, motivé par la programmation.
System F étend le λ-calcul typé avec la quantification sur les types : on peut écrire des fonctions qui marchent pour tout type. L'identité polymorphe :
id : ∀α. α → α
id = Λα. λ(x : α). xC'est la base théorique des generics en Java, des templates en C++, des type parameters en Rust et Swift, des type classes en Haskell. Le polymorphisme paramétrique a transformé l'industrie sans que la plupart des programmeurs n'aient jamais entendu le nom de Girard ou Reynolds.
Au début des années 2000, John Tromp publie le Binary Lambda Calculus (BLC) : un encodage de tout terme λ en suite de bits, avec exactement trois règles. L'objectif est minimaliste, presque obsessionnel : trouver le programme universel le plus court possible.
Tromp démontre l'existence d'un auto-interprète en 210 bits : un terme λ qui, donné l'encodage binaire d'un autre terme λ, simule sa réduction. Une machine de Turing universelle de la taille d'un tweet.
En parallèle, il invente la notation diagrammatique que ce site exploite : variables = traits verticaux, abstractions = barres horizontales, applications = jonctions en T. Une représentation purement géométrique d'un calcul, qui rend visible — littéralement — ce qu'une β-réduction fait au terme.
Y = λf. (λx. f (x x))(λx. f (x x))Le cycle se referme. Church voulait fonder les mathématiques par les fonctions. Un siècle plus tard, on regarde ces fonctions comme des formes qui se déforment lorsqu'elles s'appliquent à elles-mêmes, et on tient là quelque chose de plus profond qu'une notation : un objet géométrique. Ce site est une excuse pour le contempler.