Termination orders for 3-dimensional rewriting
Category Theory
2007-05-23 v1 Logic in Computer Science
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.
Keywords
Cite
@article{arxiv.math/0612083,
title = {Termination orders for 3-dimensional rewriting},
author = {Yves Guiraud},
journal= {arXiv preprint arXiv:math/0612083},
year = {2007}
}
Comments
30 pages, 35 figures