We present a categorical formulation of the rewriting of possibly cyclic term graphs, based on a variation of algebraic 2-theories. We show that this presentation is equivalent to the well-accepted operational definition proposed by Barendregt et al. - but for the case of circular redexes, for which we propose (and justify formally) a different treatment. The categorical framework allows us to model in a concise way also automatic garbage collection and rules for sharing/unsharing and folding/unfolding of structures, and to relate term graph rewriting to other rewriting formalisms.
|Autori:||CORRADINI A; GADDUCCI F|
|Titolo:||Rewriting on cyclic structures: Equivalence between the operational and the categorical description|
|Anno del prodotto:||1999|
|Digital Object Identifier (DOI):||10.1051/ita:1999128|
|Appare nelle tipologie:||1.1 Articolo in rivista|