×

An algebraic semantics for structured transition systems and its application to logic programs. (English) Zbl 0756.68075

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).
Reviewer: A.Corradini

MSC:

68Q55 Semantics in the theory of computing
18D35 Structured objects in a category (MSC2010)
68N17 Logic programming
68Q42 Grammars and rewriting systems

Software:

PARLOG; GHC
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Asperti, A.; Longo, G., Categories, Types and Structures, an Introduction to Category Theory for the Working Computer Scientist, (Foundations of Computing Series (1991), MIT Press: MIT Press Cambridge, MA) · Zbl 0783.18001
[2] Asperti, A.; Martini, S., Projections instead of variables, a category-theoretic interpretation of logic programs, Proc. 6th Internat. Conf. on Logic Programming, 337-352 (1989), Lisboa (Portugal)
[3] Barr, M.; Wells, C., Toposes, triples and theories, (Grundlehren der mathematischen Wissenschaften, Vol. 278 (1985), Springer: Springer Berlin) · Zbl 0567.18001
[4] Barr, M.; Wells, C., Category Theory for Computing Science (1990), Prentice Hall: Prentice Hall Englewood Cliffs, NJ · Zbl 0714.18001
[5] Bénabou, J., Structures algébraiques dans les catégories, Cahiers Topologie Géom. Différentielle Catégoriques, 10, 1-126 (1968) · Zbl 0162.32602
[6] Benson, D. B., The basic algebraic structures in categories of derivations, Inform. and Control, 28, 1-29 (1975) · Zbl 0304.68083
[7] Best, E.; Devillers, R., Sequential and concurrent behaviour in Petri net theory, Theoret. Comput. Sci., 55, 87-136 (1987) · Zbl 0669.68043
[8] Clark, K. L.; Gregory, S., PARLOG: parallel programming in logic, ACM TOPLAS, 8, 1-49 (1986) · Zbl 0592.68016
[9] Corradini, A., An algebraic semantics for transition systems and logic programming, (Ph.D. Thesis TD-8/90 (1990), Dipartimento di Informatica, Università di Pisa)
[10] Corradini, A.; Ferrari, G. L.; Montanari, U., Transition systems with algebraic structure as models of computations, (Guessarian, I., Semantics of Systems of Concurrent Processes (1990), Springer: Springer Berlin), 185-222, Lecture Notes in Computer Science
[11] Corradini, A.; Montanari, U., Towards a process semantics in the logic programming style, (Proc. 7th Symp. on Theoretical Aspects of Computer Science (STACS’90). Proc. 7th Symp. on Theoretical Aspects of Computer Science (STACS’90), Lecture Notes in Computer Science, Vol. 415 (1990), Springer: Springer Berlin), 95-108
[12] Corradini, A.; Montanari, U., An algebraic semantics of logic programs as structured transition systems, (Proc. North American Conf. on Logic Programming (NACLP’90) (1990), MIT Press: MIT Press Cambridge, MA), 788-812
[13] Corradini, A.; Montanari, U., An algebraic representation of logic program computations, (Lassez, J.; Plotkin, G., Computational Logic, Essays in Honor of Alan Robinson (1991), MIT Press: MIT Press Cambridge, MA), 584-612
[14] Corradini, A.; Montanari, U., An algebra of graphs and graph rewriting, (Proc. 4th Conf. on Category Theory and Computer Science (CTCS’91). Proc. 4th Conf. on Category Theory and Computer Science (CTCS’91), Lecture Notes in Computer Science, Vol. 530 (1991), Springer: Springer Berlin), 236-260 · Zbl 0792.68079
[15] Degano, P.; Meseguer, J.; Montanari, U., Axiomatizing net computations and processes, Proc. 4th Ann. Symp. on Logic in Computer Science, 175-185 (1989), Asilomar, CA · Zbl 0722.68085
[16] Ferrari, G., Unifying models of concurrency, (Ph.D. Thesis TD-4/90 (1990), Dipartimento di Informatica, Università di Pisa)
[17] Ferrari, G.; Montanari, U., Towards the unification of models for concurrency, (Proc. CAAP’90. Proc. CAAP’90, Lecture Notes in Computer Science, Vol. 431 (1990), Springer: Springer Berlin), 162-176 · Zbl 0758.68027
[18] Ginsburg, S., The Mathematical Theory of Context Free Languages (1966), MacGraw-Hill: MacGraw-Hill New York · Zbl 0184.28401
[19] Goguen, J. A., What is unification? A categorical view of substitution, equation and solution, (Nivat, M.; Aït-Kaci, H., Resolution of Equations in Algebraic Structures (1989), Academic Press: Academic Press New York)
[20] Goguen, J. A., A categorical manifesto, Math. Struc. Comput. Sci., 1, 49-68 (1991) · Zbl 0747.18001
[21] Gray, J. W., The category of sketches as a model for algebraic semantics, Contemp. Math., 92, 109-135 (1989)
[22] Keller, R., Formal verification of parallel programs, Comm. ACM, 7, 371-384 (1976) · Zbl 0329.68016
[23] Lawvere, F. W., Functorial semantics of algebraic theories, Proc. Nat. Acad. Sci., 50, 869-872 (1963), (Summary of Ph.D. Thesis, Columbia University.) · Zbl 0119.25901
[24] Lloyd, J. W., Foundations of Logic Programming (1987), Springer: Springer Berlin · Zbl 0547.68005
[25] MacLane, S., Categories for the Working Mathematician (1971), Springer: Springer New York
[26] Meseguer, J., General logics, (Ebbinghaus, H.-D., Proc. Logic Colloquium ’87 (1989), North-Holland: North-Holland Amsterdam) · Zbl 0691.03001
[27] Meseguer, J., Rewriting as a unified model of concurrency, (Proc. CONCUR ’90, Vol. 458 (1990), Springer: Springer Berlin), 384-400
[28] Meseguer, J.; Montanari, U., Petri nets are monoids, Inform. and Comput., 88, 105-155 (1990) · Zbl 0711.68077
[29] Milner, R., A calculus of communicating systems, (Lecture Notes in Computer Science, Vol. 92 (1980), Springer: Springer Berlin) · Zbl 0452.68027
[30] Plotkin, G., A structural approach to operational semantics, (Technical Report DAIMI FN-19 (1981), Aarhus University, Department of Computer Science: Aarhus University, Department of Computer Science Aarhus) · Zbl 1082.68062
[31] Reisig, W., Petri Nets: An Introduction, (EACTS Monographs on Theoretical Computer Science (1985), Springer: Springer Berlin) · Zbl 0521.68057
[32] Rydeheard, D. E.; Burstall, R. M., A categorical unification algorithm, (Proc. Workshop on Category Theory and Computer Programming. Proc. Workshop on Category Theory and Computer Programming, Lecture Notes in Computer Science, Vol. 240 (1985), Springer: Springer Berlin), 493-505 · Zbl 0616.68016
[33] Shapiro, E., Concurrent Prolog: a progress report, (Bibel, W.; Jorrand, Ph., Fundamentals of Artificial Intelligence. Fundamentals of Artificial Intelligence, Lecture Notes in Computer Science, Vol. 232 (1986), Springer: Springer Berlin), 277-313
[34] Tarski, A., A lattice-theoretical fixpoint theorem and its application, Pacific J. Math., 5, 285-309 (1955) · Zbl 0064.26004
[35] Ueda, K., Guarded horn clauses, ICOT TR-103 (1985) · Zbl 0771.68037
[36] Winskel, G., A compositional proof system on a category of labelled transition systems, Inform. and Comput., 87, 2-57 (1990) · Zbl 0719.68010
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.