# Congruences and Equation

An equivalence relation *&* on the underlying set (the carrier) of an algebra A of type *F* is a *congruence,* if for each n-ary function symbol *f* in *F* and elements *a _{i}, b_{i}* of A, for all i in 1 <

*i*<

*n*we have

The quotient algebra A *&* is the algebra whose carrier are the equivalence classes *A/&* and whose operations satisfy

We are interested in quotient algebras, where the congruence is defined by a set of equations *E*, which is denoted as =_{E}. For a term *t* in *T (F, X)* and the congruence *E* the equivalence class of *t* is denoted as [t]_{E}.

# Orders

A term *t* is (syntactically) an *instance* of a term *s,* denoted *s* < *t*, if *so = t* for some substitution *o*:

We say s *subsumes t* and this relation is a quasiorder (or preorder as it is sometimes called. That is, it is reflexive and transitive). We call it the *subsumption order* on terms.

A term *t* (syntactically) *encompasses* a term s, denoted s c *t*, if a sub term of *t* is an instance of *s*:

Syntactically encompassment conveys the notion that *s* appears in *t* with a context “above” and a substitution instance “below”. We say *t encompasses s* or s is *encompassed* by *t* and c is the *encompassment order.* In particular we define s c *t*, called *strict encompassment,* if s*о* is a proper sub term of t.^{[1]} So in summary we have the following *orders on terms:*

**Definition 11.1 ***(syntactic)*

- 1. A term s is a
*sub term*of*t*if s e**Sub**(t*)*and we denote this order by s <*t*. - 2. A term s
*subsumes*t, denoted s <*t*, if there exists a substitution*о*with s*о**=**t* - 3. A term s is
*encompassed*by*t*, denoted s c*t*, if there exists a substitution*о*such that s*о**e***Sub**(t).

These standard order relations are now extended to equality modulo E for the congruences induced by the equations in *E*.

**Definition 11.2 ***(modulo E)*

- 1. A term s is a
*sub term of t modulo E, denoted s <*, if there is a term_{E}t*t'**=*and s <_{E}t*t'.* - 2. A term s subsumes
*t modulo E, s*<_{E}*t*, if there exists a substitution*о*with*sо**=*_{E}t - 3. A term s is
*encompassed by t modulo E, s**c*if there is a substitution_{E}t*о*such that s*о <*._{E}t

We will now lift these order relations on terms component-wise to order relations on substitutions: for all variables in the domain of the substitution we require that the images fulfill the corresponding relation.

**Definition 11.3 ***(syntactic)*

Let V be some set of variables.

1. A substitution *о* is a *sub-substitution* of *т*, denoted as *о* < *т*, if **Dom ***(о) **= ***Dom**(t) and for all *x* in this domain *xо* is a sub term of *xт*, that is,

*xо **e* **Sub**(xт). **SUB**(t) denotes the set of sub-substitutions of *т*.

- 2. A substitution
*о subsumes*a substitution*т*or*т*is an instance of*о*, denoted*о*<^{y}*т*, if there exists a substitution*X*such that*т*=^{y}*оХ.*The relation < is a quasiorder, called the*subsumption order for substitutions*. - 3. A substitution
*о*is*encompassed*by*т*, denoted by*о*c^{y}*т*, if there exists X, such that*(оХ)*|_{y}is a sub-substitution of*т*. That is*(оХ)*|_{y}e**8иВ**(т).

The corresponding *order on substitutions modulo E, о* <_{E} *т* and *о **c** _{E} т* is defined as:

**Definition 11.4 ***(substitution ordering modulo E restricted to a set of variables) *Let V be some set of variables.

- 1. A substitution
*a*is a*sub-substitution*of*т modulo E,*denoted as*о <*т, if Dom**V***(o')*= Dom*(т)*and for all*x*in this domain,*xa*is a sub term of*x т*modulo E. - 2. A substitution
*a subsumes*a substitution*т*modulo E restricted to V, denoted as*a*т, if there exists a substitution *X*such that*т =*^{V}E*ok.*The relation*<***E**^{is }called the*subsumption order for substitutions modulo E*restricted to V.

We denote *subsumption equivalence* as *a* ~E *т*, if *a*

3. A substitution *a* is *encompassed* by *т* modulo E restricted to V, denoted *a c*^{V}E *т*, if there exists X, such that *(aX)* |_{V} is a sub-substitutionof *т* modulo E restricted to V. We denote *encompassment equivalence* as

*a «*^{V}E *т*, it holds if *a c*^{V}E *т and т c*^{V}E *a*.

An example for the syntactic sub-substitutions of *т = {x* ^ *f (a,* z)| is:

because *x {x* ^ *a} = a e* Sub(x *т) =* Sub( *f (a, z)) = {f (a, z), a,* z}; and similarly for the other elements of 8иВ(т).

To demonstrate the analogy between the better known encompassment definition for terms with the new encompassment order on substitutions, consider the terms *s* and *t* and substitutions *a* and *т*:

then s e Sub(t), but *sk e* Sub(t), i.e. s c *t*.

Now consider the substitutions

where *a e* 8иВ(т) but *aX*_{2}* e* 8иВ(т), that is *a* c *т*.

With

we can brake *т* apart into a tripartition X_{1}aX_{2}, with *V = {x, y*}:

and hence *a* encompasses *т*, *а* с *т.*

Our claim is that the encompassment order is better suited for a general framework for *E*-unification than the standard order <_{E}. To get a feeling for the advantage let us look at the following example.

Substitutions form a semigroup with respect to their composition and this fact was used to define the subsumption order on unifiers, namely

which led to the notion of a most general unifier.

Now consider the equational theory of associativity A = *{x* (*yz) = (xy)z},* that is the free semigroup, and the unification problem *Г = {ax* =A *xa}.* This has an infinite set of most general unifiers *a _{n}* = {{x ^

*a*}|

^{n}*n*> 1}. However, the essential unifier in this set seems to be intuitively a

_{0}

*= {x*^ a}, because every most general unifier contains this unifier in a certain sense, namely with

we have

Since substitutions form a semigroup, the dual of the subsumption order, namely left-composition instead of right-composition would induce a semigroup as well with the advantage that the above infinitary problem would become a unitary one. So if we use the order <* _{A}* with left composition ЗЛ :

*a =*we have a

_{A}Хт*unitary*problem. But this is not compatible with the original notion of generality and of course it would not quite work in general as long as the

*X*can be any substitution. Our solution is based on

*lifting*the encompassment order on terms to the

*encompassment order on substitutions modulo E.*In particular the encompassment order on substitutions allows us to represent

*т*as a tripartition with left

*and*right composition:

If Xi is empty this is the usual subsumption relation and if *X** _{2}* is empty then

*т*is not an instance and

*a*is a proper sub-substitution and so it is encompassed by

*т*.

- [1] Signs and notation are still not uniform in all related fields, in particular our notation is usedmore often in the literature on automated theorem proving and unification theory [6], whereas termrewriting systems usually prefer notational conventions such as ; see [22, 23].