Le λ-calcul

Lionel Vaux Auclair

I2M, université d’Aix-Marseille

M2 IMD
λ-termes

L’ensemble Λ des λ-termes est défini inductivement par :

Λ 3 s, t, . . . ::= x | λx.s | s t

où x parcourt un ensemble infini dénombrable de variables V

et les occurrences de x dans s sont liées par l’abstraction λx.s

Il faut voir ces termes comme codant des fonctions :

I λx.s abstrait la variable x dans s : c’est le code de x 7→ s ;
Ne pas confondre une expression dépendant d’une variable avec la fonction correspondante
(par exemple, x + 1 6= y + 1, tandis que (x 7→ x + 1) = (y 7→ y + 1)).
I s t est l’application du terme s au terme t ;
I le calcul fait le lien entre les deux.
β-réduction
L’expression (λx.s) t se réduit en s[t/x] (la valeur de s pour x := t).
Une analogie : si P est un polynôme en x et y , x 7→ P associe à chaque valeur de x
le polynôme en y obtenu en remplaçant x par sa valeur.
β-réduction
L’expression (λx.s) t se réduit en s[t/x] (la valeur de s pour x := t).
Une analogie : si P est un polynôme en x et y , x 7→ P associe à chaque valeur de x
le polynôme en y obtenu en remplaçant x par sa valeur.

Plus formellement :
I On note s[t/x] le résultat de la substitution de t à x dans s.
On utilise l’α-équivalence pour éviter les captures de variables libres de t.
Pour fixer les idées : exercices 1 et 2.
I On appelle redex (pour reducible expression) toute expression de la forme (λx.s) t.
I On dit que s[t/x] est le réduit de (λx.s) t, et on note (λx.s) t →β0 s[t/x].
I La β-réduction →β est la plus petite relation compatible avec la syntaxe sur Λ
contenant →β0 .
β-réduction : définition

Définition
La β-réduction →β est définie inductivement par :
I (λx.s) t →β s[t/x] pour tous s, t, x ;
I si s →β s 0 alors λx.s →β λx.s 0 , s t →β s 0 t et t s →β t s 0 pour tout t.

Autrement dit, s →β s 0 si et seulement si on peut dériver s → s 0 par les règles

suivantes :
s → s0 s → s0 t → t0
(λx.s) t → s[t/x] λx.s → λx.s 0 s t → s0 t s t → s t0
Pause ! Où est passée la logique ?
Considérons une grammaire de types fonctionnels simples :

A, B, C ::= X | A → B

et fixons une partition de V en ensembles VA pour chaque type A.

Définition (λ-termes simplement typés (à la Church))
Les termes typés sont définis inductivement comme suit :
I une variable x est du type A tel que x ∈ VA ;
I si s est de type B et x ∈ VA alors λx A .s est de type A → B ;
I si s est de type A → B et t de type A alors s t est de type B.

Ça vous rappelle quelque chose ?

Isomorphisme de Curry–Howard
Une preuve dans le système :

(ax) Γ, A ` B Γ`A⇒B Γ`A

Γ, A ` A (⇒i ) (⇒e )
Γ`A⇒B Γ`B
c’est la même chose qu’un λ-terme typé s (+ un ensemble de variables Γ ⊇ VL(s)).
Mieux :
Lemme
Si s est de type B, t est de type A et x ∈ VA alors s[t/x] est bien typé, de type B.
Démonstration: Par induction sur s.

La β-réduction = l’élimination des coupures en déduction naturelle pour ⇒.

On tirera ce fil plus tard : on étudie d’abord le λ-calcul per se.
Exemples
Quelques termes :
I I := λx.x (identité)
I K := λx.λy .x (première projection)
I 0 := λx.λy .y (deuxième projection)
I 1 := λf .λx.f x (identité sur les fonctions)
I ◦ := λf .λg .λx.f (g x) (composition)
I S := λf .λg .λx.f x (g x) (composition un peu tordue)
I 2 := λf .λx.f (f x) (2ème itération)

Notations (économisons les parenthèses)

I on note s t1 · · · tn := (· · · (s t1 ) · · ·) tn
I l’application a priorité sur l’abstraction
 

λf .λg .λx.f x (g x) se lit λf . λg . λx.{(f x) (g x)}
Exemples
Quelques termes :
I I := λx.x (identité)
I K := λx.λy .x (première projection)
I 0 := λx.λy .y (deuxième projection)
I 1 := λf .λx.f x (identité sur les fonctions)
I ◦ := λf .λg .λx.f (g x) (composition)
I S := λf .λg .λx.f x (g x) (composition un peu tordue)
I 2 := λf .λx.f (f x) (2ème itération)
Quelques réductions : en choisissant f , g , x, y ∈ V distinctes et 6∈ VL(s, t)

I s →β s λh.◦ h h →β λh.(λg .λx.h (g x)) h

K s t →β (λy .s) t →β s →β λh.λx.h (h x) = 2
0 s t →β I t →β t S s I →β (λg .λx.s x (g x)) I
1 s →β λx.s x →β λx.s x (I x) →β λx.s x x
Formes irréductibles
Jusque là, on est toujours arrivés à un terme sans redex visible.
Définition
Un terme s ∈ Λ est dit β-irréductible s’il ne contient aucun redex ou, de manière
équivalente s’il n’y a pas de s 0 t.q. s →β s 0 .
Formes irréductibles
Jusque là, on est toujours arrivés à un terme sans redex visible.
Définition
Un terme s ∈ Λ est dit β-irréductible s’il ne contient aucun redex ou, de manière
équivalente s’il n’y a pas de s 0 t.q. s →β s 0 .

Deux questions :
I peut-on toujours se ramener à une forme irréductible ?
I un terme peut-il avoir plusieurs formes irréductibles ?
Formes irréductibles
Jusque là, on est toujours arrivés à un terme sans redex visible.
Définition
Un terme s ∈ Λ est dit β-irréductible s’il ne contient aucun redex ou, de manière
équivalente s’il n’y a pas de s 0 t.q. s →β s 0 .

Deux questions :
I peut-on toujours se ramener à une forme irréductible ?
I un terme peut-il avoir plusieurs formes irréductibles ?
Considérons les termes :
I ∆ := λx.x x (auto-application)

∆ I →β I I →β I ∆ 2 →β 2 2 →β λh.2 (2 h) →β λh.λx.2 h (2 h x)
→2β λh.λx.2 h (h (h x)) →2β λh.λx.h (h (h (h x))) = 4
Formes irréductibles
Jusque là, on est toujours arrivés à un terme sans redex visible.
Définition
Un terme s ∈ Λ est dit β-irréductible s’il ne contient aucun redex ou, de manière
équivalente s’il n’y a pas de s 0 t.q. s →β s 0 .

Deux questions :
I peut-on toujours se ramener à une forme irréductible ? NON
I un terme peut-il avoir plusieurs formes irréductibles ?
Considérons les termes :
I ∆ := λx.x x (auto-application)
I Ω := ∆ ∆ (boucle infinie)

∆ ∆ →β ∆ ∆
Formes irréductibles
Jusque là, on est toujours arrivés à un terme sans redex visible.
Définition
Un terme s ∈ Λ est dit β-irréductible s’il ne contient aucun redex ou, de manière
équivalente s’il n’y a pas de s 0 t.q. s →β s 0 .

Deux questions :
I peut-on toujours se ramener à une forme irréductible ? NON
I un terme peut-il avoir plusieurs formes irréductibles ?
Considérons les termes :
I ∆ := λx.x x (auto-application)
I Ω := ∆ ∆ (boucle infinie)

λh.λx.2 h (2 h x) →2β λh.λx.2 h (h (h x))

Formes irréductibles
Jusque là, on est toujours arrivés à un terme sans redex visible.
Définition
Un terme s ∈ Λ est dit β-irréductible s’il ne contient aucun redex ou, de manière
équivalente s’il n’y a pas de s 0 t.q. s →β s 0 .

Deux questions :
I peut-on toujours se ramener à une forme irréductible ? NON
I un terme peut-il avoir plusieurs formes irréductibles ? pas évident
Considérons les termes :
I ∆ := λx.x x (auto-application)
I Ω := ∆ ∆ (boucle infinie)

λh.λx.2 h (2 h x) →2β λh.λx.h (h (2 h x))

Formes irréductibles
Jusque là, on est toujours arrivés à un terme sans redex visible.
Définition
Un terme s ∈ Λ est dit β-irréductible s’il ne contient aucun redex ou, de manière
équivalente s’il n’y a pas de s 0 t.q. s →β s 0 .

Deux questions :
I peut-on toujours se ramener à une forme irréductible ? NON
I un terme peut-il avoir plusieurs formes irréductibles ? pas évident
Considérons les termes :
I ∆ := λx.x x (auto-application)
I Ω := ∆ ∆ (boucle infinie)

Exercice 3.
Confluence

On va montrer qu’un terme se réduit à au plus une forme irréductible.

Il suffit de montrer que →β est confluente :

Définition
Soit → ⊆ A × A une relation binaire sur un ensemble A.
I On dit que → est fortement confluente si, chaque fois que a → a1 et a → a2 , il
existe un a0 ∈ A tel que a1 → a0 et a2 → a0 .
I La fermeture réflexive et transitive de → est la plus petite relation réflexive et
transitive contenant → : on la note →∗ .
I On dit que → est confluente si →∗ est fortement confluente.

Alors si s →∗β t1 et s →∗β t2 avec t1 et t2 irréductibles, on a nécessairement t1 = t2 .

Réduction et substitution
Si on essaie de prouver la confluence forte pour →β , en regardant les cas possibles de couples
de réduction s →β s1 et s →β s2 , le cas du redex (par ex. (λx.s) t →β s[t/x] et
(λx.s) t →β (λx.s) t 0 avec t →β t 0 ) nous amène étudier la réduction dans une substitution :
Lemme
I Si s →β s 0 alors s[t/x] →β s 0 [t/x].
I Si t →β t 0 alors s[t/x] →∗β s[t 0 /x].

Démonstration: Par induction sur s.

Il faut étendre à →∗β dans le deuxième cas : →β n’est pas fortement confluente (voir avec 2 (I I )).

Corollaire
Si s →∗β s 0 et t →∗β t 0 alors s[t/x] →∗β s 0 [t 0 /x].

Mais si on cherche à regarder tous les cas possibles pour des réductions s →∗β s1 et s →∗β s2
on s’y perd à cause de la transitivité.
Réduction parallèle
On utilise une méthode dûe à Tait et Martin-Löf : on étend →β en une relation
contextuelle, en autorisant la réduction simultanée d’un nombre quelconque de redex.
Définition
La β-réduction parallèle ⇒β est définie inductivement par :
I s ⇒β s pour tout s ∈ Λ ;
I si s ⇒β s 0 alors λx.s ⇒β λx.s 0 ,
I si s ⇒β s 0 et t ⇒β t 0 alors s t ⇒β s 0 t 0 et (λx.s) t ⇒β s 0 [t 0 /x].

Autrement dit, s ⇒β s 0 si et seulement si on peut dériver s → s 0 par les règles

suivantes :
s → s0 t → t0 s → s0 s → s0 t → t0
s→s (λx.s) t → s 0 [t 0 /x] λx.s → λx.s 0 s t → s0 t0
Confluence forte de la réduction parallèle
Lemme
Si s ⇒β s 0 et t ⇒β t 0 alors s[t/x] ⇒β s 0 [t 0 /x].
Démonstration: Comme pour →β .

Théorème
Si s ⇒β s1 et s ⇒β s2 alors il existe s 0 t.q. s1 ⇒β s 0 et s2 ⇒β s 0 .
Démonstration: Par induction sur la définition de chaque réduction, en utilisant le lemme de
substitution dans les cas des redex.
Corollaire
La β-réduction parallèle est confluente.
Démonstration: Une relation fortement confluente est toujours confluente.
Exercice 4.
Church–Rosser
Définition
On appelle β-équivalence la fermeture réflexive, symétrique et transitive =β de →β
(c.-à-d. la plus petite relation d’équivalence contenant →β ).

Théorème
On a s =β s 0 ssi il existe t tel que s →∗β t et s 0 →∗β t.

Démonstration:
I Il est facile de voir que →β ⊆ ⇒β , par induction sur →β .
I On a aussi ⇒β ⊆ →∗β , par induction sur ⇒β , et le lemme de substitution pour →∗β .
I Donc →∗β = ⇒∗β , et on obtient la confluence de →β .
I Le fait que le théorème s’en déduise est un fait général sur les relations binaires.
Exercice 5.
Formes normales et structure de tête
Par Church–Rosser, pour tout s ∈ Λ il y a au plus un t irréductible avec s =β t :
on dit alors que t est la forme normale de s et on note t = N(s).
Lemme
Tout λ-terme s peut s’écrire sous l’une des deux formes :
I s = λx1 . · · · λxn .(λx.u) t0 · · · tk : on dit que (λx.u) t0 est le redex de tête de s ;
I s = λx1 . · · · λxn .x t1 · · · tk : on dit que s est en forme normale de tête et que x est
sa variable de tête.
Démonstration: Par induction sur s.

Corollaire
Un λ-terme s est irréductible ssi il s’écrit s = λx1 . · · · λxn .x t1 · · · tk , avec t1 , . . . , tk
irréductibles.
Réduction de tête
Définition
La β-réduction de tête →βt est définie par la seule étape :

λx1 . · · · λxn .(λx.s) t0 · · · tk →βt λx1 . · · · λxn .s[t0 /x] t1 · · · tk

Cette réduction est fonctionnelle : il y a au plus un s 0 tel que s →βt s 0 .

Lemme
Un λ-terme s est normalisable de tête (c.-à-d. qu’il existe une forme normale de tête t
t.q. s =β t) ssi la suite des réductions de tête de s est finie.
Démonstration: Admis (pour l’instant).

La réduction de tête peut mener à une autre forme normale de tête que t
(mais elle aura la même structure de tête par confluence).
Réduction gauche
Définition
La β-réduction gauche →βg est définie inductivement par :
I si s →βt s 0 alors s →βg s 0 ;
I s →βg λx1 . · · · λxn .x t1 · · · ti0 · · · tk si
I s = λx1 . · · · λxn .x t1 · · · tk ,
I ti →βg ti0 ,
I et tj est en forme normale pour 1 ≤ j < i.

Théorème
Si s admet une forme normale, alors s →∗βg N(s).

Démonstration: Par induction sur N(s), en appliquant le lemme sur la réduction de tête.
On a donc une stratégie pour normaliser.
Exercice 6.
Références

Barendregt (exhaustif) et Krivine (économe).