Module THP Master1 2020/2021

Introduction au λ-calcul

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .

Pr. M. Mezghiche Introduction au λ-calcul

Définition des λ-termes

Syntaxe du langage du λ-calcul

L’alphabet du lambda-calcul (λC) se compose:
1. d’un ensemble de variables {x, y, z, ...}
2. de symboles auxilliaires λ, (, et ).
Les termes du lambda-calcul (λ-termes) sont définis inductivement
par:
1. chaque variable est un λ-terme,
2. si X et Y sont des λ-termes alors (XY) est un λ-terme,
3. si X est un λ-terme et x une variable alors (λx.X) est un
λ-terme.

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .

Pr. M. Mezghiche Introduction au λ-calcul

Exemples de λ-termes

λ-termes syntaxiquement corrects.

λx.x; (xy); (λxλy.(x(xy))); (λx.xy)(λxλy.(x(xy)))

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .

Pr. M. Mezghiche Introduction au λ-calcul

Convention d’écriture

Conventions

Associativité à gauche de l’application:

(((xy)z)t) − − − − − − − − − − − −− > (xyzt)

Associativité à droite de l’abstraction

λxλyλz.M − − − − − − − − − − − − − − − − − − > (λx(λy(λz.M)))

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .

Pr. M. Mezghiche Introduction au λ-calcul

Notion de Variable libre, variable liée

M ≡ λxyz.(xzt)y
1. Variables liées de M : x, y et z
2. Variable libre de M: t

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .

Pr. M. Mezghiche Introduction au λ-calcul

Notion de Substitution

Notion de Substitution
L’opération de substitution du λ-terme N à toutes les occurrences
libres de x dans M, notée [N/x]M, est définie par les clauses
suivantes:
1. ([N/x])x ≡ N
2. ([N/x])a ≡ a pour tout atome a̸=x
3. ([N/x])(PQ) ≡ ([N/x]P)([N/x]Q)
4. ([N/x])(λx.P) ≡ λx.P
5. ([N/x])(λy.P) ≡ λy.[N/x]P si y̸=x et y∈FV(N)
/ ou x∈FV(P)
/
6. ([N/x])(λy.P) ≡ λz.[N/x]([z/y]P) si y̸=x , y∈FV(N) ,
x∈FV(P) et z∈FV(NP)
/
. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .

Pr. M. Mezghiche Introduction au λ-calcul

β-réduction

Un λ-terme de la forme (λx.M)N est appelé β-redex, il lui

correspond le β-contractum [N/x]M. Le remplacement dans un
λ-terme d’un β-redex par son β-contractum définit la
β-contraction (élémentaire):

(β) (λx.M)N → [N/x]M

Une suite finie de β-contractions et de changements de variables

liées est appelée λβ-réduction. Si une telle λβ-réduction change le
λ-terme X en un λ-terme Y, nous dirons que X se β-réduit à Y,
noté:

X →λβ Y

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .

Pr. M. Mezghiche Introduction au λ-calcul

Exemples de β-réduction

1. (λx.x(xy))N →λβ [N/x](x(xy)) ≡ N(Ny).

2. (λx.y)N →λβ [N/x]y ≡ y.
3.
(λx.xx)(λy.y)N →λβ [λy.y/x](xx)N
≡ (λy.y)(λy.y)N
→ [λy.y/y]yN
≡ (λy.y)N
→ [N/y]y
≡ N.

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .

Pr. M. Mezghiche Introduction au λ-calcul

Définition: λβ-égalité

La β-réduction engendre la relation d’équivalence appelée β-égalité

ou β-conversion ( notée =λβ ):
λ-terme P est β-égal ou β-convertible au λ-terme Q (P =λβ Q) ssi:
∃ P0 , P1 ,...,Pn , λ-termes et (n ≥ 0) telle que:
P0 ≡ P
Pn ≡ Q et
Pi →λβ Pi+1 ou
Pi+1 →λβ Pi et (0 ≤ i < n).

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .

Pr. M. Mezghiche Introduction au λ-calcul

Propriétés λβ-réduction

1ème propriété de Church-Rosser. Si P →λβ M et P˙→λβ ˙N ,

alors il existe un λ-terme T tel que:

M →λβ T et N →λβ T.

2ème propriété de Church-Rosser. Si P =λβ Q, alors il existe un

λ-terme T tel que :

P →λβ T et Q →λβ T

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .

Pr. M. Mezghiche Introduction au λ-calcul

Propriétés λβ-réduction

Toute fonction possède un point fixe:

FX = X
Soit: Y = ((λx y.(y(x x y)))(λx y.(y(x x y)))) On obtient:

F(YF) = (YF)

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .

Pr. M. Mezghiche Introduction au λ-calcul

Propriétés λβ-réduction

Un λ-terme ne contenant aucun β-redex est sous β-forme normale .

Exemple:
- le terme (λx.(λy.xy)t)
- le terme (λx.(λy.xyt))
- le terme (λx.(λy.xyt))N

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .

Pr. M. Mezghiche Introduction au λ-calcul

Représentation des fonctions calculables

Représentation des entiers naturels dans le λ-calcul:

1. 0 ≡ λxy.y
2. 1 ≡ λxy.xy
3. 2 ≡ λxy.x(xy)
4. 3 ≡ λxy.x(x(xy))
...

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .

Pr. M. Mezghiche Introduction au λ-calcul

Représentation des fonctions calculables

Quelques exemples simples

1. successeur; S ≡ λxyz.y(xyz)
2. fonction Zéro; Z ≡ λx.0
3. fonction projection; Uni ≡ λx1 x2 . . . xi . . . xn .xi
4. addition; add ≡ λfgxy.fx(gxy)
5. multiplication; mult ≡ λxyz.x(yz)

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .

Pr. M. Mezghiche Introduction au λ-calcul

Représentation des fonctions récursives dans λ-calcul
Toute fonction primitive récursive f peut être définie dans le
λ-calcul.
La démonstration est par induction sur la définition de f. Le cas le
moins évident est celui où f est définie par itération.
Dans le cas où la fonction f est une fonction définie par
composition:

f(x1 , . . . , xm ) = g(h1 (x1 , . . . , xm ), . . . , hp (h1 (x1 , . . . , xm )))

la fonction f définissant f est donnée par :
f = λx1 . . . xm .g(h1 x1 . . . xm ) . . . (hp x1 . . . xm )).
Pour démontrer que le schéma de récursion primitive est
définissable supposons que l’on peut construire un terme R tel que
pour tout X, Y, k,
{
RXY0 = X,
RXYk + 1 = Yk(RXYk) .
.
.
.
.
. . . . .
. . . .
. . . .
. . . .
. . . .
. . . . .
.
.
.
.
.
.
.
.
.

Pr. M. Mezghiche Introduction au λ-calcul

Représentation des fonctions récursives dans λ-calcul

Soit f une fonction définie par récursion:

{
f(0, m1 , . . . , mn ) = g(m1 , . . . , mn )
f(k + 1, m1 , . . . , mn ) = h(k, f(k, m1 , . . . , mn ), m1 , . . . , mn )

Supposons donnés g, h les termes qui représentent les fonctions g

et h. Nous pouvons choisir le terme f qui représente f comme suit:

f = λux1 ...xm .(R(gx1 ...xm )(λuv.huvx1 ...xm )u)

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .

Pr. M. Mezghiche Introduction au λ-calcul

Représentation des fonctions récursives dans λ-calcul

f = λux1 ...xm .(R(gx1 ...xm )(λuv.huvx1 ...xm )u)

Un exemple d’application:
{
add(0, x) = U22 (0, x)
f(k + 1, x) = S(f(k, x))

add = λux.R(x)(λuv.Sv)(u)

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .

Pr. M. Mezghiche Introduction au λ-calcul

Représentation des fonctions récursives dans λ-calcul

Exemples de fonctions calculables

true = λx y.x (Valeur booléenne Vraie)
false = λx y.y (Valeur booléenne Faux)
not = λzxy.zxy (négation booléenne)
ifzero = λx.(x(K faux)K) (Test à zero)
pred = λx y z.(x(λp q.(q(p y)))(K z)I) (prédecesseur)
diff = λx y.(y pred x) (Soustraction)
fix = ((λx y.(y(x x y)))(λx y.(y(x x y)))) (Point fixeur)
lessq = λx y.(diff x y(K faux)K) (Inferieur ou egal))
if = λxyz.xyz. (fonction de test)

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .

Pr. M. Mezghiche Introduction au λ-calcul

λ-calcul et calculabilité

Thèse de Church:

Toute fonction calculable est

λ-définissable

. . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .

Pr. M. Mezghiche Introduction au λ-calcul