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

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

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.

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.

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.

Exemples

Taille des termes

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

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)$

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)$

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

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

à l'aide de la précédence $a c k > s u c c$ .

Quelques problèmes ouverts

Catégories :

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Terminaison d'un système de réécriture de Wikipédia en français (auteurs)

Игры ⚽ Поможем сделать НИР

Regardez d'autres dictionnaires:

Terminaison d'un systeme de reecriture — Terminaison d un système de réécriture On parle de terminaison d un système de réécriture lorsqu il n existe aucune chaîne infinie d objets Sommaire 1 Approche générale 1.1 Inte … Wikipédia en Français
Système de réécriture — Réécriture (informatique) Pour les articles homonymes, voir Réécriture. La réécriture (ou récriture) est un modèle de calcul utilisé en informatique, en algèbre, en logique mathématique et en linguistique. Il s’agit de transformer des objets… … Wikipédia en Français
Reecriture (informatique) — Réécriture (informatique) Pour les articles homonymes, voir Réécriture. La réécriture (ou récriture) est un modèle de calcul utilisé en informatique, en algèbre, en logique mathématique et en linguistique. Il s’agit de transformer des objets… … Wikipédia en Français
Réécriture (arithmétique) — Réécriture (informatique) Pour les articles homonymes, voir Réécriture. La réécriture (ou récriture) est un modèle de calcul utilisé en informatique, en algèbre, en logique mathématique et en linguistique. Il s’agit de transformer des objets… … Wikipédia en Français
Réécriture (informatique) — Pour les articles homonymes, voir Réécriture. La réécriture (ou récriture) est un modèle de calcul utilisé en informatique, en algèbre, en logique mathématique et en linguistique. Il s’agit de transformer des objets syntaxiques (mots, termes,… … Wikipédia en Français
Knuth-Bendix (algorithme) — La procédure de complétion de Knuth Bendix transforme un ensemble d identités (sur des termes) décrivant une structure algébrique en un système de réécriture de terme confluent et qui termine (dit alors convergent). Quand cette procédure se… … Wikipédia en Français
Knuth-bendix (algorithme) — La procédure de complétion de Knuth Bendix transforme un ensemble d identités (sur des termes) décrivant une structure algébrique en un système de réécriture de terme confluent et qui termine (dit alors convergent). Quand cette procédure se… … Wikipédia en Français
Algorithme de Knuth-Bendix — La procédure de complétion de Knuth Bendix transforme un ensemble d identités (sur des termes) décrivant une structure algébrique en un système de réécriture de terme confluent et qui termine (dit alors convergent). Quand cette procédure se… … Wikipédia en Français
Algorithmique — Organigramme de programmation représentant l algorithme d Euclide L algorithmique est l’ensemble des règles et des techniques qui sont impliquées dans la définition et la conception d algorithmes, c est à dire de processus systématiques de… … Wikipédia en Français
Sindarin — Auteur John Ronald Reuel Tolkien Parlée en le monde imaginaire de la Terre du Milieu Typologie langue flexionnelle Catégorie langue imaginaire Classification par famille … Wikipédia en Français

Dictionnaires et Encyclopédies sur 'Academic'

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

Sommaire