Lambda-calcul

Historique

Le lambda-calcul (ou λ-calcul) est un langage de programmation théorique inventé par Alonzo Church dans les années 1930. Ce langage a eu autant d'importance que les machines de Turing dans la théorie de la calculabilité.

Syntaxe

Les objets du lambda-calcul sont les lambda-termes. Il en existe trois sortes :

les variables : $x$ , $y$ , ...
les applications : si $u$ et $v$ sont des lambda-termes $u v$ est aussi un lambda-terme. On peut alors voir $u$ comme une fonction et $v$ comme un argument.
les abstractions : si $x$ est une variable et $u$ un lambda-terme alors $λ x . u$ est un lambda-terme. Intuitivement, $λ x . u$ est la fonction qui à $x$ associe $u$ .

Pour des raisons pratiques, on introduit parfois également des constantes et des opérations primitives (par exemple les entiers naturels et les opérations + et * usuelles). Du point de vue du lambda calcul « pur », ces primitives se comportent comme des variables, si ce n'est qu'on peut leur donner des règles de calcul spéciales (cf. ci-dessous).

Notations

Vous aurez remarqué qu'un lambda ne prend qu'un seul argument mais on peut contourner cet obstacle de cette façon : λx.(λy.u). Au point de vue de la notation on peut aussi écrire λx.λy.u ou λxλy.u ou tout simplement λxy.u.

Du point de vues du parenthésage x₁ x₂ ... x_n = ((x₁ x₂) ... x_n)

Variables libres

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

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

Si un lambda-terme n'a pas de variables libres alors on dit qu'il est clos.

Principes

On définit la substitution d'une variable x dans un lambda terme u dans un terme t par récurrence sur t (et on la note t[x := u]) :

si t est une variable alors t[x := u]=u si x=t et t sinon
si t = v w alors t[x := u] = v[x := u] w[x := u]
si t = λy.v alors t[x := u] = λy.(v[x := u]) si x $\neq$ t et t sinon

Dans le dernier cas on fera attention à ce que y ne soit pas une variable libre de u. En effet, elle serait alors « capturée » par le lambda externe. Si c'est le cas on renomme y et toutes ses occurrences dans v. C'est l'alpha-conversion, qui permet d'identifier $λ$ y.v et $λ$ z.v[y := z]. Autrement dit, les variables sous les lambdas sont des variables muettes.

exemples :

$λ$ x.xy[y := a] = $λ$ x.xa
$λ$ x.xy[y := x] = $λ$ z.zx(et non $λ$ x.xx, qui est totalement différent)

Réductions

On appelle rédex un terme de la forme ( $λ$ x.u) v. On définit alors la bêta-contraction (ou réduction) de ( $λ$ x.u) v comme u[x := v]; on note ? la relation de réduction: ainsi ( $λ$ x.u) v donne u[x := v]. Inversément u[x := v] est appelé le contractum de ( $λ$ x.u) v.

Exemple de réduction: ( $λ$ x.xy)a donne xy[x := a] = ay

On note ?^* la fermeture réflexive transitive de la relation ? de contraction (?^* est appelée la bêta-réduction) et =_? sa fermeture réflexive symétrique et transitive (appelée bêta-conversion ou bêta-equivalence).

On utilise également assez fréquemment une autre opération, appelée êta-réduction (ou son inverse la êta-expansion), définie ainsi : $λ$ x.ux ?_? u, lorsque x n'apparaît pas libre dans u.

Enfin, si on s'est donné des primitives, on peut fixer leur comportement calculatoire au moyen des règles de delta-réduction. Par exemple, si on s'est donné les entiers et + comme termes supplémentaires, les tables d'addition serviront de delta-règles. Comme les primitives sont par définition complètement étrangères au lambda-calcul, leurs règles de calcul peuvent a priori adopter n'importe quelle forme. Toutefois, si on veut étendre les propriétés mentionnées ci-dessous au cas d'un calcul avec des primitives, on est amené à faire quelques hypothèses sur les règles ajoutées.

La normalisation : notion de calcul

Un lambda-terme t est dit en forme normale si aucune bêta-contraction ne peut lui être appliquée, c'est-à-dire si t ne contient aucun rédex.

On dit qu'un lambda-terme t est normalisable s'il existe une forme normale u et une suite de lambda-termes t₁, ..., t_n telle que t = t₁, u = t_n et pour tout i (1 ≤ i < n) t_i ? t_i+1 ou t_i+1 ? t_i. Un tel u est appelé la forme normale de t.

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.

Souvent on appelle ce dernier théorème Théorème de Church-Rosser car les deux théorèmes sont équivalents.

Un lambda-terme est dit calculable s'il admet une forme normale. 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 que deux termes ne sont pas tous bêta-convertibles entre eux.

Voici l'exemple le plus classique de lambda-terme non calculable :
$Ω = (λ x . x x)(λ x . x x)$
Le lambda terme $Ω$ n'est pas calculable car il boucle infiniment sur lui-même.

Différents Lambda-calculs

Le lambda-calcul défini ci-dessus n'est qu'une trame syntaxique appelée à être complétée par une sémantique qui permet de donner une signification à ce que l'on fait par ce lambda-calcul. On peut distinguer deux grandes classes de lambda-calculs : les lambda-calculs non typés et les lambda-calculs typés. La différence est qu'avec les types on va restreindre les termes valides. C’est-à-dire que généralement on va chercher à enlever les termes qui ne sont pas normalisables. Le but est d'avoir un lambda-calcul qui vérfie les propriétés de Church-Rosser et de normalisation (voire normalisation forte).

Même si en restreignant les termes valides par les types on garde généralement les plus intéressants. De plus grâce à l'isomorphisme de Curry-Howard on peut relier un lambda calcul à une logique et par là un terme correspond à une preuve. Intuitivement c'est très fort parce que celà permet d'associer à une preuve mathématique un programme informatique. C'est sur celà que se basent une partie des prouveurs automatiques et semi-automatiques.

Le Lambda-calcul non typé

On va utiliser des codages pour créer les objets usuels de l'informatique. Grâce à ces objets on peut tout calculer car on peut simuler une machine de Turing. Et grâce aux théorèmes de la théorie de la calculabilité on en déduit que le lambda-calcul est un modèle universel de calcul.

Les booléens

Pour faire de vrais calculs on va faire des codages. On définit le booléen vrai par ?ab.a et faux par ?ab.b

Nous remarquons que vrai x y ?^* x et que faux x y ?^* y. Nous en déduisons un programme pour ifthenelse : ?buv.buv On pourra vérifier que ifthenelse vrai x y ?^* x et 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 ?ab.ifthenelse a b a ou = ?ab.ifthenelse a vrai b ou ?ab.ifthenelse a a b

Les entiers

Nous allons utiliser les Entiers de Church. n = ?fx.f(f(...(f x)...)) avec n f. Par exemple 0 = ?fx.x, 3 = ?fx.f(f(f x)).

Quelques fonctions

Il y a deux manières de coder la fonction successeur. Soit en ajoutant un f en tête soit en queue. Voici les deux lambda-termes :

?nfx.f(n f x)
?nfx.n f (f x)

De la même manière il est possible de faire l'addition en « concaténant » les deux lambda-termes : ?npfx.n f (p f x)

Pour coder la multiplication c'est un peu plus futé : on va utiliser le f pour « propager » une fonction sur tout le terme : ?npfx.n (p f) x

L'exponentielle n'est pas triviale contrairement à ce que son écriture laisse penser, et lors de la réduction on est obligé de renommer les variables : ?np.p n

Les itérateurs

Tout cela n'est pas très intuitif alors pour pouvoir coder des algorithmes on définit la fonction d'itération sur les entiers : iterate = ?nuv.n u v

Le truc c'est que v est le cas de base et u une fonction sur le cas de récurrence.

Par exemple l'addition qui provient de ces équations

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

On va donc programmer par itération avec le successeur sur le cas de base p. Le lambda-terme est donc ?np.iterate n successeur p. On remarquera que add ?^* n successeur p.

Les couples

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

Les listes

On peut remarquer qu'un entier est une liste qui ne contient pas de clé. En rajoutant une information on peut construire les listes d'une manière analogue aux entiers : [a₁ ; ... ; a_n] = ?gy. g a₁ (... (g a_n y)...)

Les itérateurs sur les listes

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). Cela 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

Les arbres

Le combinateur de point fixe

Le combinateur de point fixe permet de faire des boucles infinies. Ceci est pratique ou nécessaire pour programmer certaines choses comme la fonction pgcd ou la fonction d'Ackermann par exemple.

Le Lambda-calcul simplement typé

On introduit des types simples sur les termes, et on n'accepte que les termes bien typés. Outre un souci de clareté et de compréhension, cela permet d'avoir 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. En contrepartie, le pouvoir expressif de ce calcul est très limité (ainsi, l'exponentielle ne peut y être définie, ni même la fonction $n\rightarrow 2^n$ ).

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

un type de base $ι$ (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 $τ 1$ et $τ 2$ sont des types, $\tau_1\rightarrow\tau_2$ est un type.

Intuitivement, le second cas représente le type des fonctions acceptant un élément de type $τ 1$ et renvoyant un élément de type $τ 2$ .

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

si $(x,\tau)\in\Gamma$ , alors $\Gamma\vdash x:\tau$ .
si $\Gamma\cup (x,\tau_1)\vdash u:\tau_2$ , alors $\Gamma\vdash \lambda x.u:\tau_1\rightarrow\tau_2$ .
si $\Gamma\vdash u:\tau_1\rightarrow\tau_2$ et $\Gamma\vdash v:\tau_1$ , alors $\Gamma\vdash u v:\tau_2$

Si on s'est donné des primitives, il faut leur donner un type (via $Γ$ ). Dans le cas de la règle de l'abstraction, l'ajout de $x$ masque une éventuelle occurrence précédente de la variable dans $Γ$ .

Les Lambda-calculs typés d'ordres supérieurs

Le lambda-calcul simplement typé est trop restrictif pour pouvoir calculer toutes les fonctions que l'on a besoin habituellement en mathématiques et donc dans un programme informatique. Un autre modèle permet de calculer toutes les fonctions calculables dans un temps plus ou moins acceptable : la récursion primitive. Ce système permet de calculer la plupart des fonctions calculables par une machine de Turing. Le problème est au niveau de la complexité car on n'a pas de bons algorithmes de calcul et donc de manière efficace de calculer. Ce problème est réglé avec le Système T de Gödel qui fusionne la récursion primitive et le lambda-calcul simplement typé. Dans ce système on n'a pas seulement de nouveaux algorithmes mais aussi de nouveaux programmes comme la fameuse fonction d'Ackermann qui est la plus petite fonction non primitive récursive. Cependant elle est hors de portée des ordinateurs actuels car on n'aurait même pas assez de mémoire pour stocker le résultat de la fonction appliquée aux arguments 5 5 par exemple.

Bien que ce modèle permet de calculer tout ce que l'on veut avec des algorithmes corrects, théoriquement on peut faire beaucoup mieux. Notamment par l'introduction des variables de type. Cela augmente la complexité (du point de vue compréhension et non informatique) du système mais augmente considérablement le pouvoir expressif. Pour les lambdas calculs typés du second ordre on peut faire des termes qui dépendent de types, des types qui dépendent de termes et des types qui dépendent de types. En faisant la combinaison de chacun on obtient huit lambda-calculs que Barendregt modélise sous forme de cube. L'extrémité du cube opposée à celle du lambda-calcul simplement typé est le calcul des constructions dû à Thierry Coquand, et a donné naissance au système coq.

Références

Henk Barendregt, The Lambda-Calculus. Volume 103, Elsevier Science Publishing Company, Amsterdam, 1984. -
Jean-Louis Krivine, Lambda-Calcul, types et modèles, Masson 1991.
Steven Fortune, Daniel Leivant, Michael O'Donnell, The Expressiveness of Simple and Second-Order Type Structures. Journal of the ACM, Volume 30, pages 151-185, 1983.
Jean-Yves Girard, Paul Taylor, Yves Lafont, Proofs and Types, Cambridge University Press, New York, 1989 - ISBN 0-521-37181-3