The recent interest in bisimulation congruences for reduction systems, stimulated by the research on general (often graphical) frameworks for nominal calculi, has brought forward many proposals for categorical formalisms where relevant properties of observational equivalences could be auto- matically verified. Interestingly, some of these formalisms also identified suitable categories where the standard tools and techniques developed for the double-pushout approach to graph transformation could be recast, thus providing a valid alternative to the High-Level Replacement Systems paradigm. In this paper we consider the category of term graphs, and we prove that it (partly) fits in the general framework for adhesive categories. The main technical achievement concerns the proof that the category of term graphs is actually quasi-adhesive, obtained by proving the existence of suitable Van Kampen squares.
On term graphs as an adhesive category
CORRADINI, ANDREA;GADDUCCI, FABIO
2005-01-01
Abstract
The recent interest in bisimulation congruences for reduction systems, stimulated by the research on general (often graphical) frameworks for nominal calculi, has brought forward many proposals for categorical formalisms where relevant properties of observational equivalences could be auto- matically verified. Interestingly, some of these formalisms also identified suitable categories where the standard tools and techniques developed for the double-pushout approach to graph transformation could be recast, thus providing a valid alternative to the High-Level Replacement Systems paradigm. In this paper we consider the category of term graphs, and we prove that it (partly) fits in the general framework for adhesive categories. The main technical achievement concerns the proof that the category of term graphs is actually quasi-adhesive, obtained by proving the existence of suitable Van Kampen squares.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
