BRICS RS-01-21 Aceto et al.: Equational Theories of Tropical Semirings BRICS

Basic Research in Computer Science

Equational Theories of Tropical Semirings

Luca Aceto Zoltán Ésik Anna Ingólfsdóttir BRICS Report Series RS-01-21 ISSN 0909-0878 June 2001 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2001, Luca Aceto & Zoltán Ésik & Anna Ingólfsdóttir.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/01/21/

Equational Theories of Tropical Semirings

Luca Aceto^{∗}  Zoltán Ésik^{†}  Anna Ingólfsdóttir^{∗}

Abstract

This paper studies the equational theory of various exotic semirings presented in the literature. Exotic semirings are semirings whose underlying carrier set is some subset of the set of real numbers equipped with binary operations of minimum or maximum as sum, and addition as product. Two prime examples of such structures are the (max, +) semiring and the tropical semiring. It is shown that none of the exotic semirings commonly considered in the literature has a finite basis for its equations, and that similar results hold for the commutative idempotent weak semirings that underlie them. For each of these commutative idempotent weak semirings, the paper offers characterizations of the equations that hold in them, decidability results for their equational theories, explicit descriptions of the free algebras in the varieties they generate, and relative axiomatization results.

AMS Subject Classification (1991): 08A70, 08B05, 03C05, 68Q15, 68Q70. CR Subject Classification (1991): D.3.1, F.1.1, F.4.1. Keywords and Phrases: Equational logic, varieties, complete axiomatizations, relative axiomatizations, tropical semirings, commutative idempotent weak semirings, convexity, exponential time complexity.

1 Introduction

Exotic semirings, i.e., semirings whose underlying carrier set is some subset of the set of real numbers ℝ equipped with binary operations of minimum or maximum as sum, and addition as product, have been invented and reinvented many times since the late 1950s in various fields of research. This family of structures consists of semirings whose sum operation is idempotent—two prime examples are the (max, +) semiring

∗BRICS (Basic Research in Computer Science), Centre of the Danish National Research Foundation, Department of Computer Science, Aalborg University, Fr. Bajersvej 7E, 9220 Aalborg Ø, Denmark. Email: {luca,annai}@cs.auc.dk. Fax: +45 9815 9889.

†Department of Computer Science, University of Szeged, Árpád tér 2, 6720 Szeged, Hungary. Partially supported by BRICS and research grant no. T30511 from the National Foundation of Hungary for Scientific Research. This work was partly carried out while this author was visiting professor at the Department of Computer Science, Aalborg University. Email:

esik@inf.u-szeged.hu. Fax: +36-62-420292.

(ℝ ∪ {−∞}, max, +, −∞, 0)

(see [5, Chapter 3] for a general reference), and the tropical semiring

(ℕ ∪ {∞}, min, +, ∞, 0)

introduced in [34]. (Henceforth, we shall write ∨ and ∧ for the binary maximum and minimum operations, respectively.) Interest in idempotent semirings arose in the 1950s through the observation that some problems in discrete optimization could be linearized over such structures (see, e.g., [10] for some of the early references and [38] for a survey). Since then, the study of idempotent semirings has forged productive connections with such diverse fields as, e.g., performance evaluation of manufacturing systems, discrete event system theory, graph theory (path algebra), Markov decision processes, Hamilton-Jacobi theory, asymptotic analysis (low temperature asymptotics in statistical physics, large deviations), and automata and language theory (automata with multiplicities). The interested reader is referred to [14] for a survey of these more recent developments, and to [12] for further applications of the (max, +) semiring. Here we limit ourselves to mentioning some of the deep applications of variations on the tropical semiring in automata theory and the study of formal power series.

The tropical semiring (ℕ ∪ {∞}, ∧, +, ∞, 0) was originally introduced by Simon in his solution (see [34]) to Brzozowski’s celebrated finite power property problem—i.e., whether it is decidable if a regular language L has the property that, for some m ≥ 0,

L^{∗} = 1 + L + ⋯ + L^{m} .

The basic idea in Simon’s argument was to use automata with multiplicities in the tropical semiring to reformulate the finite power property as a Burnside problem. (The original Burnside problem asks if a finitely generated group must necessarily be finite if each element has finite order [7].) The tropical semiring was also used by Hashiguchi in his independent solution to the aforementioned problem [16], and in his study of the star height of regular languages (see, e.g., [17, 18, 19]). (For a tutorial introduction on how the tropical semiring is used to solve the finite power property problem, we refer the reader to [31].) The tropical semiring also plays a key role in Simon’s study of the nondeterministic complexity of a standard finite automaton [36]. In his thesis [26], Leung introduced topological ideas into the study of the limitedness problem for distance automata (see also [27]). For an improved treatment of his solutions, and further references, we refer the reader to [28]. Further examples of applications of the tropical semiring may be found in, e.g., [24, 25, 35].

The study of automata and regular expressions with multiplicities in the tropical semiring is by now classic, and has yielded many beautiful and deep results—whose proofs have relied on the study of further exotic semirings. For example, Krob has shown that the equality problem for regular expressions with multiplicities in the tropical semiring is undecidable [22] by introducing the equatorial semiring (ℤ ∪ {∞}, ∧, +, ∞, 0), showing that the equality problem for it is undecidable, and finally proving that the two decidability problems are equivalent. Partial decidability results for certain kinds of equality problems over the tropical and equatorial semirings are studied in [23].

Another classic question for the language of regular expressions, with or without multiplicities, is the study of complete axiom systems for them (see, e.g., [9, 21, 32]). Along this line of research, Bonnier-Rigny and Krob have offered a complete system of identities for one-letter regular expressions with multiplicities in the tropical semiring [6]. However, to the best of our knowledge, there has not been a systematic investigation of the equational theory of the different exotic semirings studied in the literature. This is the aim of this paper.

Our starting points are the results we obtained in [1, 2]. In [1] we studied the equational theory of the max-plus algebra of the natural numbers N_{∨} = (ℕ, ∨, +, 0), and proved that not only its equational theory is not finitely based, but, for every n, the equations in at most n variables that hold in it do not form an equational basis. Another view of the non-existence of a finite basis for the variety generated by this algebra is offered in [2], where we showed that the collection of equations in two variables that hold in it has no finite equational axiomatization.

The algebra N_{∨} is an example of a structure that we call in this paper commutative idempotent weak semiring (abbreviated henceforth to ciw-semiring). Since ciw-semirings underlie many of the exotic semirings studied in the literature, we begin our investigations in this paper by systematically generalizing the results from [1] to the structures Z_{∨} = (ℤ, ∨, +, 0) and N_{∧} = (ℕ, ∧, +, 0). Our initial step in the study of the equational theory of these ciw-semirings is the geometric characterization of the (in)equations that hold in them (Propositions 3.9 and 3.11). These characterizations pave the way to explicit descriptions of the free algebras in the varieties V(Z_{∨}) and V(N_{∧}) generated by Z_{∨} and N_{∧}, respectively, and yield finite axiomatizations of the varieties V(N_{∨}) and V(N_{∧}) relative to V(Z_{∨}) (Theorem 3.20). We then show that, like V(N_{∨}), the varieties V(Z_{∨}) and V(N_{∧}) are not finitely based. The non-finite axiomatizability of the variety V(Z_{∨}) (Theorem 3.22) is a consequence of the similar result for V(N_{∨}) and of its finite axiomatizability relative to V(Z_{∨}).

The proof of the non-existence of a finite basis for the variety V(N_{∧}) (Theorem 3.23) is more challenging, and proceeds as follows. For each n ≥ 3, we first isolate an equation e_{n}^{∧} in n variables which holds in V(N_{∧}). We then prove that no finite collection of equations that hold in V(N_{∧}) can be used to deduce all of the equations of the form e_{n}^{∧}. The proof of this technical result is model-theoretic in nature. More precisely, for every integer n ≥ 3, we construct an algebra B_{n} satisfying all the equations in at most n − 1 variables that hold in V(N_{∧}), but in which e_{n}^{∧} fails. Hence, as for V(N_{∨}), for every natural number n, the equations in at most n variables that hold in V(N_{∧}) do not form an equational basis for this variety. A similar strengthening of the non-finite axiomatizability result holds for the variety V(Z_{∨}).

We then move on to study the equational theory of the exotic semirings presented in the literature that are obtained by adding bottom elements to the above ciw-semirings. More specifically, we examine the following semirings:

Z_{∨,−∞} = (ℤ ∪ {−∞}, ∨, +, −∞, 0) ,
N_{∨,−∞} = (ℕ ∪ {−∞}, ∨, +, −∞, 0) and
N_{∨,−∞}^{−} = (ℕ^{−} ∪ {−∞}, ∨, +, −∞, 0) ,

where ℕ^{−} stands for the set of nonpositive integers. Since Z_{∨,−∞} and N_{∨,−∞}^{−} are easily seen to be isomorphic to the semirings

Z_{∧,∞} = (ℤ ∪ {∞}, ∧, +, ∞, 0) and
N_{∧,∞} = (ℕ ∪ {∞}, ∧, +, ∞, 0) ,

respectively, the results that we obtain apply equally well to these algebras. (The semirings Z_{∧,∞} and N_{∧,∞} are usually referred to as the equatorial semiring [22] and the tropical semiring [34], respectively. The semiring N_{∨,−∞} is called the polar semiring in [24].)

Our study of the equational theory of these algebras will proceed as follows. First, we shall offer some general facts relating the equational theory of a ciwsemiring A to the theory of the free commutative idempotent semiring A_{⊥} it generates. In particular, in Sect. 4.1 we shall relate the non-finite axiomatizability of the variety V(A_{⊥}) generated by A_{⊥} to the non-finite axiomatizability of the variety V(A) generated by A. Then, in Sect. 4.2, we shall apply our general study to derive the facts that all tropical semirings studied in this paper have exponential time decidable, but non-finitely based equational theory. Our general results, together with those proven in Sect. 3, will also give geometric characterizations of the valid equations in the tropical semirings Z_{∨,−∞} and N_{∨,−∞}^{−}, but not in N_{∨,−∞}. The task of providing a geometric description of the valid equations for the semiring N_{∨,−∞} will be accomplished in Sect. 4.3, where we shall also show that V(N_{∨,−∞}) can be axiomatized over V(Z_{∨,−∞}) by a single equation.

Some semirings studied in the literature are obtained by adding a top element ⊤ to a ciw-semiring A in lieu of a bottom element. We examine the general relationships that exist between the equational theory of a ciw-semiring A and that of the semiring A_{⊤} so generated in Sect. 5. This general theory, together with the previously obtained non-finite axiomatizability results, is then applied to show that several semirings with ⊤ are not finitely based either.

We conclude our investigations by examining some variations on the aforementioned semirings. These include, amongst others, structures whose carrier sets are the (nonnegative) rational or real numbers (Sect. 6.1), semirings whose product operation is standard multiplication (Sect. 6.2), the semirings studied by Mascle and Leung in [30] and [26, 27], respectively, (Sect. 6.3), and a minplus algebra based on the ordinals proposed by Mascle in [29] (Sect. 6.4). For all of these structures, we offer results to the effect that their equational theory is not finitely based, and has no axiomatization in a bounded number of variables.

Throughout the paper, we shall use standard notions and notations from universal algebra that can be found, e.g., in [8, 13].

This paper collects, and improves upon, all of the results first announced without proof in [3, 4]. In addition, the material in Sects. 5 and 6 is new.

2 Background Definitions

We begin by introducing some notions that will be used in the technical developments to follow.

A commutative idempotent weak semiring (henceforth abbreviated to ciwsemiring) is an algebra A = (A, ∨, +, 0) such that (A, ∨) is an idempotent commutative semigroup, i.e., a semilattice, (A, +, 0) is a commutative monoid, and such that addition distributes over the ∨ operation. Thus, the following equations hold in A:

x ∨ (y ∨ z) = (x ∨ y) ∨ z
x ∨ y = y ∨ x
x ∨ x = x
x + (y + z) = (x + y) + z
x + y = y + x
x + 0 = x
x + (y ∨ z) = (x + y) ∨ (x + z) .

A ciw-semiring A is positive if

x ∨ 0 = x

holds in A. It then follows that

x ∨ (x + y) = x + y

also holds in A. A homomorphism of ciw-semirings is a function which preserves the ∨ and + operations and the constant 0.

A commutative idempotent semiring, or ci-semiring for short, is an algebra (A, ∨, +, ⊥, 0) such that (A, ∨, +, 0) is a ciw-semiring which satisfies the equations

x ∨ ⊥ = x
x + ⊥ = ⊥ .

A homomorphism of ci-semirings also preserves ⊥.

Suppose that A = (A, ∨, +, 0) is a structure equipped with binary operations ∨ and + and the constant 0. Assume that ⊥ ∉ A and let A_{⊥} = A∪{⊥}. Extend the operations ∨ and + given on A to A_{⊥} by defining

\begin{aligned}a ∨ ⊥ & = & ⊥ ∨ a & = & a \\ a + ⊥ & = & ⊥ + a & = & ⊥ , \end{aligned}

for all a ∈ A_{⊥}. We shall write A_{⊥} for the resulting algebra (A_{⊥}, ∨, +, ⊥, 0), and A(⊥) for the algebra (A_{⊥}, ∨, +, 0) obtained by adding ⊥ to the carrier set, but not to the signature.

Lemma 2.1 For each ciw-semiring A, the algebra A_{⊥} is a ci-semiring.

Remark 2.2 In fact, A_{⊥} is the free ci-semiring generated by A.

Let E_{ciw} denote the set of defining axioms of ciw-semirings, E_{ci} the set of axioms of ci-semirings, and E_{ciw}^{+} the set of axioms of positive ciw-semirings. Note that E_{ciw} is included in both E_{ci} and E_{ciw}^{+}. Moreover, let V_{ciw} denote the variety axiomatized by E_{ciw}, V_{ci} the variety axiomatized by E_{ci} and V_{ciw}^{+} the variety axiomatized by E_{ciw}^{+}. Thus, V_{ci} is the variety of all ci-semirings and V_{ciw}^{+} the variety of all positive ciw-semirings. Since E_{ciw} ⊆ E_{ci} and E_{ciw} ⊆ E_{ciw}^{+}, it follows that V_{ciw} includes both V_{ciw}^{+} and the reduct of any algebra in V_{ci} obtained by forgetting about the constant ⊥.

Remark 2.3 If an equation t = u can be derived from E_{ciw} or E_{ciw}^{+}, then the set of variables occurring in t coincides with the set of variables occurring in u. In light of axiom x + ⊥ = ⊥, this does not hold true for the equations derivable from E_{ci}.

Notation 2.4 In the remainder of this paper, we shall use nx to denote the n-fold addition of x with itself, and we take advantage of the associativity and commutativity of the operations. By convention, nx stands for 0 when n = 0. In the same way, the empty sum is defined to be 0.

For each integer n ≥ 0, we use [n] to stand for the set {1, …, n}, so that [0] is another name for the empty set.

Finally, we sometimes write t(x_{1}, …, x_{n}) to emphasize that the variables occurring in the term t are amongst x_{1}, …, x_{n}.

Lemma 2.5 With respect to the axiom system E_{ciw}, every term t in the language of ciw-semirings, in the variables x_{1}, …, x_{n}, may be rewritten in the form

t = ⋁_{i∈[k]} t_{i}

where k > 0, each t_{i} is a “linear combination”

t_{i} = ∑_{j∈[n]} c_{ij}x_{j} ,

and each c_{ij} is in ℕ.

Terms of the form ⋁_{i∈[k]} t_{i}, where each t_{i} (i ∈ [k], k ≥ 0) is a linear combination of variables, will be referred to as simple terms. When k = 0, the term ⋁_{i∈[k]} t_{i} is just ⊥. (Note that k = 0 is only allowed for ci-semirings.)

Lemma 2.6 With respect to the axiom system E_{ci}, every term t in the language of ci-semirings, in the variables x_{1}, …, x_{n}, may be rewritten in the form

t = ⋁_{i∈[k]} t_{i}

where k ≥ 0, each t_{i} is a “linear combination”

t_{i} = ∑_{j∈[n]} c_{ij}x_{j} ,

and each c_{ij} is in ℕ.

For any commutative idempotent (weak) semiring A and a, b ∈ A, we write a ≤ b to mean a ∨ b = b. In any such structure, the relation ≤ so defined is a partial order, and the + and ∨ operations are monotonic with respect to it. Similarly, we say that an inequation t ≤ t′ between terms t and t′ holds in A if the equation t ∨ t′ = t′ holds. We shall write A ⊧ t = t′ (respectively, A ⊧ t ≤ t′) if the equation t = t′ (resp., the inequation t ≤ t′) holds in A. (In that case, we say that A is a model of t = t′ or t ≤ t′, respectively.) If A is a class of ciw-semirings, we write A ⊧ t = t′ (respectively, A ⊧ t ≤ t′) if the equation t = t′ (resp., the inequation t ≤ t′) holds in every A ∈ A. Note that, if A is in the variety V_{ciw}^{+}, then the inequation 0 ≤ x holds in A.

Definition 2.7 A simple inequation in the variables x_{1}, …, x_{n} is of the form

t ≤ ⋁_{i∈[k]} t_{i} ,

where k > 0, and t and the t_{i} (i ∈ [k]) are linear combinations of the variables x_{1}, …, x_{n}. We say that the left-hand side of the above simple inequation contains the variable x_{j}, or that x_{j} appears on the left-hand side of the simple inequation, if the coefficient of x_{j} in t is nonzero. Similarly, we say that righthand side of the above inequation contains the variable x_{j} if for some i ∈ [k], the coefficient of x_{j} in t_{i} is nonzero.

Note that, for every linear combination t over variables x_{1}, …, x_{n}, the inequation t ≤ ⊥ is not a simple inequation.

Corollary 2.8 With respect to the axiom system E_{ciw}, any equation in the language of ciw-semirings is equivalent to a finite set of simple inequations. Similarly, with respect to E_{ci}, any equation in the language of ci-semirings is equivalent to a finite set of simple inequations or to an inequation of the form x ≤ ⊥ (in which case the equation has only trivial models).

Proof: Let t = u be an equation in the language of ciw-semirings. By Lemma 2.5, using E_{ciw} we can rewrite t and u to simple terms ⋁_{i∈[k]} t_{i} and ⋁_{j∈[l]} u_{j} (k, l > 0), respectively. It is now immediate to see that the equation t = u is equivalent to the family of simple inequations

{t_{i} ≤ ⋁_{j∈[l]} u_{j}, u_{j} ≤ ⋁_{i∈[k]} t_{i} | i ∈ [k], j ∈ [l]} .

Assume now that t = u is an equation in the language of ci-semirings. By Lemma 2.6, using E_{ci} we can rewrite t and u to simple terms ⋁_{i∈[k]} t_{i} and ⋁_{j∈[l]} u_{j} (k, l ≥ 0), respectively. If k, l are both positive or both equal to zero, then the equation t = u is equivalent to the finite set of simple inequations given above. (Note that, if k and l are both 0, then this set is empty, and the original equation is equivalent to ⊥ = ⊥.) If k = 0 and l > 0, then the equation is equivalent to x ≤ ⊥. □

Notation 2.9 Henceforth in this study, we shall often abbreviate a simple inequation

∑_{j∈[n]} d_{j}x_{j} ≤ ⋁_{i∈[k]} ∑_{j∈[n]} c_{ij}x_{j}

as \overline{d} ≤ \{\overline{c}_{1}, …, \overline{c}_{k}\}, where \overline{d} = (d_{1}, …, d_{n}) and \overline{c}_{i} = (c_{i1}, …, c_{in}), for i ∈ [k]. We shall sometimes refer to these inequations as simple ∨-inequations.

In the main body of the paper, we shall also study some ciw-semirings that, like the structure N_{∧} = (ℕ, ∧, +, 0), have the minimum operation in lieu of maximum as their sum. The preliminary results that we have developed in this section apply equally well to these structures. In particular, the axioms for ciw-semirings dealing with ∨ become the standard ones describing the obvious identities for the minimum operation, and its interplay with +, i.e.,

x ∧ (y ∧ z) = (x ∧ y) ∧ z
x ∧ y = y ∧ x
x ∧ x = x
x + (y ∧ z) = (x + y) ∧ (x + z) .

Note that, for ciw-semirings of the form (A, ∧, +, 0), the partial order ≥ is defined by b ≥ a iff a ∧ b = a. In Defn. 2.7, we introduced the notion of simple ∨-inequation. Dually, we say that a simple ∧-inequation in the variables \overline{x} = (x_{1}, …, x_{n}) is an inequation of the form

\overline{d} · \overline{x} ≥ ⋀_{i∈[k]} \overline{c}_{i} · \overline{x} ,

where \overline{d} and the \overline{c}_{i} (i ∈ [k]) are vectors in ℕ^{n}. We shall often write

\overline{d} ≥ \{\overline{c}_{1}, …, \overline{c}_{k}\}

as a shorthand for this inequation.

3 Min-Max-Plus Weak Semirings

Our aim in this section will be to study the equational theory of the ciwsemirings that underlie most of the tropical semirings studied in the literature. More specifically, we shall study the following ciw-semirings:

Z_{∨} = (ℤ, ∨, +, 0)
N_{∨} = (ℕ, ∨, +, 0)
N_{∧} = (ℕ, ∧, +, 0)

equipped with the usual addition operation +, constant 0 and one of the operations ∨ for the maximum of two numbers and ∧ for the minimum of two numbers, i.e.,

x ∨ y = max{x, y}
x ∧ y = min{x, y} .

We shall sometimes use the fact that Z_{∨} and N_{∧} are isomorphic to the ciwsemirings

Z_{∧} = (ℤ, ∧, +, 0) and
N_{∨}^{−} = (ℕ^{−}, ∨, +, 0) ,

respectively, where ℕ^{−} stands for the set of nonpositive integers.

Our study of the equational theory of these algebras will be based on the following uniform pattern. First, we offer a geometric characterization of the simple inequations that hold in these ciw-semirings (Sect. 3.2). These characterizations pave the way to concrete descriptions of the free algebras in the varieties generated by the algebras we study, and yield relative axiomatization and decidability results (Sect. 3.3). Finally we show that none of the ciw-semirings we study is finitely based (Sect. 3.4). All of these technical results rely on a study of properties of convex sets, filters and ideals in ℤ^{n} and ℕ^{n} presented in the following section.

3.1 Convex Sets, Filters and Ideals

Suppose that \overline{v}_{1}, …, \overline{v}_{k} are vectors in ℤ^{n} or, more generally, in ℝ^{n}. A convex linear combination of the \overline{v}_{i} (i ∈ [k]) is any vector \overline{v} ∈ ℝ^{n} which can be written as

\overline{v} = λ_{1}\overline{v}_{1} + ⋯ + λ_{k}\overline{v}_{k} ,

where λ_{i} ≥ 0, i ∈ [k], are real numbers with ∑_{i=1}^{k} λ_{i} = 1.

Definition 3.1 Suppose that U is any subset of ℤ^{n}. We call U a convex set if for all convex linear combinations \overline{v} = λ_{1}\overline{v}_{1} + ⋯ + λ_{k}\overline{v}_{k} with k > 0 and \overline{v}_{i} ∈ U, i ∈ [k], if \overline{v} ∈ ℤ^{n}, then \overline{v} ∈ U.

Suppose that U ⊆ ℕ^{n}. We call U an (order) ideal if for all \overline{u}, \overline{v} in ℕ^{n}, if \overline{u} ≤ \overline{v} and \overline{v} ∈ U then \overline{u} ∈ U. Moreover, we call U a filter, if for all \overline{u} and \overline{v} as above, if \overline{u} ∈ U and \overline{u} ≤ \overline{v} then \overline{v} ∈ U. A convex ideal (respectively, convex filter) in ℕ^{n} is any ideal (resp., filter) which is a convex set.

Note that order ideals and filters are sometimes referred to as lower and upper sets, respectively.

The following fact is clear:

Proposition 3.2 The intersection of any number of convex sets in ℤ^{n} is convex. Moreover, the intersection of any number of convex ideals (convex filters) in ℕ^{n} is a convex ideal (convex filter, respectively).

Thus each set U ⊆ ℤ^{n} is contained in a smallest convex set [U] which is the intersection of all convex subsets of ℤ^{n} containing U. We call [U] the convex set generated by U, or the convex hull of U. When \overline{u} ∈ ℤ^{n}, below we shall sometimes write [\overline{u}] for [\{\overline{u}\}] = \{\overline{u}\}.

Note that we have [U] ⊆ ℕ^{n} whenever U ⊆ ℕ^{n}.

Proposition 3.3 Suppose that U ⊆ ℤ^{n} and \overline{v} ∈ ℤ^{n}. We have \overline{v} ∈ [U] iff \overline{v} is a convex linear combination of some nonzero number of vectors in U.

Suppose now that U ⊆ ℕ^{n}. By Proposition 3.2, there is a smallest convex ideal ci(U) and a smallest convex filter cf(U) in ℕ^{n} containing U. We call ci(U) and cf(U) the convex ideal and the convex filter generated by U, respectively.

For each set U ⊆ ℝ^{n}, define the ideal (U] generated by U thus:

(U] = \{\overline{d} ∈ ℕ^{n} : ∃\overline{c} ∈ U. \overline{d} ≤ \overline{c}\} .

Similarly, the filter [U) generated by U is defined as:

[U) = \{\overline{d} ∈ ℕ^{n} : ∃\overline{c} ∈ U. \overline{d} ≥ \overline{c}\} .

The following proposition will be useful in what follows. In its proof, and throughout this study, we shall use \overline{u}_{i} (i ∈ [n]) to denote the ith unit vector in ℝ^{n}, i.e., the vector whose only nonzero component is a 1 in the ith position; \overline{0} will denote the vector in ℝ^{n} whose entries are all zero. When \overline{u} ∈ ℕ^{n}, below we shall sometimes write (\overline{u}] and [\overline{u}) for (\{\overline{u}\}] and [\{\overline{u}\}), respectively.

In the following proposition, and in its proof, we write [U]_{ℝ^{n}} for the convex hull in ℝ^{n} of a set U included in ℕ^{n}.

Proposition 3.4 Suppose that U ⊆ ℕ^{n}. Then:

1. ci(U) = [(U]] = ([U]_{ℝ^{n}}], and

2. cf(U) = [[U)] = [[U]_{ℝ^{n}}).

Proof: We prove the two claims separately.

1. Note, first of all, that

[(U]] ⊆ ci(U) ⊆ ([U]_{ℝ^{n}}]

clearly holds. To complete the proof, it is therefore sufficient to show that ([U]_{ℝ^{n}}] is included in [(U]]. This is clear if n = 1. In order to prove this claim, suppose that

\overline{d} ≤ λ_{1}\overline{c}_{1} + ⋯ + λ_{k}\overline{c}_{k}

for some k > 0, \overline{d} ∈ ℕ^{n}, \overline{c}_{1}, …, \overline{c}_{k} ∈ U and λ_{1}, …, λ_{k} > 0 with ∑_{i∈[k]} λ_{i} = 1. It suffices to show that \overline{d} is in the convex hull of the set (V], where V = \{\overline{c}_{1}, …, \overline{c}_{k}\}. We shall prove this by induction on

r = n + ∑_{i∈[k]} |\overline{c}_{i}| ,

where we use |\overline{c}_{i}| to denote the weight of the vector \overline{c}_{i} (i ∈ [k]), i.e., the sum of its entries.

The base case is when r = 1. Then n = 1 and we are done.

For the inductive step, suppose that r > 1. We proceed with the proof by distinguishing two cases.

Case 1. If there exists some j ∈ [n] with d_{j} = 0, then since we aim at showing that \overline{d} ∈ [(V]], without loss of generality, we may assume that, for this j, we have c_{ij} = 0 for all i ∈ [k]. We can then remove the jth components of all the vectors to obtain \overline{d}′ and \overline{c}′_{1}, …, \overline{c}′_{k} of dimension n−1 with \overline{d}′ ≤ λ_{1}\overline{c}′_{1} + ⋯ + λ_{k}\overline{c}′_{k}. Let W = \{\overline{c}′_{1}, …, \overline{c}′_{k}\}. By induction, \overline{d}′ is in the convex hull of (W], so that \overline{d} is in the convex hull of (V]. The case that n = 1 is trivial.

Case 2. If the previous case does not apply, then d_{j} > 0 for all j ∈ [n]. Suppose that there exists some j such that c_{ij} = 1 for all i ∈ [k], where c_{ij} denotes the jth component of \overline{c}_{i}. Then also d_{j} = 1 and we may remove the jth components of the vectors to obtain \overline{d}′ and \overline{c}′_{i}, i ∈ [k], as before. Using the inductive hypothesis, it follows as in case 1 above that \overline{d} in the convex hull of (V].

Suppose now that for each j ∈ [n] there is some i_{j} ∈ [k] with c_{i_{j}j} > 1. Let \overline{e} = λ_{1}\overline{c}_{1} + ⋯ + λ_{k}\overline{c}_{k}. If for some j

\overline{d} ≤ λ_{1}\overline{c}_{1} + ⋯ + λ_{i_{j}−1}\overline{c}_{i_{j}−1} + λ_{i_{j}}(\overline{c}_{i_{j}} − \overline{u}_{j}) + λ_{i_{j}+1}\overline{c}_{i_{j}+1} + ⋯ + λ_{k}\overline{c}_{k}
= \overline{e} − λ_{i_{j}} \overline{u}_{j} ,

then, by induction, \overline{d} is contained in the convex hull of (W], where W is the set \{\overline{c}_{1}, …, \overline{c}_{i_{j}−1}, \overline{c}_{i_{j}} − \overline{u}_{j}, \overline{c}_{i_{j}+1}, … \overline{c}_{k}\} ⊆ (V]. It follows that \overline{d} is in the convex hull of (V]. Otherwise, we have that

e_{j} − λ_{i_{j}} ≤ d_{j} ≤ e_{j} ,

for all j ∈ [n]. This means that \overline{d} is inside the n-dimensional rectangle determined by the vectors

\overline{v}_{K} = \overline{e} − ∑_{j∈K} λ_{i_{j}} \overline{u}_{j} ,

where K ranges over all subsets of [n]. Since these vectors \overline{v}_{K} are all in the convex hull in ℝ^{n} of (V], it follows that \overline{d} belongs to the convex hull of (V], which was to be shown.

2. It is clear that

[[U)] ⊆ cf(U) ⊆ [[U]_{ℝ^{n}}) .

To complete the proof, we show that [[U]_{ℝ^{n}}) is included in [[U)].

To this end, let \overline{d} ∈ [[U]_{ℝ^{n}}). This means that there is a convex linear combination \overline{c} = λ_{1}\overline{c}_{1} + ⋯ + λ_{k}\overline{c}_{k} with \overline{d} ≥ \overline{c} and \{\overline{c}_{1}, …, \overline{c}_{k}\} ⊆ U. Let \overline{e} be a vector in ℕ^{n} which is maximal with respect to the pointwise order such that

\overline{d} ≥ λ_{1}(\overline{c}_{1} + \overline{e}) + ⋯ + λ_{k}\overline{c}_{k} .

Then \overline{d} ∈ [[\{\overline{c}_{1} + \overline{e}, …, \overline{c}_{k}\}]_{ℝ^{n}}). As

[\{\overline{c}_{1} + \overline{e}, …, \overline{c}_{k}\}) ⊆ [\{\overline{c}_{1}, …, \overline{c}_{k}\}) ⊆ [U) ,

to prove the claim it is sufficient to show that \overline{d} ∈ [[\{\overline{c}_{1} + \overline{e}, …, \overline{c}_{k}\})]. Therefore, without loss of generality, we may assume that \overline{e} = \overline{0}. Now we proceed with the proof as follows. Let j ∈ [n]. Since \overline{d} is not greater than or equal to a convex linear combination of \overline{c}_{1} + \overline{u}_{j}, \overline{c}_{2}, …, \overline{c}_{k}, where \overline{u}_{j} denotes the jth unit vector in ℕ^{n}, we have

\overline{d} ≱ \overline{c} + λ_{1}\overline{u}_{j} = λ_{1}(\overline{c}_{1} + \overline{u}_{j}) + λ_{2}\overline{c}_{2} + ⋯ + λ_{k}\overline{c}_{k} .

Thus, for d_{j}, viz. the jth component of \overline{d}, it holds that

∑_{i=1}^{k} λ_{j}c_{ij} ≤ d_{j} < λ_{1} + ∑_{i=1}^{k} λ_{j}c_{ij} .

As before, for any i ∈ [k], c_{ij} denotes the jth component of \overline{c}_{i}. For each K ⊆ [n], define

\overline{c}_{K} = \overline{c} + ∑_{j∈K} λ_{1}\overline{u}_{j} = λ_{1}(\overline{c}_{1} + ∑_{j∈K} \overline{u}_{j}) + λ_{2}\overline{c}_{2} + ⋯ + λ_{k}\overline{c}_{k} ,

so that \overline{c}_{∅} = \overline{c} and each \overline{c}_{K} is a convex linear combination of vectors in [\{\overline{c}_{1}, …, \overline{c}_{k}\}). The vectors \overline{c}_{K} determine an n-dimensional cube, and, by the above, \overline{d} is in this cube. Therefore, \overline{d} is a convex linear combination of the \overline{c}_{K}. In conclusion, \overline{d} is a convex linear combination of vectors in [\{\overline{c}_{1}, …, \overline{c}_{k}\}) ⊆ [U), which was to be shown. □

Remark 3.5 It is interesting to note that the equalities ci(U) = ([U]] and cf(U) = [[U]) fail. In fact, the ideal and the filter generated by a convex set are, in general, not convex. Consider, for example, the case n = 2 and U = {(0, 2), (3, 0)}. Then U is convex (cf. Defn. 3.1) since no nontrivial convex combination of the two vectors in U yields a point in ℕ^{2}. Hence ([U]] = (U] which contains (0, 2) and (2, 0). However, the convex combination

\frac{1}{2}(0, 2) + \frac{1}{2}(2, 0) = (1, 1)

does not belong to (U]. Similarly, the filter [[U]) = [U) contains (1, 2) and (3, 0), but not

\frac{1}{2}(1, 2) + \frac{1}{2}(3, 0) = (2, 1) .

Thus, it is not convex and cannot be equal to cf(U) or to [[U)].

Henceforth, we shall use [(U]] and [[U)] to denote the convex ideal and the convex filter generated by U, respectively. This notation is justified by the above proposition.

Corollary 3.6 A set U ⊆ ℕ^{n} is a convex ideal (respectively, convex filter) iff for every \overline{d} ∈ ℕ^{n}, whenever \overline{d} ≤ λ_{1}\overline{c}_{1} + ⋯ + λ_{k}\overline{c}_{k} (resp., \overline{d} ≥ λ_{1}\overline{c}_{1} + ⋯ + λ_{k}\overline{c}_{k}) where k > 0, λ_{i} ≥ 0, \overline{c}_{i} ∈ U (i ∈ [k]) and ∑_{i=1}^{k} λ_{i} = 1, it follows that \overline{d} ∈ U.

Corollary 3.7 Each convex filter in ℕ^{n} is finitely generated.

Proof: The set of minimal elements, with respect to the pointwise partial order, in any convex filter in ℕ^{n} is finite, since any antichain in ℕ^{n} is finite. Moreover, it clearly generates the filter. □

Remark 3.8 Each finite convex set in ℤ^{n} has a unique minimal generating set. Similarly, each finite ideal and each filter in ℕ^{n} has a unique minimal (finite) set of generators.

3.2 Characterization of Valid Inequations

Recall that a simple ∨-inequation in the variables \overline{x} = (x_{1}, …, x_{n}) is an inequation of the form

\overline{d}\overline{x} ≤ \overline{c}_{1}\overline{x} ∨ ⋯ ∨ \overline{c}_{k}\overline{x} ,  (1)

where k > 0, and \overline{d}, \overline{c}_{1}, …, \overline{c}_{k} ∈ ℕ^{n}. Similarly, a simple ∧-inequation is of the form

\overline{d}\overline{x} ≥ \overline{c}_{1}\overline{x} ∧ ⋯ ∧ \overline{c}_{k}\overline{x} ,  (2)

where k, \overline{d}, and \overline{c}_{i} (i ∈ [k]) are as above. We recall that (1) holds in a ciwsemiring A_{∨} = (A, ∨, +, 0) if the equation

\overline{d}\overline{x} ∨ \overline{c}_{1}\overline{x} ∨ ⋯ ∨ \overline{c}_{k}\overline{x} = \overline{c}_{1}\overline{x} ∨ ⋯ ∨ \overline{c}_{k}\overline{x}

does, i.e., when for all \overline{v} ∈ A^{n},

\overline{d}\overline{v} ≤ \overline{c}_{1}\overline{v} ∨ ⋯ ∨ \overline{c}_{k}\overline{v} .

Similarly, we say that (2) holds in a ciw-semiring A_{∧} = (A, ∧, +, 0) if the equation

\overline{d}\overline{x} ∧ \overline{c}_{1}\overline{x} ∧ ⋯ ∧ \overline{c}_{k}\overline{x} = \overline{c}_{1}\overline{x} ∧ ⋯ ∧ \overline{c}_{k}\overline{x}

does. Let U denote the set \{\overline{c}_{1}, …, \overline{c}_{k}\}. We recall that we shall sometimes abbreviate (1) as \overline{d} ≤ U and (2) as \overline{d} ≥ U. For some structures, such as Z_{∨}, it also makes sense to define when a simple inequation \overline{d} ≤ U holds in Z_{∨}, where \overline{d} ∈ ℤ^{n} and U = \{\overline{c}_{1}, …, \overline{c}_{k}\} is a finite nonempty set of vectors in ℤ^{n}.

We now proceed to characterize the collection of simple inequations (possibly with negative coefficients) that hold in the algebra Z_{∨} (and, thus, in its isomorphic version Z_{∧}).

Proposition 3.9 Suppose that \overline{d} ∈ ℤ^{n} and U = \{\overline{c}_{1}, …, \overline{c}_{k}\} is a nonempty, finite set of vectors in ℤ^{n}. A simple inequation \overline{d} ≤ U holds in Z_{∨} iff \overline{d} belongs to the set [U].

Proof: It is sufficient to prove this claim when \overline{d} = \overline{0}, for otherwise we can replace \overline{d} by \overline{0}, the vector in ℤ^{n} whose components are all 0, and U by U − \overline{d} = \{\overline{u} − \overline{d} : \overline{u} ∈ U\}, respectively.

Suppose that \overline{0} ∈ [U], i.e., that there exist real numbers λ_{1}, …, λ_{k} ≥ 0 with ∑_{i=1}^{k} λ_{i} = 1 such that

\overline{0} = λ_{1}\overline{c}_{1} + ⋯ + λ_{k}\overline{c}_{k} .

Thus, 0 = λ_{1}\overline{c}_{1}\overline{u} + ⋯ + λ_{k}\overline{c}_{k}\overline{u} for all \overline{u} ∈ ℤ^{n}. Since the λ_{i} are nonnegative and at least one of them is nonzero, this is possible only if for each \overline{u} ∈ ℤ^{n} there exists some i_{0} ∈ [k] with 0 ≤ \overline{c}_{i_{0}} \overline{u}. It thus follows that \overline{0} ≤ U holds in Z_{∨}.

To prove the other direction, suppose that \overline{0} ∉ [U]. We shall exhibit a vector \overline{u} ∈ ℝ^{n} such that \overline{c}_{i}\overline{u} < 0, for all i ∈ [k], i.e., such that for every i ∈ [k], \overline{c}_{i} and \overline{v} = −\overline{u} make an acute angle. But such a \overline{v} is easy to find: let \overline{v} be a vector in the convex hull in ℝ^{n} of U whose endpoint is closest to the origin. By the continuity of the extension of the term functions to the reals, it is now possible to find a vector with rational coefficients and then a \overline{w} ∈ ℤ^{n} such that \overline{c}_{i}\overline{w} < 0, for all i ∈ [k]. (See the proof of Lemma 6.1 for more details.) This shows that \overline{d} ≤ U does not hold in Z_{∨}, which was to be shown. □

Our order of business now will be to offer characterizations of the collections of simple inequations that hold in the algebras N_{∨} and N_{∧}. The following result connects the simple inequations that hold in these algebras, and will be useful to this effect.

Lemma 3.10 For any \overline{d}, \overline{c}_{1}, …, \overline{c}_{k} in ℕ^{n}, where k > 0,

\overline{d} ≤ \{\overline{c}_{1}, …, \overline{c}_{k}\}  (3)

holds in N_{∨} iff

\overline{e} − \overline{d} ≥ \{\overline{e} − \overline{c}_{1}, …, \overline{e} − \overline{c}_{k}\}  (4)

holds in N_{∧}, where for each i ∈ [n], the ith component of \overline{e} ∈ ℕ^{n} is the maximum of the ith components of \overline{d} and the \overline{c}_{j} (j ∈ [k]). In the same way,

\overline{d} ≥ \{\overline{c}_{1}, …, \overline{c}_{k}\}

holds in N_{∧} iff

\overline{e} − \overline{d} ≤ \{\overline{e} − \overline{c}_{1}, …, \overline{e} − \overline{c}_{k}\}

holds in N_{∨}, where \overline{e} is defined as above.

Proof: We only prove the first statement of the lemma. Equation (3) holds in N_{∨} iff

∀\overline{x} ∈ ℕ^{n}. \overline{d}\overline{x} ≤ \overline{c}_{1}\overline{x} ∨ ⋯ ∨ \overline{c}_{k}\overline{x}
⇔ ∀\overline{x} ∈ ℕ^{n}∃j ∈ [k]. \overline{d}\overline{x} ≤ \overline{c}_{j}\overline{x}
⇔ ∀\overline{x} ∈ ℕ^{n}∃j ∈ [k]. (\overline{e} − \overline{d})\overline{x} ≥ (\overline{e} − \overline{c}_{j})\overline{x}
⇔ ∀\overline{x} ∈ ℕ^{n}. (\overline{e} − \overline{d})\overline{x} ≥ (\overline{e} − \overline{c}_{1})\overline{x} ∧ ⋯ ∧ (\overline{e} − \overline{c}_{k})\overline{x} ,

viz. iff (4) holds in N_{∧}. □

The above lemma expresses a “duality” between the equational theories of N_{∨} and N_{∧}. Note, however, that the equational theory of N_{∧} is not the formal dual of the theory of N_{∨}, since the equations

x ∨ 0 = x

and

x ∧ 0 = 0

are not formal duals of each other.

Using Lem. 3.10 and results from [1], we are now in a position to offer the promised characterizations of the valid simple inequations in N_{∨} and N_{∧}.

Proposition 3.11 Suppose that \overline{d} ∈ ℕ^{n} and U is a finite nonempty set of vectors in ℕ^{n}.

1. The simple inequation \overline{d} ≤ U holds in N_{∨} iff \overline{d} belongs to the set [(U]].

2. The simple inequation \overline{d} ≥ U holds in N_{∧} iff \overline{d} belongs to the set [[U)].

Proof: The first claim is proved in [1]. The second follows from the first and Lemma 3.10. Let U = \{\overline{c}_{1}, …, \overline{c}_{k}\}, say. Let \overline{e} ∈ ℕ^{n} denote the vector whose jth component is the maximum of the jth components of \overline{d} and the \overline{c}_{i}, for each i ∈ [k]. We know that \overline{d} ≥ \{\overline{c}_{1}, …, \overline{c}_{k}\} holds in N_{∧} iff \overline{e}−\overline{d} ≤ \{\overline{e}−\overline{c}_{1}, …, \overline{e}−\overline{c}_{k}\} holds in N_{∨}. But by the first claim in the lemma this holds iff there exist real numbers λ_{j} ≥ 0, j ∈ [k], with ∑_{j=1}^{k} λ_{j} = 1 and

\overline{e} − \overline{d} ≤ λ_{1}(\overline{e} − \overline{c}_{1}) + ⋯ + λ_{k}(\overline{e} − \overline{c}_{k}) ,

i.e., when

\overline{d} ≥ λ_{1}\overline{c}_{1} + ⋯ + λ_{k}\overline{c}_{k} ,

which was to be shown. □

As a corollary of Propositions 3.9 and 3.11, we obtain decidability results for the equational theories of the algebras Z_{∨}, N_{∨} and N_{∧}.

Corollary 3.12 There exists an exponential time algorithm to decide whether an equation holds in the structures Z_{∨}, N_{∨} and N_{∧}. Moreover, it is decidable in polynomial time whether a simple inequation holds in these structures.

Proof: The problem of deciding whether an equation holds in Z_{∨}, N_{∨} and N_{∧}, can be reduced to deciding whether a finite set of simple inequations holds (Cor. 2.8). The obvious reduction may result in a number of simple inequations that is exponential in the number of variables. However, the validity of a simple inequation can be tested in polynomial time by using linear programming (see, e.g., [33]). The interested reader is referred to [1] for more information. □

Remark 3.13 The decidability of the equational theories of the structures Z_{∨}, N_{∨} and N_{∧} also follows from well-known results in logic on the decidability of Presburger arithmetic—the first-order theory of addition on the natural numbers.

It is interesting to compare the above result on the complexity of the equational theory of N_{∨} and N_{∧} with the classic results by Fischer and Rabin [11] on the complexity of the first-order theory of the real numbers under addition, and of Presburger arithmetic. There is a fixed constant c > 0 such that for every (non-deterministic) decision procedure for determining the truth of sentences of real addition and for all sufficiently large n, there is a sentence of length n for which the decision procedure runs for more than 2^{cn} steps. In the case of Presburger arithmetic, the corresponding lower bound is 2^{2^{cn}}. These bounds apply also to the minimal lengths of proofs for any complete axiomatization in which the axioms are easily recognized. Such complexity results apply mutatis mutandis to the first-order theory of the algebras N_{∨} and N_{∧}.

3.3 Free Algebras and Relative Axiomatizations

Let C(ℕ^{n}), CI(ℕ^{n}) and CF (ℕ^{n}) denote the sets of all finite nonempty convex sets, finite nonempty convex ideals, and nonempty convex filters in ℕ^{n}, respectively. We turn each of these sets into a ciw-semiring. Suppose that U, V ∈ C(ℕ^{n}). First of all, recall that the complex sum of U and V, notation U ⊕ V, is defined thus:

U ⊕ V = \{\overline{u} + \overline{v} : \overline{u} ∈ U, \overline{v} ∈ V \} .

We define

U ∨ V = [U ∪ V]
U + V = [U ⊕ V]
0 = [\overline{0}] = \{\overline{0}\} .

We define the operations in CI(ℕ^{n}) and CF (ℕ^{n}) in a similar fashion. Suppose that U, V ∈ CI(ℕ^{n}) and U′, V′ ∈ CF (ℕ^{n}). We set

U ∨ V = [(U ∪ V]]
U + V = [(U ⊕ V]]
U′ ∧ V′ = [[U′ ∪ V′)]
U′ + V′ = [[U′ ⊕ V′)] .

Moreover, we define 0 = (\overline{0}] = \{\overline{0}\} in CI(ℕ^{n}), and 0 = [\overline{0}) = ℕ^{n} in CF (ℕ^{n}).

Proposition 3.14 Each of the structures

C(ℕ^{n}) = (C(ℕ^{n}), ∨, +, 0) ,
CI(ℕ^{n}) = (CI(ℕ^{n}), ∨, +, 0) and
CF (ℕ^{n}) = (CF (ℕ^{n}), ∧, +, 0)

is a ciw-semiring. In addition, CI(ℕ^{n}) satisfies the equation

x ∨ 0 = x ,  (5)

and CF (ℕ^{n}) the equation

x ∧ 0 = 0 .  (6)

Proof: These facts can be derived easily from properties of closure operators and the complex sum operation ⊕, using Propositions 3.3 and 3.4. □

Note that (5) can be rephrased, with respect to E_{ciw}, as the inequation 0 ≤ x, and (6) as x ≥ 0. Also, writing ∨ for ∧, equation (6) takes the form x ∨ 0 = 0 that one should have if ∨ is considered to be the signature symbol instead of ∧.

For any structure A, we use V(A) to denote the variety generated by A, i.e., the class of algebras that satisfy the equations that hold in A. Our order of business will now be to offer concrete descriptions of the finitely generated free algebras in the varieties generated by Z_{∨}, N_{∨} and N_{∧}.

Theorem 3.15 For each n ≥ 0, C(ℕ^{n}) is freely generated in V(Z_{∨}) by the sets [\overline{u}_{i}], i ∈ [n].

Proof: Each C ∈ C(ℕ^{n}) may be written as ⋁_{\overline{c}∈C}\{\overline{c}\}, and, for each \overline{c} = (c_{1}, …, c_{n}) ∈ ℕ^{n}, it holds that \{\overline{c}\} = ∑_{i=1}^{n} c_{i}[\overline{u}_{i}]. It follows that C(ℕ^{n}) is generated by the sets [\overline{u}_{i}]. Suppose now that h is a function \{[\overline{u}_{1}], …, [\overline{u}_{n}]\} → ℤ, say h : [\overline{u}_{i}] ↦ x_{i}, i ∈ [n]. We need to show that h uniquely extends to a homomorphism h^{♯} : C(ℕ^{n}) → Z_{∨}. For each set C ∈ C(ℕ^{n}), define

h^{♯}(C) = ⋁_{\overline{c}∈C} \overline{c}\overline{x} ,

where \overline{x} is the vector (x_{1}, …, x_{n}). It is clear that h^{♯}([\overline{u}_{i}]) = x_{i}, for all i ∈ [n], and that h^{♯}(0) = 0. Also, if F is a nonempty finite subset of ℕ^{n}, then, by Proposition 3.9,

h^{♯}([F]) = ⋁_{\overline{u}∈[F]} \overline{u}\overline{x}
= ⋁_{\overline{u}∈F} \overline{u}\overline{x} .

Thus, for C, D ∈ C(ℕ^{n}),

h^{♯}(C ∨ D) = h^{♯}([C ∪ D])
= ⋁_{\overline{u}∈C∪D} \overline{u}\overline{x}
= ⋁_{\overline{c}∈C} \overline{c}\overline{x} ∨ ⋁_{\overline{d}∈D} \overline{d}\overline{x}
= h^{♯}(C) ∨ h^{♯}(D) .

Also,

h^{♯}(C + D) = h^{♯}([C ⊕ D])

= ⋁_{\overline{u}∈C⊕D} \overline{u}\overline{c}
= ⋁_{\overline{c}∈C} \overline{c}\overline{x} + ⋁_{\overline{d}∈D} \overline{d}\overline{x}
= h^{♯}(C) + h^{♯}(D) ,

since + distributes over ∨. This proves that h^{♯} is a homomorphism. The fact that h^{♯} is the only homomorphic extension of h is clear.

We still need to verify that C(ℕ^{n}) belongs to V(Z_{∨}). To this end, for each \overline{x} = (x_{1}, …, x_{n}) ∈ ℤ^{n}, let h\overline{x} denote the homomorphism C(ℕ^{n}) → Z_{∨} described above taking [\overline{u}_{i}] to x_{i}, i ∈ [n]. If C, D ∈ C(ℕ^{n}) with \overline{d} ∈ D − C, say, then, by Proposition 3.9,

\overline{d}\overline{y} > ⋁_{\overline{c}∈C} \overline{c}\overline{y} ,

for some \overline{y} ∈ ℤ^{n}. Thus, it holds that h\overline{y}(D) > h\overline{y}(C). It follows that the target tupling of the functions h\overline{x} is an injective homomorphism from C(ℕ^{n}) to a direct power of Z_{∨}, proving that C(ℕ^{n}) belongs to V(Z_{∨}). □

Free algebras in V(N_{∨}) and V(N_{∧}) have a similar description.

Theorem 3.16 For each n ≥ 0, CI(ℕ^{n}) is freely generated in V(N_{∨}) by the sets (\overline{u}_{i}], i ∈ [n]. Moreover, CF (ℕ^{n}) is freely generated in V(N_{∧}) by the sets [\overline{u}_{i}), i ∈ [n].

Proof: The argument is similar to the proof of Theorem 3.15. We outline the proof of the second claim.

First, the convex filters [\overline{u}_{i}), i ∈ [n], form a generating system of CF (ℕ^{n}). This follows from Corollary 3.7 by noting that if U is the convex filter generated by the finite nonempty set F, then

U = ⋀_{\overline{c}∈F}[\overline{c}) .

Moreover, for each \overline{c} = (c_{1}, …, c_{n}) ∈ ℕ^{n}, it holds that

[\overline{c}) = ∑_{i=1}^{n} c_{i}[\overline{u}_{i}) .

Let h be the assignment [\overline{u}_{i}) ↦ x_{i} ∈ ℕ, i ∈ [n]. By the above argument, h has at most one extension to a homomorphism h^{♯} : CF (ℕ^{n}) → N_{∧}. Define h^{♯} by

h^{♯}(U) = ⋀_{\overline{c}∈U} \overline{c}\overline{x} ,

where \overline{x} = (x_{1}, …, x_{n}). Thus, h^{♯}(U) is the least element of the set

\{\overline{c}\overline{x} : \overline{c} ∈ U\} ⊆ ℕ .

(Actually, the above definition makes sense for any nonempty set U ⊆ ℕ^{n}.) The proof of the fact that h^{♯} preserves the operations follows the lines of the similar verification in the proof of Theorem 3.15. One uses Proposition 3.11 in lieu of Proposition 3.9. The fact that CF (ℕ^{n}) belongs to V(N_{∧}) can be shown as the corresponding fact in the proof of Theorem 3.15. □

Remark 3.17 A complete proof of the first part of Theorem 3.16 is given in [1].

Remark 3.18 In any variety, any infinitely generated free algebra is the direct limit of finitely generated free algebras. More specifically, for any cardinal number κ, the free algebra on κ generators in V(Z_{∨}) can be described as an algebra of finite nonempty convex sets in ℕ^{κ} consisting of vectors whose components, with a finite number of exceptions, are all zero. The free algebras in V(N_{∨}) and V(N_{∧}) have similar descriptions using finitely generated convex ideals and filters, respectively.

Since N_{∨} is a subalgebra of Z_{∨}, we have that V(N_{∨}) ⊆ V(Z_{∨}). Also, since N_{∧} is isomorphic to the subalgebra N_{∨}^{−} of Z_{∨}, it holds that V(N_{∧}) ⊆ V(Z_{∨}).

Definition 3.19 Let V and V′ be two varieties of algebras such that the signature of V extends that of V′. Let E be a collection of equations in the language of V. We say that V is axiomatized over V′ by E if the collection of equations that hold in V′ together with E form a basis for the identities of V. We say that V has a finite axiomatization relative to V′ if V is axiomatized over V′ by some finite set of equations E.

In the next result we show that both V(N_{∨}) and V(N_{∧}) possess a finite axiomatization relative to V(Z_{∨}). Of course, V(Z_{∨}) is just V(Z_{∧}), since Z_{∨} and Z_{∧} are isomorphic.

Theorem 3.20 The following statements hold:

1. V(N_{∨}) is axiomatized over V(Z_{∨}) by the equation (5).

2. V(N_{∧}) is axiomatized over V(Z_{∧}) by the equation (6).

Proof: Suppose that n is any nonnegative integer. By Theorem 3.15, the map [\overline{u}_{i}] ↦ (\overline{u}_{i}], i ∈ [n], extends to a unique homomorphism h : C(ℕ^{n}) → CI(ℕ^{n}). Comparing the definitions of the operations in C(ℕ^{n}) and CI(ℕ^{n}) and using the first part of Proposition 3.4, it is easy to see that h is in fact the function U ↦ [(U]], U ∈ C(ℕ^{n}). We prove that the kernel of h is the least congruence on C(ℕ^{n}) such that the quotient satisfies (5), which implies the first claim.

It is clear that the kernel of h satisfies (5). To complete the proof, we need to show that if φ is a homomorphism C(ℕ^{n}) → B, where B is in V_{ciw}^{+}, then the kernel of h is included in the kernel of φ. But, since B is in V_{ciw}^{+}, for every U ∈ C(ℕ^{n}), it holds that

φ(U) = ⋁_{\overline{u}∈U} φ([\overline{u}]) = ⋁_{\overline{u}∈(U]} φ([\overline{u}]) = ⋁_{\overline{u}∈[(U]]} φ([\overline{u}]) = φ([(U]]) ,

so that if [(U]] = [(V]], then φ(U) = φ(V).

The proof of the second claim follows similar lines, using the second part of Proposition 3.4. □

3.4 Non-Finite Axiomatizability Results

Our order of business in this section is to show that the varieties generated by the ciw-semirings Z_{∨} and N_{∧} are not finitely based. Our starting points are the results in [1] to the effect that the variety V(N_{∨}) is not finitely based. These we restate below for ease of reference and for completeness.

Theorem 3.21

1. The variety V(N_{∨}) is not finitely based.

2. For every n ∈ ℕ, the collection of all the inequations in at most n variables that hold in V(N_{∨}) does not form an equational basis for it.

We begin by using these results, and the first part of Theorem 3.20 to prove:

Theorem 3.22 The variety V(Z_{∨}) is not finitely based. Moreover, V(Z_{∨}) has no axiomatization by equations in a bounded number of variables, i.e., there exists no natural number n such that the collection of all equations in at most n variables that hold in V(Z_{∨}) forms an equational basis for V(Z_{∨}).

Proof: The first claim is an immediate consequence of the second. To prove the second claim, we argue as follows. Assume, towards a contradiction, that there is a nonzero natural number n such that the collection of all equations in at most n variables that hold in V(Z_{∨}) forms an equational basis for V(Z_{∨}). Then, by the first part of Theorem 3.20, this collection of equations together with (5) forms an equational basis for V(N_{∨}) consisting of equations in at most n variables. However, this contradicts the second statement in Theorem 3.21. □

An alternative proof of the above result will be sketched in Remark 3.38 to follow.

We now proceed to apply the results that we have developed so far to the study of the axiomatizability of the equational theory of the algebra N_{∧}.

Our aim in the remainder of this section is to prove the following result to the effect that the variety V(N_{∧}) has no finite equational basis.

Theorem 3.23 The variety V(N_{∧}) has no finite (equational) axiomatization, i.e., there is no finite set E of equations, which hold in V(N_{∧}), and such that for all terms t_{1}, t_{2},

V(N_{∧}) ⊧ t_{1} = t_{2} iff E proves t_{1} = t_{2} .

To prove Theorem 3.23, we begin by noting that the following equations e_{n}^{∧} hold in N_{∧}, for each n ≥ 2:

e_{n}^{∧} : r_{n} ∧ s_{n} = s_{n} ,  (7)

where

r_{n} = x_{1} + ⋯ + x_{n}
s_{n} = (2x_{1} + x_{3} + x_{4} + ⋯ + x_{n−1} + x_{n})
∧ (x_{1} + 2x_{2} + x_{4} + ⋯ + x_{n−1} + x_{n})
⋮
∧ (x_{1} + x_{2} + x_{3} + ⋯ + x_{n−2} + 2x_{n−1})
∧ (x_{2} + x_{3} + x_{4} + ⋯ + x_{n−1} + 2x_{n}) .

In what follows, we shall define a sequence of ciw-semirings B_{n} (n ≥ 3) such that following holds:

For any finite set E of equations which hold in V(N_{∧}), there is an n ≥ 3 such that

B_{n} ⊧ E but B_{n} |̸= e_{n}^{∧} .

In fact, as we shall see in due course, the algebra construction that we now proceed to present also yields the following stronger result.

Theorem 3.24 There exists no natural number n such that the collection of all equations in at most n variables that hold in V(N_{∧}) forms an equational basis for V(N_{∧}).

Using Theorem 3.24, it is a simple matter to prove Theorem 3.23.

Proof of Theorem 3.23: Given a finite set E of equations that hold in V(N_{∧}), let n denote an integer larger than the number of variables in any equation belonging to E. Since the equations in at most n variables that hold in V(N_{∧}) do not form an equational basis for V(N_{∧}), the equations in E do not give an equational axiomatization of V(N_{∧}) either. □

The remainder of this section will be devoted to the proof of Theorem 3.24. We begin with some preliminary definitions and results that will pave the way to the construction of the algebras B_{n}.

Definition 3.25 The weight of a vector \overline{v} = (v_{1}, …, v_{n}) in ℕ^{n} is defined as v_{1} + ⋯ + v_{n}. The weight of a nonempty set U ⊆ ℕ^{n} is the minimum of the weights of the vectors in U.

Lemma 3.26 Let U be a nonempty subset of ℕ^{n}. If the weight of U is k, then so is the weight of [[U)]. Moreover, a weight k vector belongs to [[U)] iff it is a convex linear combination of some vectors of weight k in U.

We introduce the following notations for some vectors in ℕ^{n} related to the equation e_{n}^{∧}:

\overline{δ} = (1, …, 1)
\overline{γ}_{1} = (2, 0, 1, 1, …, 1, 1)
\overline{γ}_{2} = (1, 2, 0, 1, …, 1, 1)
⋮
\overline{γ}_{n−1} = (1, 1, 1, 1, …, 2, 0)
\overline{γ}_{n} = (0, 1, 1, 1, …, 1, 2) ,

so that in \overline{γ}_{i} (i ∈ [n]), the 2 is on the ith position and is followed by a 0. (Of course, we assume that the first position follows the nth.) All other components are 1’s. Note that

\overline{δ} = \frac{1}{n}\overline{γ}_{1} + ⋯ + \frac{1}{n}\overline{γ}_{n} .  (8)

Thus, \overline{δ} belongs to the convex filter generated by the vectors \overline{γ}_{i} (i ∈ [n]). Moreover, the system consisting of any n of the vectors \overline{δ}, \overline{γ}_{1}, …, \overline{γ}_{n} is linearly independent (cf. [1, Lemma 5.2]).

We define:

Γ = [[\{\overline{γ}_{1}, …, \overline{γ}_{n}\})]
Δ = Γ − \{\overline{δ}\} ,

so that Γ is the convex filter generated by the \overline{γ}_{i} (i ∈ [n]). Note that the only vectors of weight n in Γ are \overline{δ} and the \overline{γ}_{i} (i ∈ [n]). By (8), the set Δ is not a convex filter.

Lemma 3.27 Suppose that a nonempty subset U of ℕ^{n} satisfies:

1. The weight of U is greater than or equal to n.

2. Any vector of weight n in U belongs to the set \{\overline{δ}, \overline{γ}_{1}, …, \overline{γ}_{n}\}.

Then every vector of weight n in [[U)] lies in the set \{\overline{δ}, \overline{γ}_{1}, …, \overline{γ}_{n}\}. Moreover, \overline{γ}_{i} ∈ [[U)] iff \overline{γ}_{i} ∈ U, and \overline{δ} ∈ [[U)] iff \overline{δ} ∈ U or \{\overline{γ}_{1}, …, \overline{γ}_{n}\} ⊆ U.

Proof: Suppose that \overline{u} ∈ [[U)] has weight n. Then, by Lemma 3.26, \overline{u} is a convex linear combination of weight n vectors in U, and hence a convex linear combination of the vectors \overline{δ}, \overline{γ}_{1}, …, \overline{γ}_{n}. It follows that no component of \overline{u} is greater than 2 and at most one component is 0. Moreover, if the ith component of \overline{u} is 2, for some i, then necessarily \overline{u} = \overline{γ}_{i}. Suppose that \overline{u} = \overline{δ}. Then, since any n of the vectors \overline{δ}, \overline{γ}_{1}, …, \overline{γ}_{n} form a linearly independent system, and since \overline{δ} is a convex linear combination of the \overline{γ}_{i} (i ∈ [n]), it follows that either \overline{δ} ∈ U or \{\overline{γ}_{1}, …, \overline{γ}_{n}\} ⊆ U. □

Corollary 3.28 The unique minimal generating set of Γ is \{\overline{γ}_{1}, …, \overline{γ}_{n}\}.

Lemma 3.29 Suppose that F is a convex filter in ℕ^{n} properly included in Γ. Then F − \{\overline{δ}\} is also a convex filter.

Proof: This is clear if \overline{δ} ∉ F, so assume \overline{δ} ∈ F. Clearly, F − \{\overline{δ}\} is a convex filter unless \overline{δ} ∈ [[F − \{\overline{δ}\})]. But since each vector of weight n in F − \{\overline{δ}\} is one of the \overline{γ}_{i}, and since at least one \overline{γ}_{i} is not in F − \{\overline{δ}\}, by Lemma 3.27 we have that \overline{δ} ∉ [[F − \{\overline{δ}\})]. □

We now proceed to define the algebras B_{n} = (B_{n}, ∧, +, 0), for every n > 0.

Let B_{n} consist of the nonempty convex filters in ℕ^{n} and the set Δ = Γ−\{\overline{δ}\}. The following results will allow us to endow B_{n} with the structure of a ciwsemiring.

Corollary 3.30 If F is a convex filter, then F ∩ Δ ∈ B_{n}.

Proof: Clearly, it holds that F ∩ Δ = (F ∩ Γ) ∩ Δ. Thus we may assume that F is included in Γ. If F = Γ, the intersection is Δ. Otherwise F is properly included in Γ and F ∩ Δ = F − \{\overline{δ}\} ∈ B_{n}, by the previous lemma. □

Proposition 3.31 If the intersection of a family of sets in B_{n} is not empty, then the intersection is in B_{n}.

Proof: Let U_{i}, i ∈ I, be a family of sets in B_{n} such that U = ⋂_{i∈I} U_{i} is nonempty. If each U_{i} is different from Δ, then U is a nonempty convex filter and is thus in B_{n}. Otherwise, we have that

U = Δ ∩ ⋂{U_{i} : i ∈ I, U_{i} ≠ Δ} ,

and the result follows by the previous corollary. □

For each nonempty set U ⊆ ℕ^{n}, let cl(U) denote the least set in B_{n} containing U. (This set exists in light of the proposition above.) For each U, V ∈ B_{n}, we define

U + V = cl(U ⊕ V)
U ∧ V = cl(U ∪ V) .

Moreover, we define the constant 0 to be the set [[\overline{0})] = [\overline{0}) = ℕ^{n}. This completes the definition of the algebra B_{n} = (B_{n}, ∧, +, 0).

Recall that CF (ℕ^{n}) is freely generated by the sets [\overline{u}_{i}), i ∈ [n], in the variety generated by N_{∧}. The following result, whose easy proof is omitted, will be useful in the proof of Propn. 3.37 to follow.

Lemma 3.32 The function given by Δ ↦ Γ and U ↦ U, if U ≠ Δ, defines a homomorphism B_{n} → CF (ℕ^{n}).

To show that B_{n} is a ciw-semiring, we need:

Lemma 3.33 When n ≥ 3, the filter Γ has no decomposition in CF (ℕ^{n}) into the sum of two nonzero convex filters. Similarly, when n ≥ 3, neither Γ nor Δ has a nontrivial decomposition in B_{n} into the sum of two nonzero sets.

Proof: First we work in CF (ℕ^{n}).

Assume, towards a contradiction, that n ≥ 3, F and G are nonempty convex filters with F + G = Γ in CF (ℕ^{n}), but F, G ≠ ℕ^{n}. Let k denote the weight of F and ℓ the weight of G. Then k, ℓ > 0 and k + ℓ = n. Let F′ denote the set of all vectors of weight k in F, and define G′ ⊆ G in similar fashion. By Corollary 3.28, we have that

\{\overline{γ}_{1}, …, \overline{γ}_{n}\} ⊆ F′ ⊕ G′ ⊆ \{\overline{γ}_{1}, …, \overline{γ}_{n}, \overline{δ}\} .

Suppose that F′, say, contains a vector \overline{u} which has a component equal to 2. Then there exists an i ∈ [n] such that \overline{u} + \overline{v} = \overline{γ}_{i} for all \overline{v} ∈ G′. Hence G′ contains a unique vector and \overline{γ}_{i} is the only element of \{\overline{γ}_{1}, …, \overline{γ}_{n}\} contained in F′ ⊕ G′, contradicting Corollary 3.28. Thus, F′ contains no vector having a component equal to 2, and similarly for G′.

Since the complex sum of F′ and G′ contains the vectors \overline{γ}_{1} and \overline{γ}_{2}, there are vectors \overline{w}_{1}, \overline{w}_{2} ∈ F′ and \overline{v}_{1}, \overline{v}_{2} ∈ G′ such that

\overline{w}_{1} + \overline{v}_{1} = \overline{γ}_{1} and \overline{w}_{2} + \overline{v}_{2} = \overline{γ}_{2} .

This means that, for some b_{3}, …, b_{n} ∈ {0, 1},

\overline{w}_{1} = (1, 0, b_{3}, …, b_{n}) and
\overline{v}_{1} = (1, 0, b̃_{3}, …, b̃_{n}) ,

where b̃ denotes the complement of b, for every b ∈ {0, 1}. Similarly, since n ≥ 3, there are c_{1}, c_{4}, …, c_{n} ∈ {0, 1} such that

\overline{w}_{2} = (c_{1}, 1, 0, c_{4}, …, c_{n}) and
\overline{v}_{2} = (c̃_{1}, 1, 0, c̃_{4}, …, c̃_{n}) .

It is now easy to see that if \overline{w}_{1} + \overline{v}_{2} is in \{\overline{γ}_{1}, …, \overline{γ}_{n}, \overline{δ}\}, then \overline{w}_{2} + \overline{v}_{1} is not. Indeed, if \overline{w}_{1} + \overline{v}_{2} is in \{\overline{γ}_{1}, …, \overline{γ}_{n}, \overline{δ}\}, then c̃_{1} = 0, so that c_{1} = 1. Thus the first two components of \overline{w}_{2} + \overline{v}_{1} are 2 and 1, respectively. This contradicts our assumption that F′ ⊕ G′ is included in \{\overline{γ}_{1}, …, \overline{γ}_{n}, \overline{δ}\}.

Assume now that F +G ∈ {Γ, Δ} in B_{n}. If F, G ∈ CF (ℕ^{n}), then F +G = Γ in CF (ℕ^{n}). By the first claim, this is possible only if F or G is 0. If F = Δ, say, then G must be 0, or else F ⊕ G would only contain vectors whose weight is greater than n. This completes the proof. □

Remark 3.34 When n = 2, the set Δ does not have a non-trivial representation as the sum of two non-zero elements of B_{n}, but we have

[[{(1, 0), (0, 1)})] + [[{(1, 0), (0, 1)})] = Γ

both in B_{n} and in CF (ℕ^{n}).

Proposition 3.35 If n ≥ 3, then B_{n} is a ciw-semiring satisfying x ∧ 0 = 0.

Proof: It is obvious that both binary operations are commutative and that ∧ is idempotent. Also, the equation x∧0 = 0 holds. The fact that ∧ is associative follows from general properties of closure operators. In fact,

(A ∧ B) ∧ C = cl(A ∪ B ∪ C) = A ∧ (B ∧ C) ,

for all A, B, C ∈ B_{n}. The facts that also

(A + B) + C = A + (B + C)
(A ∧ B) + C = (A + C) ∧ (B + C)

hold follow by Lemma 3.33. The only way that these equations can fail is that one side is Δ and the other is Γ. But in that case one of A, B, C is 0, by Lemma 3.33, and then both equations hold obviously. □

Remark 3.36 For all A, B, C ∈ B_{n}, we have that

A + B + C = cl(A ⊕ B ⊕ C) .

The following result is the crux of the proof of Theorem 3.24.

Proposition 3.37 For each n ≥ 3, the algebra B_{n} satisfies any equation in at most n − 1 variables which holds in N_{∧}.

Proof: It suffices to show that B_{n} ⊧ t ≥ t′ for any simple ∧-inequation t ≥ t′ such that N_{∧} ⊧ t ≥ t′ and both t and t′ contain the same at most m < n variables, so that t = t(x_{1}, …, x_{m}) and t′ = t′(x_{1}, …, x_{m}), say. By Lemma 3.32, we only need to show that for all U_{1}, …, U_{m} in B_{n}, it is not possible that \overline{δ} ∈ V and Δ = V′, where V = t(U_{1}, …, U_{m}) and V′ = t′(U_{1}, …, U_{m}).

Assume, towards a contradiction, that for some U_{i} ∈ B_{n}, i ∈ [m], we have \overline{δ} ∈ V and Δ = V′, and that t ≥ t′ is a simple inequation in fewest variables for which this holds. Note that this implies that U_{i} ≠ 0 for every i ∈ [m]. Clearly, the weight of each U_{i} is at most n. Also, if the weight of some U_{i} is n, then m = 1 and t = x_{1}. Since t ≥ t′ holds in N_{∧} and t′ also contains x_{1}, it follows that t′ = x_{1} modulo the equations of ciw-semirings. But then t = t′ holds in B_{n}, contrary to our assumption. Thus, each U_{i} is different from Δ and is thus a nonempty convex filter. Since V ≠ Δ, it holds that V = t(U_{1}, …, U_{m}) also in CF (ℕ^{n}). Moreover, we have that t′(U_{1}, …, U_{m}) = Γ in CF (ℕ^{n}). By Lemma 3.33, it holds that V ≠ Γ. Since t ≥ t′ holds in CF (ℕ^{n}), we have that V ⊆ Γ.

Now write t′ = t′_{1} ∧ ⋯ ∧ t′_{k}, where the t′_{i} are linear combinations of the variables x_{1}, …, x_{m}. For each i ∈ [k], let V′_{i} = t′_{i}(U_{1}, …, U_{m}) in B_{n}. Each V′_{i} is included in Δ, and is in fact a proper subset of Δ, since Δ has no nontrivial decomposition in B_{n} into the sum of two sets (Lemma 3.33). Thus, each V′_{i} is a nonempty convex filter, and V′_{i} = t′_{i}(U_{1}, …, U_{m}) also in CF (ℕ^{n}). Call a t′_{i}, and the corresponding V′_{i}, relevant if the weight of V′_{i} is n. In that case V′_{i} contains some, but not all of the \overline{γ}_{1}, …, \overline{γ}_{n}, and no other vector of weight less than or equal to n. (Each relevant V′_{i} cannot contain all of the vectors \overline{γ}_{1}, …, \overline{γ}_{n}, or else, being a convex filter, it would also contain the vector \overline{δ}. This would contradict our assumption that \overline{δ} ∉ V′.)

Suppose that \overline{w}_{j} ∈ U_{j}, j ∈ [m], have minimal weight. Then for every relevant t′_{i} = ∑_{j∈[m]} c_{ij}x_{j}, it holds that ∑_{j∈[m]} c_{ij}\overline{w}_{j} has weight n and thus must be in \{\overline{γ}_{1}, …, \overline{γ}_{n}\} (Lemma 3.27). Hence, no c_{ij} can be greater than 2, and there cannot be two coefficients equal to 2. The same fact holds for the coefficients in the linear term t. Thus, two cases arise.

Case 1: t = x_{1} + ⋯ + x_{m}. Since \overline{δ} ∈ V and V is a proper subset of Γ, by Lemma 3.27 there exist vectors \overline{w}_{j} ∈ U_{j}, j ∈ [m], with \overline{δ} = \overline{w}_{1} + ⋯ + \overline{w}_{m}. Since the operations are monotonic, we may also assume that U_{j} = [[\overline{w}_{j})], for all j ∈ [m]. Indeed, we have, in B_{n},

\overline{δ} ∈ t([[\overline{w}_{1})], …, [[\overline{w}_{m})])

and

\overline{δ} ∉ t′([[\overline{w}_{1})], …, [[\overline{w}_{m})]) ,

since t′([[\overline{w}_{1})], …, [[\overline{w}_{m})]) ⊆ t′(U_{1}, …, U_{m}) = Δ. But if t′([[\overline{w}_{1})], …, [[\overline{w}_{m})]) is not Δ, then it is in CF (ℕ^{n}), and we may infer that

t([[\overline{w}_{1})], …, [[\overline{w}_{m})]) ⊆ t′([[\overline{w}_{1})], …, [[\overline{w}_{m})]) ,

contradicting the fact that \overline{δ} ∈ t([[\overline{w}_{1})], …, [[\overline{w}_{m})]) and \overline{δ} ∉ t′([[\overline{w}_{1})], …, [[\overline{w}_{m})]). Thus, t′([[\overline{w}_{1})], …, [[\overline{w}_{m})]) = Δ. Actually, we may assume that U_{j} = [[\overline{w}_{j})], for all j ∈ [m].

Assume that \overline{w}_{1} has two or more components equal to 1, say the first and the second components are 1. Since \overline{γ}_{1} ∈ Γ = t′(U_{1}, …, U_{m}) in CF (ℕ^{n}), there is a relevant t′_{i} with \overline{γ}_{1} ∈ V′_{i}. This is possible only if \overline{γ}_{1} = ∑_{j∈[m]} c_{ij}\overline{w}_{j}. But in that case the coefficient c_{i1} is 2. Thus, the first two components of \overline{γ}_{1} would be 2, which is contradiction. Hence \overline{w}_{1} has a single component equal to 1. In the same way, each of the vectors \overline{w}_{j} is a unit vector, and m = n follows, contrary to our assumption that m < n.

Case 2: t = 2x_{1} + x_{2} + ⋯ + x_{m}. In this case, we may assume that there exist \overline{w}_{1}, …, \overline{w}_{m} and \overline{v}_{1} with \overline{v}_{1} + \overline{w}_{1} + ⋯ + \overline{w}_{m} = \overline{δ}, U_{1} = [[\overline{w}_{1}, \overline{v}_{1})] and U_{j} = [[\overline{w}_{j})], for j ≥ 2. Clearly, \overline{w}_{1} and \overline{v}_{1} have equal weight, for otherwise V would contain a vector of weight strictly smaller than n. Again, we can conclude that \overline{v}_{1} and each \overline{w}_{j} have exactly one nonzero component, which is a 1. Using this, a contradiction is easily reached. Suppose that the first component of \overline{w}_{1} is 1, say. Then there must be some i such that t′_{i} = 2x_{1} + x_{2} + ⋯ + x_{m}. But then t ≥ t′ clearly holds in B_{n}. □

We are now ready to prove Theorem 3.24.

Proof of Theorem 3.24: Given an integer n ≥ 3, consider the algebra B_{n} and the simple inequation r_{n} ≥ s_{n}, where the terms r_{n} and s_{n} were defined below equation (7). For each i ∈ [n], let \overline{u}_{i} denote the ith n-dimensional unit vector whose components are all 0 except for a 1 in the ith position. We have

r_{n}([[\overline{u}_{1})], …, [[\overline{u}_{n})]) = [[\overline{δ})] and
s_{n}([[\overline{u}_{1})], …, [[\overline{u}_{n})]) = Δ

in B_{n}. Thus B_{n} |̸= r_{n} ≥ s_{n}, i.e., B_{n} |̸= e_{n}^{∧}. On the other hand e_{n}^{∧} holds in V(N_{∧}), and moreover, by Proposition 3.37, B_{n} satisfies all identities in at most n−1 variables that hold in V(N_{∧}). Hence, the collection of identities in at most n − 1 variables that hold in V(N_{∧}) does not prove e_{n}^{∧}, and thus is not a basis for V(N_{∧}). □

Remark 3.38 The model construction upon which the proof of Theorem 3.24 is based is similar in spirit to the one we used in [1] to show that the variety V(N_{∨}) is not finitely based. The proof of that result was based upon the realization that the family of equations e_{n} below hold in N_{∨}, and in fact in Z_{∨}, for each n ≥ 2:

e_{n} : r_{n} ∨ q_{n} = q_{n} ,  (9)

where r_{n} was defined below (7) and

q_{n} = (2x_{1} + x_{3} + x_{4} + ⋯ + x_{n−1} + x_{n})
∨ (x_{1} + 2x_{2} + x_{4} + ⋯ + x_{n−1} + x_{n})
⋮
∨ (x_{1} + x_{2} + x_{3} + ⋯ + x_{n−2} + 2x_{n−1})
∨ (x_{2} + x_{3} + x_{4} + ⋯ + x_{n−1} + 2x_{n}) .

In op. cit. we constructed a sequence of ciw-semirings A_{n} (n ≥ 2) which satisfy all the equations in at most n − 1 variables that hold in V(N_{∨}), but in which the equation e_{n} fails. This shows that the collection of equations in at most n − 1 variables that hold in V(N_{∨}) does not prove e_{n}, and thus is not a basis of identities for V(N_{∨}). Unlike the algebras B_{n}, the ciw-semirings A_{n} are finite, and consist of nonempty convex ideals contained [(\{\overline{γ}_{1}, …, \overline{γ}_{n}\}]], together with [(\{\overline{γ}_{1}, …, \overline{γ}_{n}\}]] − \{\overline{δ}\}.

The aforementioned results from [1] lead to an alternative proof of Theorem 3.22. Indeed, assume that there is a natural number n ≥ 2 such that the collection E_{n} of equations in at most n variables that hold in V(Z_{∨}) is a basis for it. Since the equation e_{n+1} holds in V(Z_{∨}), it follows that E_{n} proves e_{n+1}. However, this contradicts the aforementioned results from [1]. In fact, since N_{∨} is a subalgebra of Z_{∨}, the equations in E_{n} also hold in N_{∨}, and, thus, cannot prove e_{n+1}.

Remark 3.39 The alternative proof of Theorem 3.22 mentioned in the above remark is, in fact, applicable in a rather general setting. For the sake of this generalization, which is meant to apply to algebras whose addition operation need be neither commutative nor associative, we rephrase the family of equations in (9) as follows:

e′_{n} : r′_{n} ∨ q′_{n} = q′_{n}  (n ≥ 2) ,  (10)

where

r′_{n} = x_{1} + (x_{2} + (⋯ + x_{n}) ⋯)  and
q′_{n} = (x_{1} + (x_{1} + (x_{3} + (x_{4} + (⋯ + (x_{n−1} + x_{n}) ⋯)))))
∨ (x_{1} + (x_{2} + (x_{2} + (x_{4} + (⋯ + (x_{n−1} + x_{n}) ⋯)))))
⋮
∨ (x_{1} + (x_{2} + (x_{3} + (⋯ + (x_{n−2} + (x_{n−1} + x_{n−1})) ⋯))))
∨ (x_{2} + (x_{3} + (x_{4} + (⋯ + (x_{n−1} + (x_{n} + x_{n})) ⋯)))) .

(The join subterms in q′_{n} can be arbitrarily parenthesized.) The reader will find it easy to rephrase the family of equations e_{n}^{∧} given in (7) in similar fashion.

The argument used in the previous remark can be used to show, mutatis mutandis, that:

Theorem 3.40 Let V be any variety that contains N_{∨} (respectively, N_{∧}), and in which e′_{n} (resp., the rephrasing of e_{n}^{∧}) holds for every n ≥ 2. Then V has no axiomatization in a bounded number of variables.

Suppose that V is generated by the algebra A. Then, the proviso of the above statement is met if the following conditions hold:

1. N_{∨} (respectively, N_{∧}) embeds in A,

2. the ∨ (respectively, ∧) operation on A is a semilattice operation,

3. A is linearly ordered by the semilattice order, and the + operation is monotonic.

An application of Thm. 3.40 will be presented in Sect. 6.4.

Remark 3.41 Since N_{∨}^{−} is isomorphic to N_{∧}, Theorems 3.23 and 3.24 apply equally well to it.

We have presented several examples of nonfinitely based ciw-semirings. However, all of the ciw-semirings that we have studied so far are infinite. This prompts us to formulate the following:

Problem 3.1 Let A be a finite ciw-semiring. Is the variety V(A) finitely based?

4 Tropical Semirings

Our aim in this section will be to investigate the equational theory of the tropical semirings studied in the literature that are obtained by adding bottom elements to the ciw-semirings presented in the previous section. More specifically, we shall study the following semirings:

Z_{∨,−∞} = (ℤ ∪ {−∞}, ∨, +, −∞, 0) ,
N_{∨,−∞} = (ℕ ∪ {−∞}, ∨, +, −∞, 0) and
N_{∨,−∞}^{−} = (ℕ^{−} ∪ {−∞}, ∨, +, −∞, 0) .

Since Z_{∨,−∞}, N_{∨,−∞} and N_{∨,−∞}^{−} are isomorphic to the semirings

Z_{∧,∞} = (ℤ ∪ {∞}, ∧, +, ∞, 0)
N_{∧,∞}^{−} = (ℕ^{−} ∪ {∞}, ∧, +, ∞, 0) and
N_{∧,∞} = (ℕ ∪ {∞}, ∧, +, ∞, 0) ,

respectively, the results that we shall obtain apply equally well to these algebras.

The semirings Z_{∧,∞} and N_{∧,∞} are usually referred to as the equatorial semiring [22] and the tropical semiring [34], respectively. The semiring N_{∨,−∞} is called the polar semiring in [24].

Our study of the equational theory of these algebras will proceed as follows. First, we shall offer some general facts relating the equational theory of a ciwsemiring A to the theory of the ci-semiring A_{⊥} defined in Sect. 2. In particular, in Sect. 4.1 we shall provide a necessary and sufficient condition that ensures that A and A_{⊥} satisfy the same equations in the language of ciw-semirings, and a necessary and sufficient condition ensuring the validity of a simple inequation in A_{⊥} for positive ciw-semirings A. We use these conditions to relate the non-finite axiomatizability of V(A_{⊥}) to the non-finite axiomatizability of V(A). Then, in Sect. 4.2, we shall apply our general study to derive the facts that all tropical semirings have exponential time decidable, but non-finitely based equational theory. Our general results, together with those proven in Sect. 3, will also give geometric characterizations of the valid equations in the tropical semirings Z_{∨,−∞} and N_{∨,−∞}^{−}, and thus in Z_{∧,∞} and N_{∧,∞}^{−}, but not in N_{∨,−∞}, or in the isomorphic semiring N_{∧,∞}^{−}. The task of providing a geometric description of the valid equations for these semirings will be accomplished in Sect. 4.3, where we shall also show that V(N_{∨,−∞}) can be axiomatized over V(Z_{∨,−∞}) by a single equation.

4.1 Adding ⊥

In Sect. 2, we saw how to generate a ci-semiring A_{⊥} = (A_{⊥}, ∨, +, ⊥, 0) from any ciw-semiring A = (A, ∨, +, 0) by freely adding a bottom element ⊥ to it. We now proceed to study some general relationships between the equational theories of these two structures. The results that we shall obtain will be applied in Sect. 4.2 to obtain decidability and non-finite axiomatizability results for the tropical semirings associated with the ciw-semirings we studied in Sect. 3.

Recall that a simple inequation in the variables x_{1}, …, x_{n} is of the form

t ≤ ⋁_{i∈[k]} t_{i} ,

where k > 0, and t and the t_{i} (i ∈ [k]) are linear combinations of the variables x_{1}, …, x_{n}.

Definition 4.1 A simple inequation t ≤ t′ is called nonexpansive if every variable that occurs in t′ also occurs in t.

Suppose that t ≤ t′ is a simple inequation. We say that t ≤ t′ has a kernel, or that the kernel of t ≤ t′ exists, if t′ contains at least one linear subterm all of whose variables appear in t. Moreover, in this case we say that the kernel of t ≤ t′ is the simple inequation t ≤ t′′, where the linear terms of t′′ are those linear terms of t′ whose variables all appear in t.

Thus, if t ≤ t′ is nonexpansive, then its kernel is the inequation t ≤ t′. Note that the kernel of a simple inequation that holds in a ciw-semiring A need not hold in A. For example, the simple inequation x ≤ (x + y) ∨ 0 holds in every positive ciw-semiring, but its kernel x ≤ 0 only holds in trivial positive semirings.

Example 4.2 The kernel of x ≤ x ∨ y is x ≤ x. The inequations 0 ≤ x and x ≤ x + y ∨ x + z have no kernel.

Lemma 4.3 Suppose that A is a ciw-semiring. Then a simple inequation holds in A_{⊥} iff it has a kernel that holds in A. Thus, if an inequation is nonexpansive, then it holds in A iff it holds in A_{⊥}.

Proof: Suppose that t ≤ t′ is a simple inequation. If it has no kernel, then each linear subterm of t′ contains a variable not occurring in t. Assign 0 to the variables that occur in t, and ⊥ to any other variable. It follows that t evaluates to 0 while t′ evaluates to ⊥, proving that t ≤ t′ does not hold in A_{⊥}. Assume now that t ≤ t′ has kernel t ≤ t′′. If A |̸= t ≤ t′′ then for some evaluation in A of the variables appearing in t we have that the value of t in the algebra A, denoted a, is not less than, or equal to, the value b of t′′. Assign ⊥ to all other variables appearing in t′. Since in A_{⊥} term t evaluates to a and t′ evaluates to b, it follows that t ≤ t′ does not hold in A_{⊥}. On the other hand, if A ⊧ t ≤ t′′, then A_{⊥} ⊧ t ≤ t′. Indeed, this is clear when t evaluates to ⊥. Assume that t evaluates to an element of A, the carrier set of A. Then the value of each variable occurring in t belongs to the set A. Thus, since each variable of t′′ appears in t and since t ≤ t′′ holds in A, we have that the value of t is less than, or equal to, the value of t′′, which in turn is less than, or equal to, the value of t′. □

The above lemma has a number of useful corollaries relating the equational theory of a ciw-semiring with that of the free ci-semiring it generates.

Corollary 4.4 The following conditions are equivalent for a ciw-semiring A:

1. Every simple inequation that holds in A also holds in A_{⊥}.

2. Every equation in the language of ciw-semirings that holds in A also holds in A_{⊥}.

3. A and A_{⊥} satisfy the same equations in the language of ciw-semirings.

4. For each simple inequation that holds in A, the kernel of the inequation exists and holds in A.

5. There exists a set E of nonexpansive simple inequations such that E_{ciw} ∪E is an axiomatization of V(A).

When these conditions hold, V(A_{⊥}) is axiomatized by E_{ci} ∪ E, where E is given as above.

Corollary 4.5 Suppose that each simple inequation that holds in A has a kernel that holds in A. Then an equation in the language of ciw-semirings holds in A iff it holds in A_{⊥}.

Corollary 4.6 Suppose that each inequation that holds in A has a kernel that holds in A. Then V(A_{⊥}) is axiomatized over V(A) by the equations

x ∨ ⊥ = x  (11)
x + ⊥ = ⊥ .  (12)

The following result will allow us to lift (non)finite axiomatizability results from ciw-semirings to the free ci-semirings they generate.

Corollary 4.7 Suppose that each inequation that holds in A has a kernel that holds in A. Then V(A) has a finite axiomatization iff V(A_{⊥}) has. Moreover, V(A) has an axiomatization by equations in a bounded number of variables iff V(A_{⊥}) has.

Proof: We first prove that V(A) has a finite axiomatization iff so does V(A_{⊥}). One direction is obvious from Cor. 4.6. Suppose now that V(A_{⊥}) has a finite axiomatization. Then, by Cor. 4.6 and the compactness theorem, there is a finite set E of simple equations that hold in A such that E_{ci} ∪ E together with (11) and (12) is an axiomatization of V(A_{⊥}). Since simple inequations that hold in A have kernels that hold in A, we may assume that each inequation in E is nonexpansive. We claim that E_{ciw} ∪ E is an axiomatization of V(A). Indeed, all of the equations in E_{ciw} ∪ E hold in A. Assume that there is an equation t = t′ that holds in A but fails in a model B of the set of equations E_{ciw} ∪ E. Then consider the ci-semiring B_{⊥}. By Lemma 4.3, it satisfies each simple inequation in E, so that B_{⊥} is a model of E_{ci} ∪ E. But since t = t′ fails in B, it also fails in B_{⊥}, contradicting the fact that E_{ci} ∪E is an axiomatization of V(A). Thus, E_{ciw} ∪ E proves each equation that holds in A, so that V(A) has a finite axiomatization. The same reasoning proves that if V(A_{⊥}) has an equational axiomatization in a bounded number of variables, then V(A) also has such an axiomatization. □

We now turn to positive ciw-semirings.

Definition 4.8 An equation is regular if its two sides contain the same variables (cf., e.g., [37]). An inequation is regular if every variable contained in the left-hand side of the inequation also appears on the right-hand side. An inequation is strictly regular if its two sides contain the same variables.

Thus, a simple inequation is strictly regular iff it is regular and nonexpansive.

Lemma 4.9 Suppose that A is a nontrivial positive ciw-semiring and t ≤ t′ is a simple inequation that holds in A. Then t ≤ t′ is regular, i.e., every variable that appears in t also appears in t′.

Proof: Assume to the contrary that t contains a variable x which does not appear in t′. Then, substituting 0 for all other variables occurring in t or t′, we obtain that A satisfies the inequation nx ≤ 0, where n denotes the nonzero coefficient of x in t. Since A is positive it satisfies 0 ≤ x and hence x ≤ nx. It follows that x = 0 holds in A, contradicting the assumption that A is nontrivial. □

Lemma 4.10 Suppose that A is a nontrivial positive ciw-semiring. Then for each simple inequation t ≤ t′ that holds in A there is a strictly regular inequation t ≤ t′′ that also holds in A such that E_{ciw}^{+} ∪ {t ≤ t′′} proves t ≤ t′.

Proof: Let t′′ be the simple term that results from t′ by substituting 0 for each variable that does not occur in t. □

We call the nonexpansive, in fact strictly regular, inequation t ≤ t′′ constructed above the projection of t ≤ t′.

Lemma 4.11 Suppose that A is a nontrivial positive ciw-semiring. Then a simple inequation holds in A_{⊥} iff it has a strictly regular kernel that holds in A.

Proof: This follows from Lemmas 4.3 and 4.9. □

Corollary 4.12 Suppose that A is a nontrivial positive ciw-semiring. Then V(A) is axiomatized by the set of equations E_{ciw}^{+} ∪ E, where E denotes the set of all strictly regular equations that hold in A. Moreover, V(A_{⊥}) is axiomatized by E_{ci} ∪ E.

Proof: For the first part, we need to show that whenever an algebra B satisfies all the equations in E_{ciw}^{+} ∪ E, then B satisfies any equation that holds in A. But, with respect to E_{ciw}, any equation is equivalent to a finite set of simple inequations (see Corollary 2.8). Moreover, by Lemma 4.10, for every simple inequation t ≤ t′ that holds in A there is a strictly regular inequation t ≤ t′′ that also holds in A such that E_{ciw}^{+} ∪ {t ≤ t′′} proves t ≤ t′. Thus, since all such inequations hold in B, it follows that B satisfies any equation that holds in A.

For the second claim, observe that, by Lemma 4.11, any equation in E holds in A_{⊥}, as does any equation in E_{ci}. Suppose now that an algebra B satisfies all the equations in E_{ci} ∪ E. By Corollary 2.8, we only need to show that B satisfies any simple inequation that holds in A_{⊥}. Lemma 4.11 tells us that these are the simple inequations that have a strictly regular kernel that holds in A. But these inequations can be proven from those in E, and thus hold in B. □

Remark 4.13 If A is a trivial ciw-semiring, then V(A) is axiomatized by the single equation x = y. However, this equation is not provable from E_{ciw}^{+} ∪ E, where E denotes the set of all strictly regular equations that hold in A. Thus the assumption of nontriviality in the statement of the above result is necessary.

Corollary 4.14 Suppose that A is a nontrivial positive ciw-semiring. If the variety V(A_{⊥}) has a finite axiomatization then so does V(A).

Proof: Let E denote the set of strictly regular, simple inequations that hold in A. By Cor. 4.12, E_{ci} ∪ E proves all the equations satisfied by A_{⊥}. Suppose that V(A_{⊥}) is finitely axiomatizable. Then, by the compactness theorem, there is a finite set F ⊆ E such that the set of equational axioms E_{ci} ∪ F forms a complete axiomatization of V(A_{⊥}). We claim that E_{ciw}^{+} ∪ F is a complete axiomatization of the variety V(A). Indeed, all of the equations in this set hold in A. Moreover, if E_{ciw}^{+} ∪F does not form a complete set of equations for V(A), then, by Cor. 4.12, there are some algebra B and a simple inequation t ≤ t′ in E such that B satisfies all of the equations in E_{ciw}^{+} ∪ F, but such that t ≤ t′ fails in B. Consider the algebra B_{⊥}. By Lemma 2.1, B_{⊥} satisfies the equations in E_{ci}, and, by Lemma 4.11, B_{⊥} satisfies the equations in F. Since t ≤ t′ does not hold in B, it follows that t ≤ t′ does not hold in B_{⊥}. But t ≤ t′ is in E and thus holds in A_{⊥}, so that E_{ci} ∪ F is not a complete set of identities for V(A_{⊥}). □

Corollary 4.15 Suppose that A is a nontrivial positive ciw-semiring. If the variety V(A_{⊥}) has an equational axiomatization in a bounded number of variables, then so has V(A).

Proof: Assume that the set E of valid equations of A_{⊥} in at most n ≥ 3 variables forms an equational axiomatization of V(A_{⊥}). With respect to the axioms E_{ci}, each equation in E may be transformed into a a finite set of simple inequations in at most n variables. Any such inequation holds in A and is thus regular by Lemma 4.9. Now, using the equations in E_{ciw}^{+}, each inequation may be replaced by its projection which also has at most n variables. Any such simple inequation is strictly regular. Let E′ denote the resulting set of inequations. By construction, we have that E_{ci} ∪ E′ is an axiomatization of V(A_{⊥}). Moreover, since n ≥ 3, each equation in this set has at most n variables. As in the proof of the preceding corollary, we can show that E_{ciw}^{+} ∪ E′ is a complete set of axioms for V(A). □

4.2 Decidability and Non-Finite Axiomatizability

We now apply the results of the previous subsection to show that each of the tropical semirings defined thus far has a decidable but non-finitely based equational theory.

Proposition 4.16 Every simple inequation that holds in N_{∨}^{−} (respectively, in Z_{∨}) has a kernel that holds in N_{∨}^{−} (resp., in Z_{∨}).

Proof: Assume to the contrary that the simple inequation t ≤ t′ holds in N_{∨}^{−} but does not have a kernel. Then each linear subterm of t′ contains a variable that does not appear in t. If we assign −1 to all such variables and 0 to any other variable then t evaluates to 0 while t′ evaluates to a negative number. Thus t ≤ t′ fails in N_{∨}^{−}, contradicting our assumption. Since N_{∨}^{−} is a subalgebra of Z_{∨}, every simple inequation that holds in Z_{∨} also has a kernel.

We now show that the kernel t ≤ t′′ of a simple inequation t ≤ t′ that holds in N_{∨}^{−} also holds in N_{∨}^{−}. To this end, assume that t ≤ t′′ fails in N_{∨}^{−} and that t′ = t′′ ∨ u, with u such that each of its linear subterms contains a variable not occurring in t. Let \overline{x} be the vector of variables occurring in t, and \overline{y} be the vector of variables occurring in u but not in t. Since t ≤ t′′ fails in N_{∨}^{−}, there is a vector \overline{a} of nonpositive integers such that t(\overline{a}), the result of evaluating t with respect to \overline{a}, is greater than t′′(\overline{a}). Evaluate u with respect to the assignment that extends \overline{a} by mapping each variable in \overline{y} to t′′(\overline{a}). The resulting value of u is no greater than t′′(\overline{a}), showing that t ≤ t′ fails in N_{∨}^{−}.

A similar argument can be used to show that the kernels of simple inequations that hold in Z_{∨} also hold in Z_{∨}. □

Remark 4.17 In fact, the kernel of any simple inequation that holds in Z_{∨} is strictly regular.

Remark 4.18 The above proposition does not hold for positive ciw-semirings. In fact, the simple inequation 0 ≤ x has no kernel.

Theorem 4.19 For each of the tropical semirings A = Z_{∨,−∞}, N_{∨,−∞}, N_{∨,−∞}^{−}, the equational theory of V(A) is decidable in exponential time. Suppose that \overline{d} ≤ U is a simple inequation. Then \overline{d} ≤ U holds in V(Z_{∨,−∞}) if and only if \overline{d} ∈ [U] and it holds in V(N_{∨,−∞}^{−}) if and only if \overline{d} ∈ [[U)].

Proof: This follows from Prop. 4.16, the corresponding facts for the ciwsemirings Z_{∨}, N_{∨} N_{∨}^{−} and from Lem. 4.3 and Lem. 4.11. □

Remark 4.20 Clearly, a simple inequation \overline{d} ≤ U holds in V(Z_{∨}(−∞)) if and only if \overline{d} ∈ [U]. Therefore the structures Z_{∨}, Z_{∨}(−∞) and Z_{∨,−∞} satisfy the same equations in the language of ciw-semirings.

A geometric description of the equations that hold in V(N_{∨,−∞}) will be given in Sec. 4.3.

Theorem 4.21 For each of the tropical semirings A = Z_{∨,−∞}, N_{∨,−∞}, N_{∨,−∞}^{−}, the variety V(A) has no axiomatization in a bounded number of variables.

Proof: Immediate from the corresponding facts for the ciw-semirings Z_{∨}, N_{∨} N_{∨}^{−} and Corollaries 4.7 and 4.15. □

Since Z_{∧,∞} and N_{∧,∞} are isomorphic to Z_{∨,−∞} and N_{∨,−∞}^{−}, respectively, Theorems 4.19 and 4.21 also apply to these semirings.

4.3 The Algebra N_{∨}(−∞)

We now study in some more detail the structure N_{∨,−∞}, and in particular its ciw-semiring reduct N_{∨}(−∞) obtained by forgetting about the constant ⊥. For this algebra, we shall offer concrete descriptions of the free algebras in the variety it generates, characterize the simple inequations that hold in it, and obtain an axiomatization for it relative to Z_{∨}.

Given a vector \overline{c} = (c_{1}, …, c_{n}) ∈ ℕ^{n}, let nz(\overline{c}) denote the set of all integers i ∈ [n] with c_{i} ≠ 0. (That is, nz(\overline{c}) is the set of the nonzero positions in the vector \overline{c}.) When U ⊆ ℕ^{n} we define:

nz(U) = ⋃\{nz(\overline{c}) : \overline{c} ∈ U\} .

The following proposition is a reformulation of Lem. 4.3 that will be useful in the technical developments to follow.

Proposition 4.22 Let \overline{d} be a vector in ℕ^{n} and U ⊆ ℕ^{n} be nonempty and finite. The following are equivalent for a simple inequation \overline{d} ≤ U and a ciw-semiring A = (A, ∨, +, 0).

1. A_{⊥} ⊧ \overline{d} ≤ U.

2. There exists a nonempty U′ ⊆ U such that nz(U′) ⊆ nz(\overline{d}) and A ⊧ \overline{d} ≤ U′.

3. U\overline{d} = \{\overline{c} : \overline{c} ∈ U and nz(\overline{c}) ⊆ nz(\overline{d})\} is nonempty and A ⊧ \overline{d} ≤ U\overline{d}.

The characterization of the simple inequations that hold in V(N_{∨}(−∞)), the variety generated by N_{∨}(−∞), will be based on a variation on the notion of convex ideal introduced in Defn. 3.1. Note that, unlike Z_{∨} and Z_{∨}(−∞) (cf. Rem. 4.20), the ciw-semirings N_{∨} and N_{∨}(−∞) do not have the same equational theory. For instance, the inequation

0 ≤ x  (13)

holds in N_{∨}, but fails in N_{∨}(−∞). This observation, together with our characterization of the simple inequations that hold in N_{∨}, motivates the following definition.

Definition 4.23 Call a set U ⊆ ℕ^{n} a positive convex ideal if for all nonempty \{\overline{c}_{1}, …, \overline{c}_{k}\} = U′ included in U and \overline{d} ∈ ℕ^{n}, if nz(\overline{d}) ⊇ nz(U′) and there exist λ_{1}, …, λ_{k} ≥ 0, ∑_{i∈[k]} λ_{i} = 1 with \overline{d} ≤ ∑_{i∈[k]} λ_{i}\overline{c}_{i}, then \overline{d} ∈ U.

Remark 4.24 In the above definition, we may clearly replace the condition nz(\overline{d}) ⊇ nz(U′) by nz(\overline{d}) = nz(U′).

Proposition 4.25 The intersection of any family of positive convex ideals is a positive convex ideal.

Thus, each U ⊆ ℕ^{n} is included in a least positive convex ideal [(U]]^{+}. For example, the positive convex ideal [(\overline{u}_{i}]]^{+} (i ∈ [n]) generated by the ith unit vector only contains \overline{u}_{i}.

Lemma 4.26 Let U ⊆ ℕ^{n} and \overline{d} ∈ ℕ^{n}. Then \overline{d} ∈ [(U]]^{+} if and only if there exists a nonempty U′ = \{\overline{c}_{1}, …, \overline{c}_{k}\} ⊆ U such that nz(U′) ⊆ nz(\overline{d}), and \overline{d} ∈ [(U′]].

As an immediate corollary of the above lemma, we obtain a characterization of the simple inequations that hold in the algebra N_{∨}(−∞). Using this characterization and the general strategy employed in the proof of Cor. 3.12, we also immediately have that the equational theory of this algebra is decidable.

Corollary 4.27 Suppose that U is a nonempty finite set in ℕ^{n} and \overline{d} ∈ ℕ^{n}. Then:

1. \overline{d} ≤ U holds in N_{∨}(−∞) iff \overline{d} ∈ [(U]]^{+}.

2. There exists an algorithm to decide whether an equation holds in the structure N_{∨}(−∞).

Proof: We only prove the first claim. Assume that \overline{d} ≤ U holds in N_{∨}(−∞). Clearly this means that \overline{d} ≤ U also holds in N_{∨,−∞}. By Propn. 4.22, there exists a nonempty U′ ⊆ U such that nz(U′) ⊆ nz(\overline{d}) and N_{∨} ⊧ \overline{d} ≤ U′. By the first claim in Propn. 3.11, we have that \overline{d} ∈ [(U′]]. Since nz(U′) ⊆ nz(\overline{d}), Lemma 4.26 yields that \overline{d} ∈ [(U]]^{+}, which was to be shown. The proof of the converse implication is similar, and is therefore omitted. □

We now offer concrete descriptions of the free algebras in the variety generated by N_{∨}(−∞).

Let CI^{+}(ℕ^{n}) denote the set of all finite nonempty positive convex ideals in ℕ^{n}. We turn this set into a ciw-semiring. Suppose that U, V ∈ CI^{+}(ℕ^{n}). We define

U ∨ V = [(U ∪ V]]^{+}
U + V = [(U ⊕ V]]^{+}
0 = [(\overline{0}]]^{+} = \{\overline{0}\} .

Following the structure of the proof of similar statements in Sect. 3.3, it is not too hard to show that:

Theorem 4.28 For each n ≥ 0, the algebra CI^{+}(ℕ^{n}) is a ciw-semiring, and is freely generated in V(N_{∨}(−∞)) by the sets [(\overline{u}_{i}]]^{+}, i ∈ [n].

Our next aim will be to offer finite axiomatizations of the variety generated by N_{∨}(−∞) relative to those for V(Z_{∨}). This result will also yield finite axiomatizations of V(N_{∨}) relative to V(N_{∨}(−∞)). As a corollary, we shall obtain that V(N_{∨}(−∞)) is not finitely based.

Lemma 4.29 The convex hull of any nonempty set U is included in [(U]]^{+}.

Let U ⊆ ℕ^{n}. Define the positive ideal generated by U thus:

(U]^{+} = \{\overline{d} : ∃\overline{c} ∈ U such that nz(\overline{c}) = nz(\overline{d}) and \overline{d} ≤ \overline{c}\} .

The following technical result is the crux of the relative axiomatization results to follow.

Proposition 4.30 Suppose that U is a nonempty subset of ℕ^{n}. Then [(U]]^{+} is the convex hull of (U]^{+}.

Proof: The proof is similar to that of the first statement in Propn. 3.4, but we present it in full as an aid to the reader.

Since (U]^{+} ⊆ [(U]]^{+}, it follows by Lemma 4.29 that the convex hull of (U]^{+} is included in [(U]]^{+}. In order to prove the other direction, suppose that

\overline{d} ≤ λ_{1}\overline{c}_{1} + ⋯ + λ_{k}\overline{c}_{k}

for some k > 0, \overline{c}_{1}, …, \overline{c}_{k} ∈ U and λ_{1}, …, λ_{k} ≥ 0 with ∑_{i∈[k]} λ_{i} = 1. Moreover, assume that nz(\overline{d}) = nz(\{\overline{c}_{1}, …, \overline{c}_{k}\}). By Lemma 4.26, it suffices to show that \overline{d} is in the convex hull of the set (V]^{+}, where V = \{\overline{c}_{1}, …, \overline{c}_{k}\}. We shall prove this by induction on

r = k + n + ∑_{i∈[k]} |\overline{c}_{i}| ,

where we use |\overline{c}_{i}| to denote the weight of the vector \overline{c}_{i} (i ∈ [k]), i.e., the sum of its entries.

The base case is when r = 2. Then n = k = 1 and \overline{d} = \overline{c} = \overline{0}, so that our claim holds.

For the inductive step, suppose that r > 2. We proceed with the proof by distinguishing three cases.

Case 1. If there exists some j ∈ [n] with d_{j} = 0, then for this j, we have c_{ij} = 0 for all i ∈ [k]. We can then remove the jth components of all the vectors to obtain \overline{d}′ and \overline{c}′_{1}, …, \overline{c}′_{k} of dimension n − 1 with \overline{d}′ ≤ λ_{1}\overline{c}′_{1} + ⋯ + λ_{k}\overline{c}′_{k} and nz(\overline{d}′) = nz(\{\overline{c}′_{1}, …, \overline{c}′_{k}\}). Let W = \{\overline{c}′_{1}, …, \overline{c}′_{k}\}. Thus, by induction, \overline{d}′ is in the convex hull of (W]^{+}, so that \overline{c} is in the convex hull of (V]^{+}. The case that n = 1 is handled separately: we have \overline{d} = \overline{c}_{1} = ⋯ = \overline{c}_{k} = \overline{0}, and our claim is trivial.

Case 2. If there exists an i ∈ [k] with λ_{i} = 0, then it follows from the inductive hypothesis that \overline{d} is already in the convex hull of the set (W]^{+}, where W = V − \{\overline{c}_{i}\}.

Case 3. If none of the previous two cases applies, then d_{j} > 0 for all j ∈ [n] and λ_{i} > 0 for all i ∈ [k]. Suppose that there exists some j such that c_{ij} = 1 for all i ∈ [k]. Then also d_{j} = 1 and we may remove the jth components of the vectors to obtain \overline{d}′ and \overline{c}′_{i}, i ∈ [k], as before. Using the inductive hypothesis, it follows as in case 1 above that \overline{d} in the convex hull of (V]^{+}. The case that n = 1 is again handled separately.

Suppose now that for each j there is some i_{j} with c_{i_{j}j} > 1. Let \overline{e} = λ_{1}\overline{c}_{1} + ⋯ + λ_{k}\overline{c}_{k}. If for some j

\overline{d} ≤ λ_{1}\overline{c}_{1} + ⋯ + λ_{i_{j}−1}\overline{c}_{i_{j}−1} + λ_{i_{j}}(\overline{c}_{i_{j}} − \overline{u}_{j}) + λ_{i_{j}+1}\overline{c}_{i_{j}+1} + ⋯ + λ_{k}\overline{c}_{k}
= \overline{e} − λ_{i_{j}} \overline{u}_{j} ,

then, by induction, \overline{d} is contained in the convex hull of (W]^{+}, where W is the set \{\overline{c}_{1}, …, \overline{c}_{i_{j}−1}, \overline{c}_{i_{j}} −\overline{u}_{j}, \overline{c}_{i_{j}+1}, … \overline{c}_{k}\} ⊆ (V]^{+}. It follows that \overline{d} is in the convex hull of (V]^{+}. Otherwise, we have that

e_{j} − λ_{i_{j}} ≤ d_{j} ≤ e_{j} ,

for all j. But this means that \overline{d} is inside the n-dimensional rectangle determined by the vectors

\overline{v}_{K} = \overline{e} − ∑_{j∈K} λ_{i_{j}} \overline{u}_{j} ,

where K ranges over all subsets of [k]. Since these vectors \overline{v}_{K} are all in the convex hull of (V]^{+}, it follows that \overline{d} belongs to the convex hull of (V]^{+}, which was to be shown. □

Corollary 4.31 A simple inequation \overline{d} ≤ U holds in N_{∨}(−∞) iff \overline{d} is in the convex hull of (U]^{+} iff the simple inequation \overline{d} ≤ (U]^{+} holds in Z_{∨}.

Using the above results, and following the lines of the proof of Thm. 3.20, we can now show the promised results on the relative axiomatization of the varieties V(N_{∨}(−∞)) and V(N_{∨}).

Corollary 4.32 V(N_{∨}(−∞)) can be axiomatized over V(Z_{∨}) by the inequation

x ≤ x + x .  (14)

Furthermore V(N_{∨,−∞}) can be axiomatized over V(Z_{∨,−∞}) by the above inequation.

Corollary 4.33 V(N_{∨}) can be axiomatized over V(N_{∨}(−∞)), or over V(Z_{∨}), by the inequation (13).

Using the aforementioned relative axiomatization results, and following the lines of the proof of Theorem 3.22, we have that:

Corollary 4.34 The variety V(N_{∨}(−∞)) is not finitely based. Moreover, there exists no n such that the set of all equations E_{n} in at most n variables that hold in N_{∨}(−∞) is a complete axiomatization of V(N_{∨}(−∞)).

5 Adding More Constants

We now proceed our investigations of the equational theory of structures based upon ciw-semirings by investigating the effect of adding a top element ⊤ to them.

5.1 Adding ⊤

Suppose that A = (A, ∨, +, 0) is any algebra and ⊤ ∉ A. We define

a + ⊤ = ⊤ + a = ⊤
a ∨ ⊤ = ⊤ ∨ a = ⊤

for all a ∈ A_{⊤} = A ∪ {⊤}. Below we shall consider A_{⊤} equipped with the ∨ and + operations, extended as above, and the constant 0. We write A_{⊤} if ⊤ is added to the signature of the resulting algebra, and A(⊤) for the structure resulting by adding ⊤ only to the carrier set. When A is one of the ci(w)-semirings Z_{∨}, N_{∨}, etc., then we also write A_{∞} and A(∞) for A_{⊤} and A(⊤), respectively.

Proposition 5.1 Any equation that holds in A(⊤) also holds in A. Moreover, A(⊤) satisfies an equation iff the equation is regular and holds in A.

Proof: Since A is a subalgebra of A(⊤), the first claim is obvious. As for the second claim, assume that t = t′ holds in A and t and t′ contain the same variables, say x_{1}, …, x_{n}. Since t = t′ holds in A, the only way that t = t′ may fail in A(⊤) is that there exist some a_{1}, …, a_{n} such that at least one of the a_{i} is ⊤ and t(a_{1}, …, a_{n}) ≠ t′(a_{1}, …, a_{n}). But in that case both sides are ⊤.

On the other hand, if t′ contains a variable that does not appear in t, say, and if the variables of t and t′ are x_{1}, …, x_{n}, then let a_{i} ∈ A whenever x_{i} appears in t, and let a_{i} = ⊤ otherwise. We have that t(a_{1}, …, a_{n}) ∈ A but t′(a_{1}, …, a_{n}) = ⊤. Hence the equation t = t′ fails in A(⊤). □

Corollary 5.2 The algebras A and A(⊤) satisfy the same regular equations. Moreover, A and A(⊤) satisfy the same equations iff every equation that holds in A is regular.

Corollary 5.3 A is a ciw-semiring iff so is A(⊤). Suppose that A is a ciwsemiring and that every simple inequation that holds in A is regular. Then A and A(⊤) satisfy the same equations.

Proof: The first fact follows by Proposition 5.1, noting that every defining equation of ciw-semirings is regular. The second fact follows by noting that the following two conditions are equivalent for a ciw-semiring A:

1. Every equation that holds in A is regular.

2. Every simple inequation that holds in A is regular. □

Remark 5.4 The same facts hold if we consider algebras containing more constants such as algebras (A, ∨, +, ⊥, 0) equipped with a constant ⊥.

We might wish to add the symbol ⊤ also to the signature and consider equations involving ⊤ that hold in A_{⊤}. The following proposition gives a characterization of the equations of this kind that hold in A_{⊤} relative to those that hold in A.

Proposition 5.5 For any algebra A = (A, ∨, +, 0) or A = (A, ∨, +, ⊥, 0), an equation between terms possibly involving ⊤ holds in A_{⊤} iff

• either both sides contain an occurrence of ⊤;

• or neither of them does, the equation holds in A and is regular.

The simple proof is omitted. The above result has a number of useful corollaries relating the equational theories of A_{⊤} and A.

Corollary 5.6 If the equational theory of A is decidable in time O(t(n)), with t(n) ≥ n^{2}, then so is the equational theory of A_{⊤}.

Corollary 5.7 Suppose that A = (A, ∨, +, 0) or A = (A, ∨, +, ⊥, 0) is a given algebra and E is a set of equations possibly involving ⊤. Let E_{0} denote the set of equations in E not containing ⊤. Then E, together with the equations

x + ⊤ = ⊤  (15)
x ∨ ⊤ = ⊤ ,  (16)

is an equational basis for A_{⊤} iff E_{0} is a basis for the regular equations^{1} that hold in A. In particular, if all equations satisfied by A are regular, then E together with (15) and (16) is an equational basis for A_{⊤} iff E_{0} is an equational basis for A.

1This means that E_{0} consists of regular equations that hold in A. Moreover, E_{0} proves all regular equations that hold in A.

Corollary 5.8 Suppose that A is a ci(w)-semiring such that every simple inequation that holds in A is regular. Let E denote a set of equations and define E_{0} as in the statement of Cor. 5.7. Then E, together with (15) and (16), is an equational basis for A_{⊤} iff E_{0} is an equational basis for A.

Corollary 5.9 Suppose that A is a ci(w)-semiring such that such that every simple inequation that holds in A is regular. Then A has a finite basis for its identities iff so does A_{⊤}. Moreover, A has an axiomatization in a bounded number of variables iff so does A_{⊤}.

5.2 Applications

We now proceed to apply the general results developed in Sect. 5.1 to the algebras obtained by adding top elements to some of the ciw-semirings we study in this paper.

Proposition 5.10 Let A be any of the commutative idempotent (weak) semirings Z_{∨}, N_{∨}, Z_{∨,−∞}, N_{∨,−∞}, Z_{∨}(−∞) and N_{∨}(−∞). Then A(∞) and A_{∞} are not finitely based, and have no axiomatization in a bounded number of variables. Moreover, the equational theory of A_{∞} is decidable in exponential time.

Proof: Immediate from the preceding results, the fact that each of Z_{∨}, N_{∨}, Z_{∨}(−∞), N_{∨}(−∞), Z_{∨,−∞} and N_{∨,−∞} is a ci(w)-semiring satisfying only regular simple inequations, and from the results established in Sections 3 and 4. □

6 Variations on Tropical Semirings

We now examine some variations on the tropical semirings studied so far in this paper. These include structures whose carrier sets are the (nonnegative) rational or real numbers (Sect. 6.1), semirings whose product operation is standard multiplication (Sect. 6.2), and the semirings studied by Mascle and Leung in [30] and [26, 27], respectively, (Sect. 6.3). We also offer results on the equational theory of some algebras based on the ordinals proposed by Mascle in [29] (Sect. 6.4).

6.1 Structures over the Rational and Real Numbers

We now proceed to study tropical semirings over the (nonnegative) rationals and reals, and their underlying ciw-semirings. More precisely, we shall consider the following ciw-semirings:

\begin{matrix}Q_{∨} = (ℚ, ∨, +, 0) & Q_{∨}^{+} = (ℚ^{+}, ∨, +, 0) & Q_{∧}^{+} = (ℚ^{+}, ∧, +, 0) \\ R_{∨} = (ℝ, ∨, +, 0) & R_{∨}^{+} = (ℝ^{+}, ∨, +, 0) & R_{∧}^{+} = (ℝ^{+}, ∧, +, 0) , \end{matrix}

where ℚ^{+} and ℝ^{+} denote the sets of nonnegative rational and real numbers, respectively. We shall also investigate the tropical semirings associated with the aforementioned ciw-semirings, viz. the structures

\begin{matrix}Q_{∨,−∞} = (ℚ ∪ \{−∞\}, ∨, +, −∞, 0) & Q_{∨,−∞}^{+} = (ℚ^{+} ∪ \{−∞\}, ∨, +, −∞, 0) \\ R_{∨,−∞} = (ℝ ∪ \{−∞\}, ∨, +, −∞, 0) & R_{∨,−∞}^{+} = (ℝ^{+} ∪ \{−∞\}, ∨, +, −∞, 0) \\ Q_{∧,∞}^{+} = (ℚ^{+} ∪ \{∞\}, ∧, +, ∞, 0) & R_{∧,∞}^{+} = (ℝ^{+} ∪ \{∞\}, ∧, +, ∞, 0) . \end{matrix}

We begin by noting the following result, to the effect that each of the algebras on a dense carrier set has the same equational theory of its corresponding discrete structure:

Lemma 6.1

1. The ciw-semirings Q_{∨}, R_{∨} and Z_{∨} have the same equational theory.

2. The ciw-semirings Q_{∨}^{+}, R_{∨}^{+} and N_{∨} have the same equational theory.

3. The ciw-semirings Q_{∧}^{+}, R_{∧}^{+} and N_{∧} have the same equational theory.

4. The ci-semirings Q_{∨,−∞}, R_{∨,−∞} and Z_{∨,−∞} have the same equational theory.

5. The ci-semirings Q_{∨,−∞}^{+}, R_{∨,−∞}^{+} and N_{∨,−∞} have the same equational theory.

6. The ci-semirings Q_{∧,∞}^{+}, R_{∧,∞}^{+} and N_{∧,∞} have the same equational theory.

Proof: We only outline the proof of the first statement of the lemma. It is clear that the equational theory of R_{∨} is included in that of Q_{∨}, which is in turn included in that of Z_{∨}. For the converse, assume that

t(x_{1}, …, x_{n}) = t′(x_{1}, …, x_{n})

holds in Z_{∨}. Let r_{1}, …, r_{n} be rationals, and write r_{i} = p_{i}/q, where the p_{i} (i ∈ [n]) and q are integers, with q positive. Now

t(r_{1}, …, r_{n}) = \frac{t(p_{1}, …, p_{n})}{q}
= \frac{t′(p_{1}, …, p_{n})}{q}
= t′(r_{1}, …, r_{n}) .

Thus, any valid equation of Z_{∨} holds in Q_{∨}. The fact that any equation of Q_{∨} holds in R_{∨} follows from the continuity of the term functions. The proof of the other statements is similar. □

As an immediate corollary of the above lemma, and of the non-finite axiomatizability results presented earlier in the paper, we have that:

Theorem 6.2 Let A be any of the algebras Q_{∨}, R_{∨}, Q_{∨}^{+}, R_{∨}^{+}, Q_{∧}^{+}, R_{∧}^{+}, Q_{∨,−∞}, R_{∨,−∞}, Q_{∨,−∞}^{+}, R_{∨,−∞}^{+}, Q_{∧,∞}^{+} and R_{∧,∞}^{+}. Then:

1. The variety V(A) is not finitely based.

2. For every natural number n, the collection of equations in at most n variables that hold in V(A) is not a basis for its identities.

3. The equational theory of V(A) is decidable in exponential time.

Remark 6.3 The structure R_{∨,−∞} = (ℝ, ∨, +, −∞, 0) is the well-known maxplus algebra, whose plethora of applications are discussed in, e.g., [15].

All of the algebras, whose carrier sets are the set of rational or real numbers, that we have discussed so far in this section sometimes appear in their isomorphic form as min-plus algebras. As a further corollary of the above theorem, we therefore have that:

Corollary 6.4 Let A be either ℚ or ℝ. Then the algebras A_{∧} = (A, ∧, +, 0) and A_{∧,∞} = (A ∪ {∞}, ∧, +, ∞, 0) are not finitely based. Moreover, for every n ∈ ℕ, the collection of equations in at most n variables that hold in A_{∧} (respectively, A_{∧,∞}) does not form an equational basis for A_{∧} (resp., A_{∧,∞}). Finally, the equational theories of A_{∧} and A_{∧,∞} are decidable in exponential time.

6.2 Min-Max-Times Algebras

We now apply the results we have previously obtained to the study of the equational theories of the ci(w)-semirings

A_{∨,×} = (A \ {0}, ∨, ×, 1) ,
A_{∧,×} = (A \ {0}, ∧, ×, 1) ,
A_{∨,×,0} = (A, ∨, ×, 0, 1) and
A_{∧,×,0} = (A, ∧, ×, 0, 1) ,

where A is any of the sets ℕ, ℚ^{+} or ℝ^{+}, and × is standard multiplication.

Proposition 6.5 Let A be any of the sets ℕ, ℚ^{+} or ℝ^{+}. Then:

1. V(A_{∨,×}) = V(A_{∨}),

2. V(A_{∧,×}) = V(A_{∧}),

3. V(A_{∨,×,0}) = V(A_{∨,−∞}) and

4. V(A_{∧,×,0}) = V(A_{∧,−∞}).

Proof: We only show statement 1, when A is ℕ. The proof of the remaining claims is similar.

First of all, note that N_{∨} is isomorphic to the subalgebra of N_{∨,×} determined by the natural numbers that are a power of 2. Conversely, observe that N_{∨,×} is isomorphic to the algebra

(log(ℕ \ {0}), ∨, +, 0) ,

where we write log(ℕ \ {0}) for the collection of logarithms in base 2 of the positive natural numbers, via the mapping

n ↦ log n .

The above mapping is injective, and the set log(ℕ\{0}) is closed under addition, in light of the well-known equation

log(x × y) = log x + log y .

Note, furthermore, that N_{∨} is a subalgebra of (log(ℕ \ {0}), ∨, +, 0), which is itself a subalgebra of R_{∨}^{+}. By Lem. 6.1, these three algebras have the same equational theory, and thus generate the same variety. □

As a corollary of the above proposition, and of the results that we have previously established for min-max-plus ci(w)-semirings, we obtain the following result:

Corollary 6.6 Let A be any of the sets ℕ, ℚ^{+} or ℝ^{+}. Then:

1. The varieties generated by the algebras A_{∨,×}, A_{∧,×}, A_{∨,×,0} and A_{∧,×,0} are not finitely based. Moreover none of these varieties has an axiomatization in a bounded number of variables.

2. There exists an exponential time algorithm to decide whether an equation holds in the structures A_{∨,×}, A_{∧,×}, A_{∨,×,0} and A_{∧,×,0}.

6.3 Mascle’s and Leung’s Semirings

We now study the equational theory of some semirings originally proposed by Mascle and Leung, and discussed in the survey paper [31].

6.3.1 Mascle’s Semiring

In [30], Mascle introduced the semiring

P_{−∞} = (ℕ ∪ {−∞, ∞}, ∨, +, −∞, 0)

where the addition operation satisfies the identities

−∞ + x = x + (−∞) = − ∞ .

(See also the survey paper [31] for information on this and other semirings proposed by Mascle.) Note that the ci-semiring P_{−∞} is different from the structure N_{∨,−∞}(∞) we studied in Sect. 5.2. Indeed, in N_{∨,−∞}(∞) it holds that

−∞ + ∞ = ∞ + (−∞) = ∞ .

Instead, it is the case that P_{−∞} is obtained by freely adding −∞ to the ciwsemiring N_{∨}(∞).

Theorem 6.7 The variety V(P_{−∞}) is not finitely based, and affords no axiomatization in a bounded number of variables.

Proof: The variety generated by the positive ciw-semiring N_{∨}(∞) has no axiomatization in a bounded number of variables (Propn. 5.10). By Cor. 4.15, the same holds true of V(P_{−∞}). □

6.3.2 Leung’s Semiring

Leung [26, 27] introduced and studied the semiring

M = (ℕ ∪ {ω, ∞}, ∧, +, ∞, 0) ,

where the minimum operation is defined with respect to the order

0 < 1 < 2 < ⋯ < ω < ∞ ,

and addition in the tropical semiring N_{∧,∞} is completed by stipulating that

x + ω = ω + x = max{x, ω} .

Thus the carrier of M is just the ordinal ω + 2. It is easy to see that M is a ci-semiring.

We shall now proceed to show that Leung’s semiring is also not finitely based. To this end, we relate the equational theory of the tropical semiring N_{∨,−∞}^{−} to that of

M^{−} = (ℕ^{−} ∪ {−ω, −∞}, ∨, +, −∞, 0) ,

which is isomorphic to M.

Lemma 6.8 Let t ≤ t′ be a simple inequation. Then t ≤ t′ holds in N_{∨,−∞}^{−} iff it holds in M^{−}.

Proof: Clearly every simple inequation that holds in M^{−} also holds in N_{∨,−∞}^{−}. Conversely, let t ≤ t′ be a simple inequation that holds in N_{∨,−∞}^{−}. By Lem. 4.3, t ≤ t′ has a kernel that holds in N_{∨}^{−}. This kernel holds in M^{−} (again by Lem. 4.3), and so does t ≤ t′. □

As immediate corollary of the above result, we have that N_{∨,−∞}^{−} and M^{−} have the same equational theory. Since Leung’s semiring M and M^{−} are isomorphic, using Thm. 4.21, we therefore have that:

Proposition 6.9 The variety V(M) generated by the semiring M has no finite axiomatization, and no axiomatization in a bounded number of variables.

6.4 Ordinals

In [29] (see also the survey paper [31]), Mascle proposed to study min-plus algebras whose carrier sets consist of the collection of ordinals strictly smaller than a given ordinal α. Our aim in this section is to offer results to the effect that these algebras do not afford any axiomatization in a bounded number of variables. We begin by giving the precise definition of these structures.

Recall that each ordinal α can be represented as the well-ordered set of all the ordinals strictly smaller than it. When α is a power of ω, the first infinite ordinal, this set is closed under ordinal addition, giving rise to the structures

α_{∨} = (α, ∨, +, 0)  and
α_{∧} = (α, ∧, +, 0) ,

where ∨ and ∧ denote the maximum and minimum operation over ordinals, respectively. Since ordinal addition is not commutative, these structures are not ciw-semirings unless α = 1 or α = ω. However, except for commutativity of addition, they satisfy all the defining equations of ciw-semirings. Moreover, when α ≠ 1, the algebra α_{∨} contains N_{∨} as a subalgebra, and α_{∧} contains N_{∧}. In both α_{∨} and α_{∧}, the carrier set α is linearly ordered by the semilattice order, and the + operation is monotonic (see, e.g., [20]). Thus, by Thm. 3.40, we have that:

Theorem 6.10 Suppose that α ≠ 1 is a power of ω. Then V(α_{∨}) cannot be axiomatized by equations in a bounded number of variables. The same fact holds for V(α_{∧}).

When α is an ordinal of the form ω^{β}, where β is itself a power of ω, the set α is closed under ordinal product, giving rise to the structures

α_{∨,×} = (α \ {0}, ∨, ×, 1)  and
α_{∧,×} = (α \ {0}, ∧, ×, 1) .

Proposition 6.11 The structures α_{∨} and α_{∧} embed in ω_{∨,×}^{α} and ω_{∧,×}^{α}, respectively.

Proof: The function mapping any ordinal β < α to ω^{β} is an embedding, in light of the equality

ω^{β} × ω^{γ} = ω^{β+γ} ,

and we are done. □

¿From the above result, it follows that the algebra α_{∨,×} contains N_{∨,×} as a subalgebra, and α_{∧,×} contains N_{∧,×}. In both α_{∨,×} and α_{∧,×}, the carrier set α is linearly ordered by the semilattice order, and the × operation is monotonic (see, e.g., [20]). Thus, by Thm. 3.40, we have that:

Theorem 6.12 Suppose that α is an ordinal of the form ω^{β}, where β is itself a power of ω. Then V(α_{∨,×}) cannot be axiomatized by equations in a bounded number of variables. The same fact holds for V(α_{∧,×}).

Acknowledgments: We thank the anonymous referees for the extended abstract [3] whose suggestions helped us improve the paper.

References

[1] L. Aceto, Z. Ésik, and A. Ingólfsdóttir, The max-plus algebra of the natural numbers has no finite equational basis, BRICS Report RS-99-33, October 1999. Available at the URL

http://www.brics.dk/RS/99/33/index.html. To appear in Theoretical

Computer Science.

[2] , On the two-variable fragment of the equational theory of the maxsum algebra of the natural numbers, in Proceedings of the 17th International Symposium on Theoretical Aspects of Computer Science, H. Reichel and S. Tison, eds., vol. 1770 of Lecture Notes in Computer Science, Springer-Verlag, Feb. 2000, pp. 267–278. Available at the URL

http://www.brics.dk/RS/99/22/index.html.

[3] , Axiomatizing tropical semirings, in Proceedings of FoSSaCS 2001 (Foundations of Software Science and Computation Structures), F. Honsell and M. Miculan, eds., vol. 2030 of Lecture Notes in Computer Science, Springer-Verlag, Apr. 2001, pp. 42–56.

[4] , Nonfinitely based tropical semirings, in Proceedings of the Workshop on Max-plus Algebras and their Applications to Discrete-event Systems, Theoretical Computer Science, and Optimization, S. Gaubert and J. J. Loiseau, eds., IFAC (International Federation of Automatic Control) Publications, Elsevier Science, Aug. 2001, to appear.

[5] F. Baccelli, G. Cohen, G.-J. Olsder, and J.-P. Quadrat, Synchronization and Linearity, Wiley Series in Probability and Mathematical Statistics, John Wiley, 1992.

[6] A. Bonnier-Rigny and D. Krob, A complete system of identities for one-letter rational expressions with multiplicities in the tropical semiring, Theoretical Computer Science, 134 (1994), pp. 27–50.

[7] W. Burnside, On an unsettled question in the theory of discontinuous groups, Q. J. Pure and Appl. Mathematics, 33 (1902), pp. 230–238.

[8] S. Burris and H. P. Sankappanavar, A Course in Universal Algebra, Springer-Verlag, New York, 1981. The “Millennium Edition” is available

at the URL http://thoralf.uwaterloo.ca/htdocs/ualg.html.

[9] J. H. Conway, Regular Algebra and Finite Machines, Mathematics Series (R. Brown and J. De Wet eds.), Chapman and Hall, London, United Kingdom, 1971.

[10] R. Cuninghame-Green, Minimax Algebra, vol. 166 of Lecture Notes in Economics and Mathematical Systems, Springer-Verlag, 1979.

[11] M. J. Fischer and M. O. Rabin, Super-exponential complexity of Presburger arithmetic, in Complexity of Computation (Proc. SIAM-AMS Symposium, New York, 1973), vol. VII of SIAM-AMS Proceedings, Providence, R.I., 1974, American Mathematical Society, pp. 27–41.

[12] S. Gaubert, and M. Plus, Methods and applications of (max,+) linear algebra, in Proceedings of the 14th International Symposium on Theoretical Aspects of Computer Science, vol. 1200 of Lecture Notes in Computer Science, Springer-Verlag, Feb. 1997, pp. 261–282.

[13] G. Grätzer, Universal Algebra, Springer-Verlag, second ed., 1979.

[14] J. Gunawardena (ed.), Idempotency, Publications of the Newton Institute 11, Cambridge University Press, 1998.

[15] , An introduction to idempotency, in [14], pp. 1–49.

[16] K. Hashiguchi, Limitedness theorem on finite automata with distance functions, J. Comput. System Sci., 24 (1982), no. 2, pp. 233–244.

[17] , Regular languages of star height one, Information and Control, 53 (1982), pp. 199–210.

[18] , Algorithms for determining relative star height and star height, Information and Computation, 78 (1988), pp. 124–169.

[19] , Relative star-height, star-height and finite automata with distance functions, in Formal Properties of Finite Automata and Applications (J.E. Pin ed.), Lecture Notes in Computer Science 386, Springer-Verlag, 1989, pp. 74–88.

[20] P. T. Johnstone, Notes on Logic and Set Theory, Cambridge Mathematical Textbooks, Cambridge University Press, 1987.

[21] D. Krob, Complete systems of B-rational identities, Theoretical Comput. Sci., 89 (1991), pp. 207–343.

[22] , The equality problem for rational series with multiplicities in the tropical semiring is undecidable, International J. Algebra Computation, 4 (1994), pp. 405–425.

[23] , Some consequences of a Fatou property of the tropical semiring, Journal of Pure and Applied Algebra, 93 (1994), pp. 231–249.

[24] , Some automata-theoretic aspects of min-max-plus semirings, in [14], pp. 70–79.

[25] W. Kuich and A. Salomaa, Semirings, Automata, Languages, EATCS Monographs on Theoretical Computer Science 5, Springer-Verlag, 1986.

[26] H. Leung, An Algebraic Method for Solving Decision Problems in Finite Automata Theory, Ph.D. Thesis, Department of Computer Science, The Pennsylvania State University, 1987.

[27] , On the topological structure of a finitely generated semigroup of matrices, Semigroup Forum, 37 (1988), pp. 273–287.

[28] , The topological approach to the limitedness problem on distance automata, in [14], pp. 88–111.

[29] J.-P. Mascle, Quelque résultats de décidabilité sur la finitude des semigroupes de matrices, LITP Report 85-50, 1985.

[30] , Torsion matrix semigroups and recognizable transductions, in Automata, Languages and Programming, 13th International Colloquium (L. Kott ed.), vol. 226 of Lecture Notes in Computer Science, Springer-Verlag, 1986, pp. 244–253.

[31] J.-E. Pin, Tropical semirings, in [14], pp. 50–69.

[32] V. Redko, On defining relations for the algebra of regular events, Ukrainskii Matematicheskii Zhurnal, 16 (1964), pp. 120–126. In Russian.

[33] A. Schrijver, Theory of Linear and Integer Programming, John Wiley and Sons, 1986.

[34] I. Simon, Limited subsets of a free monoid, in Proceedings of the 19th Annual Symposium on Foundations of Computer Science (Ann Arbor, Mich., 1978), IEEE Computer Society, 1978, pp. 143–150.

[35] , Recognizable sets with multiplicities in the tropical semiring, in Proceedings of Mathematical Foundations of Computer Science (Carlsbad, 1988), Lecture Notes in Computer Science 324, Springer-Verlag, 1988, pp. 107–120.

[36] , The nondeterministic complexity of finite automata, in Mots, M. Lothaire ed., Hermès, 1990, pp. 384–400.

[37] W. Taylor, Equational logic, in [13], Appendix 4, pp. 378–400.

[38] U. Zimmermann, Linear and Combinatorial Optimization in Ordered Algebraic Structures, Annals of Discrete Mathematics 10, North-Holland, 1981.

Recent BRICS Report Series Publications

RS-01-21 Luca Aceto, Zoltán Ésik, and Anna Ingólfsdóttir. Equational Theories of Tropical Semirings. June 2001. 52 pp. Extended abstracts of parts of this paper have appeared in Honsell and Miculan, editors, Foundations of Software Science and Computation Structures, FoSSaCS ’01 Proceedings, LNCS 2030, 2000, pages 42–56 and in Gaubert and Loiseau, editors, Workshop on Max-plus Algebras and their Applications to Discrete-event Systems, Theoretical Computer Science, and Optimization, MAX-PLUS ’01 Proceedings, IFAC (International Federation of Automatic Control) IFAC Publications, 2001.

RS-01-20 Catuscia Palamidessi and Frank D. Valencia. A Temporal Concurrent Constraint Programming Calculus. June 2001. 31 pp.

RS-01-19 Jiří Srba. On the Power of Labels in Transition Systems. June

2001.

RS-01-18 Katalin M. Hangos, Zsolt Tuza, and Anders Yeo. Some Complexity Problems on Single Input Double Output Controllers. 2001. 27 pp.

RS-01-17 Claus Brabrand, Anders Møller, Steffan Olesen, and Michael I. Schwartzbach. Language-Based Caching of Dynamically Generated HTML. May 2001. 18 pp.

RS-01-16 Olivier Danvy, Morten Rhiger, and Kristoffer H. Rose. Normalization by Evaluation with Typed Abstract Syntax. May 2001. 9 pp. To appear in Journal of Functional Programming.

RS-01-15 Luigi Santocanale. A Calculus of Circular Proofs and its Categorical Semantics. May 2001. 30 pp.

RS-01-14 Ulrich Kohlenbach and Paulo B. Oliva. Effective Bounds on Strong Unicity in L_{1}-Approximation. May 2001. 38 pp.

RS-01-13 Federico Crazzolara and Glynn Winskel. Events in Security Protocols. April 2001. 30 pp.

RS-01-12 Torben Amtoft, Charles Consel, Olivier Danvy, and Karoline Malmkjær. The Abstraction and Instantiation of String-Matching Programs. April 2001.

RS-01-11 Alexandre David and M. Oliver Möller. From HUppaal to Uppaal: A Translation from Hierarchical Timed Automata to Flat Timed Automata. March 2001. 40 pp.