An algebraic semantics for structured transition systems and its application to logic programs (Q1199528)

The paper introduces a general methodology, based on categorical constructions, aimed at providing a uniform algebraic semantics for a large class of formalisms. This class includes Petri nets, phrase structure grammars, logic programming, and term rewriting systems. The methodology individuates three levels of description for each computational formalism, corresponding to programs, to structured transition systems, and to models, respectively. The methodology is parametric with respect to a universe category \(\mathbb{C}\): the semantics of a specified formalism is obtained by instantiating \(\mathbb{C}\) with a suitable category. A program is regarded as a graph having as nodes an object of \(\mathbb{C}\), and usually a poorer structure on arcs. Structured transition systems are defined instead as internal graphs of \(\mathbb{C}\), while models are small internal categories of \(\mathbb{C}\). Two free constructions (characterized as left adjoint functors between the corresponding categories) are considered: the first one associates each program with its induced structured transition system, and the second one maps each transition system to its free model. The last construction is proved to exist if category \(\mathbb{C}\) is essentially algebraic, generalizing to this universe the construction of the free category generated by a graph. The methodology associates with each program a category of models, where the free model is initial. The arrows of a model represent all the computations of the program at a certain level of abstraction. Since the model is an internal category of \(\mathbb{C}\), the computations are equipped with the algebraic structure of \(\mathbb{C}\): this inducs an equivalence relation on computations which is shown to captures some basic properties of true concurrency. Moreover, since the construction of the free model is a left adjoint functor, it is compositional with respect to operations on programs expressible as colimits. As a running example, the methodology is applied to phrase structure grammars (in this case \(\mathbb{C}\) is the category of monoids), while the main case study is logic programming (where \(\mathbb{C}\) becomes \(\mathbf{Cart}\), the category of small cartesian categories).