The use of a bare variable lefthand side for an equation, rule, or membership axiom may lead to unexpected nontermination. The recommended place to use them is in rules which are only going to be applied via a strategy language. Using them in membership axioms is seductive, but very tricky. For example:
subsort Prime < Nat . var N : Nat . cmb N : Prime if favoritePrimeTest(N) .will end up with the membership axiom and favoritePrimeTest being applied to every reduced term of sort Nat, including those that arise during evaluation of favoritePrimeTest(N) with likely nontermination.
Using id: or idem attributes means that you are (notionally) working with infinite congruence 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 FOO 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)) = f(f(e, e), a) = ...In particular, the pattern f(X, a) matches a with X <- 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 NAT 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 FOO2 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), a) = f(a, f(a, a)) = ...And 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 on; FOO2 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. They must be built out of free (other than attributes) constructors. 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.
When the associativity axiom is combined with a one-sided identity axiom some unexpected matching properties result. Consider the module:
fmod BAR is
sort Foo .
ops a b 1f : -> Foo .
op f : Foo Foo -> Foo [assoc left id: 1f] .
var X Y : Foo .
endfm
Then
match f(X, Y) <=? f(a, b) .yields three solutions:
Solution 1
X:Foo --> 1f
Y:Foo --> f(a, b)
Solution 2
X:Foo --> a
Y:Foo --> b
Solution 3
X:Foo --> f(a, 1f)
Y:Foo --> b
whereas the naive user may not have expected the last solution.
Matching with extension can be even more surprising:
xmatch f(X, Y) <=? f(a, b) .yields five solutions:
Solution 1
Matched portion = f(a, 1f)
X:Foo --> a
Y:Foo --> 1f
Solution 2
Matched portion = f(a, 1f)
X:Foo --> f(a, 1f)
Y:Foo --> 1f
Solution 3
Matched portion = (whole)
X:Foo --> 1f
Y:Foo --> f(a, b)
Solution 4
Matched portion = (whole)
X:Foo --> a
Y:Foo --> b
Solution 5
Matched portion = (whole)
X:Foo --> f(a, 1f)
Y:Foo --> b
Here the first two solutions match a portion f(a, 1f) of the
subject that was not apparent from the original problem. However,
if one considers the congruence class of f(a, b) they are valid
solutions that are necessary for correct simulation of congruence
class (conditional) rewriting.