On Term Graphs as an Adhesive Category

In this paper we consider the category of term graphs, and we prove that it (partly) fits in the general framework for adhesive categories, developed in [S. Lack, and P. Sobociński, Adhesive categories, in: I. Walukiewicz, editor, Foundations of Software Science and Computation Structures, Lect. Notes in Comp. Sci. 2987 (2004), pp. 273-288, P. Sobociński, “Deriving bisimulation congruences from reduction systems”, Ph.D. thesis, BRICS, Department of Computer Science, University of Aaurhus (2004)], extended in [H. Ehrig, A. Habel, J. Padberg and U. Prange, Adhesive high-level replacement categories and systems, in: G. Engels and F. Parisi-Presicce, editors, Graph Transformation, Lect. Notes in Comp. Sci. (2004)] and applied to reduction systems in [V. Sassone, and P. Sobociński, Congruences for contextual graph-rewriting, Technical Report RS-04-11, BRICS, Department of Computer Science, University of Aarhus (2004)]. 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.