The logical foundations of Maude

The foundations of a house do not have to be inspected every day: one is grateful that they are there and are sound. This section describes the logical foundations of Maude in an informal, impressionistic style, not assuming much beyond a cocktail party acquaintance with logic and mathematics. The contents of this section may be read in two ways, and at two different moments:

• before reading the rest of the manual, to obtain a bird's-eye view of the mathematical ideas underlying Maude's design and semantics; or
• after reading the rest of the manual, to gain a more unified understanding of the language's design philosophy and its foundations.

Readers with a more pragmatic interest may safely skip this section, but they may miss some of the fun.

Maude is a declarative language in the strict sense of the word. That is, a Maude program is a logical theory, and a Maude computation is logical deduction using the axioms specified in the theory/program. But which logic? There are two, one contained in the other. The seamless integration of the functional world within the broader context of concurrent, nondeterministic computation is achieved at the language level by the inclusion of functional modules as a special case of system modules. At the mathematical level this inclusion is precisely the sublogic inclusion in which membership equational logic [60,7] is embedded in rewriting logic [57,8].

A functional module specifies a theory in membership equational logic. Mathematically, we can view such a theory as a pair $(\Sigma,E\cup A)$. $\Sigma$, called the signature, specifies the type structure: sorts, subsorts, kinds, and overloaded operators. $E$ is the collection of (possibly conditional) equations and memberships declared in the functional module, and $A$ is the collection of equational attributes (assoc, comm, and so on) declared for the different operators. Computation is of course the efficient form of equational deduction in which equations are used from left to right as simplification rules.

Similarly, a system module specifies a rewrite theory, that is, a theory in rewriting logic. Mathematically, such a rewrite theory is a 4-tuple $\mathcal{R}=(\Sigma,E\cup A,\phi,R)$, where $(\Sigma,E\cup A)$ is the module's equational theory part, $\phi$ is the function specifying the frozen arguments of each operator in $\Sigma$, and $R$ is a collection of (possibly conditional) rewrite rules. Computation is rewriting logic deduction, in which equational simplification with the axioms $E\cup A$ is intermixed with rewriting computation with the rules $R$.

We can of course view an equational theory $(\Sigma,E\cup A)$ as a degenerate rewrite theory of the form $(\Sigma,E\cup A,\phi_{\emptyset},\emptyset)$, where $\phi_{\emptyset}(f) = \emptyset$, that is, no argument of $f$ is frozen, for each operator $f$ in the signature $\Sigma$. This defines a sublogic inclusion from membership equational logic (MEqLogic) into rewriting logic (RWLogic) which we can denote

$$\mbox{MEqLogic} \hookrightarrow \mbox{RWLogic}.$$

In Maude this corresponds to the inclusion of functional modules into the broader class of system modules. However, Maude's inclusion is more general: the user can give the desired freezing information for each operator in the signature of a functional module, not just the $\phi_{\emptyset}$ above.

Another important fact is that each Maude module specifies not just a theory, but also an intended mathematical model. This is the model the user has intuitively in mind when writing the module. For functional modules such models consist of certain sets of data and certain functions defined on such data, and are called algebras. For example, the intended model for a NAT module is the natural numbers with the standard arithmetic operations. Similarly, a module LIST-QID may specify a data type of lists of quoted identifiers, and may import NAT and BOOL as submodules to specify functions such as length and _in_. Mathematically, the intended model of a functional module specifying an equational theory $(\Sigma,E\cup A)$, with $\Sigma$ the signature defining the sorts, subsorts, and operators, $E$ the equations and memberships, and $A$ the equational attributes like assoc, comm, and so on, is called the initial algebra of such a theory and is denoted $T_{\Sigma/E \cup A}$.

In a similar way, a system module specifying a rewrite theory $\mathcal{R}=(\Sigma,E\cup A,\phi,R)$ has an initial model, denoted $\mathcal{T}_{\mathcal{R}}$, which in essence is an algebraic (labeled) transition system.^1.7 The states and data of this system are elements of the underlying initial algebra $T_{\Sigma/E \cup A}$. The state transitions are the (possibly complex) concurrent rewrites possible in the system by application of the rules $R$. For our bank accounts example, these transitions correspond to all the possible concurrent computations that can transform a given ``soup'' of account objects and messages into another soup. Again, this is the model the programmer of such a system has in mind.

How do the mathematical models associated with Maude modules and the computations performed by them fit together? Very well, thanks. This is the so-called agreement between the mathematical semantics (the models) and the operational semantics (the computations). In this introduction we must necessarily be brief; see Sections 4.6 and 4.7 and [7] for the whole story in the case of functional modules, and Section 5.3 and [72] for the case of system modules. Here is the key idea: under certain executability conditions required of Maude modules, both semantics coincide. For functional modules we have already mentioned that the equations should have good properties as simplification rules, so that they evaluate each expression to a single final result. Technically, these are called the Church-Rosser and termination assumptions. Under these assumptions, the final values, called the canonical forms, of all expressions form an algebra called the canonical term algebra. By definition, the results of operations in this algebra are exactly those given by the Maude interpreter: this is as computational a model as one can possibly get. For example, the results in the canonical term algebra of the operations

  length('a . 'b . 'c . nil)
  'b in ('a . 'b . 'c . nil)

are, respectively,

  s s s 0
  true

Suppose that a functional module specifies an equational theory $(\Sigma,E\cup A)$ and satisfies the Church-Rosser and termination assumptions. Let us then denote by $\mathit{Can}_{\Sigma/E\cup A}$ the associated canonical term algebra. The coincidence of the mathematical and operational semantics is then expressed by the fact that we have an isomorphism

$$T_{\Sigma/E \cup A}\cong \mathit{Can}_{\Sigma/E\cup A}.$$

In other words, except for a change of representation, both algebras are identical.

For system modules, the executability conditions center around the notion of coherence between rules and equations (see [72] and Section 5.3). The equational part $E\cup A$ should be Church-Rosser and terminating as before. A reasonable strategy (the one adopted in Maude by the rewrite command, see Chapter 5) is to first apply the equations to reach a canonical form, and then do a rewriting step with a rule in $R$. But is this strategy complete? Couldn't we miss rewrites with $R$ that could have been performed if we had not insisted on first simplifying the term to its canonical form with the equations? Coherence guarantees that this kind of incompleteness cannot happen (see Section 5.3).