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...

• Type: Journal
• Year: 2006
• Where: CORR
• Authors: Yves Guiraud
• Keywords: CORR 2006, Education, Equational Theories, Resource Management, Term Rewriting Systems