Admissible system modules

The same way that equations or memberships expressed in their fullest possible generality cannot be executed by the Maude engine except in a controlled way at the metalevel, conditional rewrite rules in their fullest generality cannot be executed either, except with a strategy at the metalevel. Nonexecutable rules should be identified by giving them the nonexec attribute.

As for functional modules, the question now becomes: what are the executability requirements on the executable statements (i.e., those without the nonexec attribute) of a system module? It turns out that a quite general class of system modules, called admissible modules, are executable by Maude's default interpreter using the rewrite, frewrite, and search commands, that will be introduced and illustrated in Section 5.4 and are further explained in Sections 16.2 and 16.4.

The admissibility requirements for the module's equations and memberships are exactly as for functional modules; they were explained in Section 4.6 and are further discussed below. Two more requirements are needed:

• each executable conditional rule should be admissible, and
• the rules should be coherent relative to the equations, as has already been mentioned in the introduction.

We explain each of these requirements below.

Given a system module $M$, a conditional^5.2 rule of the form

$$l: t \rightarrow t' \;\; {\it if} \;\; C_1 \wedge \ldots \wedge C_n$$

such that it does not have the nonexec attribute is called admissible if it satisfies the exact analogues of the admissibility requirements 1-3 in Section 4.6 for conditional equations, plus the additional requirement

1. If $C_i$ is a rewrite $u_i \rightarrow u'_i$, then
   
   $$\mathit{vars}(u_i) \subseteq \mathit{vars}(t) \cup \bigcup_{j=1}^{i-1} \mathit{vars}(C_j),$$
   
   
   and furthermore $u'_i$ is an $\mathcal{E}(M)$-pattern (for the notion of pattern see Section 4.3) for $\mathcal{E}(M)$ the equational theory underlying the module $M$.

Operationally, we try to satisfy such a rewrite condition by reducing the substitution instance $\sigma(u_i)$ to its canonical form $v_i$ with respect to the equations, and then trying to find a rewrite proof $v_i \rightarrow w_i$ (perhaps after many steps of rewriting) with $w_i$ in canonical form with respect to the equations and such that $w_i$ is a substitution instance of $u'_i$. Search for such a $w_i$ is performed by the Maude engine using a breadth-first strategy.

As for functional modules, when executing an admissible conditional rule in a system module, the satisfaction of all its conditions is attempted sequentially from left to right; but notice that now, besides the fact that many matches for the equational conditions may be possible due to the presence of equational attributes, we also have to deal with the fact that solving rewrite conditions requires search, including searching for new solutions when previous ones fail to satisfy subsequent conditions.

We now explain the coherence requirement. 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 equational theory is undecidable.

The equations and memberships specified in a system module $M$ are divided into a set $A$ of axioms corresponding to equational attributes such as associativity, commutativity, idempotency, and (left-, right- or two-sided) identity declared for different operators in the module (see Section 4.4.1), for which matching algorithms exist in the Maude implementation, and a set $E$ of equations and memberships specified in the ordinary way. As already mentioned, for $M$ to be executable, the set of executable statements in $E$ must be Church-Rosser and terminating modulo $A$, or at least ground Church-Rosser and terminating modulo $A$; that is, we require that the equational part must be equivalent to an executable functional module.

Moreover, we require that the rules $R$ in the module are coherent [72] with respect to the equations $E$ modulo $A$, or at least ground coherent. Coherence means that, given a term $t$, for each one-step rewrite of it with some rule in $R$ modulo the axioms $A$ to some term $t'$, which we denote $t \longrightarrow^{1}_{R/A} t'$, if $u$ is the canonical term we obtain by rewriting $t$ with the equations and memberships in $E$ to canonical form modulo $A$, denoted $t \longrightarrow^{!}_{E/A} u$, then there is a one-step rewrite of $u$ with some rule in $R$ modulo $A$, $u \longrightarrow^{1}_{R/A} u'$, such that $t'=_{E \cup A} u'$, which by the Church-Rosser and termination properties of $E$ modulo $A$ is equivalent to $t'$ and $u'$ having the same canonical form modulo $A$ by $E$. This requirement is described graphically in Figure 5.1.

Figure 5.1: Coherence diagram

Ground coherence is a weaker requirement: we require the exact same diagram to exist only for ground terms, and $E$ only needs to be ground Church-Rosser and terminating modulo $A$.

As explained in [72] (for the free case and for coherence modulo associativity and commutativity), for unconditional rules $R$, coherence can be checked by checking ``critical pairs'' between rules $R$ and equations $E$, and showing that the corresponding instance of the coherence diagram can be filled in for all such pairs. That is, we have to look for appropriate overlaps between lefthand sides of rules and equations using an $A$-unification algorithm, generate the corresponding critical pairs, and check their coherence. In the case of ground coherence, it is not necessary that the critical pairs can be filled in: it is enough to show that each ground instance of such pairs can be filled in. See Section 7.8 of [16] for an example of a system module that is not coherent, a discussion of the critical pairs involved, and a method to make the specification coherent. See also Section 13.4 of [16] for an example of how coherence can be checked by critical pair analysis. Similarly, for ground coherence and how to check it, see the example in Section 9.4.

Why is coherence so important? What does it mean intuitively? Rewriting modulo an equational theory $E\cup A$, which is what a rewrite theory $\mathcal{R}=(\Sigma,E\cup A,\phi,R)$ really does, is in general undecidable. The undecidability has to do with the fact that we may need to search an entire $E\cup A$-equivalence class before we can know if a class representative can be rewritten with $R$, that is, if the $E\cup A$-equivalence class can be rewritten. Coherence makes the problem decidable: all we need to do is to reduce the term to its canonical form by $E$ modulo $A$, and then rewrite with $R$ such a canonical form. In a sense, coherence reduces rewriting with $R$ modulo $E\cup A$ to rewriting with $E$ and $R$ modulo $A$, which is decidable, because we assume we have an $A$-matching algorithm.

Could we miss any rewrites that way? Coherence guarantees to us that we could not, since any rewrite of a term $t$ with $R$ must also be possible with $t$'s canonical form. Maude implicitly assumes this coherence property. For example, the rewrite command will at each step first reduce the term to canonical form with $E$ modulo $A$, and then perform a rewrite step with $R$ in a rule-fair manner. The frewrite command uses a somewhat different rewrite strategy to ensure both local fairness and rule fairness, but assumes the same coherence (or ground coherence) property (see Section 16.2 and examples in Section 5.4 below).

A last point about the execution of system modules regards frozen argument positions in operators (see Section 4.4.9). This poses a general constraint on any rewriting strategy whatsoever, including those directly supported by Maude for the rewrite and frewrite commands (see Section 5.4). The general constraint is that rewriting will never happen below one of the frozen argument positions in an operator. That is, even though many rewritings may be possible and there can be a large amount of nondeterminism (so that different rewriting strategies may lead to quite different results) rewriting under frozen arguments is always forbidden. In fact, this does not only belong to the module's operational semantics, but also to the latest initial model semantics for rewrite theories developed in [8]; we give a brief informal summary of this semantics below.

Mathematically, a system module, when ``flattened'' with its imported submodules, exactly specifies a (generalized) rewrite theory in the sense of [8], that is, a four-tuple

$$\mathcal{R}=(\Sigma,E\cup A,\phi,R),$$

where $(\Sigma,E\cup A)$ is the membership equational theory specified by the signature, equational attributes, and equation and membership statements in the module (just as in the case of functional modules); $\phi$ is a function, assigning to each operator in $\Sigma$ the set of natural numbers corresponding to its frozen arguments (the empty set when no argument is frozen); and $R$ is the collection of (possibly conditional) rewrite rules specified in the module and its submodules.

Intuitively, such a rewrite theory specifies a concurrent system. The equational theory $(\Sigma,E\cup A)$ specifies the ``statics'' of the system, that is, the algebraic structure of the set<sup>5.3</sup> of states, which is specified by the initial algebra $T_{\Sigma/E \cup A}$. The rules $R$ and the freezing information $\phi$ specify the concurrent system's ``dynamics,'' that is, the possible concurrent transitions that the system can perform. In rewriting logic, such, possibly complex, concurrent transitions exactly correspond to rewrite proofs; but since several rewrite proofs can indeed correspond to the same concurrent computation (describing, for example, different semantically equivalent interleavings), rewriting logic has an equational theory of proof equivalence [57,8].

The initial model $\mathcal{T}_{\mathcal{R}}$ of the rewrite theory $\mathcal{R}$ associates to each kind $k$ a labeled transition system (in fact, a category) whose set of states is $T_{\Sigma/E\cup A,k}$, and whose labeled transitions have the form $[\alpha]: [t] \rightarrow [t']$, with $[t],[t'] \in T_{\Sigma/E\cup A,k}$, and with $[\alpha]$ an equivalence class of rewrite proofs modulo the equational theory of proof equivalence. Indeed what the different $[\alpha]$ represent are the different ``truly concurrent'' computations of the system specified by $\mathcal{R}$.