GS·Λ theories: A syntax for higher-order graphs

Graphs and term graphs have proved strikingly flexible and expressive in modeling and specifying distributed, concurrent systems. However, even if the theory of (term) graph transformation systems is well developed, it has not yet included higher-order features, which are essential, in ordinary programming languages, to guarantee the levels of parametrisation and modularity that are required in practice. Our proposal aims at filling that gap by equipping graph-based formalisms with higher-order constructs. Our starting point has been graph substitution (gs) theories by Corradini and Gadducci, which are proved to be syntactical counterparts for term graphs (in the same way as algebraic theories are for terms). As for cartesian categories, gs categories specify symmetric monoidal categories equipped with two transformations, representing sub-term copying and garbage collection. However, for gs theories the naturality of these transformations does not hold. GS·Λ theories enrich gs theories by requiring the existence of a right adjoint a ⊸ _ to the tensor _⊗ a, for each object a. As such, they can be considered as transformation enriched autonomous categories. The resulting categories are tightly linked to the higher-order sharing theories introduced by Hasegawa: these latter are in fact reflective sub-categories of GS·Λ theories, since they are captured by an equivalent axiomatisation, except for the laws concerning the duplication of a set of values (namely, of λ-abstractions, interpreted as finished computations). Dropping those axioms allow for a neat graphical representation, expanding the wire-and-box notation developed for gs theories in a conservative manner.