Algorithme

A partir d'un terme, l'algorithme produit un autre terme. L'algorithme utilisé est le suivant :

• Appliquer la substitution à chacun des arguments du terme
• Chercher la première règle applicable à ce nouveau terme dont la condition est satisfaite
• Si une telle règle existe, l'appliquer et réappliquer la substitution au nouveau terme
• Sinon, retourner le terme courant

Lors de l'application d'une règle, deux termes se ressemblent s'ils s'unifient et si le terme provenant de la règle n'instancie pas le sous terme du terme à traduire (sinon la règle de substitution modifierait le terme original). Cela signifie que la règle f(x,y) >>> g(u,v) ne doit pas être appliquée à la variable non instanciée X. X doit restée non instanciée pour ne pas créer le sous terme g(u,v) dans le terme courant. Au contraire, une variable provenant d'une règle de réécriture doit pouvoir être instanciée.