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

AbstractWe present a general methodology aimed at providing an algebraic semantics for a large class of formalisms. The methodology, which generalizes the algebraic treatment of Petri nets proposed by Meseguer and Montanari (1990) individuates three levels of description of a formalism (i.e., programs, structured transitions systems, and models), and defines two free constructions which generate in an automatic way the induced transition system and the free model of a program. These constructions are parametric with respect to the structure of states and transitions: instantiating them in various ways, different formalisms can be treated.The construction of the free model extends the algebraic structure of transitions to the computations of a program, thus producing a category having as arrows abstract computations, i.e., equivalence classes of concrete computations. Interestingly, the equivalence relation induced on computations captures some basic properties of true concurrency. Moreover, by general categorical properties the construction of the free model is compositional w.r.t. various forms of program union.As a running example, we apply the methodology to phrase structure grammars, while the main case study is logic programming. For both formalisms the free model is shown to include all the computations at a natural level of abstraction: the free model of a grammar includes all its derivation trees as arrows, while the arrows of the free model of a logic program are parallel refutations