×

Mapping tile logic into rewriting logic. (English) Zbl 0903.08010

Parisi Presicce, Francesco (ed.), Recent trends in algebraic development techniques. 12th international workshop, WADT ’97, Tarquinia, Italy, June 3–7, 1997. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 1376, 62-91 (1998).
Summary: Rewriting logic extends to concurrent systems with state changes the body of theory developed within the algebraic semantics approach. It is both a foundational tool and the kernel language of several implementation efforts (Cafe, ELAN, Maude). Tile logic extends (unconditional) rewriting logic since it takes into account state changes with side effects and synchronization. It is especially useful for defining compositional models of computation of reactive systems, coordination languages, mobile calculi, and causal and located concurrent systems. In this paper, the two logics are defined and compared using a recently developed algebraic specification methodology, membership equational logic. Given a theory \(T\), the rewriting logic of \(T\) is the free monoidal 2-category, and the tile logic of \(T\) is the free monoidal double category, both generated by \(T\). An extended version of monoidal 2-categories, called 2VH-categories, is also defined, able to include in an appropriate sense the structure of monoidal double categories. We show that 2VH-categories correspond to an extended version of rewriting logic, which is able to embed tile logic, and which can be implemented in the basic version of rewriting logic using suitable internal strategies. These strategies can be significantly simpler when the theory is uniform. A uniform theory is provided in the paper for CCS, and it is conjectured that uniform theories exist for most process algebras.
For the entire collection see [Zbl 0889.00030].

MSC:

08A70 Applications of universal algebra in computer science
68Q65 Abstract data types; algebraic specification
18C10 Theories (e.g., algebraic theories), structure, and semantics
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q55 Semantics in the theory of computing
18D05 Double categories, \(2\)-categories, bicategories and generalizations (MSC2010)
18D10 Monoidal, symmetric monoidal and braided categories (MSC2010)

Software:

CafeOBJ; ELAN; Maude
PDFBibTeX XMLCite