Termination orders for 3-dimensional rewriting
classification
🧮 math.CT
cs.LO
keywords
polygraphsrewritinggivenordersterminationclasscommutativecomputational
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.