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

Un article de Wikipédia, l'encyclopédie libre.

On parle de terminaison d'un système de réécriture $\rightarrow_R$ lorsqu'il n'existe aucune chaîne infinie d'objets $t_0 \rightarrow_R t_1 \rightarrow_R t_2 \rightarrow_R \ldots$

Sommaire

1 Approche générale
- 1.1 Interprétation
- 1.2 Ordre de réduction
2 Exemples
3 Quelques problèmes ouverts

[modifier] Approche générale

La relation de réécriture associée à un système de réécriture $R$ est l'ensemble des couples de termes $t, t'$ tels que $t$ se réécrive en $t'$ par une règle de $R$ . On dit alors qu'un système de réécriture termine si et seulement si la relation de réécriture qui lui est associée est bien fondée.

Le formalisme des systèmes de réécriture étant suffisamment puissant pour coder par exemple les machines de Turing, il est clair que la terminaison des systèmes de réécriture est indécidable.

Il existe cependant des arguments de terminaison utilisables dans certains cas.

[modifier] Interprétation

On se donne un ensemble muni d'un ordre bien fondé (par exemples les entiers naturels). À 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.

[modifier] Ordre de réduction

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 $f$ d'arité $n$ de la signature, pour tous termes $s_1,\ldots,s_n$ et $t$ , si $s i > t$ alors $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 $σ$ , pour tous termes $s$ et $t$ , si $s > t$ alors $σ s > σ t$ ;
il est bien fondé.

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

[modifier] Exemples

[modifier] Taille des termes

Exemple: $f(f(X)) \rightarrow f(X)$

[modifier] Interprétation polynomiale

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

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

$p(z,X) \rightarrow X$
$p(s(X),Y) \rightarrow s(p(X,Y))$

On choisit

$w (z) = 1$
$w (s (T)) = 1 + w (T)$
$w (p (T 1, T 2)) = 2 w (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 = $w (p (z, X)) = 2 w (z) + w (X) = 2 + w (X)$
- poids de la partie droite = $w (X)$
Règle 2,
- partie gauche : $w (p (s (X), Y)) = 2 w (s (X)) + w (Y) = 2 + 2 w (X) + w (Y)$ ,
- partie droite : $w (s (p (X, Y))) = 1 + 2 w (X) + w (Y)$

[modifier] Ordre récursif sur les chemins

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 $s = f(s_1,\ldots,s_n)$ et $t = g(t_1,\ldots,t_m)$ . On dit que $s$ est plus grand que $t$ pour l'ordre RPO associé à la précédence > si

$f = g$ et $\{s_1,\ldots,s_n\}$ est plus grand que $\{t_1,\ldots,t_m\}$ pour l'ordre multiensemble associé au RPO ; ou
$f > g$ et pour tout $j$ , $s$ est plus grand que $t j$ pour l'ordre RPO ; ou
il existe un $i$ tel que $s i$ soit plus grand que $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 $f = g$ que pour tout $j$ , $s$ est plus grand que $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 $t$ est un sous-terme de $s$ , alors $s$ est plus grand que $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 :

$ack(0,y)\rightarrow succ(y)$