# Essentially Nullary Theories

Gordon Plotkin [63] conjectured in his seminal paper in 1972, that there may be sets of most general unifiers modulo E, that are not recursively enumerable, that is, subsumption modulo *E* is not a “well quasiorder”.

Definition 11.6 A *quasiorder* > *on a set S is a well quasiorder,* if for any infinite descending chain s_{0} > si > s_{2} > ••• in S there exists some *i < j* such that *s** i* <

*s*

*and there are no infinite anti chains, where an anti chain consists of incomparable elements with respect to >.*

**j**In the early 1980 s the first equational theories of unification type nullary were discovered [30] and in particular idempotent semigroups (with the axioms of associativity and idempotency, also called bands [2, 69]), became well known. So a natural question is: are there essentially nullary theories as well? Franz Baader gave in [3] an example of an equational theory F and a nullary matching problem for F, which is illuminating for our demonstration here as well. We show first, that this particular problem, which is nullary in the traditional sense, is *essentially unitary, that is it is e-unitary* in this new sense. This and other examples presented in 4.1 and 4.2 below gave rise to the early hope that there are no e-nullary theories and that many infinitary problems may collapse to e-finitary or even e-unitary problems. However a slight modification of *F* and of the matching problem shows that there are unfortunately still essentially nullary (*e-nullary*) problems as well.

Let *F* be the following equational theory with constant symbols *a* and *b* and the function symbols *f, g, h* and *q*

Let *Г** _{1}* be the equational unification problem

*q (x)*

*=*

*?*

_{F}*b*, with

*V*

*=*Var

*(Г*

_{1}*)*

*= {*

*x*} and let щ

*(x)*be defined as щ

_{0}

*(x)*=

*x*and щ

_{+1}

*(x*) =

*f (a, щ (x*)) for

*i*> 0.

Franz Baader shows in [3], that the following complete set of *F*-unifiers of Г_{1}, *c** U*?

_{F}*(Г)*

**= {***в*

_{0}*, в*

_{1}*, в*

_{2}*,..*

*with*

**.}***0*

_{i}={*x*^

*g(xy*

**'***, щ*(b))}, has an infinite

decreasing chain with respect to > *_{F}*, namely

*0*>

_{0}_{F}

*0*>

_{1}_{F}

*0*>

_{2}_{F}...

Clearly *0**_{i}* >

_{F}

*0*

*+ь because with*

_{i}*X*

*= {*

*y*

*'*^

*f (a, y*

*'*

*)*

*}*and with the axioms in

*F*we have:

The chain 0_{0} *>*_{F} *0*_{1}* >*_{F} *0*_{2}* >*_{F} *? ??* has no lower bound, hence *Г*_{1} is indeed nullary. Now, let us look at the encompassment ordering modulo *F* for the same problem.

As the following reasoning shows, the theory *F* is no longer *nullary* in the ordinary sense, but in fact it collapses to an *e-unitary* theory.

As before *0** _{0}* encompasses

*0*

_{1}*,*i.e.

*0*

*^*

_{0}_{F}

*6*

_{1}*,*because with

*X = {y'*^

*f (a, y')}:*

But in this case 0_{1} also encompasses 0_{0} modulo *F*, since there are substitutions

X_{1>0} *= {x* ^ *g(x', y', f (a, q(x*)))} and X_{2},_{0} = *e* such that 0_{1} *= _{F}* X

_{1>0}0

_{0}X

_{2},

_{0}, because:

Therefore *0i* encompasses 0_{0} for i ^ 1, because *0i = {x* ^ *g(xy', v _{i} (b)} =_{F}*

*{x* ^ *g(x', y', Vi (q(x*))}0_{0}. Since ^_{F} is transitive, 0_{0} encompasses all *0i* modulo *F*, because with *X _{i} = {y'* ^

*Vi*(yO} we have 0

_{0}

*=*^

_{F}0iX_{i}={x*g(xVi*(y

*'), Vi (b))} =*1

_{F}*{x*^

*g(xy', b)}.*Consequently they all are encompassment equivalent. Taking 0

_{0}as the representative for this equivalent class, 0

_{0}is the only essential

*F*-unifier for

*Г*

_{1}, which means, that

*Г*

*is now an*

_{1}*e-unitary problem.*

But unfortunately not all is well: this collapse does not hold in general and in fact a slight modification of *F* and Г_{1} turns this back into an e-nullary problem. Consider the equational theory *H* defined by the following axioms, which are almost identical to the theory F, except in axiom H3:

Using *vi (x*) as defined before take the following *H*-unification problem:

Г2 = *{q(x) =H h(b, b, b)}*

Let the rewrite ^* _{Hi}* denote the rule from left to wright of the axiom Hi, i=1,2,3,4. For example the rule for H2 is

*h(x, y, f (a, z)) ^*2

_{H}*h(x, y, z).*Analogously —

*denotes the rule from right to left.*

_{Hi }We now want to show that the complete set of unifiers for *Г*_{1}*,* i.e. *cU ?*_{F} *(Г*_{1}*)* is the same (up to renaming) as the set *cU ?*_{H}*(Г*_{2}*).* For this we need a few observations.^{[1]}

Proposition 11.3 *Every unifier for Г*_{1}* or* Г_{2} *is of the form о = {x — g(si, s*_{2}*,* s_{3})}, *where the S***i ***are some terms.*

This is easy to see as *q(x)o =?*_{F} *b* (or *q(x)o =?*_{H} *h (b, b, b))* must first apply axiom *F** _{4}* (or H

_{4}) respectively.

Proposition 11.4 *For every unifier о = {x — g(s, s*_{2}*,* s_{3})} *for Г*_{2}*, the correctness ofq (x )o =***? _{H} **

*h(b, b, b) can be shown by a minimal sequence of rewrites of the form q(g(si, s*

*2*

*, s*

*3*

*))*-h4

*h*(s1, s2, s3) —H

_{2}

*h(si, s*

*2*

*, b) —*

**H***3*

*h(b, b, b), n*^ 0,

*where n*

*>0*

*is the smallest number of steps.*

*Proof* The first step with — _{H4} is obvious, as no other axiom applies and as immediate is the last step with *— **_{H}*3.

For the intermediate sequence we show by induction:

*h(s*_{1}*, s*_{2}*, s*_{3}*) —*_{H}*2** h(s*_{1}*, s*_{2}*, b)* if and only if s_{3} = *p*_{n} *(b),* where n

is the smallest number of steps and *p*_{n} *(b) = f (a, p*_{n}*-1**)* is defined as above.

Using induction over the minimal number of rewrite steps:

*n =* 1 : s_{3} = *p*_{1}(b) = *f (a, b) =^ h*(s_{1}, s_{2}, s_{3}) = *h(s*_{1}*, s*_{2}*, f (a, b))*

** ** H*2

*h*(s1, s2,

*b )*

*n — n +* 1 : s3 = *(P***n***+**1**(b) = f (a, p***n ***(b))) =^*

*h(s*_{1}*, s*_{2}*, f (a, p*_{n}*(b))) —*_{H}*2** h(s*_{1}*, s*_{2}*, p*_{n}*(b))* and by induction hypothesis

*h(s**1**, s**2**, у (b)) —*^{n}H*2** h(s**1**, s**2**, b).*

*n =* 1 : *h(s**1**, s**2**, s**3**)* -h2 *h(s _{u} s*

*2*

*, b) =^ s*

*3*

*= f (a, b)*i.e. s3 = p1(b).

*n — n +*1 :

*h(s*

*1*

*, s*

*2*

*, s*

*3*

*)**h2

*h*(s1, s2, s3

*) —*

^{n}H*2*

*h(s*

_{u}s*2*

*, b)*=^ s3 =

*pn(b)*using the induction hypothesis. Therefore

*h(s*

_{1}*, s*

_{2}*, s*

_{3}*) —*

_{H}*2*

*h*(s

_{1}, s

_{2},

*p*

_{n}(b)).But this is only possible if *f (a, p*_{n} *(b)) = p*_{n}*+**1**(b).*

Hence *h*(s1, s2, s3) *h(s _{u} s*

*2*

*, b)*and s3 =

*P*

**n***+*

*1*

*(b).*?

Lemma 11.2 *The unification problems ^:q(x) =***? _{F} **

*b and Г*

_{2}*.^(x) =*

**?**_{H}*h(b, b, b) have the same complete set of unifiers (up to renaming): cU ?f (Г*

*1*

*) = cU ? h (Г*

*2*

*).*

*Proof* “ =^”

Every unifier in *cU ?*_{F}*(Г*_{1}*)* is in *cU ?*_{H}*(Г*_{2}*):*

By Proposition 11.3 every unifier is of the form *о = {x — g(s*_{1}*, s*_{2}*,* s_{3})}. So let *o*_{F} *= {x — g(s*_{1}*, s*_{2}*,* s_{3})} be in *cU?*_{F}*(Г*_{1}*)* then there exists a chain of equational steps: q(x)a_{F} = *q(g(si, S**2**, S**3*)) ^fa h(si, S*2**, S**3**) ^ ^{n}*

_{F}*2*

*h(si, s*

_{2}, b) ^

**F***3 b, n*^ 0, where each F-step involves just one axiom from F.

W.l.o.g. we may also assume that the axiom F_{3} = *h (x, y, b)* is only used once as the last step. But then

q(x)a# = *q(g(s**1**, S**2**, S**3*)) ^h4 *h(s**1**, S**2**, S**3**) ^*^{n}_{m} h(s_{u} S*2**, b) h(b, b, b),*

*n* ^ 0, is also a valid sequence, since H and F have the same axioms except for

*H*3 and *F*3.

Hence *a**_{F}* is also a unifier for

*Г*

_{2}.Now for the other direction, let *a**_{H}* be aunifier in

*cU*?

_{H}*(Г*By Proposition 11.3 it is of the form

_{2}).*a*

_{H}*= {x*^

*g(s*s

_{iy}s_{2},_{3})} and by Proposition 11.4 there exists a chain q(x)ah =

*q(g(si, S*

*2*

*, S*

*3*)) ^ha h(S

*1*

*, S*

*2*

*, S*

*3*)

*^*

^{n}

_{H}*2 h(si, S*

*2*

*, b) h(b, b, b),*with

*n*^ 0, which has no application of

*H*3 except for the last step. But then q(x)aF =

*q(g(si, S*

*2*

*, S*

*3*

*)) ^*

**F***4 h(si, S*

*2*

*, S*

*3*

*) ^*

^{n}F*2 h(si, S*

*2*

*, b) ^*

**F***3 b*is a valid sequence in H as well and hence

*a*

*is a unifier for Г*

_{H}_{1}and so it is in

*cU ?*

_{F}*(Г*(up to renaming). ?

_{1})Theorem 11.1 *There are essentially nullary and essentially infinitary theories.*

*Proof* The infinite chain 0_{O} ? _{H} *6** _{i}* Z1

_{H}

*0*Z1

_{2}_{H}...

*has no lower bound.*Otherwise, there would be indices

*i, j*with 1 ^

*i < j*, such that

*0j*=!

_{H}

*0i*. That is

*0i*is encompassed by

*0j*, hence

*x0iX*, with

_{i}<_{H}x0j*X*^

_{i}= {y'*yj_*(

_{i}*y')}.*But this is impossible, because

*x*

*0*

*j = g(xyj*(

*y'), yj (b))*and there is no

*H*-equivalent term,

*x*

*0*

*j =*with a sub term of

_{H}pj*pj*which contains a term beginning with the symbol g. Only the axiom Hi contains g. This axiom introduces, or deletes only

*f*symbols, so a sub term beginning with

*g*never comes up. This means, that there is no tripartition of any

*0*

*i =*

^{V}h

*0*

*i*+iX. But then the encompassment relation =!

_{H}specializes to the instantiation relation >

_{H}and the above chain is identical to the >

_{F}chain, so the minimality condition cannot be fulfilled (see [3]). Hence

*H*must be an e-nullary theory. ?

Intuitively the point is that in the theory *F* it was possible to derive a term with *g(x', y', b)* as a sub term. For example:

But this chain of equations is not valid in the term algebra modulo *H*.

Currently we are experimenting with a stronger relation than encompassment so that there are no nullary theories.

- [1] Unfortunately we do not know if the axioms H1 to H4 can be directed into a canonical rewritesystem as the axioms F1 to F4 in ([2]). So we make a little detour and look at the actual derivation,instead of the more elegant proof by Franz Baader for F1 to F4, based on the canonical rewritesystem for F, in ([2]). Thanks to Franz Baader for this hint.