Chapitre 6 : λ-calcul

TD : λ-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).

  1. réduire ( true M ) et ( false M ), où M désigne un terme quelconque ;

  2. 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 0true et iszero nfalse 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 ) )

  1. Réduire 3 ( nextpair f ) ( pair x x ) .
  2. 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).

  3. En déduire une définition d'un terme sub codant la soustraction (avec la convention m - n = 0 si m < n) .

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 MM ( 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 U4 effectuées pendant ce calcul.

Note : on posera U1 = pred U, U2 = pred U1 , etc. , et on se dispensera d'écrire les réductions U13, etc. car l'opérateur pred est trop compliqué — voir exercice ci-dessus.

Solutions

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 xI

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 00 M = ( λ f x . x ) M → λ x . x = I

Exercice 2 (énoncé ci-dessus).

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

  2. 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 00 false truetrue

(en fait, comme on l'a remarqué, false et 0 désignent le même terme), mais :

not 11 false truefalse trueI
not 22 false truefalse (false true) → I

etc. (les dernières réductions utilisent false MI, 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 ) truetrue M NM

Exercice 5 (énoncé ci-dessus).

  1. 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 )

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

  3. Soustraction :

    sub = λ m n . n pred m

Exercice 10 (énoncé ci-dessus).

BA A → λ y . y ( A A y )

d'où :

B MM ( 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 fD = λ 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 UF fact Uif ( 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 ) UU ( λ 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 true4 M trueM ( 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 U1U1 ( λ 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 ) truefalse

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 U22) 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 U31 :

V3 → … → λ f . V4 ( U3 f )

Mais cette fois :

V4 = fact ( U4 ) → … → iszero U4 1 ( mul U4 ( fact ( pred U4 ) ) )
iszero U4U4 ( λ x . false ) true0 ( λ x . false ) truetrue

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 .