Collapse theories

Using id: or idem attributes means that you are (conceptually) working with infinite equivalence classes, and that many lefthand side patterns will match in unexpected ways. Unlike OBJ3, Maude has true collapse matching algorithms, rather than identity completion, and it does not try to omit problematic matches. Consider for example the module

  fmod COLLAPSE-ID-EX is
    sort Foo .
    ops a e : -> Foo .
    op f : Foo Foo -> Foo [left id: e] .
    var X : Foo .
    eq f(X, a) = ...
  endfm

Then we have

  a = f(e, a) = f(e, f(e, a)) =  ...

In particular, the pattern f(X, a) matches a with $\texttt{X }\leftarrow\texttt{ e}$, leading to possible nontermination. You should be wary of having an operator with an identity element as the top symbol for a lefthand side. One useful trick when you need a pattern like f(X, a) is to use a pattern f(Y, a) where Y has a sort lower than that of the identity element. For example,

  fmod COLLAPSE-NAT-EX is
    sorts Nat NzNat .
    subsort NzNat < Nat .
    op 0 : -> Nat .
    op s : Nat -> NzNat .
    op + : Nat Nat -> Nat [assoc comm id: 0] .
    op + : Nat NzNat -> Nat [assoc comm id: 0] .
    var X : Nat .
    var Y : NzNat .
    eq +(s(X), Y) = s(+(X, Y)) .
  endfm

Here +(s(X), Y) cannot match s(0) because, although s(0) = +(s(0), 0) by the identity attribute, Y cannot match 0.

Rewriting with the idem attribute is even riskier. For example,

  fmod COLLAPSE-IDEM-EX is
    sort Foo .
    ops a b : -> Foo .
    op f : Foo Foo -> Foo [idem] .
    var X : Foo .
    eq a = b .
  endfm

We then have

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

Thus, if a can be rewritten by an equation, then any number of rewrites can be done by using the idem axiom to create new copies of a. In fact, the current implementation would choose the obvious rewrite and just produce b, but this should not be relied upon; COLLAPSE-IDEM-EX is a nonterminating system. The only safe way to use idem is as follows. Whenever a connected component is the domain and range of an operator having the idem attribute, then its sorts are poisoned. Terms of poisoned sorts must never rewrite other than by rules under the control of a strategy, that is, using metalevel descent functions. Such terms must be built out of free constructors--operators that may have equational attributes such as comm, but may not have equations with these operators at the top. Of course, it is ok to have defined functions that work on such constructor terms; it is just that the terms themselves may not rewrite.