1.4 Exemple 2. Comment représenter le couple en l-calcul
La structure de données couple est ``quelque chose'' qui, étant donnés
deux objets a et b, contient ces deux objets et la possibilité de les
``récupérer''. Supposons avoir défini une fonction
cons qui, à partir de
a et de b nous rend le couple (a, b).Il faudra que l'objet ``rendu'' par
cons nous permette de lui appliquer deux fonctions,
fst et snd qui vérifient les équations suivantes :
| fst (cons a b) = a |
| snd (cons a b) = b |
Pour la fonction cons nous pouvons donner la définition:
Appliquée à A et B elle donne:
| cons A B |
= |
l xyf.((f x)y) A B |
| |
® |
l f. f A B |
Or le terme l f. f A B est capable de capturer des termes qui remplaceront
f. En particulier nous pouvons remplacer f par des fonctions first et
second capables de sélectionner le premier ou le deuxième parmi les
arguments auxquelles elles sont appliquées :
-
first = l xy.x
- second = l xy.y
fst et snd seront ainsi définies :
-
fst = l x.(x first)
- snd = l x.(x second)