Rewriting with both equations and rules
takes place by matching a lefthand side term against the subject term to
be rewritten. The most common form of matching is syntactic matching, in
which the lefthand side term is matched as a tree on the (tree representation
of the) subject term (see Section 4.7).
For example, the matching of the lefthand sides for the
equations defining the length and _in_ functions above is
performed by syntactic matching. But we have already encountered another,
more expressive, form of matching, namely, equational matching in the
bank accounts example: the lefthand side
< I : Account | bal : M > credit(I, N)
has the (empty syntax) multiset union operator __ as its top operator,
but, thanks to its assoc and comm equational attributes,
it is matched not as a tree, but as a multiset. Therefore, the
match will succeed provided that the subject multiset
contains instances of the terms
< I : Account | bal : M > and credit(I, N)
in which the variable I is instantiated the same way in both
terms, regardless of where those instances appear in the multiset, that
is, modulo associativity and commutativity.
In general, a binary operator declared in a Maude module can be defined with any1.4 combination of equational attributes of: associativity, commutativity, left-, right-, or two-sided identity, and idempotency. Maude then generates an equational matching algorithm for the equational attributes of the different operators in the module, so that each operator is matched modulo its equational attributes. This manual will illustrate with various examples the expressive power afforded by this form of equational matching (see Section 4.8).