Unconditional equations

Unconditional equations are declared using the keyword eq, followed by a term (its lefthand side), the equality sign =, then a term (its righthand side), optionally followed by a list of statement attributes (see Section 4.5 later in this chapter) enclosed in square brackets, and ending with white space and a period. Thus the general scheme is the following:

  eq $\langle$Term-1$\rangle$ = $\langle$Term-2$\rangle$ [$\langle$StatementAttributes$\rangle$] .

The terms t and t' in an equation t = t' must both have the same kind. In order for the equation to be executable, any variable appearing in t' must also appear in t. Equations not satisfying this requirement can also be declared (for example, to document a lemma holding true in the module) but in such a case they should always be specified with the nonexec attribute (see Section 4.5.3). We can add equations axiomatizing the addition operation in our NUMBERS module as follows, where we distinguish two cases for the second argument, according to whether it is zero or not:

  vars N M : Nat .
  eq N + zero = N .
  eq N + s M = s (N + M) .

The following equations define the symmetric difference operation sd on natural numbers, which returns the result of subtracting the smaller from the larger of its two arguments.

  eq sd(N, N) = zero .
  eq sd(N, zero) = N .
  eq sd(zero, N) = N .
  eq sd(s N, s M) = sd(N, M) .

In general, in a functional module one can specify equations (and also conditional equations, as explained in Section 4.3) in three different ways:

1. in the style given above, in which case they are assumed to be executable as simplification rules from left to right;
2. in the same style as above, but with the nonexec attribute (see Section 4.5.3), in which case Maude does not use them for simplification (except at the metalevel with a user-given strategy, see Section 11.5); and
3. as equational attributes of specific operators (see Section 4.4.1).

For example, a binary operator f can be declared assoc and comm, telling Maude that it satisfies the associativity and commutativity axioms. Such equational attributes should not be written explicitly as equations in the specification. There are two reasons for this. Firstly, this is redundant, since they have already been declared as equational attributes. Secondly, although declaring such equations either only explicitly as equations, or twice--one time as equational attributes and another as explicit equations--does not affect the mathematical semantics of the specification, that is, the initial algebra that the specification denotes (see Section 4.3), it does however drastically alter the specification's operational semantics. For example, if the comm attribute for f were to be stated as an equation f(X, Y) = f(Y, X), then using the equation as a simplification rule applied to the term, say, f(a, b), would lead to the nonterminating chain of equational simplifications

  f(a, b) = f(b, a) = f(a, b) = f(b, a) = ...

This is quite bad, since we want the equations specified by method (1) to be used as simplification rules and assume them to be terminating and Church-Rosser, so that they always simplify a term to a unique result that cannot be further simplified. Instead, if comm is declared as an equational attribute, the above kind of looping does not happen: Maude then simplifies terms modulo the declared equational attributes, so that the terms f(a, b) and f(b, a) would indeed be treated as identical. For more on equational attributes see Section 4.4.1.