Otherwise

Sometimes, in the definition of an operation by equations, there are certain cases that can be easily defined by equations, and then some remaining case or cases that it is more difficult or cumbersome to define. One would in such situations like to say, otherwise, that is, in all remaining cases not covered by the above equations, do so and so.^4.10

Consider, for example, the problem of membership of a natural number in a finite set of numbers.

  op _in_ : Nat NatSet -> Bool .

The easy part is to define when a number belongs to a set:

  var N : Nat .
  var NS : NatSet .
  eq N in N ; NS = true .

It is somewhat more involved to define when it does not belong. A simple way is to use the otherwise (abbreviated owise) attribute and give the additional equation:

  eq N in NS = false [owise] .

The intuitive operational meaning is clear: if the first equation does not match, then the number in fact is not in the set, and the predicate should be false. But what is the mathematical meaning? That is, how can we interpret the meaning of the second equation so that it becomes a useful shorthand for an ordinary equation? After all, the second equation, as given, is even more general than the first and in direct contradiction with it. We of course should reject any constructs that violate the logical semantics of the language.

Fortunately, there is nothing to worry about, since the owise attribute is indeed a shorthand for a corresponding conditional equation. We first explain the idea in the context of this example and then discuss the general construction. The idea is that, whether an equation, or a set of equations, defining the meaning of an operation $f$ match a given term, is itself a property defined by a predicate, say $enabled_{f}$, which is effectively definable by equations. In our example we can introduce a predicate enabled-in, telling us when the first equation applies, by just giving its lefthand side arguments as the predicate's arguments:

  op enabled-in : [Nat] [NatSet] -> [Bool] .
  eq enabled-in(N, N ; NS) = true .

Note that we do not have to define when the enabled-in predicate is false. That is, this predicate is really defined on the kind [Bool]. Our second owise equation is simply a convenient shorthand for the conditional equation

  ceq N in NS = false if enabled-in(N, NS) =/= true .

This is just a special case of a completely general theory transformation that translates a specification containing equations with the owise attribute into a semantically equivalent specification with no such attributes at all. A somewhat subtle aspect of this transformation^4.11 is the interaction between owise equations and the operator evaluation strategies discussed in Section 4.4.7. Suppose that an owise equation was used in defining the semantics of an operator $f$. If $f$ was (implicitly or explicitly) declared with a strategy, say,

$$f: s_{1}\ldots s_{n}\rightarrow s \;\;\; [\texttt{strat} \;\; (i_1 \ldots i_k 0)] \; .$$

then, the $enabled_{f}$ predicate should be defined with the same strategy,

$$enabled_{f}: [s_{1}] \ldots [s_{n}] \rightarrow \texttt{[Bool]} \;\;\; [\texttt{strat} \;\; (i_1 \ldots i_k 0)]\; .$$

This will make sure that the reduction of $f$'s arguments prior to applying equations for $f$--including the equations that will be introduced in our transformation to replace the owise equations--takes place in exactly the same way for $f$ and for $enabled_{f}$, so that failure of matching the normal equations is correctly captured by the failure of the $enabled_{f}$ predicate. Furthermore, as we shall see, after the failure of matching the non-owise equations, the matching substitution obtained when we apply the desugared version of an owise equation will then properly take into account the evaluation of those arguments of $f$ specified by $f$'s evaluation strategy.

In general, if we are defining the equational semantics of an operation $f: s_{1} \ldots s_{n} \rightarrow s$ and we have given a partial definition of that operation by (possibly conditional) equations

$$\begin{eqnarray*} f(u^{1}_{1},\ldots,u^{1}_{n}) & = & t_{1} \;\; \textit{if} \;\... ...m}_{1},\ldots,u^{m}_{n}) & = & t_{m} \;\; \textit{if} \;\; C_{m} \end{eqnarray*}$$

then we can give one or more owise equations defining the function in the remaining cases by means of equations of the form

$$\begin{eqnarray*} f(v^{1}_{1},\ldots,v^{1}_{n}) & = & t'_{1} \;\; \textit{if} \;... ...'_{k} \;\; \textit{if} \;\; C'_{k} \;\; \mbox{\texttt{[owise]}} \end{eqnarray*}$$

We can view such owise equations as shorthand notation for corresponding ordinary conditional equations of the form

$$\begin{eqnarray*} f(y_{1},\ldots,y_{n}) = t'_{1} & \textit{if} & enabled_{f}(y_... ...}_{n}) := enabled_{f}(y_{1},\ldots,y_{n}) \\ & \wedge & C'_{k} \end{eqnarray*}$$

where the variables $y_{1},\ldots,y_{n}$ are fresh new variables not appearing in any of the above owise equations, and with $y_{i}$ of kind $[s_{i}]$, $1 \leq i \leq n$. All this assumes that in the transformed specification we have declared the predicate $enabled_{f}: [s_{1}] \ldots [s_{n}] \rightarrow \texttt{[Bool]}$, with the same evaluation strategy as $f$. Note the somewhat subtle use of the matching equations (see Section 4.3) $enabled_{f}(v^{j}_{1},\ldots,v^{j}_{n}) := enabled_{f}(y_{1},\ldots,y_{n})$, $1 \leq j \leq k$, in the conditions. Since $f$ and $enabled_{f}$ have the same strategy, after the arguments of the matching instance of the expression $enabled_{f}(y_{1},\ldots,y_{n})$ become evaluated according to the strategy, we are then able to match $enabled_{f}(v^{j}_{1},\ldots,v^{j}_{n})$ to that result, obtaining the desired substitution for the variables of the lefthand side of the $j^{th}$ owise equation. That is, we obtain the same substitution as the one we would have obtained matching $f(v^{j}_{1},\ldots,v^{j}_{n})$ to the same subject term after its subterms under $f$ had been evaluated according to $f$'s strategy.

Of course, the semantics of the $enabled_{f}$ predicate is defined in the expected way by the equations

$$\begin{eqnarray*} enabled_{f}(u^{1}_{1},\ldots,u^{1}_{n}) & = & \texttt{true} \;... ...^{m}_{n}) & = & \texttt{true} \;\; \textit{if} \;\; C_{m} \;\; . \end{eqnarray*}$$

The possibility of using multiple owise equations allows us to simplify definitions of functions defined by cases on data with nested structure. Here is a simple, if silly, example in which the sort R has elements a(n) and b(n), for natural numbers n, and the sort S has elements g(r) and h(r), with r of sort R. The operation f treats constructors g and h differently, distinguishing only whether the subterm of sort R is constructed by a or not. Again, the predefined module NAT of natural numbers (Section 7.2) is imported by means of a protecting declaration (Section 6.1.1).

  fmod OWISE-TEST1 is
    protecting NAT .

    sorts R S .
    op f : S Nat -> Nat .
    ops g h : R -> S .
    ops a b : Nat -> R .

    var  r : R .
    vars m n : Nat .
    eq f(g(a(m)), n) = n .
    eq f(h(a(m)), n) = n + 1 .
    eq f(g(r), n) = 0 [owise] .
    eq f(h(r), n) = 1 [owise] .
  endfm

The four cases are illustrated by the following reductions.

  Maude> red f(g(a(0)), 3) .
  result NzNat: 3

  Maude> red f(g(b(0)), 3) .
  result Zero: 0

  Maude> red f(h(b(0)), 3) .
  result NzNat: 1

  Maude> red f(h(a(0)), 3) .
  result NzNat: 4

The subtle interaction between owise equations and operator evaluation strategies can be illustrated by the following example:

  fmod OWISE-TEST2 is
    sort Foo .
    ops a b c d : -> Foo .
    op f : Foo -> Foo [strat (0 1 0)] .
    op g : Foo -> Foo [strat (0)] .

    var X : Foo .
    eq b = c .
    eq f(a) = d .
    eq f(X) = g(X) [owise] .
  endfm

Now consider the term f(b). Intuitively, one could expect that, given that the first equation for f cannot be applied to this term, the owise equation is applied obtaining the term g(b), and this is then expected to be the final result of the reduction, because the strategy (0) for g forbids evaluating its argument. However, as we can see in the following reduction, this is not the case.

  Maude> red f(b) .
  result Foo: g(c)

The result is g(c), because the owise equation is not considered until after evaluating the final 0 in the strategy for f, and by then f(b) is simplified to f(c) as instructed by the 1 in such strategy; then, the owise equation applied to f(c) produces g(c).

It can be interesting to consider the semantically equivalent transformed specification:

  fmod OWISE-TEST2-TRANSFORMED is
    sort Foo .
    ops a b c d : -> Foo .
    op f : Foo -> Foo [strat (0 1 0)] .
    op enabled-f : Foo -> Bool [strat (0 1 0)] .
    op g : Foo -> Foo [strat (0)] .

    vars X Y : Foo .
    eq b = c .
    eq f(a) = d .
    eq enabled-f(a) = true .
    ceq f(Y) = g(X)
      if enabled-f(Y) =/= true /\ enabled-f(X) := enabled-f(Y) .
  endfm

  Maude> red f(b) .
  result Foo: g(c)

where, as pointed out in our comments on the general transformation, the fact that enabled-f has the same strategy as f and the use of the matching equation

  enabled-f(X) := enabled-f(Y)

are crucial for obtaining a semantically equivalent specification.