L'objectif est de pouvoir réécrire un terme en un autre terme.
Pour cela nous avons besoin de la description des termes avant et après la traduction.
Une règle de réécriture est de la forme LHS >>> RHS.
LHS est un sous terme du terme à traduire.
RHS est la traduction de LHS.
Parfois la traduction dépend des instances du terme à traduire.
Par exemple, on peut avoir besoin de faire certains calculs ou de filtrer certains termes avant la traduction.
Pour cela, on rajoute à ces règles une condition.
Cette condition est un programme Prolog qui exprime soit une simple condition, soit un calcul de la traduction.
Une règle de réécriture sera donc de la forme LHS >>> RHS if COND.
Pour lever l'ambiguïté lorsque deux règles ou plus sont applicables,
on suppose que c'est la première qui doit l'être (ce choix est courant en Prolog).
Une substitution est un ensemble ordonné de règles de réécriture.
Considérons l'exemple suivant. Soit une expression arithmétique à simplifier. Cette expression peut contenir des nombres et des variables. On utilise la substitution suivante :
(X+Y)*Z >>> X*Z+Y*Z Z*(X+Y) >>> (X+Y)*Z X+(Y+Z) >>> (X+Y)+Z 1*X >>> X X*1 >>> X X+Y >>> Z if (number(X), number(Y), Z is X+Y) X*Y >>> Z if (number(X), number(Y), Z is X*Y) X+Y >>> Y+X if (number(Y), \+ number(X)) X*Y >>> Y*X if (number(Y), \+ number(X))
La traduction du terme (1+x+2)*(2+y+3) est le terme 15+3*y+5*x+y*x.