Friday 1st April 2016, 10:30: GPO: a total well-founded monotonic path ordering for directed rooted labelled graphs, Jean-Pierre Jouannaud (Université Paris-Sud, École Polytechnique).

The Equational, Rational Path Ordering is a well-founded ordering on certain graph expressions whose definition is inspired by that of the Recursive Path Ordering, and which enjoys all properties that have made RPO popular, in particular well-foundedness and monotonicity. Being equational, the ordering is also compatible with any given congruence on expressions satisfying certain axiomatic properties. Associativity and commutativity is an example of such a congruence. Last, but not least, the ordering decreases when sharing decreases, a crucial property if one wants to avoid dandling pointers when rewriting expressions with sharing, and increases, as expected, when unfolding rational branches.

We are indeed interested in a generalization of algebraic expressions called operadic, in which elements are graphs whose each vertex 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. Further, some function symbols may be associative-commutative, implying that the corresponding vertex can be related to an unbounded number of other vertices having a different label. Operadic expressions occur in algebraic topology, and in various areas of computer science, notably concurrency and type theory. Rewriting operadic expressions is very much like rewriting algebraic expressions. ERPO provides with a first building block for computing with operadic expressions.

Joint work with Nachum dershowitz and Jianqi Li.