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 s0 > si > s2 > ••• in S there exists some i < j such that si < sj and there are no infinite anti chains, where an anti chain consists of incomparable elements with respect to >.

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, cU?F(Г) = {в0, в1, в2,...} with 0i ={x ^ g(xy', щ (b))}, has an infinite

decreasing chain with respect to > F, namely 00 >F 01 >F 02 >F ...

Clearly 0i >F 0i+ь because with X = {y' ^ f (a, y')} and with the axioms in F we have:

The chain 00 >F 01 >F 02 >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 00 encompasses 01, i.e. 00 ^F 61, because with X = {y' ^ f (a, y')}:

But in this case 01 also encompasses 00 modulo F, since there are substitutions

X1>0 = {x ^ g(x', y', f (a, q(x)))} and X2,0 = e such that 01 =F X1>0 00 X2,0, because:

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

{x ^ g(x', y', Vi (q(x))}00. Since ^F is transitive, 00 encompasses all 0i modulo F, because with Xi = {y' ^ Vi (yO} we have 00 =F 0iXi ={x ^ g(xVi (y'), Vi (b))} =F 1 {x ^ g(xy', b)}. Consequently they all are encompassment equivalent. Taking 00 as the representative for this equivalent class, 00 is the only essential F-unifier for Г1, which means, that Г1 is now an 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)) ^H2 h(x, y, z). Analogously —Hi denotes the rule from right to left.

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 ?H2). For this we need a few observations.[1]

Proposition 11.3 Every unifier for Г1 or Г2 is of the form о = {x — g(si, s2, s3)}, where the Si 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 F4 (or H4) respectively.

Proposition 11.4 For every unifier о = {x — g(s, s2, s3)} 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, s2, s3)) -h4 h(s1, s2, s3) —H2 h(si, s2, b) —H3 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 H3.

For the intermediate sequence we show by induction:

h(s1, s2, s3) —H2 h(s1, s2, b) if and only if s3 = pn (b), where n

is the smallest number of steps and pn (b) = f (a, pn-1) is defined as above.

Using induction over the minimal number of rewrite steps:

n = 1 : s3 = p1(b) = f (a, b) =^ h(s1, s2, s3) = h(s1, s2, f (a, b))

* H2 h (s1, s2, b )

n — n + 1 : s3 = (Pn+1(b) = f (a, pn (b))) =^

h(s1, s2, f (a, pn(b))) —H2 h(s1, s2, pn(b)) and by induction hypothesis

h(s1, s2, у (b)) —nH2 h(s1, s2, b).

n = 1 : h(s1, s2, s3) -h2 h(su s2, b) =^ s3 = f (a, b) i.e. s3 = p1(b). n — n + 1 : h(s1, s2, s3) *h2 h(s1, s2, s3) —nH2 h(su s2, b) =^ s3 = pn(b) using the induction hypothesis. Therefore h(s1, s2, s3) — H2 h(s1, s2, pn(b)).

But this is only possible if f (a, pn (b)) = pn+1(b).

Hence h(s1, s2, s3) h(su s2, b) and s3 = Pn+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 ?F1) is in cU ?H2):

By Proposition 11.3 every unifier is of the form о = {x — g(s1, s2, s3)}. So let oF = {x — g(s1, s2, s3)} be in cU?F1) then there exists a chain of equational steps: q(x)aF = q(g(si, S2, S3)) ^fa h(si, S2, S3) ^nF2 h(si, s2, b) ^F3 b, n ^ 0, where each F-step involves just one axiom from F.

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

q(x)a# = q(g(s1, S2, S3)) ^h4 h(s1, S2, S3) ^nm h(su S2, b) h(b, b, b),

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

H3 and F3.

Hence aF is also a unifier for Г2.

Now for the other direction, let aH be aunifier in cU ?H2). By Proposition 11.3 it is of the form aH = {x ^ g(siy s2, s3)} and by Proposition 11.4 there exists a chain q(x)ah = q(g(si, S2, S3)) ^ha h(S1, S2, S3) ^nH2 h(si, S2, b) h(b, b, b), with n ^ 0, which has no application of H3 except for the last step. But then q(x)aF = q(g(si, S2, S3)) ^F4 h(si, S2, S3) ^nF2 h(si, S2, b) ^F3 b is a valid sequence in H as well and hence aH is a unifier for Г1 and so it is in cU ?F 1) (up to renaming). ?

Theorem 11.1 There are essentially nullary and essentially infinitary theories.

Proof The infinite chain 0O ? H 6i Z1H 02 Z1H ... 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 x0iXi <H x0j, with Xi = {y' ^ yj_i (y')}. But this is impossible, because x0j = g(xyj (y'), yj (b)) and there is no H-equivalent term, x0j = H pj with a sub term of 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 0i =Vh 0i+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.
< Prev   CONTENTS   Source   Next >