An Algebraic Presentation of Term Graphs, via GS-Monoidal Categories

We present a categorical characterization of term graphs (i.e., finite, directed acyclic graphs labeled over a signature) that parallels the well-known characterization of terms as arrows of the algebraic theory of a given signature (i.e., the free Cartesian category generated by it). In particular, we show that term graphs over a signature Σ are one-to-one with the arrows of the free gs-monoidal category generated by Σ. Such a category satisfies all the axioms for Cartesian categories but for the naturality of two transformations (the discharger ! and the duplicator ▽), providing in this way an abstract and clear relationship between terms and term graphs. In particular, the absence of the naturality of ▽ and ! has a precise interpretation in terms of explicit sharing and of loss of implicit garbage collection, respectively