-équivalence
La correspondance que l'on vient d'évoquer n'est valide que si
la logique de 
Prolog comprend l'axiome de
-équivalence*.
Autrement,
deux termes non-
-équivalents,
et 
,
ne seraient pas distingués car
.
Muni de la -équivalence,
on peut pousser cette correspondance jusqu'à un idiome de programmation
où -abstraction et quantification universelle sont symétriques.
Cela permet de convertir à volonté des -abstractions en des
quantifications universelles et des -variables en des constantes
universelles.
Cette symétrie sert de fil directeur à notre
reconstruction pragmatique de Prolog* [Belleannée et al. 95],
mais elle a aussi des conséquences importantes pour
l'implémentation
[Brisset et Ridoux 92b].
Figure 7: Réduction de graphe et 
-rédex
La représentation des termes qui est la plus commode pour l´unification*
modulo 
-équivalence est leur
forme normale de tête -longue* [Huet 75].
Pour ne pas avoir à la calculer à chaque unification,
les termes sont systématiquement représentés de cette manière dès leur
création.
On construit ainsi beaucoup de -abstractions que l'on peut juger
artificielles,
et aussi beaucoup de 
-rédex qui le sont autant.
Il ne faudrait pas mobiliser toute la procédure de réduction de graphe pour ces
-rédex.
Pour cela,
on distingue les -abstractions issues d'une
-expansion
en les appelant des 
-abstractions.
La procédure de réduction de graphe peut alors reconnaître les -rédex
construits à l'aide de
-abstractions :
on les appelle des -rédex*.
Ceux là peuvent être réduits en construisant simplement une nouvelle
application
(voir à la figure 7
la nouvelle application
où le pointeur vers 
est remplacé par un pointeur vers 
).
Il ne faut noter comme tels que les -rédex qui le
resteront quelles que soient les -réductions qui leur seront appliquées :
ce sont les -rédex qui sont en
forme normale de tête*.
Les -variables sont aussi -expansées et cela est la cause
d'une autre forme de
-rédex «abusifs».
À cause de la -expansion,
une -variable 
de type fonctionnel aura toutes ces occurrences
remplacées par 
.
Lorsqu'une
-réduction cause le remplacement de la -variable
par un terme 
,
c'est toute sa forme
-expansée qu'il faut remplacer,
et pas seulement .
En effet,
remplacer seulement par
créerait des -rédex parasites de la forme 
.
Il faut donc reconnaître les -variables -expansées.
Cela se fait de la même manière que pour reconnaître les -rédex.
La combinaison de ces deux heuristiques produit un gain de complexité
important.
Par exemple,
sachant que 
dénote 
et est -expansé en
et que 
dénote 
,
le terme 
est -expansé en
,
et se -normalise naïvement en un nombre d'étapes
qui est en cube du nombre de .
Ce nombre devient quadratique quand la première heuristique est appliquée
et linéaire lorsque les deux le sont.
On peut s'en convaincre en regardant la trace de la
-réduction
naïve de la forme -expansée de
.
-réductions emboîtent des -abstractions.
-rédex qui nécessitent de nombreuses duplications.
Les termes dupliqués sont soulignés.
Ils ne sont pas des combinateurs,
car la -variable 
y est libre,
et n'offrent donc pas prise à l'heuristique de la section précédente.
cause encore plus de -rédex parasites, ...
Le coût de duplication est proportionnel à la taille des termes soulignés.
Le coût total est donc cubique.
Avec la première heuristique,
les étapes de -réduction sont les mêmes,
mais il n'y a plus de duplication.
Le coût total devient quadratique.
La deuxième heuristique va éviter d'emboîter des
-abstractions.
Il y a donc moins de -rédex et moins de -réductions.
La trace de la -réduction avec les deux heuristiques est la suivante,
où les numéros correspondent aux mêmes étapes que pour la -réduction
naïve.
-abstractions.
-réduction suffit pour atteindre le troisième ,
et ...
Le coût de la -réduction de chaque est constant.
Le coût total est donc linéaire avec le nombre de .
Le point de départ de cette discussion sur l'effet de la
-équivalence
sur l'implémentation était la symétrie entre les deux quantifications
essentiellement universelles, et 
.
Cette symétrie se traduit par des remplacements de -variables
par des constantes universelles*,
ou de constantes universelles par des -variables.
Ces remplacements sont fréquents et le programmeur les exprime par des
-rédex.
Il est aussi fréquent qu'un remplacement soit suivi peu après par le
remplacement inverse.
À cause des duplications qu'elle implique
(même en considérant les heuristiques décrites),
la réduction de graphe n'est pas le bon choix pour implémenter ce qui n'est
en fait qu'un changement de point de vue sur un terme.
Nous avons donc choisi d'adapter la technique des
substitutions explicites* [Revesz 88]
à la réduction de graphe,
mais uniquement pour traiter la correspondance entre
constantes universelles et -variables
(
*).
Cela permet de défaire l'effet d'un remplacement simplement en enlevant
la substitution explicite qui le représente.
Il faut bien sûr trouver une représentation 
de ces nouveaux objets,
qui sont essentiellement des triplets de termes 
(pour 
remplace 
dans 
),
et programmer les opérations associées :
création, propagation, suppression et réalisation de substitution explicite.
De ces deux développements un peu techniques sur le rôle des combinateurs
et de la -équivalence,
il faut retenir qu'un système complexe ne se
range pas facilement dans une catégorie préétablie.
Par exemple,
notre implémentation de Prolog met en 
uvre la réduction de graphe,
mais lui ajoute des améliorations qui correspondent à des traits particulier
de Prolog.
La réduction de graphe fournit un cadre général dont la principale qualité
est la simplicité,
celle de la gestion de mémoire en particulier.
Nous l'avons choisi pour cela.
La réduction de graphe prévoit des opérations qui sont parfois coûteuses,
et une première forme d'amélioration consiste à trouver des heuristiques
qui permettent de remplacer les opérations coûteuses par des opérations
qui le sont moins ou même de simplement les éviter.
Une seconde forme d'amélioration consiste à ajouter à la réduction de graphe
des opérations qui viennent d'autres paradigmes comme les substitutions
explicites.