4.3 Semantics of Object-Oriented and System Modules

As already pointed out, the logic of Maude is the membership logic variant of rewriting logic MRWLogic. A system module is then a rewrite theory R in such a logic. In the unparameterized case its semantics is the initial model T_R, that was constructed for the unsorted case in Section 4.2.2. That is, the initial model T_R is the algebra of all rewriting computations for ground terms in the theory. From a systems perspective this model describes all the concurrent behaviors that the system so axiomatized can exhibit. From that perspective, a term t denotes a state of the system, and a proof term alpha: t --> t' denotes a possibly concurrent computation.

A system module can contain one or more parameter theories. The inclusion from the parameter(s) into the module then gives rise to a free extension functor [36], which provides the semantics for the module. This of course means that we can compose systems by putting together the rewrite theories in which they are specified, as done in Full Maude.

A rewrite theory has both rules and equations, so that rewriting is performed modulo such equations. However, this does not mean that the Maude implementation must have a matching algorithm for each equational theory that a user might specify, which is impossible, since matching modulo an arbitrary theory is undecidable. What we instead require for theories in system modules is that:

• The equations are divided into a set A of axioms, for which matching algorithms exist in the Maude implementation,⁴⁶ and a set E of equations that are Church-Rosser, terminating and sort decreasing modulo A; that is, the equational part must be equivalent to a functional module.
• The rules R in the module are coherent [61] (or at least what might be called "weakly coherent" [38, Section 5.2.1][60]) with the equations E modulo A. This means that appropriate critical pairs exist between rules and equations, allowing us to intermix rewriting with rules and rewriting with equations without loosing rewrite computations by failing to perform a rewrite that would have been possible before an equational deduction step was taken. In this way, we get the effect of rewriting modulo E U A with just a matching algorithm for A. In particular, a simple strategy available in these circumstances is to always reduce to canonical form using E before applying any rule in R. This is precisely the strategy adopted by the Maude interpreter.

The semantics of object-oriented modules is entirely reducible to that of system modules, in the sense that--as explained in Section 3.2.2 and in [38]--there is a systematic desugaring process translating each object-oriented module into its corresponding system module [38]. The particular ontology supported by object-oriented modules is something very much worth keeping, and it does not exist for general system modules. For example, in an object-oriented configuration we have objects that maintain their identity across their state changes, and the notions of fairness adequate for them are more specialized than those appropriate for arbitrary system modules. The approach taken in Maude is to provide a logical semantics for concurrent object-oriented programming by taking rewriting logic as its foundation, and then defining in a rigorous way higher-level object-oriented concepts above such a foundation. The papers [38, 39] provide good background on such foundations. Talcott's paper [58] gives rewriting logic foundations for actors from a somewhat different viewpoint. The paper [45] shows how, for object-oriented modules satisfying some simple requirements, their initial model semantics coincides with a very natural partial order of events truly concurrent semantics.

The basic ideas about the reflective semantics of Maude have already been discussed in Section 2.5. Much more detail can be found in [15, 10].