Terminaison d'un système de réécriture

On se donne un ensemble muni d'un ordre bien fondé (par exemple les entiers naturels[2]). À chaque terme on associe un élément de cet ensemble, qui sera appelé son poids. Il suffit ensuite de démontrer que toute réduction par le système de réécriture entraîne une diminution stricte du poids.

On considère les termes construit à partir d'une signature et d'un ensemble de variables. Un ordre > sur ces termes est appelé ordre de réduction s'il vérifie les trois points suivants :

• il est monotone, c'est-à-dire que pour tout symbole de fonction ${\displaystyle f}$ d'arité ${\displaystyle n}$ de la signature, pour tous termes ${\displaystyle s_{1},\ldots ,s_{n}}$ et ${\displaystyle t}$, si ${\displaystyle s_{i}>t}$ alors ${\displaystyle f(s_{1},\ldots ,s_{i},\ldots ,s_{n})>f(s_{1},\ldots ,t,\ldots ,s_{n})}$ ;
• il est stable par substitution, c'est-à-dire que pour toute substitution ${\displaystyle \sigma }$, pour tous termes ${\displaystyle s}$ et ${\displaystyle t}$, si ${\displaystyle s>t}$ alors ${\displaystyle \sigma s>\sigma t}$ ;
• il est bien fondé.

On peut alors démontrer qu'un système de réécriture se termine si et seulement s'il existe un ordre de réduction qui contient la relation de réécriture associée.

Exemple: ${\displaystyle f(f(X))\rightarrow f(X)}$

À tout terme ${\displaystyle T}$ on va associer un poids ${\displaystyle w(T)}$ qui est un entier positif : à tout symbole de fonction d'arité ${\displaystyle n}$ on associe un polynôme à ${\displaystyle n}$ variables ; le poids d'un terme ${\displaystyle f(s_{1},\ldots ,s_{n})}$ sera la valeur du polynôme associé à ${\displaystyle f}$ au point ${\displaystyle (w(s_{1}),\ldots ,w(s_{n}))}$.

Exemple (avec symboles p,s,z, d'arités respectives 2,1,0)

• ${\displaystyle p(z,X)\rightarrow X}$
• ${\displaystyle p(s(X),Y)\rightarrow s(p(X,Y))}$

On choisit

• ${\displaystyle w(z)=1}$
• ${\displaystyle w(s(T))=1+w(T)}$
• ${\displaystyle w(p(T_{1},T_{2}))=2w(T_{1})+w(T_{2})}$

Il est facile de vérifier que le poids de la partie gauche de chaque règle est strictement supérieur à celui de sa partie droite :

• Règle 1,
  • poids de la partie gauche = ${\displaystyle w(p(z,X))=2w(z)+w(X)=2+w(X)}$
  • poids de la partie droite =${\displaystyle w(X)}$
• Règle 2,
  • partie gauche : ${\displaystyle w(p(s(X),Y))=2w(s(X))+w(Y)=2+2w(X)+w(Y)}$,
  • partie droite : ${\displaystyle w(s(p(X,Y)))=1+2w(X)+w(Y)}$

L'ordre récursif sur les chemins (RPO, de l'anglais recursive path ordering) est un exemple d'ordre de réduction.

On se donne un ordre > sur les symboles de fonction, appelé précédence, pas obligatoirement total mais bien fondé si on veut que le RPO le soit aussi. Soit deux termes ${\displaystyle s=f(s_{1},\ldots ,s_{n})}$ et ${\displaystyle t=g(t_{1},\ldots ,t_{m})}$. On dit que ${\displaystyle s}$ est plus grand que ${\displaystyle t}$ pour l'ordre RPO associé à la précédence > si

• ${\displaystyle f=g}$ et ${\displaystyle \{s_{1},\ldots ,s_{n}\}}$ est plus grand que ${\displaystyle \{t_{1},\ldots ,t_{m}\}}$ pour l'ordre multiensemble associé au RPO ; ou
• ${\displaystyle f>g}$ et pour tout ${\displaystyle j}$, ${\displaystyle s}$ est plus grand que ${\displaystyle t_{j}}$ pour l'ordre RPO ; ou
• il existe un ${\displaystyle i}$ tel que ${\displaystyle s_{i}}$ soit plus grand que ${\displaystyle t}$ pour l'ordre RPO.

Il existe en fait plusieurs variantes du RPO, dans lesquelles, en cas d'égalité du symbole de fonction en tête, on compare les arguments en utilisant l'ordre lexicographique associé au RPO (lexicographic path ordering, ou LPO), ou encore en utilisant un ordre qui dépend du symbole de fonction (RPO avec statut). Dans le cas du LPO, il faut également vérifier si ${\displaystyle f=g}$ que pour tout ${\displaystyle j}$, ${\displaystyle s}$ est plus grand que ${\displaystyle t_{j}}$ pour l'ordre LPO.

L'ordre ainsi défini est bien un ordre de réduction, et même plus, puisqu'il vérifie la propriété du sous-terme : si ${\displaystyle t}$ est un sous-terme de ${\displaystyle s}$, alors ${\displaystyle s}$ est plus grand que ${\displaystyle t}$, quelle que soit la précédence choisie. Certains systèmes de réécriture terminent bien qu'il soit impossible de le montrer à l'aide d'un ordre vérifiant la propriété de sous-terme.

Grâce au RPO (en fait à sa variante LPO), on peut montrer la terminaison de la fonction d'Ackermann :

${\displaystyle ack(0,y)\rightarrow succ(y)}$

${\displaystyle ack(succ(x),0)\rightarrow ack(x,succ(0))}$

${\displaystyle ack(succ(x),succ(y))\rightarrow ack(x,ack(succ(x),y))}$

à l'aide de la précédence ${\displaystyle ack>succ}$.