Conditional equations and memberships

Equational conditions in conditional equations and memberships are made up of individual equations $t=t'$ and memberships $t:s$. A condition can be either a single equation, a single membership, or a conjunction of equations and memberships using the binary conjunction connective /\ which is assumed to be associative. Thus the general form of conditional equations and memberships is the following:

  ceq $\langle$Term-1$\rangle$ = $\langle$Term-2$\rangle$
    if $\langle$EqCondition-1$\rangle$ /\ ... /\ $\langle$EqCondition-k$\rangle$
    [$\langle$StatementAttributes$\rangle$] .

  cmb $\langle$Term$\rangle$ : $\langle$Sort$\rangle$
    if $\langle$EqCondition-1$\rangle$ /\ ... /\ $\langle$EqCondition-k$\rangle$
    [$\langle$StatementAttributes$\rangle$] .

Furthermore, the concrete syntax of equations in conditions has three variants, namely:

• ordinary equations t = t',
• matching equations t := t', and
• abbreviated Boolean equations of the form t, with t a term in the kind [Bool], abbreviating the equation t = true.

Any term t in the kind [Bool] can be used as an abbreviated Boolean^4.1 equation. . The Boolean terms appearing most often in abbreviated Boolean equations are terms using the built-in equality _==_ and inequality _=/=_ predicates, and the built-in membership predicates _:: S with S a sort, including Boolean combinations of such terms with not_, _and_, _or_ and other Boolean connectives (see Section 7.1 for a detailed description of all these operators). For example, the following Boolean terms in the NUMBERS module (assuming that a ``greater than'' operator _>_ has also been defined in NUMBERS),

  N == zero
  M =/= s zero
  not (K :: NzNat)
  (N > zero or M =/= s zero)

can appear as abbreviated Boolean equations in a condition, abbreviating, respectively, the equations:

  (N == zero) = true
  (M =/= s zero) = true
  not (K :: NzNat) = true
  (N > zero or M =/= s zero) = true

To illustrate the use of conditional equations and memberships, let us reconsider the path example from Section 3.5. The following conditional statements express the key membership defining path concatenation and the associativity of this operator:

  var  E : Edge .
  vars P Q R S : Path .
  cmb E ; P : Path if target(E) = source(P) .
  ceq (P ; Q) ; R = P ; (Q ; R)
    if target(P) = source(Q) /\ target(Q) = source(R) .

The conditional membership axiom (introduced by the keyword cmb) states that an edge concatenated with a path is also a path when the target node of the edge coincides with the source node of the path. This has the effect of defining path concatenation as a partial operation on paths, although it is total on the kind [Path] of ``confused paths.''

Assuming variables P, E, and S declared as above, source and target operations over paths are defined by means of conditional equations with matching equations in conditions as follows:^4.2

  ceq source(P) = source(E) if E ; S := P .
  ceq target(P) = target(S) if E ; S := P .

Matching equations^4.3are mathematically interpreted as ordinary equations; however, operationally they are treated in a special way and they must satisfy special requirements. Note that the variables E and S in the above matching equations do not appear in the lefthand sides of the corresponding conditional equations. In the execution of these equations, these new variables become instantiated by matching the term E ; S against the canonical form of the subject term bound to the variable P (see Section 4.7). In order for this match to decide the equality with the ground term bound to P, the term E ; S must be a pattern. Given a functional module $M$, we call a term $t$ an $M$-pattern if for any well-formed substitution $\sigma$ such that for each variable $x$ in its domain the term $\sigma(x)$ is in canonical form with respect to the equations in $M$, then $\sigma(t)$ is also in canonical form. A sufficient condition for $t$ to be an $M$-pattern is the absence of unifiers between its nonvariable subterms and lefthand sides of equations in $M$.

Ordinary equations $t=t'$ in conditions have the usual operational interpretation, that is, for the given substitution $\sigma$, $\sigma(t)$ and $\sigma(t')$ are both reduced to canonical form and are compared for equality, modulo the equational attributes specified in the module's operator declarations such as associativity, commutativity, and identity. Finally, abbreviated Boolean equations are just a special case of ordinary equations once they are expanded out.

The satisfaction of the conditions is attempted sequentially from left to right. Since in Maude matching takes place modulo equational attributes, in general many different matches may have to be tried until a match of all the variables satisfying the condition is found.

The above equations for source and target illustrate the use of matching equations to bind variables locally, in much the same way that let is used in some functional programming languages. In this example, since the matching is purely syntactic, the matching substitution is unique and gives a simple way to name parts of a structure or to name a complicated expression which appears multiple times in the main equation.

For $M$-patterns where some operators are matched modulo some equational attributes, matching substitutions need not be unique. This provides another way of using matching equations, namely to perform a search through a structure without any need to explicitly define a function that does this. For example, for sequences of natural numbers we can define a predicate _occurs-inner_ that determines if a number occurs in a sequence other than at one of the ends. If one only cares about positive results,^4.4 the following will work.

  op _occurs-inner_ : [Nat] [NatSeq] -> [Bool] .
  ceq N:Nat occurs-inner NS:NatSeq = true
    if (NS0:NatSeq N:Nat NS1:NatSeq) := NS:NatSeq .

Note that this equation could also be written as

  eq N:Nat occurs-inner NS0:NatSeq N:Nat NS1:NatSeq = true .

In both cases we check whether the sequence contains the natural number N:Nat, but making sure that the sequence contains other elements both before and after N:Nat.^4.5 With the above definition added to the numbers module, the term

  zero occurs-inner (zero zero zero zero zero)

reduces to true, while the term

  zero occurs-inner (zero zero)

does not reduce further.

Matching equations in conditions give great expressive power, but some care is needed in using them to define operations. Consider adding the following to the numbers module, in an attempt to define a test for the presence of s s zero in a sequence of natural numbers.

  op hasTwo : [NatSeq] -> [Bool] .
  ceq hasTwo(NS:NatSeq) = N:Nat == s s zero
    if NS0:NatSeq N:Nat NS1:NatSeq := NS:NatSeq .

With this addition to the numbers module, hasTwo(zero zero) does not get reduced, since the condition requires at least three numbers in the sequence. The term hasTwo(zero (s s zero) zero) reduces to true. The term hasTwo(zero (s zero) (s s zero) zero) also gets reduced, although it may return true or false; probably not what was intended. The problem is that there are several matches, each giving a different answer, so the conditional equation does not define a function. In fact, this conditional equation causes the Church-Rosser property to fail, and semantically identifies true and false, thus leading to an inconsistent theory. In contrast, as will be seen in Chapter 5, a rule with such a matching condition is not a problem, and does have the effect of searching a sequence of natural numbers for s s zero.

In summary, all the sort, subsort, and operator declarations and all the statements in a functional module (plus the functional modules imported if any) define an equational theory in membership equational logic [60,7]. Such a theory can be described in mathematical notation as a pair $(\Sigma,E\cup A)$, where $\Sigma$ is the signature, that is, the specification of the sorts, subsorts, kinds, and operators in the module, $E$ is the collection of statements (equations and memberships, possibly conditional) and $A$ is the set of equational attributes, such as assoc and comm, declared for some operators (that is, extra equations that are treated in a special way by the Maude interpreter to simplify modulo such attributes, see Section 4.4.1).

The family of ground terms definable in the syntax of $\Sigma$ defines a model called a $\Sigma$-algebra and denoted $T_{\Sigma}$. In $T_{\Sigma}$, terms syntactically different denote different elements, so that $T_{\Sigma}$ will not satisfy the equations in $E\cup A$, unless they are trivial equations such as $f(X) = f(X)$. The question is, what is the optimal model of the theory $(\Sigma,E\cup A)$? Goguen and Burstall's answer is: a model satisfying the axioms $E\cup A$ and such that it has no junk (that is, all elements can be denoted by ground $\Sigma$-terms), and no confusion (that is, only elements that are forced to be equal by the axioms $E\cup A$ are identified). Such a model, called the initial algebra of the equational theory $(\Sigma,E\cup A)$, exists [60], is denoted $T_{\Sigma/E \cup A}$, and provides the mathematical semantics of the Maude functional module specifying $(\Sigma,E\cup A)$.

Mathematically, $T_{\Sigma/E \cup A}$ can be constructed as the quotient of $T_{\Sigma}$ in which the equivalence classes are those terms that are provably equal using the axioms $E\cup A$. Operationally, assuming that the axioms $E$ are Church-Rosser and terminating modulo $A$ (see Section 4.7), there is a much more intuitive equivalent description of $T_{\Sigma/E \cup A}$, namely as the family of canonical forms for the ground $\Sigma$-terms modulo $A$, that is, those terms that cannot be further simplified by the equations in $E$ modulo $A$. That is, as explained in Section 1.2, we have then an isomorphism

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

between the initial algebra $T_{\Sigma/E \cup A}$ and the canonical term algebra $\mathit{Can}_{\Sigma/E\cup A}$.

The Maude interpreter computes such canonical forms, which can be viewed as the values denoted by the corresponding functional expressions, with the reduce command (see Section 16.2 for details and Section 4.9 for examples).