Département d'Informatique
Licence Informatique 2001-2002
Programmation Fonctionnelle
19 novembre



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

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

    1. λ x . λ y . (λ x . y   λ y . x)
    2. λ x . λ y . (λ x . y   λ y . x)
    3. λ x . (x   (λ y . (λ x . x   y)   x))
    4. λ a . (λ b . a   λ b . (λ a . a   b))
    5. (λ free . bound   λ bound . (λ free . free   bound))
    6. (λ x . x   y)   (λ y . y)    et    (λ x . (x   y))   (λ y . y)
    7. λ x . λ y . λ z . (λ z . (z   λ x . y))
    8. (λ x . λ y . (x   z   (y   z)))   (λ x . (y   λ y . y))

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

    1. λ x .(x   λ y .y) λ x. λ y.x

    2. λ x .(λ x . x   λ y .x) λ y. x

    3. λ x .λ y . (x   y) λ x . y

    4. λ x .λ y . (y   x) λ y . x

    5. λ x .λ y . (y   x) λ x . y

    6. λ x . λ y . (z   x   (y   z)) λ x . (y   λ y . y)

    7. λ x . (z   x   λ y . (y   z)) λ x . (y   λ y . y)

    8. λ x . (z   λ y. (x   (y   z))) λ x . (y   λ y . y)

II   Ordre de réduction

Pour chacune des λ-expressions suivantes, réduire l'expression sous forme normale en utilisant:
  1. la stratégie NOR (ordre normal),
  2. la stratégie AOR (ordre applicatif).
    1. λ x .(λ z . z   x   y)   λ y . y

    2. λ x . λ y . (z   (λ z . (z   λ x . y )))

    3. λ y . (+   (λ x . x   y)   y)   (λ y. (*   2   y)   1)

    4. λ f . λ x . (f   x)   λ x . λ a . (x   a)   λ x . x   λ y. y

    5. λ x .λ y.(x   z   (y   z))   λ x . (λ y . y   y)

    6. λ h .( λ x . (h   (x   x))   λ x . (h   (x   x)))   λ 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).


    1. λ x . λ y . (*   x   x)   2   (λ x . (+   x   1)   5)

    2. λ t . λ x . (t   x)   λ y . λ x . (+   x   y)

    3. λ t . λ x . (t   x)   λ y . λ x . (+   x   y)   (λ y. (+   y   1)   5)

    4. λ t . λ y . (λ x . (t   x)   y)   λ x . (*   x   x)   (λ x . (+   x   1)   5)

    5. λ f . λ a . (f   a)   λ a. λ x . (λ b . (x   b)   a)   4   λ x .x
This document was translated from LATEX by HEVEA.