Stratégies de réduction (où l'on détermine les conditions d'application des règles de conversion et le choix du redex lors d'une réduction)
I Le problème de capture de variable
Variable libre, variable liée.
Pour chacune des λ-expressions suivantes
et pour chaque occurrence de variable,
indiquer si la variable est libre ou liée.
λ x . λ y . (λ x . y λ y . x)
λ x . λ y . (λ x . y λ y . x)
λ x . (x (λ y . (λ x . xy) x))
λ a . (λ b . a λ b . (λ a . ab))
(λ free . bound λ bound . (λ free . freebound))
(λ x . xy) (λ y . y) et (λ x . (xy)) (λ y . y)
λ x . λ y . λ z . (λ z . (z λ x . y))
(λ x . λ y . (xz (yz))) (λ x . (y λ y . y))
Régles de α- et β-conversion.
Pour chacun des redex suivants, indiquer si l'on peut
appliquer directement la régle de b-conversion,
sinon appliquer la a-conversion nécessaire.
λ x .(x λ y .y) λ x. λ y.x
λ x .(λ x . x λ y .x) λ y. x
λ x .λ y . (xy) λ x . y
λ x .λ y . (yx) λ y . x
λ x .λ y . (yx) λ x . y
λ x . λ y . (zx (yz)) λ x . (y λ y . y)
λ x . (zx λ y . (yz)) λ x . (y λ y . y)
λ x . (z λ y. (x (yz))) λ x . (y λ y . y)
II Ordre de réduction
Pour chacune des λ-expressions suivantes,
réduire l'expression sous forme normale
en utilisant:
la stratégie NOR (ordre normal),
la stratégie AOR (ordre applicatif).
λ x .(λ z . zxy) λ y . y
λ x . λ y . (z (λ z . (z λ x . y )))
λ y . (+ (λ x . xy) y) (λ y. (* 2 y) 1)
λ f . λ x . (fx) λ x . λ a . (xa) λ x . x λ y. y
λ x .λ y.(xz (yz)) λ x . (λ y . yy)
λ h .( λ x . (h (xx)) λ x . (h (xx))) λ f . λ x.x (+ 1 5)
III Réduction faible
Pour chacune des λ-expressions suivantes,
vérifier que l'expression est fermée, puis
appliquer la réduction faible avec la
stratégie AOR (évaluation affairée des langages fonctionnels).
λ x . λ y . (* xx) 2 (λ x . (+ x 1) 5)
λ t . λ x . (tx) λ y . λ x . (+ xy)
λ t . λ x . (tx) λ y . λ x . (+ xy) (λ y. (+ y 1) 5)
λ t . λ y . (λ x . (tx) y)
λ x . (* xx) (λ x . (+ x 1) 5)
λ f . λ a . (fa) λ a. λ x . (λ b . (xb) a) 4 λ x .x