Syntaxe, sémantique et lambda-calcul

26 septembre 2026 — Programmation fonctionnelle, Modèles de calcul

Nous choisissons les idées que nous représentons par les symboles non-définis et les faits que nous énonçons par les P non-démontrées; (…) Alors, le système des idées que nous avons choisi d’abord n’est qu’une interprétation du système des symboles non-définis; mais, au point de vue déductif, cette interprétation peut être ignorée par le lecteur, qui peut librement la remplacer, dans sa pensée, par une autre interprétation qui vérifie les conditions énoncées par les P non-démontrées. (…) Ainsi les questions logiques acquièrent une complète indépendance à l’égard des questions empiriques ou psychologiques (et, en particulier, du problème de la connaissance)
— Alessandro Padoa, Essai publié en 1901

Dans cet article, je voudrais vous parler du lambda-calcul, que l’on peut voir comme une sorte de langage de programmation ésotérique basé sur une syntaxe très concise.

Il permet néanmoins d’implémenter les mêmes fonctions qu’un langage de programmation classique : les plus geeks apprécieront peut-être ce projet !

Une façon plus sophistiquée de dire cela est de dire que le lambda-calcul est un modèle de calcul complet au sens de Turing.

Par ailleurs, des langages de programmation fonctionnels comme Haskell, OCaml ou Lean utilisent une représentation interne des programmes fortement inspirée du lambda-calcul, ce qui fait que les considérations abordées ici peuvent avoir des implications très concrètes.

Tout ce que je présente ici est détaillé de façon plus approfondie dans le cours de Jean Goubault-Larrecq.

La syntaxe du lambda-calcul

Le langage du lambda-calcul peut se définir (en notation BNF) de la façon suivante :

$\Lambda := V|\Lambda\Lambda|\lambda V. \Lambda$

Cette notation définit l’ensemble des phrases valides du langage — on parlera plutôt de termes.

$V$ désignant l’ensemble des variables, les termes du lambda-calcul peuvent donc être de trois formes :

• Les variables (e.g. $x$)
• Les applications, de la forme $MN$ où $M$ et $N$ sont deux termes bien formés (e.g. $(\lambda y.xy) z$, $xy$ ou $(\lambda x.xx)(\lambda x.xx)$)
• Les abstractions, de la forme $\lambda v.M$ où $v$ désigne une variable et $M$ un terme bien formé (e.g. $\lambda x.xy$)

La β-réduction : un jeu formel ?

Quand on considère une abstraction comme $\lambda x.x$, on a envie de la considérer comme une fonction (dans ce cas l’identité). De même, on pourrait avoir envie de considérer une application comme le fait d’invoquer une fonction (le premier terme de l’application) sur un argument (le second terme).

La β-réduction (beta-réduction) capture en quelque sorte cette idée. Cependant, il ne s’agit pas ici de donner un sens aux termes mais plutôt de décrire un jeu formel qui correspond simplement à des manipulations syntaxiques sur les termes.

Cette opération, notée $\to_\beta$, consiste à remplacer dans un sous-terme de la forme $(\lambda v.M) N$ les occurrences de $v$ dans $M$ par $N$.

Par exemple :

• $(\lambda x.x) y \to_\beta y$ (on retrouve l’idée que $\lambda x.x$ se comporte comme l’identité)
• $(\lambda x.xx)(\lambda x.xx) \to_\beta (\lambda x.xx)(\lambda x.xx)$ : la β-réduction redonne ici le même terme
• $(\lambda x.(\lambda y.xy)) y \to_\beta \lambda z.yz$

Dans le troisième exemple, j’ai utilisé implicitement la règle d’α-conversion (alpha-conversion) pour remplacer $\lambda y.xy$ par $\lambda z.xz$. Il s’agit d’une règle qui permet de renommer les variables, permettant notamment d’éviter les conflits de noms.

En pratique, les implémentations du lambda-calcul utilisent généralement des indices positionnels plutôt que des noms pour désigner les variables liées, ce qui permet d’éviter ce genre de considérations (c’est notamment le cas dans Lean).

Ainsi défini, le lambda-calcul semble être un jeu de manipulations formelles sur des chaînes de caractères, la réduction (j’omettrai dorénavant le β) correspondant à une opération que l’on peut effectuer de façon séquentielle, comme une forme de calcul :

Ce calcul correspond, d’une certaine façon, à l’égalité $1 + 1 = 2$.

On notera que je n’ai pas discuté ici des stratégies de réduction (le calcul présenté correspond à une stratégie externe gauche), qui ont une importance en pratique dans les langages dérivés du lambda-calcul.

Je vous invite à regarder cette belle vidéo, qui met en animation des calculs de ce type d’une façon très visuelle.

Un modèle de calculabilité

J’ai récemment publié une présentation des modèles de calcul, qui permettent de formaliser théoriquement la notion d’algorithme. En particulier :

• Les machines de Turing, qui décrivent une machine à état effectuant des calculs étape par étape en ayant accès à une bande de mémoire.
• Les fonctions récursives générales, qui définissent mathématiquement une classe de fonctions calculables sur les entiers naturels.

Le lambda-calcul, en s’appuyant sur la β-réduction et un certain encodage des entiers naturels (utilisé implicitement dans mon exemple qui précède), permet également de définir une notion de calcul, aussi riche que celles de ces deux modèles. Le cours évoqué en préambule revient sur cette richesse et démontre que le lambda-calcul permet d’exprimer toutes les fonctions récursives générales, ce qui en fait un langage Turing-complet. Cette capacité repose notamment sur des combinateurs comme le combinateur $Y$ (qui a donné son nom à un célèbre incubateur de start-ups…) qui permet d’accéder à une forme de récursion.

Il me semble assez notable, alors que le modèle des machines de Turing s’appuie sur une idée sous-jacente de machine et que les fonctions récursives sont définies à partir de concepts mathématiques préexistants (à commencer par les entiers naturels), que le lambda-calcul repose exclusivement sur des opérations syntaxiques.

Extensionnalité et η-conversion

Dans les Éléments, Euclide tenta de formaliser la géométrie plane à l’aide d’un système de cinq axiomes. La question de la démonstrabilité du cinquième à partir des quatre premiers agita pendant longtemps les mathématiciens, jusqu’à ce que près de deux millénaires plus tard un modèle de géométrie respectant les axiomes d’Euclide à l’exception du cinquième fut produit, démontrant l’indépendance de ce dernier.

J’ai aussi évoqué l’exemple de l’axiome de Pasch (et les insuffisances logiques de la présentation d’Euclide) dans l’article Quelques aspects de la mécanisation de la géométrie. Je n’y reviendrai pas plus ici, mais il est tentant d’établir un parallèle avec une question relative au lambda-calcul.

Si l’on interprète un terme $\lambda x . fx$ comme une fonction de la variable $x$, on pourrait s’attendre à ce que celui-ci soit équivalent d’une certaine façon au terme $f$. Ceci correspond à un principe d’extensionnalité : une fonction est entièrement définie par les valeurs qu’elle prend en chaque point de son domaine.

Le lambda-calcul est-il extensionnel ?

Rendre cette question précise dans le cadre du lambda-calcul demande de définir une relation d’équivalence $=_\beta$ entre termes. Cette relation se définit assez directement à partir de la réduction $\to_\beta$ : je vous renvoie au cours que j’ai mentionné pour les détails, mais il s’agit essentiellement d’identifier les termes égaux à réductions près et d’étendre ceci pour obtenir une relation d’équivalence.

La question de l’extensionnalité devient alors :

A-t-on $\lambda x . fx =_\beta f$ pour tout terme $f$ dont $x$ n’est pas une variable libre ? (◇)

Les sémantiques dénotationnelles

Il se trouve que la question qui précède peut être traitée par des considérations purement syntaxiques, notamment grâce au puissant théorème de Church-Rosser (qui précède historiquement les considérations sémantiques).

Il est néanmoins possible d’utiliser une autre approche, que l’on peut mettre en parallèle de ma digression concernant la géométrie euclidienne, puisqu’elle consiste à construire un modèle du lambda-calcul qui ne vérifie pas le principe d’extensionnalité (◇).

Le logicien Dana Scott a proposé dans les années 70, différents modèles dénotationels du lambda-calcul.

Comme remarqué précédemment, le lambda-calcul décrit des règles syntaxiques, mais il ne propose pas de sémantique associée : quelle interprétation pourrait-on donner aux termes du lambda-calcul ?

La réponse n’est pas unique et, de fait, Dana Scott a proposé plusieurs constructions mathématiques compatibles avec les règles du lambda-calcul.

Une difficulté particulière dans ces constructions est que, si l’on interprète les termes du lambda-calcul par des éléments d’un ensemble $D$ (le domaine), et si l’on souhaite qu’une application $MN$ soit interprétée comme l’évaluation d’une fonction (associée à $M$) sur un argument (l’interprétation de $N$), on a alors besoin de transformations $r : D \to [D \to D]$ et $i : [D \to D] \to D$ telles que $r \circ i$ soit l’identité.

Ceci amène à considérer des espaces de fonctions $[D \to D]$ très contraints par rapport à l’ensemble des fonctions $D \to D$ (je laisse le lecteur mathématicien essayer d’en imaginer la raison); c’est un vaste sujet de recherches mathématiques…

Une famille de modèles proposés par Dana Scott, notés $D_\infty$, satisfont la propriété d’extensionnalité (◇). Un autre modèle, noté $P\omega$ et présenté ultérieurement, ne satisfait pas cette extensionnalité.

En pratique, le principe d’extensionnalité est généralement ajouté explicitement au lambda-calcul à travers une règle d’η-conversion (eta-conversion) explicite.

Dans le noyau de Lean 4 (qui repose sur une version typée du lambda-calcul), on retrouve par exemple cette notion dans le vérificateur de types.

---

Vous pouvez commenter cette entrée sur Bluesky, Twitter ou Mathstodon.
N'hésitez pas également à m'envoyer un email (thomas@lipsum.dev).

---

• ← Blague, énigme et raisonnement automatisé