Polynomial Time Uniform Word Problems

STANLEY BURRIS

Dept. of Pure Mathematics, University of Waterloo, Waterloo, Ontario, Canada N2L 3G1

(snburris@thoralf.uwaterloo.ca)

We have two polynomial time results for the uniform word problem for a quasivariety Q:

• The uniform word problem for Q can be solved in polynomial time iff one can find a certain congruence on finite partial algebras in polynomial time.

• Let Q^{⋆} be the relational class determined by Q. If any universal Horn class between the universal closure S(Q^{⋆}) and the weak embedding closure S̄(Q^{⋆}) of Q^{⋆} is finitely axiomatizable then the uniform word problem for Q is solvable in polynomial time. This covers Skolem’s 1920 solution to the uniform word problem for lattices and Evans’ 1953 applications of the weak embeddability property for finite partial V algebras.

1 Introduction

In 1920 Skolem [14] showed that the decidability of Th_{∀}(Lat), the universal theory of lattices, depended solely on the decidability of Th_{C}(Lat), the clause theory of lattices, and this in turn depended solely on the decidability of Th_{∀H}(Lat), the universal Horn theory of lattices. (In 1943 McKinsey [13] would independently formulate the same result for any class K closed under direct products.) Skolem then proved Th_{∀H}(Lat) is decidable; and this, as we know, is equivalent to saying that the uniform word problem for lattices is solvable. He was essentially using ideas from the modern subject of fixed point logic as well as the construction of the free lattice completion of a partial lattice. We will return to Skolem’s method in the last section. This remarkable piece of work was completely overlooked until early 1992. As it turns out, the algorithm of Skolem for the uniform word problem of lattices is an efficient polynomial time algorithm, and it was rediscovered in the late 1980’s by Cosmadakis [5], and by Freese [7] (who implemented it in a computer program). Cosmadakis used this to show that Th_{C}(Lat) can be decided in polynomial time, and that Th_{∀}(Lat) is co-NP-complete.

In the following we use the abbreviated phrase “A weakly embeds into K” to mean there is a one-one homomorphism from A into some member of K.

In 1943 McKinsey [13] showed that if a \underline{finitely axiomatizable variety} K has the property

[ \begin{matrix}if a finite partial algebra weakly embeds into K \\ then it weakly embeds into some finite member of K \end{matrix} ]  (1)

then the uniform word problem for K is solvable. He applied this to lattices and obtained an exponential time algorithm.

In 1953 Evans [6] introduced finite partial K algebras for any variety K with a finite set of equational axioms Σ, namely a finite partial algebra P needs to satisfy, for r(x⃗) ≈ s(x⃗) in Σ, respectively r(x⃗) ≈ f(s_{1}(x⃗), ⋯, s_{n}(x⃗)) in Σ (we assume Σ is symmetric),

[ \begin{matrix}(i) r(a⃗), s(a⃗) are defined in P imply r(a⃗) = s(a⃗); \\ (ii) r(a⃗), s_{1}(a⃗), ⋯, s_{n}(a⃗) are defined in P imply f is defined at (s_{1}(a⃗), ⋯, s_{n}(a⃗)). \end{matrix} ]  (2)

Then Evans proved that the uniform word problem for such K is solvable iff

[ \begin{matrix}there is an algorithm to determine which finite partial K algebras \\ weakly embed into K. \end{matrix} ]  (3)

From this he extracted his method for proving that K has a solvable uniform word problem, namely

[ every finite partial K algebra weakly embeds into K. ]  (4)

He applied this to lattices, groupoids, loops and quasigroups.

In 1979 Grätzer [9] reworked Evans’ approach and showed that the uniform word problem for a finitely axiomatizable variety K is solvable iff

[ \begin{matrix}there is an algorithm to determine which finite partial algebras \\ weakly embed into K. \end{matrix} ]  (5)

At this time we do not know if having a polynomial time algorithm in either (3) or (5) will give the solvability of the uniform word problem in polynomial time. (The converse holds in either case.) However (4) is a sufficient condition for the uniform word problem to be solvable in polynomial time. (We will return to this fact at the end of the last section.) This lack of an ‘iff’ result for polynomial time algorithms led us to search for a problem regarding finite partial algebras whose polynomial time solution would be equivalent to the solvability of the uniform word problem in polynomial time. Our first goal is to demonstrate such by showing, for any \underline{quasivariety} K, that

[ \begin{matrix}there is a polynomial time algorithm to find the smallest congruence θ \\ on a finite partial algebra P such that P/θ weakly embeds into K \end{matrix} ]  (6)

is indeed equivalent to K having a uniform word problem which is solvable in polynomial time.

Then we will use this result to give what we think is the correct global perspective from which to view the concrete successes of Skolem and Evans. Let K^{⋆} be the relational version of K, i.e., replace each n-ary function symbol f by an n + 1 ary relation symbol r_{f}, and make the obvious changes in the members of K to get the members of K^{⋆}. Let S(K^{⋆}) be the class of substructures of K^{⋆}, and let S̄(K^{⋆}) be the class of structures which can be weakly embedded (i.e., there is a one-one homomorphism) into K^{⋆}. S(K^{⋆}) and S̄(K^{⋆}) are both elementary classes axiomatizable by universal Horn sentences. The condition that we want to draw attention to is

[ there is a finitely axiomatizable universal Horn class H with S(K^{⋆}) ⊆ H ⊆ S̄(K^{⋆}). ]  (7)

We will show that (7) implies the uniform word problem for a quasivariety K is solvable in polynomial time; and we claim that Skolem’s and Evans’ applications will be special cases of (7).

Throughout we will assume that we are working with finite languages L of algebras.

2 Partial Algebras

A basic tool for analyzing polynomial time uniform word problems is the use of partial algebras. In this section we make the appropriate definitions and list the basic results needed. In the following P and Q are partial algebras in a given language L of algebras.

Definition 1. A mapping α : P → Q is a morphism from P to Q if, for any n-ary operation f, if f(p_{1}, ⋯, p_{n}) is defined in P then f(αp_{1}, ⋯, αp_{n}) is defined in Q and αf(p_{1}, ⋯, p_{n}) = f(αp_{1}, ⋯, αp_{n}).

We write α : P → Q if α is a morphism from P to Q. A morphism α : P → Q is a weak embedding if α is one-one; we write α : P ⟶^{1−1} Q in this case.

Definition 2. An equivalence relation θ on P is a congruence of P if for each n-ary operation f we have

\begin{matrix}p_{1}θp′_{1}, ⋯, p_{n}θp′_{n} \\ f(p_{1}, ⋯, p_{n}) is defined \\ f(p′_{1}, ⋯, p′_{n}) is defined \end{matrix} \}  ⇒  f(p_{1}, ⋯, p_{n})θf(p′_{1}, ⋯, p′_{n}).

Con P is the set of congruences of P. Definition 3. Let θ ∈ Con P. Define P/θ to the the partial algebra with universe P/θ and operations defined by f(p_{1}/θ, ⋯, p_{n}/θ) = p/θ if there are p′_{i} with p_{i}θp′_{i} and f(p′_{1}, ⋯, p′_{n}) is defined and in p/θ. Definition 4. Define Π_{i∈I}P_{i} on Π_{i∈I}P_{i} by f(p_{1}, ⋯, p_{n}) = p iff f(p_{1}(i), ⋯, p_{n}(i)) = p(i) for all i ∈ I. Definition 5. An expansion P̂ of P is any partial algebra on P such that for each operation symbol f in L, the domain of f^{P} is a subset of the domain of f P̂, and f P̂ agrees with f^{P} on the domain of the latter.

With these definitions it is straightforward to verify the following (see Burmeister [3], Grätzer [9]):

• If α : P → Q and Q̂ is an expansion of Q then α : P → Q̂.

• Δ, ∇ ∈ Con P.

• If α : P → Q then Ker α ∈ Con P.

• If θ ∈ Con P then ν : P → P/θ, where ν is the natural map.

• If α : P → Q and θ is a congruence of P with θ ⊆ Ker α then, with ν the natural map from P to P/θ, there is a (unique) morphism β : P/θ → Q such that β ∘ ν = α. If θ = Ker α then β is a weak embedding.

• Con P is closed under ⋂. Definition 6. For K a class of algebras, P ⟶^{1−1} K means P weakly embeds into K.

A key definition is the following. Definition 7. For K be a class of algebras let

μ_{K}(P) = ⋂{θ ∈ Con P : P/θ ⟶^{1−1} K}.

Using the above properties we have

• If K is a quasivariety then μ_{K}(P) is the smallest congruence θ of P such that P/θ ⟶^{1−1} K.

3 The Word Poblem

We briefly review the definitions. Given a language L of algebras, a presentation Π for this language is an ordered pair ⟨G, R⟩ where G is a set of generators (i.e., constants) and R is a set of defining relations (i.e., ground equations) over L ∪ G. A word w for Π is a ground term in the language L ∪ G.

The word problem for a class K of L algebras is concerned with determining, for any presentation Π, which ground equations w ≈ w′ follow from Th(K), the first-order theory of K, and the defining relations R, i.e., when Th(K) ∪ R ⊢ w ≈ w′ holds. (We will write this as Π ⊢_{K} w ≈ w′.) Usually one considers the word problem for varieties K, for then to each presentation Π there corresponds an algebra A, with generators named by the generators of Π, such that Π ⊢_{K} w ≈ w′ holds iff A ⊧ w ≈ w′. Such an algebra A also exists when K is a quasivariety; then A is in the variety generated by K, but not necessarily in K.

The uniform word problem for K is said to be solvable if there is an algorithm which decides if Π ⊢_{K} w ≈ w′ for every finite presentation Π for L and for every pair of words w, w′. [A word of \underline{caution}: some authors use the phrase word problem to mean the word problem for the infinitely generated free algebra in a variety K, i.e., for the equational theory of K. This is not the convention used here.]

It is easy to see that the uniform word problem for K is solvable iff the universal Horn theory Th_{∀H}(K) is decidable since

Th(K) ∪ R ⊢ w ≈ w′  iff  Th(K) ⊢ ⋀ R → w ≈ w′.

This simple connection between the uniform word problem and the universal Horn theory is our main reason for extending the definition of the uniform word problem to arbitrary classes K of L algebras — we are really studying universal Horn theories, but we want the reader to remember the important application to traditional uniform word problems.

4 Partial Algebras and the Word Problem

Given a presentation Π = ⟨G, R⟩ for the language L, and words w, w′ , we define the partial algebra T_{Π,w,w′} to be the restriction of the ground term algebra T for the language L ∪ G to the subterms of w, w′ and the subterms of all s and t for which s ≈ t ∈ R.

For any L ∪ G algebra A there is a unique morphism from T to A (as T is absolutely free), and this restricts to the unique morphism α : T_{Π,w,w′} → A. Let φ be the congruence on T_{Π,w,w′} generated by {⟨s, t⟩ : s ≈ t ∈ R}. Then A ⊧ w ≈ w′ iff φ ⊆ Ker α. Define P_{Π,w,w′} = T_{Π,w,w′}/φ. Then for any L ∪ G algebra A there is a most one L ∪ G morphism β : P_{Π,w,w′} → A, and such exists iff A ⊧ R.

Now suppose A is an L ∪ G algebra which satisfies R, and let β : P_{Π,w,w′} → A (the unique morphism). Then A ⊧ w ≈ w′ iff ⟨w, w′⟩ ∈ Ker β. This leads to a basic result.

Proposition 8. Let K be a quasivariety of L algebras, and let Π = ⟨G, R⟩ be a presentation for L, and let w, w′ be words. Then

Π ⊢_{K} w ≈ w′  iff  ⟨w, w′⟩ ∈ μ_{K}(P_{Π,w,w′}).  (8)

Proof. Clearly Π ⊢_{K} w ≈ w′ iff every L ∪ G algebra A whose L reduct A|_{L} is in K and which satisfies R also satisfies w ≈ w′. For such an A let β : P_{Π,w,w′} → A (the unique morphism). Then, as noted above, A ⊧ w ≈ w′ iff ⟨w, w′⟩ ∈ Ker β. Now A|_{L} ∈ K implies μ_{K}(P_{Π,w,w′}) ⊆ Ker β; and for a suitable choice of A we have equality. Thus

A ⊧ Th(K) ∪ R implies A ⊧ w ≈ w′

holds iff ⟨w, w′⟩ ∈ μ_{K}(P_{Π,w,w′}).

This leads to the following decidability result.

Proposition 9. The uniform word problem for a quasivariety K is solvable iff there is an algorithm to find μ_{K}(P) for P any finite partial L algebra.

Proof. Suppose the uniform word problem for K is solvable. Given a finite partial algebra P let R be the finite set of ground equations f(p_{1}, ⋯, p_{n}) ≈ p which hold in P, and let Π = ⟨P, R⟩. Then for p_{1}, p_{2} ∈ P we have ⟨p_{1}, p_{2}⟩ ∈ μ_{K}(P) iff Π ⊢_{K} p_{1} ≈ p_{2}, so we can effectively find μ_{K}(P).

Conversely, suppose we can effectively find the μ_{K}(P). Then to decide if Π ⊢_{K} w ≈ w′ we simply determine if ⟨w, w′⟩ ∈ μ_{K}(P_{Π,w,w′}).

Using this (or simply working through the proof in [9]) one has the following straightforward generalization of Grätzer’s result for finitely axiomatizable varieties.

Corollary 10. The uniform word problem for a quasivariety K is solvable iff (5) holds.

The main reason we focus on the construction of μ_{K}(P) is the following polynomial time version of Proposition 9.

Proposition 11. The uniform word problem for a quasivariety K is solvable in polynomial time iff there is a polynomial time algorithm to find μ_{K}(P) for P any finite partial L algebra.

Proof. Use the same steps as in the proof of Proposition 9, noting that in the direction (⇒) we apply a polynomial time algorithm polynomially many times to find μ_{K}(P); and in the direction (⇐) observe that one can construct P_{Π,w,w′} in polynomial time.

Example 12. Kozen’s result [11], that the uniform word problem for the class K of all L algebras is solvable in polynomial time, is clear since μ_{K}(P) = Δ in this case.

Example 13. Evans’ condition (4) says that μ_{K}(P) is the smallest congruence of P closed under (2)(i) and (ii); hence μ_{K}(P) can be found in polynomial time if (4) holds.

Let us say a few words about the limitations of (4). Evans knew that this does not hold for all varieties with solvable uniform word problem. With the development of complexity we have a new indicator that the uniform word problem will not be polynomial time, and hence (4) cannot hold. Namely if we show the uniform word problem is co-NP-hard then we expect the uniform word problem to require superpolynomial time, and (4) to fail — else P = NP.

Examples where the uniform word problem is co-NP-hard include: any finitely generated non-nilpotent variety of rings (see Burris & Lawrence [4]), any non-trivial finitely generated variety of lattices (see Bloniarz, Hunt, & Rosenkrantz [2]), any variety generated by a finite nonsolvable group (Lawrence), and any congruence distributive variety generated by a two-element algebra (Berman & Blok [1] and Willard). In all of the above examples we actually use the fact that the equational theory (or the equivalence problem) is co-NP-complete.

In general we can see very little relation between the equational theory and the uniform word problem for K, except that the latter is at least as difficult as the former. For groups we have an extreme case where the equational theory is polynomial time but the uniform word problem is unsolvable. All finitely generated quasivarieties have, of course, a simply exponential solvable uniform word problem.

We would like to know the answer to the following question.

Problem 1. Are the polynomial time versions of (3) or (5) in the first section equivalent to the solvability of the uniform word problem in polynomial time?

We remark that it is easy to show that the polynomial time versions of (3) and (5) are equivalent conditions; and both hold if the uniform word problem is solvable in polynomial time.

Cosmadakis [5] showed that the universal theory of lattices is co-NP-complete since the uniform word problem is solvable in polynomial time. If the polynomial time version of (5) holds for any nontrivial class of L algebras K then we can easily show that Th_{∀}(K) is co-NP-complete. Actually one can say a bit more in this direction.

Proposition 14. For any nontrivial quasivariety K the following are equivalent:

(a) Determining if a finite partial algebra weakly embeds into K is an NP problem.

(b) The universal theory Th_{∀}(K) is co-NP-complete.

(c) The uniform word problem for K is co-NP.

Proof. (a) ⇒ (b): Since K is a nontrivial class its universal theory must be co-NP-hard as one can interpret propositional formulas as universal formulas by simply replacing a propositional variable P_{i} by x_{i} ≈ y_{i}. Next, if φ is a universal sentence which does not hold in K then there is a small finite partial algebra which can be weakly embedded in K which witnesses the fact that φ does not hold. From (a) it follows that the collection of universal sentences which do not hold in K is NP, so the universal theory of K is co-NP.

(b) ⇒ (c) is trivial as Th_{∀H}(K) ⊆ Th_{∀}(K).

(c) ⇒ (a): Let P be a finite partial algebra, and let tables(x_{1}, ⋯, x_{n}) be a conjunction of atomic formulas which describe the partial operations of P. Then P ⟶^{1−1} K iff tables(x_{1}, ⋯, x_{n}) → x_{i} ≈ x_{j} is not in Th_{∀H}(K) for i < j; and this is in NP.

An interesting example regarding Proposition 14 is that of commutative semigroups, where each finite presentation Π has a word problem solvable in polynomial time, but the uniform word problem for commutative semigroups is exponential space complete (due to Mayr & Meyer [12]; see also Kharlampovich & Sapir [10]).

5 The Role of Finitely Axiomatizable Universal Horn Theories

Let L be a language of algebras and let L^{⋆} be the corresponding language of relational structures obtained, as we described in the first section, by replacing each n ary f in L by an n + 1 ary r_{f}. Then, for each (partial or total) L algebra A there is a corresponding L^{⋆} structure A^{⋆} such that

A ⊧ f(a_{1}, ⋯, a_{n}) ≈ a  iff  A^{⋆} ⊧ r_{f}(a_{1}, ⋯, a_{n}, a).

If K is a class of (partial or total) L algebras then S(K^{⋆}), the class of substructures of members of K^{⋆}, corresponds to some of the partial algebras P such that P ⟶^{1−1} K; namely we have

P ⟶^{1−1} K  iff  P̂^{⋆} ∈ S(K^{⋆}) for some expansion P̂ of P.

On the other hand S̄(K^{⋆}), the class of structures that can be weakly embedded into K^{⋆}, is precisely {P^{⋆} : P ⟶^{1−1} K}. If K is an elementary class then one can show S(K^{⋆}) and S̄(K^{⋆}) are closed under ultraproducts, and hence they are also elementary classes; and as they are closed under substructures they are universal classes, i.e., axiomatizable by universal sentences. If K is an elementary class closed under direct products, then one can furthermore show that S(K^{⋆}) and S̄(K^{⋆}) are closed under direct products as well, and hence they are universal Horn classes.

Definition 15. For any class C of structures let C_{fin} be the class of finite members of C. If there is an algorithm to determine which finite structures are in C_{fin} then we say C_{fin} is effectively recognizable.

Examples of classes C with C_{fin} effectively recognizable include any finitely axiomatizable C, or more generally, any L reduct of a class axiomatized by finitely many (higher order) statements.

Lemma 16. Let K be a class of L algebras such that there is a class C with C_{fin} effectively recognizable and S(K^{⋆}) ⊆ C ⊆ S̄(K^{⋆}). Then one can effectively determine if a finite partial algebra P ⟶^{1−1} K.

Proof. Observe that for a finite partial algebra P, P ⟶^{1−1} K iff there is an expansion P̂ such that P̂^{⋆} ∈ C_{fin}. Now P has only finitely many expansions P̂, and as P̂^{⋆} ∈ C_{fin} can be checked, we have the desired algorithm.

Proposition 17. If K is a quasivariety and C_{fin} is effectively recognizable with S(K^{⋆}) ⊆ C ⊆ S̄(K^{⋆}) then the uniform word problem for K is solvable.

Proof. Use the previous lemma and Corollary 10.

We do not know if a polynomial time version of Proposition 17 holds.

Problem 2. If K is a quasivariety and S(K^{⋆}) ⊆ C ⊆ S̄(K^{⋆}) with C_{fin} recognizable in polynomial time does it follow that the uniform word problem for K is solvable in polynomial time?

From Proposition 17 and known results on unsolvable word problems we can conclude that for K = groups, rings, semigroups, etc., for any choice of C with S(K^{⋆}) ⊆ C ⊆ S̄(K^{⋆}), we have C_{fin} is not effectively recognizable; hence in particular C is not finitely axiomatizable, nor a reduct of a finitely axiomatizable class.

Theorem 18. Let K be a quasivariety such that there is a finitely axiomatizable universal Horn class H with S(K^{⋆}) ⊆ H ⊆ S̄(K^{⋆}). Then the uniform word problem for K is solvable in polynomial time.

Proof. Let Σ be a finite set of universal Horn sentences axiomatizing H. Let θ be a binary relation symbol and define Σ(θ) to be the following set of universal Horn sentences:

i. replace ≈ in members of Σ by θ;

ii. add the congruence axioms:

xθx, xθy → yθx, xθy ∧ yθz → xθz x_{1}θx′_{1} ∧ ⋯ ∧ x_{n}θx′_{n} ∧ r_{f}(x_{1}, ⋯, x_{n}, x) ∧ r_{f}(x′_{1}, ⋯, x′_{n}, x′) → xθx′

For P a finite partial L algebra let P^{⋆}(θ) denote the expansion of P^{⋆} by a binary predicate θ. The key observation is that since Σ(θ) is a set of universal Horn statements there is a smallest extension P̂ of P and a smallest θ such that P̂(θ) satisfies Σ(θ). This is because, as Skolem observed, universal Horn sentences can be thought of as rules for generating simultaneously a monotone sequence of extensions of the predicates; so starting with P^{⋆}(∅) we obtain in polynomial time the least fixpoints of the monotonically increasing r_{f} and θ. This θ is clearly a congruence on P, and indeed the smallest congruence such that P/θ has an expansion P̂/θ whose relation version P̂/θ^{⋆} is in H. But then θ is the smallest congruence such that P/θ ⟶^{1−1} K, i.e., θ = μ_{K}(P). We have a polynomial time algorithm to find μ_{K}(P), so by Proposition 9 the uniform word problem is solvable in polynomial time.

Example 19. If we let K be the class of all L algebras then S(K^{⋆}) = S̄(K^{⋆}); and this class is axiomatized by statements asserting the r_{f} are partial functions. Thus again we have Kozen’s result that the class K of all L algebras has a polynomial time uniform word problem.

Example 20. Skolem’s 1920 paper defined lattices as relational structures axiomatized by the following:^{1}

Skolem’s Rules

1.  x ≤ x
2.  x ≤ y ∧ y ≤ z → x ≤ z
3_{M}. Mxyz → z ≤ x ∧ z ≤ y
3_{J}. Jxyz → x ≤ z ∧ y ≤ z
4_{M}. Mxyz ∧ w ≤ x ∧ w ≤ y → w ≤ z
4_{J}. Jxyz ∧ x ≤ w ∧ y ≤ w → z ≤ w

(x ∼ y means x ≤ y and y ≤ x in the following)

5_{M}. Mxyz ∧ x ∼ x′ ∧ y ∼ y′ ∧ z ∼ z′ → Mx′y′z′
5_{J}. Jxyz ∧ x ∼ x′ ∧ y ∼ y′ ∧ z ∼ z′ → Jx′y′z′
6_{M}. ∀x∀y∃zMxyz
6_{J}. ∀x∀y∃zJxyz

His main result shows that any finite model M of 1–5 can be weakly embedded in model of 1–6 with no expansion of ≤ on M. He then uses 1–5 to analyze universal Horn sentences, starting with what is essentially T_{Π,w,w′}^{⋆} and using 1–5 to generate the minimal fixpoints M, J, ≤ of 1–5.

A straightforward reading of Skolem’s proof shows, in our terminology, that he used 1–5 to generate μ_{Lat}(P). Another way of viewing Skolem’s result is simply that 1–5 axiomatize the universal closure of his structures; or, factoring out the congruence determined by ≤, and using x ≤ y as an abbreviation for x ∧ y ≈ x, the following is a finite axiomatization of S(Lat^{⋆}):

x ≤ x

x ≤ y ∧ y ≤ x → x ≈ y x ≤ y ∧ y ≤ z → x ≤ z r_{∧}(x, y, z) → z ≤ x ∧ z ≤ y r_{∨}(x, y, z) → x ≤ z ∧ y ≤ z r_{∧}(x, y, z) ∧ w ≤ x ∧ w ≤ y → w ≤ z r_{∨}(x, y, z) ∧ x ≤ w ∧ y ≤ w → z ≤ w.

Next we note that Evans’ condition (4) can be translated as universal Horn formulas in the language L^{⋆}. For example, to say that the associative law x_{1}(x_{2}x_{3}) ≈ (x_{1}x_{2})x_{3} holds, where defined, could be expressed by:

Mx_{2}x_{3}y_{1} ∧ Mx_{1}y_{1}y_{2} ∧ Mx_{1}x_{2}y_{3} ∧ My_{3}x_{3}y_{4} → y_{2} ≈ y_{4}.

1Skolem used different notation for join, meet and the ordering relation.

And to say that if the left side is defined and the maximal subterms of the right side are defined implies the right side is defined could be expressed (in view of (2)(i)) by

Mx_{2}x_{3}y_{1} ∧ Mx_{1}y_{1}y_{2} ∧ Mx_{1}x_{2}y_{3} → My_{3}x_{3}y_{2}.

Example 21. One can view Evans condition (4) as asserting that the universal Horn class H defined by translating (2)(i),(ii) into relation form in the language L^{⋆}, plus axioms to state the r_{f} define partial functions, is finitely axiomatizable and satisfies S(K^{⋆}) ⊆ H ⊆ S̄(K^{⋆}).

Example 22. For K the variety of commutative semigroups we see that S(K^{⋆}) is not finitely axiomatizable (as the uniform word problem requires exponential space).

Example 23. Let K be a finitely generated quasivariety with a co-NP-complete uniform word problem, as in the examples mentioned after Example 13, e.g. distributive lattices. Then one expects that any universal Horn class H with S(K^{⋆}) ⊆ H ⊆ S̄(K^{⋆}) is not finitely axiomatizable — otherwise P = NP.

Finally, we are interested in knowing more about the interaction of the classes K, S(K^{⋆}), and S̄(K^{⋆}). If any elementary class E with S(K^{⋆}) ⊆ E ⊆ S̄(K^{⋆}) is finitely axiomatizable, so is K^{⋆} (just add axioms to Ax(E) that say the r_{f} define total functions), and hence so is K. However we do not know of any other connections involving finite axiomatizability; and we do not know if there are any quasivarieties K such that S(K^{⋆}) and S̄(K^{⋆}) are not finitely axiomatizable but the uniform word problem for K is solvable in polynomial time.

Acknowledgement: These investigations have benefited considerably from past discussions with Ralph Freese on the uniform word problem for lattices, and on the software he has written for such. The main result, Theorem 18, was discovered while the author was lecturing at the University of Lisbon on Universal Algebra and Computing as a guest of Margarita Ramalho and the Gulbenkian Foundation.

References

[1] J. Berman and W.J. Blok, Equational dependencies. J. Inform. Process. Cybernet. EIK 28 (1992), 215–225.

[2] P. Bloniarz, H.B. Hunt III, and D.J. Rosenkrantz, On the computational complexity of algebra on lattices. Siam J. Computing 16 (1987), 129–148.

[3] P. Burmeister, “A Model Theoretic Oriented Approach to Partial Algebras”. Band 32, Akademie-Verlag, 1986.

[4] S. Burris and J. Lawrence, The equivalence problem for finite rings. J. Symbolic Computation, 15 (1993), 67–71.

[5] S.S. Cosmadakis, The word and generator problem for lattices. Information and Computation 77 (1988), 192–217.

[6] T. Evans, T. (1953). Embeddability and the word problem. J. London Math. Soc. 28 (1953), 76–80.

[7] R.S. Freese, Private communication. 1992.

[8] R.S. Freese, Finitely presented lattices: canonical forms and the covering relation. Trans. Amer. Math. Soc. 312 (1989), 841–860.

[9] G. Grätzer, “Universal Algebra.” 2^{nd} edition, 1979, Springer-Verlag.

[10] O.G. Kharlampovich and M.V. Sapir, “Algorithmic Problems in Varieties”. (Preliminary version, 1993.)

[11] D. Kozen, Complexity of finitely presented algebras. Proceedings of the 9^{th} Symposium, STOC, 1977, 164–177.

[12] E.W. Mayr and A.R. Meyer, The complexity of the word problem for commutative semigroups and polynomial ideals. Adv. in Math. 46 (1982), 305–329.

[13] J.C.C. McKinsey, The decision problem for some classes of sentences without quantifiers. J. Symbolic Logic 8 (1943), 61-76.

[14] Th. Skolem, Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit und Beweisbarkeit mathematischen Sätze nebst einem Theorem über dichte Mengen. Videnskabsakademiet i Kristiania, Skrifter I, No. 4, 1920, 1–36. Also in “Th. Skolem, Selected Works in Logic”, ed. by Jens Erik Fenstad, Scand. Univ. Books, Universitetsforlaget, Oslo, 1970, pp. 103–136.