Equational attributes

Equational attributes are a means of declaring certain kinds of equational axioms in a way that allows Maude to use these equations efficiently in a built-in way. Currently Maude supports the following equational attributes:

• assoc (associativity),
• comm (commutativity),
• idem (idempotency),
• id: $\langle$Term$\rangle$ (identity, with the corresponding term for the identity element),
• left id: $\langle$Term$\rangle$ (left identity, with the corresponding term for the left identity element), and
• right id: $\langle$Term$\rangle$ (right identity, with the corresponding term for the right identity element).

An operator can be declared with several of these attributes, which may appear in any order in the attribute declaration. However, these attributes are only allowed for binary operators satisfying the following requirements:

• For left id:, it is required that the right domain sort and the range sort belong to the same kind.
• For right id:, it is required that the left domain sort and range sort belong to the same kind.
• For assoc, comm, id:, and idem, both domain sorts and the range sort must belong to the same kind.

These requirements are checked at parse time, and if the check fails a warning is output and the operator loses its attributes.

Furthermore, we have the following additional requirements:

• The attribute idem cannot be used in any combination of attributes that includes assoc, because the necessary matching and normalization algorithms have not been implemented yet. This requirement is quietly enforced by ignoring the attribute idem where necessary.
• Only one identity attribute (left id:, right id:, or id:) is allowed. This is enforced by a warning and by ignoring all but the first such attribute.

• Combining the attribute comm with either left id: or right id: silently turns the identity attribute into an id:.

• All subsort-overloaded instances of an operator must have the same attributes. This is further explained in Section 4.4.6.

Semantically, declaring a set of equational attributes for an operator is equivalent to declaring the corresponding equations for the operator. Operationally, using equational attributes to declare such equations avoids termination problems and leads to much more efficient evaluation of terms containing such an operator. In fact, the effect of declaring equational attributes is to compute with equivalence classes modulo such equations. This, besides being very expressive, avoids what otherwise would be insoluble termination problems. For example, if a commutativity equation like x + y = y + x is declared as an ordinary equation, then it will easily produce looping, nonterminating simplifications. If it is instead declared with an equational attribute comm, this looping behavior does not happen.

In our numbers example we can add a constant nil for the empty sequence and refine the declaration of sequence concatenation so that concatenation is associative with identity nil.

  op nil : -> NatSeq .
  op __ : NatSeq NatSeq -> NatSeq [assoc id: nil] .

As another example, we can form lists of Booleans as a supersort BList of Bool in an extension of the BOOL module (see Section 7.1) with a ``cons'' operator _._ having nil as a right identity:

  sort BList .
  subsort Bool < BList .
  op nil : -> BList .
  op _._ : Bool BList -> BList [right id: nil] .

Note that, when equational attributes are declared, equational simplification using the other equations in the module does not take place at the purely syntactic level of replacing syntactic equals by equals, but is understood modulo the equational attributes. Therefore, the proper understanding of the notions of Church-Rosser and terminating equations, and of canonical forms, is now modulo the equational attributes that have been declared. We discuss matching and equational simplification modulo axioms in Section 4.8.

For example, by declaring the addition operation on natural numbers modulo 3 as commutative,

  op _+_ : Nat3 Nat3 -> Nat3 [comm] .

it is enough to have the following equations to define its behavior on all possible combinations of arguments:

  vars N3 : Nat3 .
  eq N3 + 0 = N3  .
  eq 1 + 1 = 2 .
  eq 1 + 2 = 0 .
  eq 2 + 2 = 1 .

The equations

  eq 0 + N3 = N3  .
  eq 2 + 1 = 0 .

are not needed, because they are subsumed by the first and third equations above, due to commutativity of _+_.

Notice that membership axioms and matching modulo associativity can interact in undesirable ways, as explained in Section 13.2.8.