Conditional rewriting logic as a unified model of concurrency. (English) Zbl 0758.68043

This work attempts to clearify the notion of a concurrent system by proposing a model theory for deduction, i.e., the proof theory of rewriting. The 82 pages of the paper are organized in 6 sections which are shortly described as follows:
In the first section it is argued why and how rewriting logic is a logic of action and, as such, being intrinsically of concurrent nature.
Section 2 contains the basics of rewriting and the rule of (concurrent) deduction are given.
The semantics is given in Secion 3 by interpreting the rewriting rules as rules of generation. The initial model is proven to be sound and complete.
Section 4 proposes the language MAUDE which includes OBJ-3 and serves as a semantics of rewrite rule programs as concurrent systems.
Section 5 shows in detail how many well known concurrent systems can be viewed as concurrent rewriting systems.
The 5 sections are completed with a discussion of related work and a list of 125 references.


68Q55 Semantics in the theory of computing
03C65 Models of other mathematical theories
03B80 Other applications of logic


Maude; Simula 67; UNITY; OBJ3
Full Text: DOI


[1] Abadi, M.; Cardelli, L.; Curien, P.-L.; Lévy, J.-J., Explicit substitution, (), 31-46
[2] Agha, G., Actors, (1986), MIT Press Cambridge, MA
[3] Agha, G.; Hewitt, C., Concurrent programming using actors, (), 37-53
[4] ()
[5] Aida, H.; Goguen, J.; Meseguer, J., Compiling concurrent rewriting onto the rewrite rule machine, (), to appear
[6] Aida, H.; Leinwand, S.; Meseguer, J., Architectural design of the rewrite rule machine ensemble, (), also, Tech. Report SRI-CSL-90-17
[7] Andreoli, J.-M.; Pareschi, R., LO and behold! concurrent structured processes, (), 44-56
[8] Appel, A.; MacQueen, D., A standard ML compiler, (), 301-324, Lecture Notes in Computer Science
[9] Asperti, A., A logic for concurrency, (November 1987), Unpublished manuscript
[10] Badouel, E., Conditional rewrite rules as an algebraic semantics of processes, (May 1990), INRIA, Technical Report 1226
[11] Banâtre, J.-P.; Le Mètayer, D., The GAMMA model and its discipline of programming, Sci. comput. programming, 15, 55-77, (1990) · Zbl 0715.68054
[12] Barendregt, H.P., The lambda calculus, its syntax and semantics, (1984), North-Holland Amsterdam · Zbl 0551.03007
[13] Barr, M.; Wells, C., Toposes, triples and theories, (1985), Springer Berlin · Zbl 0567.18001
[14] Bauderon, M.; Courcelle, B., Graph expressions and graph rewriting, Math. systems theory, 20, 83-127, (1987) · Zbl 0641.68115
[15] Bergstra, J.; Tucker, J., Characterization of computable data types by means of a finite equational specification method, (), 76-90, Lecture Notes in Computer Science
[16] Berry, G.; Boudol, G., The chemical abstract machine, (), 81-94
[17] Bloom, S., Varieties of ordered algebras, J. comput. system sci., 13, 200-212, (1976) · Zbl 0337.06008
[18] Boudol, G., Computational semantics of term rewriting systems, (), 169-236
[19] Boudol, G., Towards a lambda calculus for concurrent and communicating systems, (), 149-161, Lecture Notes in Computer Science
[20] Boudol, G.; Castellani, I., Permutation of transitions: an event structure semantics for CCS and SCCS, (), 411-427, Lecture Notes in Computer Science · Zbl 0683.68029
[21] Chandy, K.M.; Misra, J., Parallel program design: A foundation, (1988), Addison-Wesley Reading, MA · Zbl 0717.68034
[22] Clément, D.; Despeyroux, J.; Hascoet, L.; Kahn, G., Natural semantics on the computer, (), 49-89, also, Information Processing Society of Japan, Technical Memorandum PL-86-6
[23] Clinger, W., Foundations of actor semantics, (1981), Massachusetts Institute of Technology, Artificial Intelligence Laboratory, AI-TR-633
[24] Corradini, A.; Montanari, U., An algebraic semantics of logic programs as structured transition systems, (), 788-812
[25] Courcelle, B., Infinite trees in normal form and recursive equations having a unique solution, Math. systems theory, 13, 131-180, (1979) · Zbl 0418.68013
[26] Courcelle, B.; Nivat, M., The algebraic semantics of recursive program schemes, (), 16-30, Lecture Notes in Computer Science · Zbl 0384.68016
[27] Cousineau, G.; Curien, P.-L.; Mauny, M., The categorical abstract machine, Sci. comput. programming, 8, 173-202, (1987) · Zbl 0634.68078
[28] Curien, P.-L., Categorical combinators, sequential algorithms and functional programming, (1986), Pitman London · Zbl 0643.68004
[29] Curry, H.B.; Feys, R., Combinatory logic, (1968), North-Holland Amsterdam · Zbl 0175.27601
[30] Dahl, O.-J.; Myhrhaug, B.; Nygaard, K., The simula 67 common base language, (1970), Norwegian Computing Center Oslo, Publication S-22
[31] Degano, P.; Meseguer, J.; Montanari, U., Axiomatizing net computations and processes, (), 175-185
[32] Degano, P.; Meseguer, J.; Montanari, U., Axiomatizing the algebra of net computations and processes, (November 1990), SRI International, Computer Science Laboratory, submitted
[33] Dershowitz, N.; Jouannaud, J.-P., Rewrite systems, (), 243-320 · Zbl 0900.68283
[34] Dershowitz, N.; Kaplan, S.; Plaisted, D., Infinite normal forms, (), 249-262, Lecture Notes in Computer Science
[35] Ehrig, H., Introduction to the algebraic theory of graph grammars, (), 1-69, Lecture Notes in Computer Science
[36] Engelfriet, J., Net-based description of parallel object-based systems, or POTs and pops, Noordwijkerhout FOOL workshop, (May 1990), Technical report
[37] Engelfriet, J.; Leih, G.; Rozenberg, G., Parallel object-based systems and Petri nets, I and II, ()
[38] Freyd, P., Aspects of topoi, Bull. austral. math. soc., 7, 1-76, (1972) · Zbl 0252.18001
[39] Futatsugi, K.; Goguen, J.; Jouannaud, J.-P.; Meseguer, J., Principles of OBJ2, (), 52-66
[40] Girard, J.-Y., Towards a geometry of interaction, (), 69-108
[41] Gödel, K., On undecidable propositions of formal mathematical systems, (), 39-74
[42] Goguen, J.A., Semantic specifications for the rewrite rule machine, (), 216-234, Lecture Notes in Computer Science
[43] Goguen, J., Sheaf semantics for concurrent interacting objects, Proc. REX school on foundations of object-oriented programming, noorwijkerhout, The Netherlands, (May 28-June 1, 1990), to appear
[44] Goguen, J., How to prove algebraic inductive hypotheses without induction: with applications to the correctness of data type representations, (), 356-373, Lecture Notes in Computer Science
[45] Goguen, J.; Jouannaud, J.-P.; Messeguer, J., Operational semantics of order-sorted algebra, (), 221-231, Lecture Notes in Computer Science
[46] Goguen, J.; Kirchner, C.; Kirchner, H.; Mégrelis, A.; Meseguer, J.; Winkler, T., An introduction to OBJ3, (), 258-263, Lecture Notes in Computer Science
[47] Goguen, J.; Kirchner, C.; Meseguer, J., Concurrent term rewriting as a model of computation, (), 53-93, Lecture Notes in Computer Science
[48] Goguen, J.; Meseguer, J.; Goguen, J.; Meseguer, J., Unifying functional, object-oriented and relational programming with logical semantics, (), 21, 10, 153-162, (1986), also
[49] Goguen, J.; Meseguer, J., Software for the rewrite rule machine, (), 628-637
[50] Goguen, J.; Meseguer, J., Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Technical report SRI-CSL-89-10, (July 1989), SRI International, Computer Science Lab
[51] Goguen, J.; Tardo, J., OBJ-0 preliminary users manual, (1977), UCLA, Semantics and theory of computation report 10
[52] Goguen, J.; Thatcher, J.; Wagner, E., An initial algebra approach to the specification, correctness and implementation of abstract data types, (), 80-149
[53] Goguen, J.; Thatcher, J.; Wagner, E.; Wright, J., Initial algebra semantics and continuous algebras, J. ACM, 24, 1, 68-95, (1977) · Zbl 0359.68018
[54] Guessarian, I., Algebraic semantics, Vol. 99, (1981), Springer Berlin, Lecture Notes in Computer Science · Zbl 0474.68010
[55] Gunter, C.; Gehlot, V., Nets as tensor theories, (1989), Dept. of Computer and Information Science, University of Pennsylvania, Technical Report MS-CIS-89-68
[56] Harrison, P.G.; Reeve, M.J., The parallel graph reduction machine alice, (), 181-202, Lecture Notes in Computer Science
[57] Hesselink, W.H., A mathematical approach to nondeterminism in data types, ACM trans. prog. lang. sys., 10, 87-117, (1988) · Zbl 0825.68330
[58] Hindley, J.R.; Seldin, J.P., Introduction to combinators and λ-calculus, (1986), Cambridge University Press Cambridge · Zbl 0614.03014
[59] Hoare, C.A.R., Communicating sequential processes, (1985), Prentice-Hall Englewood Cliffs, NJ · Zbl 0637.68007
[60] Huet, G., Formal structures for computation and deduction, (1986), INRIA
[61] Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, J. ACM, 18th symposium on mathematical foundations of computer science, 27, 797-821, (1977), preliminary version in · Zbl 0458.68007
[62] Hughes, J., Super-combinators: a new implementation method for applicative languages, (), 1-10
[63] H. Hussmann, Nondeterministic algebraic specifications and nonconfluent term rewriting, Computer Science Dept., TU Munich. · Zbl 0708.68043
[64] Janssens, D.; Rozenberg, G., Actor grammars, Math. systems theory, 22, 75-107, (1989) · Zbl 0677.68082
[65] Jayaraman, B.; Plaisted, D., Functional programming with sets, (), 194-210, Lecture Notes in Computer Science
[66] Johnsson, Th., Target code generation from G-machine code, (), 119-559, Lecture Notes in Computer Science · Zbl 0641.68043
[67] Peyton Jones, S.L.; Clack, C.; Salkild, J.; Hardie, M., GRIP — a high-performance architecture for parallel graph reduction, (), 98-112, Lecture Notes in Computer Science
[68] Jouannaud, J.-P.; Kirchner, H., Completion of a set of rules modulo a set of equations, SIAM J. comput., 15, 1155-1194, (1986) · Zbl 0665.03005
[69] (), Lecture Notes in Computer Science
[70] Kelly, G.M.; Street, R., Review of the elements of 2-categories, (), 75-103, Lecture Notes in Math.
[71] Kennaway, R., On “on graph rewritings”, Theoret. comput. sci., 52, 37-58, (1987) · Zbl 0636.68028
[72] Kennaway, R., Graph rewriting in some categories of partial morphisms, (1990), School of Information Systems, University of East Anglia, Technical report
[73] Kieburtz, R., The G-machine: a fast, graph-reduction evaluator, (), 400-413, Lecture Notes in Computer Science
[74] Kirchner, C.; Kirchner, H.; Meseguer, J., Operational semantics of OBJ3, (), 287-301, Lecture Notes in Computer Science
[75] Kleene, S.C., General recursive functions of natural numbers, Math. ann., 112, 5, 727-742, (1936) · Zbl 0014.19402
[76] Klop, J.W., Combinatory reduction systems, (1980), Mathematisch Centrum Amsterdam · Zbl 0466.03006
[77] Lafont, Y., The linear abstract machine, Theoret. comput. sci., 59, 157-180, (1988) · Zbl 0648.68016
[78] Lambek, J., Subequalizers, Canad. math. bull., 13, 337-349, (1979) · Zbl 0201.02302
[79] Lambek, J., Deductive systems and categories II, (), 76-122, Lecture Notes in Math. · Zbl 0198.33701
[80] Lawvere, F.W., Adjointness in foundations, Dialectica, 23, 3/4, 281-296, (1969) · Zbl 0341.18002
[81] Leinwand, S.; Goguen, J.A.; Winkler, T., Cell and ensemble architecture for the rewrite rule machine, (), 869-878
[82] Lévy, J.-J., Optimal reductions in the lambda calculus, (), 159-191
[83] MacLane, S., Categories for the working Mathematician, (1971), Springer Berlin
[84] Martí-Oliet, N.; Meseguer, J., An algebraic axiomatization of linear logic models, (), Technical Report SRI-CSL-89-11, SRI International, Computer Science Lab, December 1989. to appear in
[85] Martí-Oliet, N.; Meseguer, J., From Petri nets to linear logic, (), 313-340, Lecture Notes in Computer Science
[86] Martí-Oliet, N.; Meseguer, J., Inclusions and subtypes, (December 1990), SRI International, Computer Science Lab, submitted
[87] Meseguer, J., Varieties of chain-complete algebras, J. pure appl. algebra, 19, 347-383, (1980) · Zbl 0445.18008
[88] Meseguer, J., A Birkhoff-like theorem for algebraic classes of interpretations of program schemes, (), 152-168, Lecture Notes in Computer Science
[89] Meseguer, J., The category of commutations of σ-term rewriting systems, (December 1987), SRI International, Unpublished manuscript
[90] Meseguer, J., On order-complete universal algebra and enriched functorial semantics, (), 294-301, Lecture Notes in Computer Science · Zbl 0368.18006
[91] Meseguer, J., General logics, (), 275-329
[92] Meseguer, J., A logical theory of concurrent objects, (), 101-115
[93] Meseguer, J., Rewriting as a unified model of concurrency, (), 384-400, Lecture Notes in Computer Science
[94] Meseguer, J., Rewriting as a unified model of concurrency, (February 1990), SRI International, Computer Science Laboratory, revised June 1990
[95] Meseguer, J.; Goguen, J., Initiality, induction and computability, (), 459-541 · Zbl 0571.68004
[96] Meseguer, J.; Montanari, U., Petri nets are monoids: A new algebraic foundation for net theory, (), 155-164
[97] Meseguer, J.; Montanari, U., Petri nets are monoids, Inform. and comput., SRI tech report SRI-CSL-88-3, 88, 105-155, (January 1988), appeared as
[98] Meseguer, J.; Winkler, T., Parallel programming in maude, (), in press; see also SRI Report SRI-CSL-91-08
[99] Milner, R., Communication and concurrency, (1989), Prentice-Hall Englewood Cliffs, NJ · Zbl 0683.68008
[100] Milner, R., Functions as processes, () · Zbl 0766.68036
[101] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes I and II, ()
[102] Mosses, P., Unified algebras and institutions, (1989), Computer Science Department, Aarhus University, Technical Report DAIMI PB-274 · Zbl 0716.68066
[103] Nivat, M., On the interpretation of recursive program schemes, Sympos. math., XV, 225-281, (1975)
[104] O’Donnell, M.J., Computing in systems described by equations, Vol. 58, (1977), Springer Berlin, Lecture Notes in Computer Science · Zbl 0421.68038
[105] O’Donnell, M.J., Equational logic as a programming language, (1985), MIT Press Cambridge, MA · Zbl 0636.68004
[106] O’Donnell, M.J., Survey of the equational logic programming project, ()
[107] Pitts, A., An elementary calculus of approximations, (December 1987), University of Sussex, Unpublished manuscript
[108] Plotkin, G.D., A structural approach to operational semantics, (1981), Computer Science Dept., Aarhus University, Technical Report DAIMI FN-19
[109] Plump, D., Implementing term rewriting by graph reduction: termination of combined systems, (), Lecture Notes in Computer Science, to appear
[110] Porat, S.; Francez, N., Fairness in term rewriting systems, (May 3, 1990), Manuscript, Technion
[111] Power, A.J., An abstract formulation of rewrite systems, (), 300-312, Lecture Notes in Computer Science
[112] Pratt, V., Modeling concurrency with geometry, (), 311-322
[113] Raoult, J.-C., On graph rewritings, Theoret. comput. sci., 32, 1-24, (1984) · Zbl 0551.68065
[114] Raoult, J.-C.; Vuillemin, J., Operational and semantic equivalence between recursive programs, J. ACM, 27, 772-796, (1980) · Zbl 0447.68004
[115] Reichel, H., Initial computability, algebraic specifications, and partial algebras, (1987), Oxford University Press Oxford · Zbl 0634.68001
[116] Rydeheard, D.E.; Stell, J.G., Foundations of equational deduction; A categorical treatment of equational proofs and unification algorithms, (), 114-139, Lecture Notes in Computer Science · Zbl 0664.03041
[117] Seely, R., Modelling computations: a 2-categorical framework, (), 65-71
[118] Seely, R.A.G., Linear logic, *-autonomous categories and cofree coalgebras, (), 371-382 · Zbl 0674.03007
[119] Sernadas, A.; Fiadeiro, J.; Sernadas, C.; Ehrich, H.-D., Abstract object types: A temporal perspective, (), 324-350, Lecture Notes in Computer Science
[120] Shapiro, E., The family of concurrent logic programming languages, ACM computing surveys, 21, 413-510, (1989)
[121] Stark, E.W., Concurrent transition systems, Theoret. comput. sci., 64, 221-269, (1989) · Zbl 0671.68027
[122] Tison, S., Fair termination is decidable for ground systems, (), 462-476, Lecture Notes in Computer Science
[123] Toyama, Y.; Klop, J.W.; Barendregt, H.P., Termination for the direct sum of term rewriting systems, (), 477-491, Lecture Notes in Computer Science · Zbl 0885.68093
[124] Watson, I.; Woods, V.; Watson, P.; Banach, R.; Greenberg, M.; Sargeant, J., Flagship: A parallel architecture for declarative programming, Proc. 15th ann. internat. symp. on computer architecture, 124-130, (1988)
[125] ()
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.