Well-founded Path Orderings for Drags

Abstract : The definition herein of the Graph Path Ordering (GPO) on certain graph expressions is inspired by that of the Recursive Path Ordering (RPO), and enjoys all those properties that have made RPO popular, in particular, well-foundedness and monotonicity on variable-free terms. We are indeed interested in a generalization of algebraic expressions called operadic expressions, which are finite graphs each vertex of which is labelled by a function symbol, the arity of which governs the number of vertices it relates to in the graph. These graphs are seen here as terms with sharing and back-arrows. Operadic expressions are themselves multiplied (an associative operation) to form monomials, which are in turn summed up (an associative commutative operation) to form polynomials. Operadic expressions and their polynomials occur in algebraic topology, and in various areas of computer science, notably concurrency and type theory. Rewriting basic operadic expressions is very much like rewriting algebraic expressions, while rewriting their monomials and polynomials is very much like the Groebner basis theory. GPO provides an initial building block for computing with operadic expressions and their polynomials.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [7 references]  Display  Hide  Download

Contributor : Jean-Pierre Jouannaud <>
Submitted on : Monday, June 13, 2016 - 10:59:57 AM
Last modification on : Wednesday, March 27, 2019 - 4:41:27 PM


Files produced by the author(s)


  • HAL Id : hal-01330907, version 1


Nachum Dershowitz, Jean-Pierre Jouannaud, Jianqi Li. Well-founded Path Orderings for Drags. Proceedings Higher Dimensional Rewriting and Applications, Jun 2016, Porto, Portugal. ⟨hal-01330907⟩



Record views


Files downloads