Termination orders for 3-dimensional rewriting

11 years 5 months ago
Termination orders for 3-dimensional rewriting
Abstract: This paper studies 3-polygraphs as a framework for rewriting on two-dimensional words. A translation of term rewriting systems into 3-polygraphs with explicit resource management is given, and the respective computational properties of each system are studied. Finally, a convergent 3-polygraph for the (commutative) theory of Z/2Z-vector spaces is given. In order to prove these results, it is explained how to craft a class of termination orders for 3-polygraphs. Outline This paper starts with the introductory section 1 on equational theories and term rewriting systems. It gives notations and graphical representations that are used in the sequel. Then, it focuses on one major restriction of term rewriting, namely the fact that it cannot provide convergent presentations for commutative equational theories: equational theories that contain a commutative binary operator. Section 2 studies the resource management operations of permutation, erasure and duplication: they are implicit...
Yves Guiraud
Added 11 Dec 2010
Updated 11 Dec 2010
Type Journal
Year 2006
Where CORR
Authors Yves Guiraud
Comments (0)