Université Louis Pasteur
Strasbourg
Département d'Informatique
Licence et Maîtrise d'Informatique 2001-2002
Programmation Fonctionnelle
Vendredi 21 décembre












λ-contrôle
durée: 2h
aucun document autorisé



Quelques recommandations relatives à la présentation (dont il sera évidemment tenu compte):
Lorsqu'il s'agit de réduire une λ-expression, préciser la règle de conversion utilisée (α, β ou η-conversion) et pour la β-conversion indiquer le redex choisi avec le signe ^. Pour gagner du temps et raccourcir les expressions, il est possible d'utiliser les noms de λ-expression déja définis. Par exemple, on pourra noter vrai à la place de λ x . λ y . x s'il a été posé que vrai = λ x . λ y . x


I   Couples

Les combinateurs S, K, I, B et C vérifient les égalités suivantes:

S  f  g  x = (f  x)  (g  x)
K  x  y = x
I  x = x
B  f  g  x = f  (g  x)
C  f  g  x = (f  x)   g

On définit tuple2, index1 et index2 comme suit (en utilisant les combinateurs S, K, I, B et C):
tuple2 = B   C   (C   I)
index1 = C   I   K
index2 = C   I   (K   I)

Vérifier que tuple2, index1 et index2 modélisent les fonctions sur les couples.
Pour cela, montrer que:
index1 (tuple2  a  b) = a
index2 (tuple2  a  b) = b

II   Fractions

Dans cette section, on cherche un modèle des nombres rationnels positifs ( Q+).
Pour modéliser les entiers naturels ( N) on utilise le modèle de Church rappelé ci-dessous:
La λ-expression qui modélise l'entier n est notée n et définie par:
n
= λ f . λ x .(fn   x)
où (fn   x) est n fois l'application de f sur x, c'est-à-dire:
(f0   x) = x
(f1   x) = (f   x)
(f2   x) = (f   (f   x))
(f3   x) = (f   (f   (f   x)))
...
(fn   x) = (f   ... (f   (f
 
n   ×
  x))   ...)


L'addition et la multiplication dans N sont modélisées ainsi:
addN = λ n . λ m . λ f . λ x .(n   f   (m   f   x))
multN = λ n .λ m . λ f . (m   (n   f))

  1. Réduire sous Forme Normale (en utilisant n'importe quelle stratégie de réduction)
    les expressions suivantes:
    addN  
    1
    		 
    1
    addN  
    2
    		 
    3
    addN  
    3
    		 
    2
    multN  
    1
    		 
    2
    multN  
    3
    		 
    2

  2. Vérifier que pour tout entier n:
    addN  
    n
    		 
    0
    		=
    n
    multN  
    n
    		 
    1
    		=
    n


  3. En utilisant la section I (sur les couples),
    donner une expression permettant de modéliser un nombre rationnel positif a/b.

  4. Comment s'exprime l'addition et la multiplication dans Q+ dans le modèle de la question précédente ? Nommer ces expressions addQ et multQ.
    (indications: a/b+c/d = a× d+c× b/b× d et a/b×c/d = a× c/b× d)
This document was translated from LATEX by HEVEA.