Membership axioms can interact with assoc or iter operator attributes in undesirable ways.
The reason is that, for completeness, the operator declarations would have to be tried on every subterm of every member of the equivalence class, and this is not done (for efficiency reasons) in the current implementation, giving rise to some warnings.
For associative operators declared at the sort level, membership axioms will be applied only at the top, they will not be applied to subterms in the process of applying an operator declaration to compute the sort. For example in the following module
fmod ASSOC-MB-EX1 is
sort Foo .
op f : Foo Foo -> Foo [assoc comm] .
op e : -> [Foo] .
ops a b c d : -> Foo .
mb f(a, e) : Foo .
endfm
the membership axiom will not be used to lower the sort of f(a, f(b, e)) to foo as it does not match at the top.
Recall from Sections 3.9.3 and 4.8 that terms built with associative operators can be written in flattened form. This is the notation used for f-terms in the following examples.
Maude> red f(a, b, e) .
Warning: membership axioms are not guaranteed to work correctly for
associative symbol f as it has declarations that are not at the
kind level.
reduce in ASSOC-MB-EX1 : f(e, a, b) .
rewrites: 0 in 0ms cpu (0ms real) (~ rews/sec)
result [Foo]: f(e, a, b)
Maude> red f(a, b, e, a) . reduce in ASSOC-MB-EX1 : f(e, a, a, b) . rewrites: 0 in 0ms cpu (0ms real) (~ rews/sec) result [Foo]: f(e, a, a, b)
Maude> red f(e, b, e, a) . reduce in ASSOC-MB-EX1 : f(e, e, a, b) . rewrites: 0 in 0ms cpu (0ms real) (~ rews/sec) result [Foo]: f(e, e, a, b)
Maude> red f(a, b, e, e, a) . reduce in ASSOC-MB-EX1 : f(e, e, a, a, b) . rewrites: 0 in 0ms cpu (0ms real) (~ rews/sec) result [Foo]: f(e, e, a, a, b)
Maude> red f(a, a, b, e, e, a) . reduce in ASSOC-MB-EX1 : f(e, e, a, a, a, b) . rewrites: 0 in 0ms cpu (0ms real) (~ rews/sec) result [Foo]: f(e, e, a, a, a, b)
Here the intuition is that each e forces the result to the kind level,
unless there is an a to bring it back down. Unfortunately, for
f(a, b, e) we would need to use the membership axiom on a proper
subterm, and then use the declaration at the top to arrive at the sort
Foo, and this is not allowed.
Note that the warning produced by Maude is a per module warning and is only printed once, when the first reduction or rewriting command is given in the module.
The module ASSOC-MB-EX1 above can be rewritten so that sort computations work as expected as follows:
fmod ASSOC-MB-EX2 is
sort Foo .
op f : [Foo] [Foo] -> [Foo] [assoc comm] .
op e : -> [Foo] .
ops a b c d : -> Foo .
mb f(X:Foo, Y:Foo) : Foo .
mb f(a, e) : Foo .
endfm
Maude> red f(a, b, e) . reduce in ASSOC-MB-EX2 : f(e, a, b) . rewrites: 2 in 0ms cpu (1ms real) (~ rews/sec) result Foo: f(e, a, b)
Maude> red f(a, b, e, a) . reduce in ASSOC-MB-EX2 : f(e, a, a, b) . rewrites: 3 in 0ms cpu (0ms real) (~ rews/sec) result Foo: f(e, a, a, b)
Maude> red f(e, b, e, a) . reduce in ASSOC-MB-EX2 : f(e, e, a, b) . rewrites: 6 in 0ms cpu (0ms real) (~ rews/sec) result [Foo]: f(e, e, a, b)
Maude> red f(a, b, e, e, a) . reduce in ASSOC-MB-EX2 : f(e, e, a, a, b) . rewrites: 11 in 0ms cpu (0ms real) (~ rews/sec) result Foo: f(e, e, a, a, b)
Maude> red f(a, a, b, e, e, a) . reduce in ASSOC-MB-EX2 : f(e, e, a, a, a, b) . rewrites: 12 in 0ms cpu (0ms real) (~ rews/sec) result Foo: f(e, e, a, a, a, b)
Here the operator declaration is at the kind level, and the effect of the declaration of f in ASSOC-MB-EX1 is obtained by an extra membership axiom.13.2
Let us see another example of this situation, starting with a module specifying non-empty lists of natural numbers.
fmod SIMPLE-NAT-LIST is
protecting NAT .
sort NatList .
subsort Nat < NatList .
op __ : NatList NatList -> NatList [assoc] .
endfm
It seems natural to specify sorted lists of natural numbers by importing SIMPLE-NAT-LIST and then defining a subsort of NatList.
fmod NAIVE-SORTED-NAT-LIST is
protecting SIMPLE-NAT-LIST .
sort SortedNatList .
subsort Nat < SortedNatList < NatList .
vars I J : Nat .
var SNL : SortedNatList .
cmb I J : SortedNatList if I <= J .
cmb I J SNL : SortedNatList if I <= J /\ J SNL : SortedNatList .
endfm
Maude> red 0 1 2 3 4 5 6 7 8 9 .
Warning: membership axioms are not guaranteed to work correctly for
associative symbol __ as it has declarations that are not at the
kind level.
reduce in NAIVE-SORTED-NAT-LIST : 0 1 2 3 4 5 6 7 8 9 .
rewrites: 1354 in 0ms cpu (0ms real) (~ rews/sec)
result SortedNatList: 0 1 2 3 4 5 6 7 8 9
To avoid this, we can rewrite the module above so that we only use kind-level operator declarations (notice the form of the arrow) and convert all sort-level operator declarations into memberships.
fmod NAT-LIST-KIND is
protecting NAT .
sort NatList .
subsort Nat < NatList .
op __ : NatList NatList ~> NatList [assoc] .
mb I:NatList J:NatList : NatList .
endfm
fmod SORTED-NAT-LIST-KIND is
protecting NAT-LIST-KIND .
sort SortedNatList .
subsort Nat < SortedNatList < NatList .
vars I J : Nat .
var SNL : SortedNatList .
cmb I J : SortedNatList if I <= J .
cmb I J SNL : SortedNatList if I <= J /\ J SNL : SortedNatList .
endfm
Maude> red 0 1 2 3 4 5 6 7 8 9 . reduce in SORTED-NAT-LIST-KIND : 0 1 2 3 4 5 6 7 8 9 . rewrites: 1354 in 0ms cpu (0ms real) (~ rews/sec) result SortedNatList: 0 1 2 3 4 5 6 7 8 9