Rewriting on cyclic structures: Equivalence between the operational and the categorical description

¹ Dipartimento di Informatica, University of Pisa, Corso Italia 40, 56125 Pisa, Italy; andrea@di.unipi.it.
² Division of Informatics, University of Edinburgh, Mayfield Road, EH9 3JZ Edinburgh, U.K.; fabio@dcs.ed.ac.uk.

Received: 16 December 1998
Revised: 2 August 1999
Revised: 1 September 1999

Abstract

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.

Résumé

Nous présentons une formulation catégorique de la réécriture des graphes cycliques des termes, basée sur une variante de 2-theorie algébrique. Nous prouvons que cette présentation est équivalente à la définition opérationnelle proposée par Barendregt et al., mais pas dans le cas des radicaux circulaires, pour lesquels nous proposons (et justifions formellement) un traitement différent. Le cadre catégoriel nous permet de modeler également la “garbage collection” automatique, et des règles de “sharing/unsharing” et “folding/unfolding” des structures. En outre, ce cadre nous permet d'exploiter pour associer la réécriture des graphes des termes à d'autres formalismes de réécriture.