Terminaison d'un système de réécriture
![Si ce bandeau n'est plus pertinent, retirez-le. Cliquez ici pour en savoir plus.](http://upload.wikimedia.org/wikipedia/commons/thumb/3/38/Info_Simple.svg/12px-Info_Simple.svg.png)
![](http://upload.wikimedia.org/wikipedia/commons/thumb/a/a1/2017-fr.wp-orange-source.svg/45px-2017-fr.wp-orange-source.svg.png)
Cet article ne cite pas suffisamment ses sources ().
Si vous disposez d'ouvrages ou d'articles de référence ou si vous connaissez des sites web de qualité traitant du thème abordé ici, merci de compléter l'article en donnant les références utiles à sa vérifiabilité et en les liant à la section « Notes et références ».
En pratique : Quelles sources sont attendues ? Comment ajouter mes sources ?
La terminaison d'un système de réécriture porte sur un système de réécriture abstrait et affirme que toute chaîne de réduction de termes de la forme est finie. Elle est souvent présentée en disant qu'il n'y a aucune chaîne de réduction infinie.
Approche générale des techniques pour la terminaison
La relation de réécriture associée à un système de réécriture est l'ensemble des couples de termes tels que se réécrive en par une règle de . On dit alors qu'un système de réécriture se termine si et seulement si la relation de réécriture qui lui est associée est bien fondée. Autrement dit, le prédicat « se termine » est le plus petit prédicat au sens de l'inclusion qui satisfait la propriété suivante[1].
- Si et si se termine alors se termine.
On notera que cette propriété implique
- Si est en forme normale alors se termine.
Les systèmes de réécriture sont suffisamment puissants pour coder par exemple les machines de Turing ou le problème de correspondance de Post, il en découle que la terminaison des systèmes de réécriture est indécidable[2].
Heureusement, des arguments de terminaison incomplets sont utilisables dans beaucoup cas.
Interprétation
On se donne un ensemble muni d'un ordre bien fondé (par exemple les entiers naturels[3]). À 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 d'arité de la signature, pour tous termes et , si alors ;
- il est stable par substitution, c'est-à-dire que pour toute substitution , pour tous termes et , si alors ;
- 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.
Exemples
Taille des termes
Exemple:
Interprétation polynomiale[4]
À tout terme on va associer un poids qui est un entier positif : à tout symbole de fonction d'arité on associe un polynôme à variables ; le poids d'un terme sera la valeur du polynôme associé à au point .
Exemple (avec symboles p,s,z, d'arités respectives 2,1,0)
On choisit
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 =
- poids de la partie droite =
- Règle 2,
- partie gauche : ,
- partie droite :
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[5].
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 et . On dit que est plus grand que pour l'ordre RPO associé à la précédence > si
- et est plus grand que pour l'ordre multiensemble associé au RPO ; ou
- et pour tout , est plus grand que pour l'ordre RPO ; ou
- il existe un tel que soit plus grand que 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 que pour tout , est plus grand que 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 est un sous-terme de , alors est plus grand que , 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 :
à l'aide de la précédence .
Notes et références
- ↑ On dit alors que le prédicat est héréditaire (en) pour la relation de réécriture.
- ↑ « Index of / », sur perso.eleves.ens-rennes.fr (consulté le )
- ↑ On peut aussi prendre des ordinaux.
- ↑ Jocelyne Rouyer, « Preuves de terminaison de systèmes de réécriture fondées sur les interprétations polynomiales. Une méthode basée sur le théorème de Sturm », RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, vol. 25, no 2, , p. 157–169 (ISSN 1290-385X, lire en ligne, consulté le )
- ↑ Frédéric Blanqui, « Terminaison des systèmes de réécriture d'ordre supérieur basée sur la notion de clôture de calculabilité », theses.hal.science, Université Paris-Diderot - Paris VII, (lire en ligne, consulté le )
Portail des mathématiques
Portail de la logique
Portail de l'informatique théorique