Chapitre 6 : λ-calcul |
Exercice 1 (corrigé ci-dessous). Soit M un terme du λ-calcul ; réduire autant que possible les expressions suivantes : add M 0, add 0 M, mul M 0, mul 0 M, mul M 1, mul 1 M, et exp M 0.
Exercice 2 (corrigé ci-dessous).
réduire ( true M ) et ( false M ), où M désigne un terme quelconque ;
donner des définitions pour les opérateurs logiques and, or et not. Conseil : ces définitions commencent par if .
Exercice 3 (corrigé ci-dessous). Ecrire un terme qui code le test iszero, de telle sorte que iszero 0 → true et iszero n → false si n est un entier de Church différent de 0.
Exercice 4 (corrigé ci-dessous). On code un couple par le terme
pair = λ x y f . f x y
Donner les définitions de first et second de telle sorte que, pour tous termes M, N on ait les réductions :
first ( pair M N ) → M , second ( pair M N ) → N.
Exercice 5 (corrigé ci-dessous). On considère le terme nextpair défini par :
nextpair = λ f p . pair ( second p ) ( f ( second p ) )
En déduire une définition d'un terme pred codant la fonction prédécesseur, inverse de la fonction successeur (le prédécesseur de 0 est 0).
Exercice 10 (corrigé ci-dessous). Soit A = λ x y . y ( x x y ), et B = A A. Montrer que pour tout λ-terme M, on a :
B M → M ( B M )
Exercice 20 (corrigé ci-dessous). Construire le graphe des réductions possibles de mul 2 3 en 6. Montrer qu'il y a 90 calculs de longueur 9, et 12 de longueur 7 (on appelle calcul une suite de réductions transformant mul 2 3 en 6).
Exercice 21 (corrigé ci-dessous). Réduire fact U, en appliquant rigoureusement une stratégie externe gauche, et en supposant que la forme normale de U est 4. Compter le nombre de réductions U → 4 effectuées pendant ce calcul.
Note : on posera U1 = pred U, U2 = pred U1 , etc. , et on se dispensera d'écrire les réductions U1 → 3, etc. car l'opérateur pred est trop compliqué — voir exercice ci-dessus.
Exercice 1 (énoncé ci-dessus).
add M 0 =
( λ m n f x . m f ( n f x ) )
M 0
→
λ f x . M f ( 0 f x )
→
λ f x . M f x
On ne peut pas réduire plus sans connaître M, mais on est sûr que la dernière expression, appliquée à deux arguments A et B, se réduit toujours en M A B ; il existe en λ-calcul une troisième règle, appelée η-réduction (en plus de l'α-conversion et de la règle fondamentale de β-réduction), pour traiter ce cas, et convertir λ x . M x en M ; deux η-conversions successives donnent donc :
λ f x . M f x = λ f . ( λ x . M f x ) →η λ f . M f →η M
De même :
add 0 M → λ f x . 0 f ( M f x ) → λ f x . M f x →η M
car 0 "tue" son premier argument, pour ne garder que le second.
mul M 0 =
( λ m n f . n ( m f ) )
M 0
→
λ f . 0 ( M f ) =
λ f . ( λ g x . x ) ( M f )
→
λ f . ( λ x . x ) =
λ f x . x =
0
mul 0 M
→
λ f . M ( 0 f )
→
λ f . M ( λ x . x ) =
λ f . M I
Cette fois impossible d'aller plus loin sans supposer que M est un entier ; si c'est le cas M I se réduit en I, par exemple :
2 I → λ x . I ( I x ) → λ x . I x → I
et λ f . I = λ f x . x = 0.
mul M 1
→
λ f . 1 ( M f )
→
λ f . M f
→η M
mul 1 M
→
λ f . M ( 1 f )
→
λ f . M ( λ x . f x )
→η
λ f . M f
→η
M
Les dernières transformations, ci-dessus, sont des η-conversions.
exp M 0 = ( λ m n . n m ) M 0 → 0 M = ( λ f x . x ) M → λ x . x = I
Exercice 2 (énoncé ci-dessus).
true M = ( λ x y . x ) M
→ λ y . M
(ce terme code la fonction constante
égale à M) ;
false M = ( λ x y . y ) M
→ λ y . y = I .
and = λ p q . if p q false ; or = λ p q . if p true q ; not = λ p . if p false true .
On peut supprimer if dans les définitions ci-dessus, mais elles deviennent moins lisibles.
Exercice 3 (énoncé ci-dessus). La première idée est d'utiliser not :
not 0 → 0 false true → true
(en fait, comme on l'a remarqué, false et 0 désignent le même terme), mais :
not 1 → 1 false true → false true
→ I
not 2 → 2 false true →
false (false true) → I
etc. (les dernières réductions utilisent false M → I, pour tout terme M, voir exercice précédent). La solution consiste à remplacer, dans la définition de not, le terme false par la fonction constante égale à false, autrement dit :
iszero = λ p . if p ( λ x . false ) true .
(comme toujours, if est facultatif). On vérifie facilement que cette fois la réduction de iszero n fournit ( λ x . false ) true dès que l'entier n est différent de 0, car itérer une fonction constante ne change pas celle-ci (sauf si on l'itère zéro fois).
Exercice 4 (énoncé ci-dessus). On définit : first = λ p . p true , et : second = λ p . p false . Par exemple :
first ( pair M N )
→
first ( λ f . f M N )
→
( λ f . f M N ) true
→
true M N → M
Exercice 5 (énoncé ci-dessus).
Exemple :
3 ( nextpair f )
( pair x x )
→
nextpair f
( nextpair f
( nextpair f
( pair x x ) ) )
→
nextpair f
( nextpair f ( pair x (
f x ) )
→
nextpair f ( pair ( f x ) (
f 2 x ) )
→
pair ( f 2 x )
( f 3 x )
Prédécesseur :
pred = λ n f x . first ( n ( nextpair f ) ( pair x x ) )
Par exemple :
pred 3 → λ f x . first
( 3 ( nextpair f ) ( pair x x ) )
→
λ f x . first
( pair ( f 2 x )
( f 3 x ) )
→
λ f x . f 2 x = 2
ou bien :
pred 0 → λ f x . first
( 0 ( nextpair f ) ( pair x x ) )
→
λ f x . first
( pair x x )
→
λ f x . x = 0
Soustraction :
sub = λ m n . n pred m
Exercice 10 (énoncé ci-dessus).
B ≡ A A → λ y . y ( A A y )
d'où :
B M → M ( A A M ) ≡ M ( B M )
Le terme B est l'opérateur de point fixe de Turing, qui permet de passer de B M à M ( B M ) par β-réductions, et non simplement par β-équivalence (c'est pourquoi nous avons employé exceptionnellement le signe ≡ ci-dessus, pour désigner la définition de B ).
Exercice 20 (énoncé ci-dessus). Contrairement aux exercices précédents, on s'interdit ici d'effectuer plusieurs réductions simultanées.
( λ m n f . n ( m f ) ) 2 3
=
( λ m . ( λ n . ( λ
f . n ( m f ) ) ) ) 2 3
→
( λ n . ( λ
f . n ( 2 f ) ) ) 3
Deux réductions sont possibles, l'une externe, qui fournit le terme M1, l'autre interne, qui fournit le terme M2.
M1 = λ f . 3 ( 2 f )
M2 = ( λ n . ( λ
f . n ( λ t . f ( f t )
) ) ) 3
Commençons par traiter M1 ; deux réductions sont possibles, l'une externe, qui fournit le terme M11, l'autre interne, qui fournit le terme M12.
M11 =
λ f x . 2 f
( 2 f ( 2 f x ) )
M12 =
λ f . 3 (
λ t . f ( f t ) )
M2 possède une seule réduction, qui conduit au terme M12. Commençons par traiter M11 ; trois réductions 2 f → D = λ t . f ( f t ) sont possibles, l'une externe, qui fournit le terme M111, la seconde "médiane", qui fournit le terme M112, enfin une réduction interne, qui fournit le terme M113.
M111 =
λ f x . D
( 2 f ( 2 f x ) )
M112 =
λ f x . 2 f
( D ( 2 f x ) )
M113 =
λ f x . 2 f
( 2 f
( D x ) )
A nouveau trois réductions possibles pour M111 :
M1111 =
λ f x . f
( f ( 2 f ( 2 f x ) ) )
M1112 =
λ f x . D
( D ( 2 f x ) )
M1113 =
λ f x . D
( 2 f ( D x ) )
Deux réductions possibles pour M1111 :
M11111 = λ f x . f
( f ( D ( 2 f x ) ) )
M11112 = λ f x . f
( f ( 2 f ( D x ) ) )
Deux réductions possibles pour M11111 :
M111111 = λ f x . f
( f ( f ( f
( 2 f x ) ) ) )
= λ f x . f 4
( 2 f x )
M111112 = λ f x . f
( f ( D ( D x ) ) )
Enfin :
M111111 → M1111111 = λ f x . f 4
( D x )
→
λ f x . f 4
( f ( f x ) ) = 6
Soit 9 réductions externes pour réduire mul 2 3 en 6.
Retour en arrière (backtrack), deux réductions possibles pour M111112 :
M1111121 = λ f x . f
( f ( f ( f ( D x ) ) ) )
= M1111111
M1111122 = λ f x . f
( f ( D ( f ( f x ) ) ) )
→ 6
ce qui achève le graphe des réductions de M11111 ; retour en arrière et traitement de M11112 :
M11112 = λ f x . f
( f ( 2 f ( D x ) ) )
→
M111121 =
λ f x . f
( f ( D ( D x ) ) ) = M111112
M111122 = λ f x . f
( f ( 2 f ( f ( f x ) ) ) )
→ M1111122
ce qui achève le graphe des réductions de M1111, etc.
En examinant ces exemples, on comprend qu'il y a 27 termes (y compris M11) qu'on peut atteindre par réductions successives à partir de M11. Chacun de ces termes correspond à un sommet d'un cube de côté 2 ; le sommet (0, 0, 0) correspond au corps de M11, soit 2 f ( 2 f ( 2 f x ) ) ; puis on progresse dans l'une des trois directions, selon l'occurrence de 2 f qu'on choisit de réduire en D ; enfin chaque occurrence de D peut être réduite en f 2, ce qui explique qu'il y a trois positions (0, 1, 2) sur chaque axe, indiquant le progrès de la réduction d'une occurrence de 2 f. Comme ces réductions sont indépendantes les unes des autres (ce qui est rare en λ-calcul), on obtient un graphe simple en forme de cube. Par exemple voici les sommets du cube parcourus pendant le calcul suivant :
Position sur le cube |
Notation arborescente |
Terme | |
---|---|---|---|
(0, 0, 0) | M11 | λ f x . 2 f ( 2 f ( 2 f x ) ) | → |
(1, 0, 0) | M111 | λ f x . D ( 2 f ( 2 f x ) ) | → |
(2, 0, 0) | M1111 | λ f x . f ( f ( 2 f ( 2 f x ) ) ) | → |
(2, 0, 1) | M11112 | λ f x . f ( f ( 2 f ( D x ) ) ) | → |
(2, 1, 1) | M111121 | λ f x . f ( f ( D ( D x ) ) ) | → |
(2, 1, 2) | M1111212 | λ f x . f ( f ( D ( f ( f x ) ) ) ) | → |
(2, 2, 2) | λ f x . f ( f ( f ( f ( f ( f x ) ) ) ) ) | = 6 |
Toutes les suites de réductions de M11 en 6 ont la même longueur 6 ; en ajoutant les trois réductions qui conduisent de mul 2 3 à M11, on obtient ainsi une famille de calculs de longueur 9 ; le nombre exact de ces calculs est donné par le coefficient multinomial 6! / ( 2! 2! 2! ), soit 90.
Par contre M12 = λ f . 3 D se réduit directement en λ f x . D ( D ( D x ) ) , qui se réduit en trois étapes (par 6 chemins distincts) en 6 ; soit au total 12 calculs de longueur 7 (il y a 2 façons de réduire mul 2 3 en M12).
Exercice 21 (énoncé ci-dessus).
fact U
→
F fact U
→
if ( iszero U ) 1
( mul U
( fact ( pred U ) ) )
→
→
( iszero U ) 1
( mul U
( fact ( pred U ) ) )
car if = λx y z . x y z ; dans la suite cette élimination du symbole if sera implicite. Le redex externe le plus à gauche (en cas d'hésitation, dessiner l'arbre de l'expression) est maintenant :
iszero U = ( λ p . p ( λ x . false ) true ) U → U ( λ x . false ) true
Il faut maintenant réduire U, ce qui par hypothèse donne 4 ; en notant M = λ x . false, on a :
U M true → 4 M true → M ( M ( M ( M true) ) ) → false
en notant que la dernière réduction externe se fait bien en une seule étape, car M ignore son argument ; c'est un cas où une réduction interne serait plus longue (4 étapes). Nous avons obtenu la forme normale de iszero U, d'où :
fact U → … → false 1 ( mul U ( fact ( pred U ) ) ) → mul U ( fact ( pred U ) )
car false = λ x y . y ; d'autre part mul = λ m n f . n ( m f ), et posons U1 = pred U, ainsi que V1 = fact U1 :
mul U V1 → λ f . V1 ( U f )
Attention à l'ordre des arguments de mul, si on les échange (ce qui est possible, puisque le produit est commutatif), le calcul obtenu est très différent ; ici le prochain terme à réduire est V1 :
V1 =
fact U1
→ … →
→
iszero U1 1
( mul U1
( fact ( pred U1 ) ) )
iszero U1
→
U1
( λ x . false ) true
Nous ne ferons pas le calcul explicite de U1 = pred U, car l'opérateur pred n'est pas simple… ; mais on peut raisonnablement espérer obtenir 3 comme résultat, après quoi :
3 ( λ x . false ) true → false
comme précédemment; d'où :
V1
→ … →
false 1
( mul U1
( fact ( pred ( U1 ) ) )
→
→
mul U1
( fact ( pred ( U1 ) ) )
→
λ f . V2 ( U1 f )
en posant U2 = pred U1 , et V2 = fact U2 . Un calcul analogue au précédent (et comportant donc une réduction U2 → 2) permettra de réduire V2 :
V2 → … → mul U2 ( fact ( pred ( U2 ) ) ) → λ f . V3 ( U2 f )
en posant U3 = pred U2 , et V3 = fact U3 . Enfin, en utilisant une réduction U3 → 1 :
V3 → … → λ f . V4 ( U3 f )
Mais cette fois :
V4 =
fact ( U4 )
→ … →
iszero U4 1
( mul U4
( fact ( pred U4 ) ) )
iszero U4
→
U4
( λ x . false ) true
→
0 ( λ x . false ) true
→
true
et donc la forme normale de V4 est 1. Noter comment la stratégie externe gauche a réduit d'abord l'expression booléenne à true, qui ignore son second argument, et évite ainsi le calcul du terme qui se termine par pred U4 . On peut commencer la remontée :
V3 → … → λ f . 1 ( U3 f ) → λ f x . U3 f x
car 1 = λ g x . g x = λ g . ( λ x . g x ) ; il faut à nouveau réduire U3 en 1, d'où :
V3
→ … →
λ f x . 1 f x
→
λ f x . f x = 1
V2
→ … →
λ f . 1 ( U2 f )
→
λ f x . U2 f x
Il faut à nouveau réduire U2 en 2, d'où :
V2
→ … →
λ f x . 2 f x
→
λ f x . f ( f x ) = 2
V1
→ … →
λ f . 2 ( U1 f )
→
λ f x . U1 f
( U1 f x )
On réduit l'occurrence externe de U1 en 3, d'où :
V1 → … → λ f x . 3 f ( U1 f x ) → λ f x . f ( f ( f ( U1 f x ) ) )
On réduit maintenant l'occurence interne de U1 , et on obtient 6 pour forme normale de V1 . Enfin :
fact U → … → mul U V1 → λ f . V1 ( U f ) → … → λ f . 6 ( U f )
Il ne faut pas tricher, et ne pas réduire U tout de suite ; la stratégie externe donne :
λ f . 6 ( U f ) → λ f x . U f ( U f ( U f ( U f ( U f ( U f x ) ) ) ) )
Six réductions successives de U en 4 donneront progressivement, de l'extérieur vers l'intérieur, le résultat attendu 24 !
Nous avons évalué U, puis U1 , … , U4 pour chacun des tests iszero, soit 5 réductions de U. Lors de la remontée des calculs, on a évalué à nouveau U3 et U2 , chacun une fois ; U1 a été évalué deux fois, et enfin U six fois, soit 10 évaluations de U pendant cette remontée. Au total U a été évalué 15 fois, et on a aussi perdu du temps à calculer plusieurs fois les mêmes prédécesseurs ; ne pas oublier que par exemple chaque calcul de U2 = pred U1 , suppose qu'on recalcule U1 .