Lambda-calcul

L'idée de base du lambda-calcul est que tout est fonction. Une fonction est en particulier exprimée par une expression qui peut contenir des fonctions qui ne sont pas encore définies : ces dernières sont alors remplacées par des variables. Il existe une opération de base, appelée application :

Appliquer l'expression ${\displaystyle A}$ (qui décrit une fonction) à l'expression ${\displaystyle B}$ (qui décrit une fonction) se note ${\displaystyle A~B}$.

On peut aussi fabriquer des fonctions en disant que si E est une expression[2], on crée la fonction qui à x fait correspondre l'expression E; On écrit λx.E cette nouvelle fonction[3].

Le nom de la variable n'est pas plus important qu'il ne l'est dans une expression comme ∀x P(x) qui est équivalente à ∀y P(y) . Autrement dit si E[y/x] est l'expression E dans laquelle toutes les occurrences de x ont été renommées en y, on considérera que les expressions λx.E et λy.E[y/x] sont équivalentes.

En utilisant les outils dont on vient de se doter, on obtient, par applications et abstractions, des fonctions assez compliquées que l'on peut vouloir simplifier ou évaluer. Simplifier une application de la forme (λx.E) P revient à la transformer en une variante de l'expression E dans laquelle toute occurrence libre de x est remplacée par P. Cette forme de simplification s'appelle une contraction (ou une β-contraction si l'on veut rappeler que l'on applique la règle β du lambda-calcul).

Sur cette base, on peut construire quelques fonctions intéressantes, comme la fonction identité ${\displaystyle I}$, qui est la fonction qui à ${\displaystyle x}$ fait correspondre ${\displaystyle x}$, autrement dit la fonction ${\displaystyle \lambda x.x}$. On peut aussi construire la fonction constante égale à ${\displaystyle x}$, à savoir ${\displaystyle \lambda y.x}$.

De là on peut construire la fonction qui fabrique les fonctions constantes, pourvu qu'on lui donne la constante comme paramètre, autrement dit la fonction ${\displaystyle \lambda x.(\lambda y.x)}$, c'est-à-dire la fonction qui à ${\displaystyle x}$ fait correspondre la fonction constamment égale à ${\displaystyle x}$.

On peut aussi par exemple construire une fonction ${\displaystyle C}$ qui permute l'utilisation des paramètres d'une autre fonction, plus précisément si ${\displaystyle M}$ est une expression, on voudrait que ${\displaystyle ((C~M)~x)~y}$ fonctionne comme ${\displaystyle (M~y)~x}$. La fonction ${\displaystyle C\,}$ est la fonction ${\displaystyle \lambda z.(\lambda x.(\lambda y.(z~y)~x))}$. Si on applique la fonction ${\displaystyle C\,}$ à ${\displaystyle M\,}$ on obtient ${\displaystyle (\lambda z.(\lambda x.(\lambda y.(z~y)~x)))\;M}$ que l'on peut simplifier en ${\displaystyle (\lambda x.(\lambda y.(M~y)~x))}$.

Jusqu'à maintenant nous avons été assez informels[4]. L'idée du lambda-calcul consiste à fournir un langage précis pour décrire les fonctions et les simplifier.

Alonzo Church connaissait la relation entre son calcul et celui des Principia Mathematica de Russell et Whitehead. Or ceux-ci utilisent la notation ${\displaystyle {\hat {x}}f(x)}$ pour noter l'abstraction, mais Church utilisa à la place la notation ${\displaystyle {\hat {~~}}xf(x)}$ qui devint par la suite ${\displaystyle \lambda x.f(x)}$[6]. Peano a lui aussi défini l'abstraction dans son Formulaire de mathématique[7], il utilise notamment la notation, ${\displaystyle a{\bar {x}}}$ pour noter la fonction ${\displaystyle f}$ telle que ${\displaystyle fx=a}$[8].

Pour délimiter les applications, on utilise des parenthèses, mais par souci de clarté, on omet certaines parenthèses. Par exemple, on écrit x₁ x₂ ... x_n pour ((x₁ x₂) ... x_n).

Il y a en fait deux conventions :

• Association à gauche, l'expression ((M₀ M₁) (M₂M₃)) s'écrit M₀ M₁ (M₂M₃). Quand une application s'applique à une autre application, on ne met de parenthèse que sur l'application de droite. Formellement, la grammaire du lambda calcul parenthésé est alors :Λ ::= Var | λ Var. L | Λ L ; L ::= Var | λ Var. L | (Λ L)
• Parenthésage du terme de tête, l'expression ((M₀ M₁) (M₂M₃)) s'écrit (M₀) M₁ (M₂) M₃. Un terme entre parenthèses est le premier d'une suite d'applications. Ainsi les arguments d'un terme sont facilement identifiables. Formellement, la grammaire du lambda-calcul parenthésé est alors :Λ ::= Var | λ Var. Λ | (Λ) Λ⁺.

Shönfinkel et Curry ont introduit la curryfication : c'est un procédé pour représenter une fonction à plusieurs arguments. Par exemple, la fonction qui au couple (x, y) associe u est considérée comme une fonction qui, à x, associe une fonction qui, à y, associe u. Elle est donc notée : λx.(λy.u). Cela s'écrit aussi λx.λy.u ou λxλy.u ou tout simplement λxy.u. Par exemple, la fonction qui, au couple (x, y) associe x+y sera notée λx.λy.x+y ou plus simplement λxy.x+y.

Dans les expressions mathématiques en général et dans le lambda calcul en particulier, il y a deux catégories de variables : les variables libres et les variables liées (ou muettes). En lambda-calcul, une variable est liée[9] par un λ. Une variable liée a une portée[10] et cette portée est locale. De plus, on peut renommer une variable liée sans changer la signification globale de l'expression entière où elle figure. Une variable qui n'est pas liée est dite libre.

Par exemple dans l'expression ${\displaystyle \textstyle \int _{a}^{b}{(x+y)~dy}}$, la variable ${\displaystyle x}$ est libre, mais la variable ${\displaystyle y}$ est liée (par le ${\displaystyle dy}$). Cette expression est « la même » que ${\displaystyle \textstyle \int _{a}^{b}{(x+z)~dz}}$ car ${\displaystyle y}$ était un nom local, tout comme l'est ${\displaystyle z}$. Par contre ${\displaystyle \textstyle \int _{a}^{b}{(z+y)~dy}}$ ne correspond pas à la même expression car le ${\displaystyle z}$ est libre.

Tout comme l'intégrale lie la variable d'intégration, le ${\displaystyle \lambda }$ lie la variable qui le suit.

Exemples:

• Dans ${\displaystyle \lambda x.xy}$, la variable ${\displaystyle x}$ est liée et la variable ${\displaystyle y}$ est libre. Ce terme est α-équivalent au terme ${\displaystyle \lambda t.ty}$.

• ${\displaystyle \lambda xyzt.z(xt)ab(zsy)}$ est α-équivalent à ${\displaystyle \lambda wjit.i(wt)ab(isj)}$.

• ${\displaystyle \lambda b.\lambda n.b}$ est α-équivalent à ${\displaystyle \lambda p.\lambda t.p}$.

On définit l'ensemble VL(t) des variables libres d'un terme t par récurrence :

• si ${\displaystyle x}$ est une variable alors VL(${\displaystyle x}$) = {${\displaystyle x}$}
• si u et v sont des lambda-termes alors VL(u v) = VL(u) ∪ VL(v)
• si ${\displaystyle x}$ est une variable et u un lambda-terme alors VL(λ${\displaystyle x}$.u) = VL(u) \{${\displaystyle x}$}

Un terme qui ne contient aucune variable libre est dit clos (ou fermé). On dit aussi que ce lambda-terme est un combinateur (d'après le concept apparenté de logique combinatoire).

Un terme qui n'est pas clos est dit ouvert.

Théorème de Church-Rosser : soient t et u deux termes tels que t =_β u. Il existe un terme v tel que t →^* v et u →^* v.

Théorème du losange (ou de confluence) : soient t, u₁ et u₂ des lambda-termes tels que t →^* u₁ et t →^* u₂. Alors il existe un lambda-terme v tel que u₁ →^* v et u₂ →^* v.

Grâce au Théorème de Church-Rosser on peut facilement montrer l’unicité de la forme normale ainsi que la cohérence du lambda-calcul (c'est-à-dire qu'il existe au moins deux termes distincts non bêta-convertibles).

On peut décrire la structure des termes en forme normale qui forment l'ensemble ${\displaystyle NF}$. Pour cela on décrit des termes dits neutres qui forment l'ensemble ${\displaystyle NE}$. Les termes neutres sont les termes dans lesquels une variable (par exemple ${\displaystyle x}$) est appliquée à des termes en forme normale. Ainsi, par exemple, ${\displaystyle xN_{1}...N_{p}}$ est neutre si ${\displaystyle N_{1}}$ ... ${\displaystyle N_{p}}$ sont en forme normale. Les termes en forme normale sont les termes neutres précédés de zéro, un ou plusieurs λ, autrement dit, des abstractions successives de termes en forme normale. Ainsi ${\displaystyle \lambda x.\lambda y.xN_{1}...N_{p}}$ est en forme normale. On peut décrire les termes en forme normale par une grammaire.

${\displaystyle NF::=NE\mid \lambda x.NF}$

${\displaystyle NE::=Var\mid NE\ NF}$

Exemples : ${\displaystyle x}$ est neutre, donc aussi en forme normale. ${\displaystyle \lambda x.x}$ est en forme normale. ${\displaystyle xx}$ est neutre. ${\displaystyle \lambda x.xx}$ est en forme normale. Par contre, ${\displaystyle (\lambda x.x)y}$ n'est pas en forme normale car il n'est pas neutre et il n'est pas une abstraction d'un terme en forme normale, mais aussi parce qu'il est lui-même un β-rédex, donc β-réductible.

Des codages simulent les objets usuels de l'informatique dont les entiers naturels, les fonctions récursives et les machines de Turing. Réciproquement le lambda-calcul peut être simulé par une machine de Turing. Grâce à la thèse de Church on en déduit que le lambda-calcul est un modèle universel de calcul.

Dans la partie Syntaxe, nous avons vu qu'il est pratique de définir des primitives. C'est ce que nous allons faire ici.

vrai = λab.a

faux = λab.b

Ceci n'est que la définition d'un codage, et l'on pourrait en définir d'autres.

Nous remarquons que : vrai x y →^* x et que : faux x y →^* y

Nous pouvons alors définir un lambda-terme représentant l'alternative: if-then-else. C'est une fonction à trois arguments, un booléen b et deux lambda termes u et v, qui retourne le premier si le booléen est vrai et le second sinon.

ifthenelse = λbuv.(b u v).

Notre fonction est bien vérifiée: ifthenelse vrai x y = (λbuv.(b u v)) vrai x y ; ifthenelse vrai x y → (λuv.(vrai u v)) x y ; ifthenelse vrai x y →^* (vrai x y) ; ifthenelse vrai x y →^* ( (λab.a) x y) ; ifthenelse vrai x y →^* x.

On verra de la même manière que ifthenelse faux x y →^* y.

À partir de là nous avons aussi un lambda-terme pour les opérations booléennes classiques : non = λb.ifthenelse b faux vrai ; et = λab.ifthenelse a b faux (ou bien λab.ifthenelse a b a) ; ou = λab.ifthenelse a vrai b (ou bien λab.ifthenelse a a b).

Ce qui suit est un codage en lambda-calcul des entiers que l'on appelle entiers de Church, du nom de leur concepteur. On pose : 0 = λfx.x, 1 = λfx.f x, 2 = λfx.f (f x), 3 = λfx.f (f (f x)) et d'une manière générale : n = λfx.f (f (...(f x)...)) = λfx.f ⁿx avec f itérée n fois.

Ainsi, l'entier n est vu comme la fonctionnelle qui, au couple ≺f, x≻, associe f ⁿ(x).

Il y a deux manières de coder la fonction successeur, soit en ajoutant un f en tête, soit en queue. Au départ nous avons n = λfx.f ⁿ x et nous voulons λfx.f ⁿ⁺¹ x. Il faut pouvoir rajouter un f soit au début des f (« sous » les lambdas), soit à la fin.

• Si nous choisissons de le mettre en tête, il faut pouvoir entrer « sous » les lambdas. Pour cela, si n est notre entier, on forme d'abord n f x, ce qui donne f ⁿ x. En mettant un f en tête, on obtient : f (n f x) → f(f ⁿ x) = f ⁿ⁺¹ x. Il suffit alors de compléter l'entête pour reconstruire un entier de Church : λfx.f (n f x) = λfx.f ⁿ⁺¹ x . Enfin pour avoir la « fonction » successeur, il faut bien entendu prendre un entier en paramètre, donc rajouter un lambda. Nous obtenons λnfx.f(n f x). Le lecteur pourra vérifier que (λnfx.f(n f x)) 3 = 4, avec 3 = λfx.f(f(f x))) et 4 = λfx.f(f(f(f x)))).

• Si par contre nous voulions mettre le f en queue, il suffit d'appliquer n f x non pas à x, mais à f x, à savoir n f (f x), ce qui se réduit à fⁿ (f x) = fⁿ⁺¹ x. On n'a plus qu'à refaire l'emballage comme dans le cas précédent et on obtient λnfx.n f (f x). La même vérification pourra être faite.

Les autres fonctions sont construites avec le même principe. Par exemple l'addition, en « concaténant » les deux lambda-termes : λnpfx.n f (p f x).

Pour coder la multiplication, on utilise le f pour « propager » une fonction sur tout le terme : λnpf.n (p f)

Le prédécesseur et la soustraction ne sont pas simples non plus. On en reparlera plus loin.

On peut définir le test à 0 ainsi : if0thenelse = λnab.n (λx.b) a, ou bien en utilisant les booléens λn.n (λx.faux) vrai.

Définissons d'abord une fonction d'itération sur les entiers : itère = λnuv.n u v

v est le cas de base et u une fonction. Si n est nul, on calcule v, sinon on calcule u ⁿ(v).

Par exemple l'addition qui provient des équations suivantes

• add(0, p) = p
• add(n+1, p) = add(n,p+1)

peut être définie comme suit. Le cas de base v est le nombre p, et la fonction u est la fonction successeur. Le lambda-terme correspondant au calcul de la somme est donc : add = λnp.itère n successeur p. On remarquera que add n p →^* n successeur p.

On peut coder des couples par c = λz.z a b où a est le premier élément et b le deuxième. On notera ce couple (a, b). Pour accéder aux deux parties on utilise π₁ = λc.c (λab.a) et π₂ = λc.c (λab.b). On reconnaîtra les booléens vrai et faux dans ces expressions et on laissera le soin au lecteur de réduire π₁(λz.z a b) en a.

On peut remarquer qu'un entier est une liste dont on ne regarde pas les éléments, en ne considérant donc que la longueur. En rajoutant une information correspondant aux éléments, on peut construire les listes d'une manière analogue aux entiers : [a₁ ; ... ; a_n] = λgy. g a₁ (... (g a_n y)...). Ainsi : [] = λgy.y ; [a₁] = λgy.g a₁ y ; [a₁ ; a₂] = λgy.g a₁ (g a₂ y).

De la même manière qu'on a introduit une itération sur les entiers on introduit une itération sur les listes. la fonction liste_it se définit par λlxm.l x m comme pour les entiers. Le concept est à peu près le même mais il y a des petites nuances. Nous allons voir par un exemple.

exemple : La longueur d'une liste est définie par

• longueur ([]) = 0
• longueur (x :: l) = 1 + longueur l

x :: l est la liste de tête x et de queue l (notation ML). La fonction longueur appliquée sur une liste l se code par : λl.liste_it l (λym.add (λfx.f x) m) (λfx.x) ou tout simplement λl.l (λym.add 1 m) 0.

Le principe de construction des entiers, des couples et des listes se généralise aux arbres binaires :

• constructeur de feuille : feuille = λngy.y n
• constructeur de nœud : nœud = λbcgy.g (b g y) (c g y) (avec b et c des arbres binaires)
• itérateur : arbre_it = λaxm.a x m

Un arbre est soit une feuille, soit un nœud. Dans ce modèle, aucune information n'est stockée au niveau des nœuds, les données (ou clés) sont conservées au niveau des feuilles uniquement. On peut alors définir la fonction qui calcule le nombre de feuilles d'un arbre : nb_feuilles = λa.arbre_it a (λbc.add b c) (λn.1), ou plus simplement: nb_feuilles = λa.a add (λn.1)

Pour définir le prédécesseur sur les entiers de Church, il faut utiliser les couples. L'idée est de reconstruire le prédécesseur par itération : pred = λn.π₁ (itère n (λc.(π₂ c, successeur (π₂ c))) (0,0)). Puisque le prédécesseur sur les entiers naturels n'est pas défini en 0, afin de définir une fonction totale, on a ici adopté la convention qu'il vaut 0.

On vérifie par exemple que pred 3 →^* π₁ (itère 3 (λc.(π₂ c, successeur (π₂ c))) (0,0)) →^* π₁ (2,3) →^* 2.

On en déduit que la soustraction est définissable par : sub = λnp.itère p pred n avec la convention que si p est plus grand que n, alors sub n p vaut 0.

En combinant prédécesseur et itérateur, on obtient un récurseur. Celui-ci se distingue de l'itérateur par le fait que la fonction qui est passée en argument a accès au prédécesseur.

rec = λnfx.π₁ (n (λc.(f (π₂ c) (π₁ c), successeur (π₂ c))) (x, 0))

Un combinateur de point fixe permet de construire pour chaque F, une solution à l'équation X = F X . Ceci est pratique pour programmer des fonctions qui ne s'expriment pas simplement par itération, telle que le pgcd, et c'est surtout nécessaire pour programmer des fonctions partielles.

Le combinateur de point fixe le plus simple, dû à Curry, est : Y = λf.(λx.f(x x))(λx.f(x x)). Turing a proposé un autre combinateur de point fixe : Θ = (λx. λy. (y (x x y))) (λx. λy. (y (x x y))).

On vérifie que ${\displaystyle Y\ g\ =_{\beta }\ g(Y\ g)}$ quel que soit g. Grâce au combinateur de point fixe, on peut par exemple définir une fonction qui prend en argument une fonction et teste si cette fonction argument renvoie vrai pour au moins un entier : teste_annulation = λg.Y (λfn.ou (g n) (f (successeur n))) 0.

Par exemple, si on définit la suite alternée des booléens vrai et faux : alterne = λn.itère n non faux, alors, on vérifie que : teste_annulation alterne →^* ou (alterne 0) (Y (λfn.ou (alterne n) (f successeur n)) (successeur 0)) →^* ou (alterne 1) (Y (λfn.ou (alterne n) (f successeur n)) (successeur 1)) →^* vrai.

On peut aussi définir le pgcd : pgcd = Y (λfnp.if0thenelse (sub p n) (if0thenelse (sub n p) p (f p (sub n p))) (f n (sub p n))).

Le récurseur et le point fixe sont des ingrédients clés permettant de montrer que toute fonction partielle récursive est définissable en λ-calcul lorsque les entiers sont interprétés par les entiers de Church. Réciproquement, les λ-termes peuvent être codés par des entiers et la réduction des λ-termes est définissable comme une fonction (partielle) récursive. Le λ-calcul est donc un modèle de la calculabilité.

On annote les termes par des expressions que l'on appelle des types. Pour cela, on fournit un moyen de donner un type à un terme. Si ce moyen réussit, on dit que le terme est bien typé. Outre le fait que cela donne une indication sur ce que « fait » la fonction, par exemple, elle transforme les objets d'un certain type en des objets d'un autre type, cela permet de garantir la normalisation forte, c'est-à-dire que, pour tous les termes, toutes les réductions aboutissent à une forme normale (qui est unique pour chaque terme de départ). Autrement dit, tous les calculs menés dans ce contexte terminent. Les types simples sont construits comme les types des fonctions, des fonctions de fonctions, des fonctions de fonctions de fonctions vers les fonctions, etc. Quoi qu'il puisse paraître, le pouvoir expressif de ce calcul est très limité (ainsi, l'exponentielle ne peut y être définie, ni même la fonction ${\displaystyle n\rightarrow 2^{n}}$).

Plus formellement, les types simples sont construits de la manière suivante:

• un type de base ${\displaystyle \iota }$ (si on a des primitives, on peut aussi se donner plusieurs types de bases, comme les entiers, les booléens, les caractères, etc. mais cela n'a pas d'incidence au niveau de la théorie).
• si ${\displaystyle \tau _{1}}$ et ${\displaystyle \tau _{2}}$ sont des types, ${\displaystyle \tau _{1}\rightarrow \tau _{2}}$ est un type.

Intuitivement, le second cas représente le type des fonctions acceptant un élément de type ${\displaystyle \tau _{1}}$ et renvoyant un élément de type ${\displaystyle \tau _{2}}$.

Un contexte ${\displaystyle \Gamma }$ est un ensemble de paires de la forme ${\displaystyle (x,\tau )}$ où ${\displaystyle x}$ est une variable et ${\displaystyle \tau }$ un type. Un jugement de typage est un triplet ${\displaystyle \Gamma \vdash t:\tau }$ (on dit alors que ${\displaystyle t}$ est bien typé dans ${\displaystyle \Gamma }$), défini récursivement par:

• si ${\displaystyle (x,\tau )\in \Gamma }$, alors ${\displaystyle \Gamma \vdash x:\tau }$.
• si ${\displaystyle \Gamma \cup (x,\tau _{1})\vdash u:\tau _{2}}$, alors ${\displaystyle \Gamma \vdash \lambda x\!:\!\tau _{1}.u\,:\,\tau _{1}\rightarrow \tau _{2}}$.
• si ${\displaystyle \Gamma \vdash u:\tau _{1}\rightarrow \tau _{2}}$ et ${\displaystyle \Gamma \vdash v:\tau _{1}}$, alors ${\displaystyle \Gamma \vdash uv:\tau _{2}}$

Si on a ajouté des constantes au lambda calcul, il faut leur donner un type (via ${\displaystyle \Gamma }$).

Le lambda-calcul simplement typé est trop restrictif pour exprimer toutes les fonctions calculables dont on a besoin en mathématiques et donc dans un programme informatique. Un moyen de dépasser l'expressivité du lambda-calcul simplement typé consiste à autoriser des variables de type et à quantifier sur elles, comme cela est fait dans le système F ou le calcul des constructions.

• Machine de Krivine
• Machine SECD
• Stratégie d'évaluation (informatique)
• Substitution explicite

• (en) Logiciel java en ligne de lambda-calcul
• Notices d'autorité :

  • BnF (données)
  • IdRef
  • LCCN
  • GND
  • Israël
  • Lettonie