Département d'Informatique

Licence Informatique 2001-2002

Programmation Fonctionnelle

7 janvier

Compilation du λ-calcul
(ou comment améliorer l'efficacité de la réduction de graphe
en éliminant systématiquement toutes les variables)

I Règles de compilation : combinateurs S, K, I

La fonction comb qui transforme une λ-expression en du code SKI est définie par:

comb(k) = k

comb(E₁ E₂) = comb(E₁) comb(E₂)

comb(λ x . E) = [x] comb(E) où

[x] (E₁ E₂) = S ([x] E₁) ([x] E₂)

[x] k = K k (si k ≠ x)

[x] x = I

où k dénote une constante ou une variable.

Exemple : comb(λ x . (+ x 2)) donne S (S (K +) I) (K 2)
Vérification : λ x . (+ x 2) 1 &rarr (+ 1 2)
S (S (K +) I) (K 2) 1 → (+ 1 2)

Déterminer le code SKI des λ-expressions suivantes:
1. λ y . (y 1)
2. λ x . (+ x x)
3. λ x . λ y . (x y)
4. λ x . λ y . (y x)
5. λ x . λ y . (+ x y)
Vérifier le résultat des questions précédentes
en choisissant des arguments arbitraires.

II Règles d'optimisation : combinateurs B, C, ...

Optimiser le code SKI obtenu en I.1. en utilisant les règles suivantes:

S (K E₁) (K E₂) = K (E₁ E₂)	(1)
S (K E) I = E	(2)
S (K E₁) E₂ = B E₁ E₂	(3)
S E₁ (K E₂) = C E₁ E₂	(4)

Exemple :

S (S (K +) I) (K 2) (2)

= S + (K 2) (4)

= C + 2

Réponses :

1. comb(λ y . (y 1)) = S I (K 1)
2. comb(λ x . (+ x x))
  
  = S (S (K +) I) I
3. comb(λ x . λ y . (x y))
  
  = S (S (K S) (S (K K) I)) (K I)
4. comb(λ x . λ y . (y x))
  
  = S (S (K S) (K I)) (S (K K) I)
5. comb(λ x . λ y . (+ x y))
  
  = [x] (S (S (K +) (K x)) I)
  
  = S (S (K S) (S (S (K S) (S (K K) (K +))) (S (K K) I))) (K I)

S I (K 1) (4)

= C I 1
S (S (K +) I) I (2)

= S + I
S (S (K S) (

S (K K) I

)) (K I)
(2)

= S

(S (K S) K)

(K I)
(3)

= S (B S K) (K I) (4)

= C (B S K) I
S (

S (K S) (K I)

) (S (K K) I)
(1)

= S (K (S I)) (

S (K K) I

)
(2)

= S (K (S I)) K (3)

= B (S I) K

S (S (K S) (S (S (K S) (

S (K K) (K +)

)) (S (K K) I))) (K I)

(1)

= S (S (K S) (S (

S (K S) (K (K +))

) (S (K K) I))) (K I)

(1)

= S (S (K S) (S (K (S (K +))) (

S (K K) I

))) (K I)

(2)

= S (

S (K S) (S (K (S (K +))) K)

) (K I)

(3)

= S (B S (

S (K (S (K +))) K

)) (K I)

(3)

= C (B S (B (S (K +)) K)) I

Support du TD :

comb(λ y . (y 1))

= [y] comb((y 1))

= [y] (comb(y) comb(1))

= [y] (y 1)

= S ([y] y) ([y] 1)

= S I (K 1)

comb(λ x . (+ x x))

= [x] comb(+ x x))

= [x] (comb(+) comb(x) comb(x))

= [x] (+ x x)

= S ([x] (+ x)) ([x] x)

= S (S ([x] +) ([x] x)) ([x] x)

= S (S (K +) I) I

comb(λ x . λ y . (x y))

= [x] comb(λ y . (x y))

= [x] ([y] comb(x y))

= [x] ([y] (comb(x) comb(y)))

= [x] ([y] (x y))

= [x] (S ([y] x) ([y] y))

= [x] (S (K x) I)

= S ([x] (S (K x))) ([x] I)

= S (S ([x] S) ([x] (K x))) ([x] I)

= S (S ([x] S) (S ([x] K) ([x] x))) ([x] I)

= S (S (K S) (S (K K) I)) (K I)

comb(λ x . λ y . (y x))

= [x] comb(λ y . (y x))

= [x] ([y] comb(y x))

= [x] ([y] (comb(y) comb(x)))

= [x] ([y] (y x))

= [x] (S ([y] y) ([y] x))

= [x] (S I (K x))

= S ([x] (S I)) ([x] (K x))

= S (S ([x] S) ([x] I)) (S ([x] K) ([x] x))

= S (S (K S) (K I)) (S (K K) I)

comb(λ x . λ y . (+ x y))

= [x] comb(λ y . (+ x y))

= [x] ([y] comb(+ x y))

= [x] ([y] (comb(+) comb(x) comb(y)))

= [x] ([y] (+ x y))

= [x] (S ([y] (+ x)) ([y] y))

= [x] (S (S ([y] +) ([y] x)) ([y] y))

= [x] (S (S (K +) (K x)) I)

= S ([x] (S (S (K +) (K x)))) ([x] I)

= S (S ([x] S) ([x] (S (K +) (K x)))) ([x] I)

= S (S ([x] S) (S ([x] (S (K +))) ([x] (K x)))) ([x] I)

= S (S ([x] S) (S (S ([x] S) ([x] (K +))) ([x] (K x)))) ([x] I)

= S (S ([x] S) (S (S ([x] S) (S ([x] K) ([x] +))) ([x] (K x)))) ([x] I)

= S (S ([x] S) (S (S ([x] S) (S ([x] K) ([x] +))) (S ([x] K) ([x] x)))) ([x] I)

= S (S (K S) (S (S (K S) (S (K K) (K +))) (S (K K) I))) (K I)

S I (K 1) = C I 1
S (S (K +) I) I (2)

= S + I
S (S (K S) (S (K K) I)) (K I) (4)

= C (S (K S) (S (K K) I)) I (3)

= C (B S (S (K K) I)) I (2)

= C (B S K) I
S (S (K S) (K I)) (S (K K) I) (1)

= S (K (S I)) (S (K K) I) (3)

= B (S I) (S (K K) I) (2)

= B (S I) K