More on matching and simplification modulo

In the Maude implementation, rewriting modulo $A$ is accomplished by using a matching modulo $A$ algorithm. More precisely, given an equational theory $A$, a term $t$ (corresponding to the lefthand side of an equation) and a subject term $u$, we say that $t$ matches $u$ modulo $A$ (or that $t$ $A$-matches $u$) if there is a substitution $\sigma$ such that $\sigma(t) =_{A} u$, that is, $\sigma(t)$ and $u$ are equal modulo the equational theory $A$ (compare with the syntactic definition of matching in Section 4.7 above).

Given an equational theory $A = \cup_{i} A_{f_{i}}$ corresponding to all the attributes declared in different binary operators, Maude synthesizes a combined matching algorithm for the theory $A$, and does both equational simplification (with equations) and rewriting (with rules in system modules, see Chapter 5) modulo the axioms $A$.

Note, however, that for operators $f$ whose equational axioms $A$ include the associativity axiom, to achieve the effect of simplification modulo $A$ using an $A$-matching algorithm, we have to attempt matching a lefthand side of the form $f(t_{1}, t_{2})$ not only on a subject term $u$, but also on all its $f$-subterms, that is, on those ``fragments'' of the top structure of the term that could be matched by $f(t_{1}, t_{2})$. For example, assuming a binary associative operator f and constants a, b, c, and d of the appropriate sort, the term $t = \texttt{f(a,b)}$ does not match the term $u = \texttt{f(a, f(b, f(c, d)))}$, that is, there is no substitution making both terms equal modulo associativity; however, because of associativity of f, $u$ is equivalent to f(f(a, b), f(c, d)) and then $t$ trivially matches the first subterm. This becomes easier to see using mixfix notation; if $f =$_._, then $t =$ a . b and $u =$ a . b . c . d, and we clearly see that $t$ matches a fragment of $u$. For the case where the only axiom is associativity, the _._-subterms of a . b . c . d are

  a . b
  a . b . c
  b . c
  b . c . d
  c . d

If the operation _._ had been declared both associative and commutative, then we should add to those the additional subterms

  a . c
  a . d
  b . d
  a . b . d
  a . c . d

If the term $f(t_{1}, t_{2})$ matches either $u$ or an $f$-subterm of $u$ modulo $A$, then we say that $f(t_{1}, t_{2})$ matches $u$ with extension modulo $A$ (or that $f(t_{1}, t_{2})$ $A$-matches $u$ with extension). For example, the lefthand side of the equation a . b = e matches a . b . c . d with extension modulo associativity, and the lefthand side of a . d = g matches a . b . c . d with extension modulo associativity and commutativity.

For $f$ a binary operator with equational attributes $A_f$ including the associativity axiom, we now define how a subject term $u$ is $A_f$-rewritten with extension using an equation $f(t_1, t_2) = v$. First of all, $f(t_1, t_2)$ must $A_f$-match with extension a maximal $f$-subterm $w$ of $u$ (that is, an $f$-subterm of $u$ that is not itself an $f$-subterm of a bigger $f$-subterm). This means that there is an $f$-subterm $w_0$ of $w$ and a substitution $\sigma$ such that $\sigma(f(t_1,\ t_2)) =_{A_f} w_0$. Then, the corresponding $A_f$-rewriting with extension step rewrites $u$ to the term obtained by replacing the subterm $w_0$ by $\sigma(v)$.

Note that a term $f(t_{1}, t_{2})$ $A_f$-matches with extension a maximal $f$-subterm if and only if it $A_f$-matches without extension some $f$-subterm. This is of course the important practical advantage of $A$-matching and $A$-rewriting with extension, namely, that only maximal $f$-subterms of a term have to be inspected to get the effect of rewriting equivalence classes modulo $A$. For more technical details on rewriting modulo a set of axioms, see, e.g., [23].

Matching with extension for an associative operator essentially corresponds to matching without extension for a collection of associated equations. For example, we could have ``generalized'' the equation a . b = e with _._ associative to the equations

  eq a . b = e .
  eq X . a . b = X . e .
  eq a . b . Y = e . Y .
  eq X . a . b . Y = X . e . Y .

so that we could have achieved the same effect by rewriting only at the top of maximal $f$-subterms (without extension). Similarly, for _._ associative and commutative, we could have generalized the same equation a . b = e to the equations

  eq a . b = e .
  eq a . b . Y = e . Y .

In Maude this generalization does not have to be performed explicitly as a transformation of the specification. It is instead achieved implicitly in a built-in way by performing $A$-matching with extension. If the equational axioms declared for a binary operator $f$ include the associativity axiom, then a subject term $u$ with $f$ as its top operator is internally represented (but this representation can also be externally used, see Section 3.9.3) as the flattened term $f(u_{1},\ \ldots, u_{n})$, with the $u_{1}, \ldots, u_{n}$ having top operators different from $f$. Furthermore, if a (two-sided) identity element $e$ has been declared for $f$, then $u_{i} \neq e, 1 \leq i \leq n$. That is, we assume in this case that all identities have been simplified away.

Relative to this internal representation, it is then easy to define the notion of an $f$-subterm. If the axioms of $f$ include associativity but not commutativity, then the $f$-subterms of the term $f(u_{1},\ \ldots, u_{n})$ are all terms of the form $f(u_{k}, \ldots, u_{k + h})$ with $1 \leq k \leq n - 1$ and $1 \leq h \leq n -k$.

Similarly, if the axioms of $f$ include associativity and commutativity, then the $f$-subterms of $f(u_{1},\ \ldots, u_{n})$ are all terms of the form $f(u_{k_{1}}, \ldots, u_{k_{h}})$ with $1 \leq k_{i_1} < \cdots < k_{i_h} \leq n$, and $2 \leq h \leq n$.

The concepts of positions in a term and depth of a term, that are important in many situations, refer to this flattened form. The compact notation for terms constructed with operators having the iter attribute (Section 4.4.2) is also considered a form of flattened notation, so that, for the purpose of calculating term depth, if the top level is at level 0, then the occurrence of X:Foo in f^3(X:Foo) is at level 1, not level 3.

Adding axioms for an identity element $e$ to a possibly associative and/or commutative operation $f$ leads to some subtle cases, where the proper application of the general notions may not always coincide with the user's expectations. To begin with, unexpected cases of nontermination may be introduced by an unwary user. For example, the equation

  eq a . X = b . a .

will cause nontermination when _._ is declared associative with identity 1, since we have, for example,

$$\begin{eqnarray*} \verb d . a  & \rightarrow & \verb d . b . a  \\ & \rightarr... ...arrow & \verb d . b . b . \cdots\verb  . b . a  \\ & \vdots & \end{eqnarray*}$$

by instantiating each time the variable X to the identity element 1.

A second source of unexpected behavior is the fact that a lefthand side involving an associative operator may, in the presence of an additional identity attribute, match a term not involving at all that operator. Thus, for the above equation, we have also the nonterminating chain of rewriting steps

$$\begin{eqnarray*} \verb a  & \rightarrow & \verb b . a  \\ & \rightarrow & \ve... ...ightarrow & \verb b . b . \cdots\verb  . b . a  \\ & \vdots & \end{eqnarray*}$$

In a similar way, in the presence of an identity element, the user's expectations about when a lefthand side will match with extension a subject term may not fully agree with the proper technical definition. Consider, for example, a binary operation _._ that is associative and commutative, and that has an identity element 1, and let

  eq a . X = c .

be an equation. Then,

1. The lefthand side a . X matches the subject term a modulo the axioms by instantiating X to 1, giving rise to the simplification
   
   $$\verb a  \rightarrow \verb  c .$$
   
   

2. The same lefthand side matches the subject term a . b . c with extension in three different ways, namely, with substitutions $\texttt{X} \mapsto \verb b . c$, $\texttt{X} \mapsto \verb b$, and $\texttt{X} \mapsto \verb c$, giving rise to the three simplifications
   
   $$\verb a . b . c  \rightarrow \verb  c$$
   
   
   
   
   $$\verb a . b . c  \rightarrow \verb  c . c$$
   
   
   
   
   $$\verb a . b . c  \rightarrow \verb  b . c$$
   
   

3. For the same subject term a . b . c, the substitution $\texttt{X} \mapsto \texttt{1}$ is not a match with extension of the above lefthand side, because the term a . 1 is not a _._-subterm of the term a . b . c. However, because of item 1 above, we know that the equation will match that way not at the top, but ``one level down,'' leading to the simplification
   
   $$\verb a . b . c  \rightarrow \verb  c . b . c$$
   
   

It is also important to realize that there is no match with extension between the lefthand side of the equation a = b and the subject term a . b . c (because the lefthand side a is not a _._-term), although again the equation will match that way not at the top, but ``one level down,'' leading to the simplification

$$\verb a . b . c  \rightarrow \verb  b . b . c$$

Of course, lefthand sides may contain several operators, each matched modulo a different theory. Maude will then match each fragment of a lefthand side according to its given theory.

Consider, for example, the following specification where _._ is associative and _+_ is associative and commutative:

  fmod XMATCH-TEST is
    sort Elt .
    ops a b c d e : -> Elt .
    op _._ : Elt Elt -> Elt [assoc] .
    op _+_ : Elt Elt -> Elt [assoc comm] .
    vars X Y Z : Elt .
    eq X . (Y + Z) = (X . Y) + (X . Z) [metadata "distributivity"] .
  endfm

The lefthand side of the distributivity equation will produce 12 matches with extension for the subject term

  a . b . (c + d + e)

Enumerating these by hand would be tedious and error prone, however Maude provides the xmatch command (see also Section 16.3) for just this purpose:

  xmatch X . (Y + Z) <=? a . b . (c + d + e) .

The output given by Maude consists of the substitution for each match with extension together with the portion of the subject actually matched:

  Maude> xmatch X . (Y + Z) <=? a . b . (c + d + e) .
  xmatch in XMATCH-TEST : X . Z + Y <=? a . b . c + d + e .
  Decision time: 0ms cpu (0ms real)

  Solution 1
  Matched portion = (whole)
  X:Elt --> a . b
  Y:Elt --> c
  Z:Elt --> d + e

  Solution 2
  Matched portion = b . (c + d + e)
  X:Elt --> b
  Y:Elt --> c
  Z:Elt --> d + e

  Solution 3
  Matched portion = (whole)
  X:Elt --> a . b
  Y:Elt --> d
  Z:Elt --> c + e

  Solution 4
  Matched portion = b . (c + d + e)
  X:Elt --> b
  Y:Elt --> d
  Z:Elt --> c + e

  Solution 5
  Matched portion = (whole)
  X:Elt --> a . b
  Y:Elt --> e
  Z:Elt --> c + d

  Solution 6
  Matched portion = b . (c + d + e)
  X:Elt --> b
  Y:Elt --> e
  Z:Elt --> c + d

  Solution 7
  Matched portion = (whole)
  X:Elt --> a . b
  Y:Elt --> c + d
  Z:Elt --> e

  Solution 8
  Matched portion = b . (c + d + e)
  X:Elt --> b
  Y:Elt --> c + d
  Z:Elt --> e

  Solution 9
  Matched portion = (whole)
  X:Elt --> a . b
  Y:Elt --> c + e
  Z:Elt --> d

  Solution 10
  Matched portion = b . (c + d + e)
  X:Elt --> b
  Y:Elt --> c + e
  Z:Elt --> d

  Solution 11
  Matched portion = (whole)
  X:Elt --> a . b
  Y:Elt --> d + e
  Z:Elt --> c

  Solution 12
  Matched portion = b . (c + d + e)
  X:Elt --> b
  Y:Elt --> d + e
  Z:Elt --> c

Note that extension is only used for matching the top operation, _._ in this example, but not _+_. This is the reason why the subterm Y + Z of the lefthand side should match the entire maximal _+_-subterm of the subject term, and not just some _+_-subterm.

For operators with the iter attribute, the situation with matching is analogous to the assoc theory, so that proper subterms of say f^3(X:Foo), such as f^2(X:Foo) and f(X:Foo), can also be matched by means of extension.