Download Fichier PDF

126
Chapitre 8. Compilation des règles et des stratégies
– cas où fAC = G (s et t ont les mêmes symboles de tête)
α
mcf (fAC (sα1 1 , . . . ,sp p ),t) = fAC (uγ11 , . . . ,uγkk ) tel que (uγ11 , . . . ,uγkk ) est la fusion triée (sans
α
occurrence multiple) de (sα1 1 , . . . ,sp p ) et (tβ1 1 , . . . ,tβmm ).
De la définition précédente de mcf , il est facile de déduire le résultat suivant : soient s =
α
fAC (sα1 1 , . . . ,sp p ) et t deux termes en forme canonique, la fonction mcf appliquée à s et t
α
retourne la forme canonique de fAC (sα1 1 , . . . ,sp p ,t). En conséquence, la construction d’un terme,
en partant des feuilles (bottom-up), et en utilisant la fonction mcf , assure que le résultat est en
forme canonique.
Renormalisation des instances réductibles. On peut remarquer qu’à chaque fois qu’une fonction C
est appelée pour réduire un terme t = f (s1 , . . . ,sn ), les sous-termes s1 , . . . ,sn sont en forme
normale. Et lorsque la règle l → r est appliquée pour réduire le terme t, on pourrait penser que
les instances des variables de l sont elles-même en forme normale. C’est d’ailleurs ce qui nous a
amené à réutiliser directement les instances définies par σ pour construire le terme réduit rσ.
C’est en effet le cas, mais seulement pour les variables de l qui n’apparaissent pas directement
sous un symbole AC.
Supposons maintenant que la racine du terme t soit un symbole AC. Sa représentation canonique est de la forme t = fAC (s1 , . . . ,sn ). Ici encore, les sous-termes s1 , . . . ,sn sont irréductibles
par construction. Mais lorsqu’on applique une règle de la forme fAC (x,y) → r(x,y), il se peut
que les instances des variables x et y ne soient plus irréductibles : considérons la substitution
σ = {x 7→ fAC (s1 , . . . ,sk ),y 7→ fAC (sk+1 , . . . ,sn )}, pour k ≥ 2, l’instance de x peut être réduite
par la règle fAC (x,y) → r(x,y), par exemple. Il faut donc renormaliser les instances des variables qui apparaissent directement sous un symbole AC du membre gauche, avant de pouvoir
les utiliser pour construire le terme réduit.
La plupart des systèmes étudiés (Maude, OBJ, Brute) n’effectuent pas cette renormalisation
au bon moment, ce qui les amène à construire un membre droit de règle réductible. Lorsque r(x,y)
est un terme non linéaire en x et que l’instance de x est réductible, ces systèmes construisent une
instance de r(x,y) qui risque d’entraı̂ner de multiples renormalisations de x. Il est difficile d’être
plus précis ici, simplement parce que le traitement des termes non linéraires dépend grandement
des représentations choisies et des optimisations implantées. Dans Maude, par exemple, suivant
que les sous-termes réductibles sont partagés ou non, le comportement sera différent. Certaines
implantations décorent systématiquement, à l’exécution, tous les termes pour savoir s’ils sont
réductibles ou non. Cette approche est assez difficile à mettre en œuvre, et surtout coûteuse
en temps. De plus, elle n’aurait que peu d’intérêt pour ELAN, dans la mesure où une grande
majorité des termes sont irréductibles par construction (parce que nous utilisons une stratégie
de normalisation leftmost-innermost).
C’est pourquoi nous avons choisi de renormaliser systématiquement, avant de les utiliser, les
instances des variables qui apparaissent directement sous un symbole AC du membre gauche. Les
résultats expérimentaux montrent que cette approche permet d’éviter un grand nombre d’étapes
de réécriture, simplement parce que le processus de renormalisation est mis en facteur. Nous
avons cependant constaté que même si certaines instances de variables étaient potentiellement
réductibles, dans la pratique, ces instances sont majoritairement irréductibles. C’est ce qui nous
a amené à définir un critère pour déterminer, dans certains cas, l’irréductibilité d’une instance de
variable apparaissant directement sous un symbole AC du membre gauche de la règle appliquée.
Soit un motif l = fAC (x,t1 , . . . ,tn ), un sujet s = fAC (s1 , . . . ,sm ) et une substitution σ telle
que lσ =AC s. L’objectif est de définir un critère efficace, pour savoir si xσ est irréductible.
On sait que les sous-termes s1 , . . . ,sm sont en forme normale par construction, on sait aussi