Associativity and idempotency

Remember that the attributes assoc and idem (see Section 4.4.1) cannot be used together in any combination of attributes, because the appropriate matching and normalization algorithms have not been developed yet.

This requirement is quietly enforced by ignoring the attribute idem where necessary.

Let us consider the following example, in which we wrongly declare an operator with the attributes assoc and idem appearing together.

  fmod WRONG-NAT-SET is
    pr NAT .
    sort WNatSet .
    subsort Nat < WNatSet .
    op none : -> WNatSet [ctor] .
    op __ : WNatSet WNatSet -> WNatSet
         [ctor assoc comm idem id: none] .
  endfm

When we reduce a term like, e.g., 4 4 5 2, the duplication does not disappear, because Maude has ignored the idempotency attribute; the remaining attributes are applied as usual.

  Maude> red 4 4 5 2 .
  result WNatSet: 2 4 4 5

We can solve this by adding explicitly an idempotency equation, as we have seen, for example, in Section 7.12.2.

Combining idem with attributes other than assoc is all right. For example, the following module combines idempotency with commutativity.

  fmod COMM-IDEM-EX is
    pr NAT .
    sort CI .
    subsort Nat < CI .
    op f : CI CI -> CI [ctor comm idem] .

    vars N M : Nat .
    var  C : CI .

    op g : CI -> Nat .
    eq g(f(N, M)) = 0 .
    eq g(C) = 1 [owise] .
  endfm

  Maude> red f(2, 2) .
  result NzNat: 2

  Maude> red f(2, 3) == f(3, 2) .
  result Bool: true

Notice that in this module, because of matching modulo commutativity and idempotency, the first equation for g can be applied to a term such as, e.g., g(2). For example, we have the following reductions:

  Maude> red g(2) .
  result Zero: 0

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

  Maude> red g(f(2, f(3, 4))) .
  result NzNat: 1