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 ai, bi 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 <E t, if there is a term t' =Et and s < t'.
  • 2. A term s subsumes t modulo E, s <E t, if there exists a substitution о with =E t
  • 3. A term s is encompassed by t modulo E, s cE t if there is a substitution о 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 is a sub term of , that is,

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 о cy т, 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 о cE т 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 о <V т, if Dom (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 т =VE 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 and т a.

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

a «VE т, it holds if a cVE т and т cVE 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 aX2 e 8иВ(т), that is a c т.

With

we can brake т apart into a tripartition X1aX2, 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 an = {{x ^ an}| n > 1}. However, the essential unifier in this set seems to be intuitively a0 = {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 = A Хт we have 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 X2 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].
 
Source
< Prev   CONTENTS   Source   Next >