Accueil |

Lambda-calcul

   

Sommaire
1 Historique
2 Définition
3 Notations
4 Principes
5 Calcul
6 Différents Lambda-calculs
7 Livres recommandés

Historique

Le lambda-calcul est un langage théorique inventé par Alonzo Church dans les années 30. Ce langage a eu autant d'importance que les machines de Turing dans la théorie de la Calculabilité.

Définition

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

En fait les lambdas sont des fonctions et on calcule à  partir des applications.

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.λ.u ou λxλy.u ou tout simplement λxy.u

Du point de vue du parenthésage x1 x2 ... xn = ((x1 x2) ... xn)

On définit les variables libres d'un terme par récurrence :

Principes

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

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 note t[x ← u]) :

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 occurences 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 :

On appelle rédex un terme de la forme (λx.u) v. On définit alors la réduction par (λx.u) v → u[x ← v] et u[x ← v] est appelé le contractum de (λx.u) v.

(λx.xy)a → xy[x ← a] = ay

On note →* sa fermeture transitive et =Β sa fermeture réflexive (la bêta-réduction), symétrique et transitive.

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, o๠x n'apparaît pas libre dans u.

Calcul

On dit qu'un lambda-terme t est normalisable si il existe une suite de lambda-termes t1, ..., tn telle que t = t1, u = tn et pour tout i (1 ≤ i < n) ti → ti+1 ou ti+1 → ti. u est appelé la forme normale de t.

Théorème de Church-Rosser (ou de confluence) : soient t, u1 et u2 des lambda-termes tels que t →* u1 et t →* u2. Alors il existe un lambda-terme v tel que u1 →* v et u2 →* v.

Un lambda-terme est dit calculable si il admet une forme normale.

Voici l'exemple le plus classique de lambda-terme non calculable : Δ = λx.xx Le lambda terme Δ Δ n'est pas calculable car Δ Δ →* Δ Δ

Différents Lambda-calculs

Le Lambda-calcul non typé

On va utiliser des codages pour créer les objets usuels de l'informatique.

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. Sous 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

A 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 true 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 :

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'exponentienne 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 celà  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

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 π1 = λc.c (λab.a) et π2 = λ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 π1(λ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 : [a1 ; ... ; an] = λgy. g a1 (... (g an 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 : La longueur d'une liste est définie par

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 exemples

Le Lambda-calcul simplement typé

On introduit des types simples sur les termes. 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).

Le Lambda-calcul typé du second ordre

Pour pouvoir calculer plus de choses on introduit des variables de type. Cela augmente la complexité (au niveau compréhension) du système mais augmente considérablement le pouvoir expressif.

Livres recommandés