Conditional rules

Conditional rewrite rules can have very general conditions involving equations, memberships, and other rewrites; that is, in their mathematical notation they can be of the form

$$l: t \rightarrow t' \;\; {\it if} \;\; (\bigwedge_{i} u_{i}=v... ...{j} w_{j}:s_{j}) \wedge (\bigwedge_{k} p_{k}\rightarrow q_{k})$$

with no restriction on which new variables may appear in the righthand side or the condition. There is no need for the condition listing first equations, then memberships, and then rewrites: this is just a notational abbreviation, since they can be listed in any order. However, in Maude, conditions are evaluated from left to right, and therefore the order in which they appear, although mathematically inessential, is very important operationally (see Section 5.3).

In their Maude representation, conditional rules are declared with syntax

  crl [$\langle$Label$\rangle$] : $\langle$Term-1$\rangle$ => $\langle$Term-2$\rangle$
    if $\langle$Condition-1$\rangle$ /\ ... /\ $\langle$Condition-k$\rangle$
    [$\langle$StatementAttributes$\rangle$] .

where the rule's label can instead be declared as a statement attribute, or can be omitted altogether. In either of these two alternatives, the square brackets enclosing the label and the colon are then omitted.

As in conditional equations, the condition can consist of a single statement or can be a conjunction formed with the associative connective /\. But now conditions are more general, since in addition to equations and memberships they can also contain rewrite expressions, for which the concrete syntax t => t' is used. Furthermore, equations, memberships, and rewrites can be intermixed in any order. As for functional modules, some of the equations in conditions can be either matching equations or abbreviated Boolean equations.

We can illustrate the usefulness of rewrite expressions in rule conditions by presenting a small fragment of a Maude operational semantics for Milner's CCS language given in [71]:

  sorts Label Act Process ActProcess .
  subsorts Qid < Label < Act .
  subsort Process < ActProcess .

  op ~_ : Label -> Label .
  op tau : -> Act .
  op {_}_ : Act ActProcess -> ActProcess [frozen] .
  op _|_ : Process Process ->  Process [frozen assoc comm] .

  vars P P' Q Q' : Process .
  var  L : Label .

  crl [par] : P | Q => {tau} (P' | Q')
    if P => {L} P' /\ Q => {~ L} Q' .

The conditional rule par expresses the synchronized transition of two processes composed in parallel. The condition of the rule states that the synchronized transition can take place if one process can perform an action named L and the other can perform the complementary action named ~ L. In this representation of CCS, the action performed is remembered by the resulting expression, which is a term of sort ActProcess.

Note the use of the frozen attribute in some of the operators (see Section 4.4.9).