Lemme de Newman

vignette|Confluence. vignette|Confluence locale. En mathématiques et en informatique, plus précisément dans la théorie des relations binaires, le lemme de Newman dit qu'une relation binaire noethérienne est confluente si elle est localement confluente. Une démonstration relativement simple (induction sur une relation bien fondée) est due à Gérard Huet en 1980. La démonstration originale de Newman est plus compliquée, mais la méthode des diagrammes décroissants montre bien comment elle fonctionne. Une relation binaire est noethérienne (ou se termine) si toute chaîne d'éléments reliés les uns aux autres par la relation est finie. Elle est localement confluente lorsque si depuis un élément t, on peut aller à t1 par la relation et on peut aussi aller à t2, alors de t1 et de t2 on peut aller par une chaîne de relations à un même élément t'. Elle est confluente lorsque si depuis un élément t, en appliquant une suite de relations on obtient t1, et en appliquant une autre suite de relations on obtient t2, alors t1 et t2 peuvent tous les deux aller vers un même élément t'. Considérons la relation binaire suivante → : a → b et b → a a → x b → y La relation est localement confluente ; par exemple, a → x et a → b et x et b vont tous deux vers x (b → a → x). Par contre, la relation binaire n'est pas confluente : a → x et a → b → y, mais x et y ne peuvent aller vers un même élément (en effet depuis x ou y aucune flèche ne part). vignette|Démonstration du lemme de Newman. On applique la confluence locale (en vert) puis deux fois l'hypothèse d'induction (en orange et brun). Le lemme de Newman se démontre par induction en utilisant le fait que la relation est noethérienne. Considérons la propriété P(t) : si t → t1, t → t2, alors t1 et t2 vont vers le même élément t'. Si t → t1 en 0 étape (cela signifie t1 = t) ou si t → t2 en 0 étape (cela signifie t2 = t), t1 et t2 vont vers le même élément t'. Les autres cas sont illustrés par la figure de droite. Si l'on sait qu'un système de réécriture est noethérien alors la confluence locale est décidable.

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Concepts associés (5)

Abstract rewriting system

In mathematical logic and theoretical computer science, an abstract rewriting system (also (abstract) reduction system or abstract rewrite system; abbreviated ARS) is a formalism that captures the quintessential notion and properties of rewriting systems. In its simplest form, an ARS is simply a set (of "objects") together with a binary relation, traditionally denoted with ; this definition can be further refined if we index (label) subsets of the binary relation.

Confluence (informatique)

vignette|Le nom « confluence » est le même que celui utilisé en géographie : deux cours d'eau se rejoignent. En mathématiques, ou en informatique, la confluence d'une relation binaire est définie comme la propriété suivante : Pour tous éléments tels que et , il existe un élément tel que et . La confluence est équivalente à la propriété de Church-Rosser. La confluence locale est une propriété plus faible que la confluence, utile pour les systèmes de réécriture. Elle est définie par : Pour tous éléments tels que et , il existe un élément tel que et .

Normal form (abstract rewriting)

In abstract rewriting, an object is in normal form if it cannot be rewritten any further, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all. Many properties of rewriting systems relate to normal forms. Stated formally, if (A,→) is an abstract rewriting system, x∈A is in normal form if no y∈A exists such that x→y, i.e. x is an irreducible term. An object a is weakly normalizing if there exists at least one particular sequence of rewrites starting from a that eventually yields a normal form.