Memberships for iterated operators

In analogy to interaction of associative operators and membership declarations, terms constructed with a stack of iterated operators may not be assigned the expected sort when it is necessary to apply a membership axiom to a subterm in order to infer the sort. Again, if an iter operator is declared at the sort level, Maude will not apply membership axioms to subterms in order to calculate the sort of a subterm before attempting to apply the operator declaration to calculate the sort of the whole term. As an example, consider the following module:

  fmod ITER-MB-EX1 is
    sort Foo .
    op f : Foo -> Foo [iter] .
    op e : -> [Foo] .

    mb f(e) : Foo .
  endfm

  Maude> red f(e) .
  Warning: membership axioms are not guaranteed to work correctly for
      iterated symbol f as it has declarations that are not at the
      kind level.
  reduce in ITER-MB-EX1 : f(e) .
  rewrites: 1 in 0ms cpu (0ms real) (~ rews/sec)
  result Foo: f(e)

  Maude> red f(f(e)) .
  reduce in ITER-MB-EX1 : f^2(e) .
  rewrites: 0 in 0ms cpu (0ms real) (~ rews/sec)
  result [Foo]: f^2(e)

  Maude> red f(f(f(e))) .
  reduce in ITER-MB-EX1 : f^3(e) .
  rewrites: 0 in 0ms cpu (0ms real) (~ rews/sec)
  result [Foo]: f^3(e)

Here the intuition is that e is at the kind level, but f(e) is not. Unfortunately, for f(f(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 declarations applying above membership axioms for iterated operators are not allowed.

Again, recall that the warning that membership axioms may not work is only given once per module. Here it just happens that it is given in response to a reduction command that does give the right answer.

The example can be rewritten so that membership axioms can be used to compute the desired sort as follows:

  fmod ITER-MB-EX2 is
    sort Foo .
    op f : [Foo] -> [Foo] [iter] .
    op e : -> [Foo] .

    mb f(X:Foo) : Foo .
    mb f(e) : Foo .
  endfm

  Maude> red f(e) .
  reduce in ITER-MB-EX2 : f(e) .
  rewrites: 1 in 0ms cpu (0ms real) (~ rews/sec)
  result Foo: f(e)

  Maude> red f(f(e)) .
  reduce in ITER-MB-EX2 : f^2(e) .
  rewrites: 2 in 0ms cpu (0ms real) (~ rews/sec)
  result Foo: f^2(e)

  Maude> red f(f(f(e))) .
  reduce in ITER-MB-EX2 : f^3(e) .
  rewrites: 3 in 0ms cpu (0ms real) (~ rews/sec)
  result Foo: f^3(e)

Here the operator declaration is at the kind level, and as in the associativity example in the previous section, the effect of the old declaration is obtained by an extra membership axiom. Note that using membership axioms in this way loses the efficiency for big towers of operators, which is the whole point of the iter theory.