Système de réécriture abstraite

En logique mathématique et en informatique théorique , un système de réécriture abstrait (également appelé système de réduction (abstrait) ou système de réécriture abstrait ; abrégé ARS ) est un formalisme qui capture la notion et les propriétés essentielles des systèmes de réécriture . Dans sa forme la plus simple, un ARS est simplement un ensemble (d'« objets ») associé à une relation binaire , traditionnellement désignée par ; cette définition peut être encore affinée si nous indexons (étiquetons) des sous-ensembles de la relation binaire. Malgré sa simplicité, un ARS est suffisant pour décrire des propriétés importantes des systèmes de réécriture comme les formes normales , la terminaison et diverses notions de confluence .

Historiquement, il existe plusieurs formalisations de la réécriture dans un cadre abstrait, chacune avec ses idiosyncrasies. Cela est dû en partie au fait que certaines notions sont équivalentes, voir plus loin dans cet article. La formalisation la plus fréquemment rencontrée dans les monographies et les manuels, et qui est généralement suivie ici, est due à Gérard Huet (1980).

Un système de réduction abstrait ( ARS ) est la notion la plus générale (unidimensionnelle) de spécification d'un ensemble d'objets et de règles qui peuvent être appliquées pour les transformer. Plus récemment, les auteurs utilisent également le terme de système de réécriture abstrait . (La préférence pour le mot « réduction » ici au lieu de « réécriture » constitue une dérogation à l'utilisation uniforme de « réécriture » dans les noms de systèmes qui sont des particularisations d'ARS. Étant donné que le mot « réduction » n'apparaît pas dans les noms de systèmes plus spécialisés, dans les textes plus anciens, système de réduction est synonyme d'ARS.)

Un ARS est un ensemble A , dont les éléments sont généralement appelés objets, ainsi qu'une relation binaire sur A , traditionnellement notée →, et appelée relation de réduction , relation de réécriture ou simplement réduction . Cette terminologie (enracinée) utilisant le terme « réduction » est un peu trompeuse, car la relation ne réduit pas nécessairement une certaine mesure des objets.

Dans certains contextes, il peut être utile de distinguer certains sous-ensembles de règles, c'est-à-dire certains sous-ensembles de la relation de réduction →, par exemple la relation de réduction entière peut être constituée de règles d'associativité et de commutativité . Par conséquent, certains auteurs définissent la relation de réduction → comme l'union indexée de certaines relations ; par exemple si , la notation utilisée est (A, → ₁ , → ₂ ).

En tant qu'objet mathématique, un ARS est exactement le même qu'un système de transition d'état non étiqueté , et si la relation est considérée comme une union indexée, alors un ARS est le même qu'un système de transition d'état étiqueté, les indices étant les étiquettes. L'objet de l'étude et la terminologie sont cependant différents. Dans un système de transition d'état , on s'intéresse à l'interprétation des étiquettes comme des actions, tandis que dans un ARS, l'accent est mis sur la façon dont les objets peuvent être transformés (réécrits) en d'autres.

Supposons que l'ensemble des objets soit T = { a , b , c } et que la relation binaire soit donnée par les règles a → b , b → a , a → c et b → c . On remarque que ces règles peuvent être appliquées à la fois à a et à b pour obtenir c . De plus, rien ne peut être appliqué à c pour le transformer davantage. Une telle propriété est clairement importante.

Définissons d’abord quelques notions et notations de base.

• De même, , et sont des fermetures de , la relation inverse de .

Un objet x dans A est dit réductible s'il existe un autre y dans A et ; sinon, il est dit irréductible ou une forme normale . Un objet y est dit une forme normale de x si et y est irréductible. Si x a une forme normale unique , alors celle-ci est généralement notée . Dans l'exemple 1 ci-dessus, c est une forme normale, et . Si chaque objet a au moins une forme normale, l'ARS est dite normalisante .

Une notion apparentée, mais plus faible que l'existence de formes normales, est celle de deux objets pouvant être joints : x et y sont dits joignables s'il existe un z ayant la propriété que . À partir de cette définition, il est évident que l'on peut définir la relation de joignabilité comme , où est la composition des relations . La joignabilité est généralement notée, de manière quelque peu déroutante, également par , mais dans cette notation la flèche vers le bas est une relation binaire, c'est-à-dire que nous écrivons si x et y sont joignables.

On dit qu'un ARS possède la propriété de Church-Rosser si et seulement si implique pour tous les objets x , y . De manière équivalente, la propriété de Church-Rosser signifie que la fermeture symétrique réflexive transitive est contenue dans la relation de jointabilité. Alonzo Church et J. Barkley Rosser ont prouvé en 1936 que le calcul lambda possède cette propriété ; d'où le nom de la propriété. Dans un ARS avec la propriété de Church-Rosser, le problème verbal peut être réduit à la recherche d'un successeur commun. Dans un système de Church-Rosser, un objet a au plus une forme normale ; c'est-à-dire que la forme normale d'un objet est unique si elle existe, mais elle peut très bien ne pas exister.

Plusieurs propriétés, plus simples que Church-Rosser, lui sont équivalentes. L'existence de ces propriétés équivalentes permet de prouver qu'un système est de type Church-Rosser avec moins de travail. De plus, les notions de confluence peuvent être définies comme des propriétés d'un objet particulier, ce qui n'est pas possible pour Church-Rosser. On dit qu'un ARS est,

• confluent si et seulement si pour tous w , x et y dans A , implique . En gros, la confluence dit que peu importe la façon dont deux chemins divergent d'un ancêtre commun ( w ), les chemins se rejoignent en un successeur commun. Cette notion peut être raffinée comme propriété d'un objet particulier w , et le système appelé confluent si tous ses éléments sont confluents.
• semi-confluent si et seulement si pour tous w , x et y dans A , implique . Cela diffère de la confluence par la réduction en une seule étape de w à x .
• localement confluente si et seulement si pour tous w , x et y dans A , implique . Cette propriété est parfois appelée confluence faible .

Théorème. Pour un ARS, les trois conditions suivantes sont équivalentes : (i) il possède la propriété de Church-Rosser, (ii) il est confluent, (iii) il est semi-confluent.

Corollaire . Dans un ARS confluent si alors

• Si x et y sont tous deux des formes normales, alors x = y .
• Si y est une forme normale, alors .

En raison de ces équivalences, on rencontre dans la littérature une certaine variation dans les définitions. Par exemple, dans Terese, la propriété de Church-Rosser et la confluence sont définies comme étant synonymes et identiques à la définition de la confluence présentée ici ; la propriété de Church-Rosser telle que définie ici reste sans nom, mais est donnée comme une propriété équivalente ; cet écart par rapport aux autres textes est délibéré. En raison du corollaire ci-dessus, on peut définir une forme normale y de x comme un y irréductible avec la propriété que . Cette définition, trouvée dans Book et Otto, est équivalente à celle courante donnée ici dans un système confluent, mais elle est plus inclusive dans un SRA non confluent.

La confluence locale n'est pas équivalente aux autres notions de confluence données dans cette section, mais elle est strictement plus faible que la confluence. Le contre-exemple typique est , qui est localement confluente mais pas confluente (cf. image).

Un système de réécriture abstrait est dit terminal ou noethérien s'il n'y a pas de chaîne infinie . (Cela signifie simplement que la relation de réécriture est une relation noéthérienne .) Dans un système de réécriture abstrait terminal, chaque objet a au moins une forme normale, il est donc normalisant. L'inverse n'est pas vrai. Dans l'exemple 1 par exemple, il existe une chaîne de réécriture infinie, à savoir , même si le système est normalisant. Un système de réécriture abstrait confluent et terminal est appelé canonique , ou convergent . Dans un système de réécriture abstrait convergent, chaque objet a une forme normale unique. Mais il suffit que le système soit confluent et normalisant pour qu'une normale unique existe pour chaque élément, comme on le voit dans l'exemple 1.

Théorème ( lemme de Newman ) : Un ARS terminal est confluent si et seulement s'il est localement confluent.

La preuve originale de ce résultat par Newman en 1942 était assez compliquée. Ce n'est qu'en 1980 que Huet a publié une preuve beaucoup plus simple exploitant le fait que lorsque est se termine, on peut appliquer l'induction bien fondée .