It is well-known that a term rewriting system can be faithfully described by a cartesian 2-category, where horizontal arrows represent terms, and cells represent rewriting sequences. In this paper we propose a similar, original 2-categorical presentation for term graph rewriting. Building on a result presented in [8], which shows that term graphs over a given signature are in one-to-one correspondence with arrows of a gs-monoidal category freely generated from the signature, we associate with a term graph rewriting system a gs-monoidal 2-category, and show that cells faithfully represent its rewriting sequences. We exploit the categorical framework to relate term graph rewriting and term rewriting, since gs-monoidal (2-)categories can be regarded as "weak" cartesian (2-)categories, where certain (2-)naturality axioms have been dropped.
CITATION STYLE
Corradini, A., & Gadducci, F. (1997). A 2-categorical presentation of term graph rewriting. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1290, pp. 87–105). Springer Verlag. https://doi.org/10.1007/bfb0026983
Mendeley helps you to discover research relevant for your work.