BRICS RS-99-22 Aceto et al.: On Equations in Two Variables in the Max-Sum Algebra BRICS

Basic Research in Computer Science

On the Two-Variable Fragment of the Equational Theory of the Max-Sum Algebra of the Natural Numbers

Luca Aceto Zoltán Ésik Anna Ingólfsdóttir

BRICS Report Series RS-99-22 ISSN 0909-0878 August 1999 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1999, 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/99/22/

On the Two-Variable Fragment of the Equational Theory of the Max-Sum Algebra of the Natural Numbers

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

Abstract

This paper shows that the collection of identities in two variables which hold in the algebra N of the natural numbers with constant zero, and binary operations of sum and maximum does not have a finite equational axiomatization. This gives an alternative proof of the non-existence of a finite basis for N—a result previously obtained by the authors. As an application of the main theorem, it is shown that the language of Basic Process Algebra (over a singleton set of actions), with or without the empty process, has no finite ω-complete equational axiomatization modulo trace equivalence.

AMS Subject Classification (1991): 08A70, 08B05, 03C05, 68Q70. ACM Computing Classification System (1998): F.4.1. Keywords and Phrases: Equational logic, varieties, complete axiomatizations, process algebra, trace equivalence.

1 Introduction

Since Birkhoff’s original developments, equational logic has been one of the classic topics of study within universal algebra. (See, e.g., [7, 8, 9] for surveys of results in this area of research.) In particular, the research literature is, among other things, rich in results, both of a positive and negative nature, on the existence of finite bases for theories (i.e. finite sets of axioms for them).

∗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, A. József University, Árpád tér 2, 6720 Szeged, Hungary. Partially supported by grant no. T30511 from the National Foundation of Hungary for Scientific Research. Email: esik@inf.u-szeged.hu. Fax: +36-62-420292.

‡Supported by a research grant from the Danish Research Council.

In this paper, we contribute to the study of equational theories that are not finitely based by continuing our analysis of the equational theory of the algebra N of the natural numbers with constant zero, and binary operations of summation and maximum (written ∨ in infix form). Our investigations of this equational theory started in the companion paper [1]. In op. cit. we showed that the equational theory of N is not finitely based. Moreover, we proved that, for all n ≥ 0, the collection of all the equations in at most n variables that hold in N does not form an equational basis.

The equational theory of N is surprisingly rich in non-trivial families of identities. For example, the following infinite schemas of equations also hold in N:

\begin{matrix}e_{n} : & nx_{1} ∨ … ∨ nx_{n} ∨ (x_{1} + … + x_{n}) = nx_{1} ∨ … ∨ nx_{n} \\ e′_{n} : & nx ∨ ny = n(x ∨ y) , \end{matrix}

where n ∈ ℕ, and nx denotes the n-fold sum of x with itself.

Let Eq_{2}(N) denote the collection of equations that hold in N containing occurrences of two distinct variables. A natural question suggested by the family of equations e′_{n} above is the following:

Is there a finite set E of equations that hold in N such that E ⊢ Eq_{2}(N)?

This paper is devoted to proving that no finite axiomatization exists for Eq_{2}(N). Apart from its intrinsic mathematical interest, this result offers yet another view of the non-existence of a finite axiomatization for the variety generated by N proven in [1].

The proof of our main technical result is model-theoretic in nature, and follows standard lines. The details are, however, rather challenging. More precisely, for every prime number p, we construct an algebra A_{p} in which all the equations that hold in N and whose “measure of complexity” is strictly smaller than p hold, but neither e_{p} nor e′_{p} hold in A_{p}. As a consequence of this result, we obtain that not only the equational theory of N is not finitely based, but not even the collection of equations in two variables included in it is.

We also provide an application of our main result to process algebra [2]. More precisely, we show that trace equivalence has no finite ω-complete equational axiomatization for the language of Basic Process Algebra [3] over a singleton alphabet, with or without the empty process [10].

Although the proof of our main theorem uses results from [1], we have striven to make the paper self contained. The interested reader is referred to op. cit. and the textbooks [4, 5] for further background information.

2 The Max-Sum Algebra

Let N = (ℕ, ∨, +, 0) denote the algebra of the natural numbers equipped with the usual sum operation +, constant 0 and the operation ∨ for the maximum of two numbers, i.e.,

x ∨ y = max{x, y} .

We study the equational theory of the algebra N—that is, the collection Eq(N) of equations that hold in N. The reader will have no trouble in checking that the following axioms, that express expected properties of the operations of maximum and sum, hold in N:

\begin{matrix}∨1 & x ∨ y = y ∨ x \\ ∨2 & (x ∨ y) ∨ z = x ∨ (y ∨ z) \\ ∨3 & x ∨ 0 = x \end{matrix} \begin{matrix}+1 & x + y = y + x \\ +2 & (x + y) + z = x + (y + z) \\ +3 & x + 0 = x \\ +∨ & (x ∨ y) + z = (x + z) ∨ (y + z) \end{matrix}

This set of equations will be denoted by Ax_{1}. Note that the equation (x + y) ∨ x = x + y is derivable from +3 and +∨, and, using such an equation, it is a simple matter to derive the idempotency law for ∨, i.e.,

∨4 x ∨ x = x .

We denote by Ax_{0} the set consisting of the equations ∨1, ∨2, ∨4, +1–+3 and +∨. Moreover, we let V_{0} stand for the class of all models of Ax_{0}, and V_{1} for the class of all models of the equations Ax_{1}. Thus, both V_{0} and V_{1} are varieties and, by the above discussion, V_{1} is a subvariety of V_{0}, i.e., V_{1} ⊆ V_{0}.

Since the reduct (A, ∨) of any algebra A = (A, +, ∨, 0) in V_{0} is a semilattice, we can define a partial order ≤ on the set A by a ≤ b if and only if a ∨ b = b, for all a, b ∈ A. This partial order is called the induced partial order. When A is in the variety V_{1}, the constant 0 is the least element of A with respect to ≤. Moreover, for any A ∈ V_{0}, the ∨ and + operations are monotonic with respect to the induced partial order.

The axiom system Ax_{1} completely axiomatizes the collection of equations in at most one variable which hold in the algebra N. However, the interplay between the operations of maximum and sum generates some nontrivial collections of equations in two or more variables. For example, the following infinite schemas of equations, which will play an important role in the technical developments of this paper, also hold in N:

\begin{matrix}e_{n} : & nx_{1} ∨ … ∨ nx_{n} ∨ (x_{1} + … + x_{n}) = nx_{1} ∨ … ∨ nx_{n} \\ e′_{n} : & nx ∨ ny = n(x ∨ y) , \end{matrix}

where n ∈ ℕ, nx denotes the n-fold sum 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. It is not too difficult to see that, for any n, the equation e_{n} is derivable from Ax_{1} and e′_{n}.

Let Eq_{2}(N) denote the collection of equations that hold in N containing occurrences of two distinct variables. A natural question suggested by the family of equations e′_{n} above is the following:

Is there a finite subset E of Eq(N) such that E ⊢ Eq_{2}(N)?

The remainder of this paper is devoted to proving that no finite axiomatization exists for Eq_{2}(N). Apart from its intrinsic mathematical interest, this result offers yet another view of the non-existence of a finite axiomatization for the variety generated by N proven in [1].

3 Explicit Description of the Free Algebras

In this section we give a brief review of some results on the equational theory of the algebra N that we obtained in [1]. (The proofs of the results stated in this section may be found ibidem.) We start by offering an explicit description of the free algebras in the variety V generated by N. Since N satisfies the equations in Ax_{1}, we have that V is a subvariety of V_{1}, i.e., V ⊆ V_{1}.

For the sake of clarity, and for future reference, we shall describe the finitely generated free algebras in V. We recall that any infinitely generated free algebra is a directed union of the finitely generated free ones. (The interested reader is referred to [4] for this and other basic results in universal algebra that we shall use in what follows.)

Let n ≥ 0 denote a fixed integer. The set ℕ^{n} is the collection of all n-dimensional vectors over ℕ. Let P_{f}(ℕ^{n}) denote the collection of all finite nonempty subsets of ℕ^{n}, and define the operations in the following way: for all U, V ∈ P_{f}(ℕ^{n}),

U ∨ V := U ∪ V
U + V := \{\overline{u} + \overline{v} : \overline{u} ∈ U, \overline{v} ∈ V \}
0 := \{\overline{0}\} ,

where \overline{0} stands for the vector whose components are all 0. For each i ∈ [n] = \{1, …, n\}, let \overline{u}_{i} denote the ith unit vector in ℕ^{n}, i.e., the vector whose only non-zero component is a 1 in the ith position.

Proposition 3.1 The algebra P_{f}(ℕ^{n}) is freely generated in V_{0} by the n singleton sets \{\overline{u}_{i}\}, i ∈ [n], containing the unit vectors.

Note that the induced partial order on P_{f}(ℕ^{n}) is given by set inclusion.

It is easy to see that any term t in the variables x_{1}, …, x_{n} (n ≥ 0) can be rewritten, using the equations in Ax_{0}, to the maximum of linear combinations of the variables x_{1}, …, x_{n}, i.e., there are m ≥ 1, and c_{i}^{j} ∈ ℕ for j ∈ [n] and i ∈ [m] such that the equation

t = ⋁_{i∈[m]}( ∑_{j∈[n]} c_{i}^{j}x_{j})

holds in V_{0}. (The empty sum is defined to be 0.) We refer to such terms as normal forms. Thus we may assume that any equation which holds in a given subvariety of V_{0} is in normal form, i.e., of the form t_{1} = t_{2} where t_{1} and t_{2} are normal forms. Furthermore, an equation

t_{1} ∨ … ∨ t_{m} = t′_{1} ∨ … ∨ t′_{m′}

holds in a subvariety of V_{0} if and only if, for all i ∈ [m] and j ∈ [m′],

t_{i} ≤ t′_{1} ∨ … ∨ t′_{m′} and t′_{j} ≤ t_{1} ∨ … ∨ t_{m}

hold in the subvariety. We refer to an inequation of the form

t ≤ t_{1} ∨ … ∨ t_{m}

where t, t_{1}, …, t_{m} are linear combinations of variables, as simple inequations.

A simple inequation t ≤ t_{1} ∨ … ∨ t_{m} that holds in N is irredundant if, for every j ∈ [m],

N |̸= t ≤ t_{1} ∨ … ∨ t_{j−1} ∨ t_{j+1} ∨ … ∨ t_{m} .

By the discussion above, we may assume, without loss of generality, that every set of inequations that hold in N consists of simple, irredundant inequations only.

In order to give an explicit description of the finitely generated free algebras in V_{1}, we need to take into account the effect of equation ∨3. Let ≤ denote the pointwise partial order on ℕ^{n}. As usual, we say that a set U ⊆ ℕ^{n} is an order ideal, if \overline{u} ≤ \overline{v} and \overline{v} ∈ U jointly imply that \overline{u} ∈ U, for all vectors \overline{u}, \overline{v} ∈ ℕ^{n}. Each set U ⊆ ℕ^{n} is contained in a least ideal (U]_{n}, the ideal generated by U. The relation that identifies two sets U, V ∈ P_{f}(ℕ^{n}) if (U]_{n} = (V]_{n} is a congruence relation on P_{f}(ℕ^{n}), and the quotient with respect to this congruence is easily seen to be isomorphic to the subalgebra I_{f}(ℕ^{n}) of P_{f}(ℕ^{n}) generated by the finite non-empty ideals.

For each i ∈ [n], let (\overline{u}_{i}]_{n} denote the principal ideal generated by the unit vector \overline{u}_{i}, i.e., the ideal (\{\overline{u}_{i}\}]_{n}.

Proposition 3.2 I_{f}(ℕ^{n}) is freely generated in V_{1} by the n principal ideals (\overline{u}_{i}]_{n}.

Again, the induced partial order on I_{f}(ℕ^{n}) is the partial order determined by set inclusion.

We note that, if n ≥ 2, then the equation e_{n} fails in I_{f}(ℕ^{n}), and a fortiori in V_{1}. Since for n ≥ 2 the equation e_{n} holds in N but fails in V_{1}, in order to obtain a concrete description of the free algebras in V we need to make further identifications of the ideals in I_{f}(ℕ^{n}). Technically, we shall start with P_{f}(ℕ^{n}).

Let \overline{v}_{1}, …, \overline{v}_{k} (k ≥ 1) be vectors in ℕ^{n}, and suppose that λ_{i} (i ∈ [k]) are non-negative real numbers with ∑_{i∈[k]} λ_{i} = 1. We call the vector of real numbers ∑_{i∈[k]} λ_{i}\overline{v}_{i} a convex linear combination of the \overline{v}_{i}.

Definition 3.3 We call a set U ⊆ P_{f}(ℕ^{n}) a convex ideal if for any convex linear combination ∑_{i∈[k]} λ_{i}\overline{v}_{i}, with \overline{v}_{i} ∈ U for all i ∈ [k], and for any \overline{v} ∈ ℕ^{n}, if

\overline{v} ≤ ∑_{i=1}^{k} λ_{i}\overline{v}_{i}

in the pointwise order, then \overline{v} ∈ U.

Note that any convex ideal is an ideal. Moreover, the intersection of any number of convex ideals is a convex ideal. Thus, any subset U of ℕ^{n} is contained in a least convex ideal, [U]_{n}. When U is finite, so is [U]_{n}. We let \overline{c} ≤ U mean that the simple inequation

\overline{c} · \overline{x} ≤ ⋁_{\overline{d}∈U} \overline{d} · \overline{x}

holds in N. Then we have the following useful characterization of the simple inequations that hold in N.

Lemma 3.4 Suppose that U ∈ P_{f}(ℕ^{n}) and \overline{c} ∈ ℕ^{n}. Then \overline{c} ∈ [U]_{n} iff \overline{c} ≤ U.

Let ∼ denote the congruence relation on P_{f}(ℕ^{n}) that identifies two sets of vectors iff they generate the same least convex ideal. It is immediate to see that the quotient algebra P_{f}(ℕ^{n})/ ∼ is isomorphic to the following algebra CI_{f}(ℕ^{n}) = (CI_{f}(ℕ^{n}), ∨, +, 0) of all non-empty finite convex ideals in P_{f}(ℕ^{n}). For any two I, J ∈ CI_{f}(ℕ^{n}),

I ∨ J = [I ∪ J]_{n}
I + J = [\{\overline{u} + \overline{v} : \overline{u} ∈ I, \overline{v} ∈ J\}]_{n}
0 = \{\overline{0}\} .

Indeed, an isomorphism P_{f}(ℕ^{n})/ ∼→ CI_{f}(ℕ^{n}) is given by the mapping U/ ∼↦ [U]_{n}.

Recall that, for each i ∈ [n], \overline{u}_{i} denotes the ith unit vector in ℕ^{n}. For each i ∈ [n], the set [\overline{u}_{i}]_{n} = (\overline{u}_{i}]_{n} = \{\overline{u}_{i}, \overline{0}\} is the least convex ideal containing \overline{u}_{i}.

Theorem 3.5 CI_{f}(ℕ^{n}) is freely generated by the n convex ideals [\overline{u}_{i}]_{n} in the variety V.

As a corollary of Theorem 3.5, we obtain the following alternative characterization of simple equations which hold in the algebra N.

Corollary 3.6 Let \overline{c}, \overline{d}_{j} (j ∈ [m]) be vectors in ℕ^{n}. Then \overline{c} ≤ \{\overline{d}_{1}, …, \overline{d}_{m}\} iff there are λ_{1}, …, λ_{m} ≥ 0 such that λ_{1} + … + λ_{m} = 1 and \overline{c} ≤ λ_{1}\overline{d}_{1} + … + λ_{m}\overline{d}_{m} with respect to the pointwise ordering. Moreover, if \overline{c} ≤ \{\overline{d}_{1}, …, \overline{d}_{m}\} is irredundant, then λ_{1}, …, λ_{m} > 0.

The above result offers a geometric characterization of the simple inequations in Eq(N), viz. an inequation \overline{c}·\overline{x} ≤ \overline{d}_{1} ·\overline{x}∨…∨\overline{d}_{m} ·\overline{x} (where \overline{x} = (x_{1}, …, x_{n}) is a vector of variables) holds in N iff the vector \overline{c} lies in the ideal generated by the convex hull of the vectors \overline{d}_{1}, …, \overline{d}_{m}.

4 The Two Variable Fragment of the Equational Theory is not Finitely Based

We now proceed to apply the results that we have recalled in the previous section to the study of the two variable fragment of the equational theory of the algebra N. The main aim of this paper is to prove the following result to the effect that the collection of equations Eq_{2}(N) cannot be deduced using any finite number of equations in Eq(N).

Theorem 4.1 There is no finite set E of equations in Eq(N) such that E ⊢ Eq_{2}(N).

To prove Thm. 4.1 we shall define a sequence of algebras A_{n} (n ≥ 1) in V_{1} such that following holds:

For any finite set E of equations which hold in N, there is an n such that

A_{n} ⊧ E but A_{n} |̸= e′_{n} .

Recalling that, for any n, the equation e_{n} is derivable from e′_{n} and Ax_{1}, it is sufficient to prove the statement above with e′_{n} replaced by e_{n}. Furthermore, in light of our previous analysis, the result we are aiming at in this section, viz. Thm. 4.1, may now be reformulated as follows.

Proposition 4.2 Let E be a finite set of simple, irredundant equations such that N ⊧ E. Then there is an n ∈ ℕ and an algebra A_{n} ∈ V_{1} such that A_{n} ⊧ E but A_{n} |̸= e_{n}.

The non-existence of a finite axiomatization of the two variable fragment of the equational theory of N follows easily from Prop. 4.2 and the preceding discussion. In fact, let E be any finite subset of Eq(N). Without loss of generality, we may assume that E includes Ax_{1}, and that E \ Ax_{1} consists of simple, irredundant equations. Then, by Prop. 4.2, there is an algebra A_{n} ∈ V_{1} such that A_{n} ⊧ E but A_{n} |̸= e_{n}. Since e_{n} is derivable from Ax_{1} and e′_{n}, it follows that A_{n} |̸= e′_{n}. We may therefore conclude that E ⊬ Eq_{2}(N), which was to be shown.

4.1 The Algebras A_{n}

We let the weight of a vector \overline{u} ∈ ℕ^{n}, notation |\overline{u}|, be defined as the sum of its components. (Equivalently |\overline{u}| = \overline{u} · \overline{δ}_{n} where \overline{δ}_{n} = (1, …, 1).) To define the algebra A_{n}, where n ≥ 1 is a fixed integer, let us call a set I ⊆ ℕ^{n} an n-convex ideal if it is an ideal and for any convex linear combination \overline{v} = λ_{1}\overline{v}_{1} +…+λ_{m}\overline{v}_{m} and vector \overline{u} ∈ ℕ^{n} of weight |\overline{u}| < n, if \overline{v}_{1}, …, \overline{v}_{m} ∈ I and \overline{u} ≤ \overline{v}, where ≤ is the pointwise order, then \overline{u} ∈ I. It is clear that any convex ideal in ℕ^{n} is n-convex. Any set U ⊆ ℕ^{n} is contained in a least nconvex ideal, denoted [[U]]_{n}. (The subscript n will often be omitted when it is clear from the context.) Call a vector \overline{v} = (v_{1}, …, v_{n}) ∈ ℕ^{n} n-ok, written ok_{n}(\overline{v}), if |\overline{v}| ≤ n and

|\overline{v}| = n ⇒ ∃i ∈ [n]. v_{i} = n .

A set of vectors is n-ok if all of its elements are. Note that if U is a finite non-empty set consisting of n-ok vectors, then [[U]] is also finite and contains only n-ok vectors.

The algebra A_{n} consists of all non-empty (finite) n-convex ideals of n-ok vectors, as well as the element ⊤. The operations are defined as follows: for all I, J ∈ A_{n}, I, J ≠ ⊤, let

K = \{\overline{u} + \overline{v} : \overline{u} ∈ I, \overline{v} ∈ J\} .

Then,

I + J := \{ \begin{matrix}[[K]] & if K contains only n−ok vectors \\ ⊤ & otherwise. \end{matrix}
I ∨ J := [[I ∪ J]]
0 := \{\overline{0}\} = [[\overline{0}]] .

Moreover, we define ⊤ + I = ⊤ ∨ I = ⊤, and symmetrically, for all I ∈ A_{n}.

Proposition 4.3 For each n ≥ 1, A_{n} ∈ V_{1}.

Proof: For every I ∈ I_{f}(ℕ^{n}), let h(I) = [[I]], if I contains only n-ok vectors, otherwise let h(I) = ⊤. This defines a surjective homomorphism h : I_{f}(ℕ^{n}) → A_{n}. Thus A_{n} is a quotient algebra of I_{f}(ℕ^{n}), and the result follows from Proposition 3.2. □

We shall now show that, for every n ≥ 2, the algebra A_{n} is not in V. In particular, if n ≥ 2, then the equations e_{n} and e′_{n} do not hold in A_{n}.

Lemma 4.4 If n ≥ 2 then A_{n} |̸= e_{n} and A_{n} |̸= e′_{n}.

Proof: Assume that n ≥ 2. Let J_{i} = [[\{\overline{u}_{i}\}]]_{n} (i ∈ [n]), where \overline{u}_{i} denotes the ith unit vector in ℕ^{n}. Then, since n ≥ 2,

J_{1} + … + J_{n} = ⊤ .

Furthermore, for i ∈ [n],

nJ_{i} = [[\{(\overbrace{0, …, 0, n}^{i places}, 0 …, 0)\}]]_{n}

and therefore

nJ_{1} ∨ … ∨ nJ_{n} = [[{(n, 0, …, 0, 0), …, (0, 0, …, 0, n)}]]_{n} ≠ ⊤ .

It follows that e_{n} fails in A_{n}. Since e_{n} is derivable from Ax_{1} and e′_{n}, Prop. 4.3 yields that e′_{n} also fails in A_{n}. □

Note that the induced partial order on A_{n} has ⊤ as its top element, and coincides with the inclusion order over the elements in A_{n} that are different from ⊤. For K ∈ P_{f}(ℕ^{n}), by slightly abusing notation, we let [[K]] stand for [[K]] in the original sense if K contains only n-ok vectors and ⊤ otherwise. With this extension of the definition of [[ ]] we have that [[K]]+[[L]] = [[K +L]] for all K, L ∈ P_{f}(ℕ^{n}). Using this notation, denoting the induced preorder on A_{n} by ⊑_{n}, we obtain the following alternative characterization of A_{n} as a quotient algebra of P_{f}(ℕ^{n}), which will be used in the technical developments to follow.

Let L, M ∈ P_{f}(ℕ^{n}). We write

L ≤ M ⇔ ∀\overline{u} ∈ L. \overline{u} ≤ M .

Now,

A_{n} = {[[L]] : L ∈ P_{f}(ℕ^{n})}

where

[[L]] ⊑_{n} [[M]] iff L ⪯_{n} M

and

L ⪯_{n} M ⇔ [ok_{n}(M) ⇒ (ok_{n}(L) ∧ L ≤ M)] .

We use ≈_{n} to denote the kernel of ⪯_{n}. Similarly Lemma 3.4 provides us with the following characterization of CI_{f}(ℕ^{n}):

CI_{f}(ℕ^{n}) = {[L] : L ∈ P_{f}(ℕ^{n})}

where, by Lemma 3.4,

[L] ⊆ [M] iff L ≤ M .

We extend the definition of the weight function to elements of P_{f}(ℕ^{n}) thus:

|L| = max\{|\overline{u}| : \overline{u} ∈ L\} .

Now we have the following easy, but useful result.

Lemma 4.5 If L ≤ M then |L| ≤ |M|.

We recall that ∼ denotes the kernel of the preorder ≤.

Lemma 4.6

1. For all m and all L ∈ P_{f}(ℕ^{n}), mL ∼ \{m\overline{u} : \overline{u} ∈ L\}.

2. If p is prime and m < p then m[[K]]_{p} = [[\{m\overline{u}|\overline{u} ∈ K\}]]_{p}.

Proof: We prove the two statements in turn.

1. Let K = \{m\overline{u} : \overline{u} ∈ L\}. We shall prove that mL ∼ K. Obviously K ⊆ mL, which in turn implies that K ≤ mL. To prove that mL ≤ K holds, assume \overline{v} = \overline{v}_{1} + … + \overline{v}_{m} ∈ mL, where \overline{v}_{1}, …, \overline{v}_{m} ∈ L, and that \overline{r} ∈ ℕ^{n}. Let i\overline{r} be the index of the largest amongst the numbers \overline{v}_{1} · \overline{r}, …, \overline{v}_{m} · \overline{r}. Then we have

\overline{v} · \overline{r} = \overline{v}_{1} · \overline{r} + … + \overline{v}_{m} · \overline{r} ≤ (m\overline{v}_{i\overline{r}}) · \overline{r}

where m\overline{v}_{i\overline{r}} ∈ K. This proves the first statement in the lemma.

2. The case m = 1 is trivial so we may assume that m > 1. To prove the statement in this case, let L = \{m\overline{v}|\overline{v} ∈ K\}. Suppose that p is a prime number and 2 ≤ m < p. In light of our previous remarks, it is sufficient to show that mK ≈_{p} L. First we recall that

mK = \underbrace{K + … + K}_{m times} = \{\overline{v}_{1} + … + \overline{v}_{m} : \overline{v}_{i} ∈ K, i ∈ [m]\} .

In particular this implies that L ⊆ mK and therefore that L ⪯_{p} mK. To prove that mK ⪯_{p} L holds we proceed as follows. We know from Lemma 4.6(1) that mK ≤ L. It is therefore sufficient to prove that ¬ok_{p}(mK) implies ¬ok_{p}(L). To this end, assume that there is a \overline{v}_{1} + … + \overline{v}_{m} ∈ mK which is not p-ok and let \overline{v}_{i} be the vector of maximum weight amongst \overline{v}_{1}, … \overline{v}_{m}. Then

|m\overline{v}_{i}| = m|\overline{v}_{i}| ≥ |\overline{v}_{1}| + … |\overline{v}_{m}| ≥ p .

That m|\overline{v}_{i}| = p is impossible, as p is prime and m ≥ 2. Therefore |m\overline{v}_{i}| = m|\overline{v}_{i}| > p which means that m\overline{v}_{i} is not p-ok. As m\overline{v}_{i} ∈ L, this proves that L is not p-ok, which was to be shown. □

Note that Lemma 4.6(2) does not hold in general if p is not prime. For instance, if p = 4, m = 2 and K = {(2, 0), (0, 2)}, then

⊤ = m[[K]]_{p} ≠ [[{(4, 0), (0, 4)}]]_{p} .

In what follows we let the simple inequation

a^{1}x_{1} + … + a^{m}x_{m} ≤ c_{1}^{1}x_{1} + … + c_{1}^{m}x_{m} ; ∨ ; ⋮ ; ∨ ; c_{k}^{1}x_{1} + … + c_{k}^{m}x_{m}

be represented by (a^{i})^{i≤m} ≤ (c_{j}^{i})_{j≤k}^{i≤m} (or sometimes simply by \overline{a} ≤ \overline{\overline{C}} if the meaning is clear from the context), where (a^{i})^{i≤m} denotes the the row vector

(a^{1}, ⋯, a^{m}) and (c_{j}^{i})_{j≤k}^{i≤m} the k × m matrix [ \begin{matrix}c_{1}^{1} … c_{1}^{m} \\ ⋮ & ⋮ \\ c_{k}^{1} … c_{k}^{m} \end{matrix} ]. We also let an

instantiation of the variables x_{1}, …, x_{m} by the singleton sets \{\overline{η}_{1}\}, …, \{\overline{η}_{m}\} (or equivalence classes generated by these sets) be represented as

\overline{\overline{η}} = [ \overline{η}_{1} ; ⋮ ; \overline{η}_{m} ] = [ \begin{matrix}η_{1}^{1} … η_{1}^{n} \\ ⋮ & ⋮ \\ η_{m}^{1} … η_{m}^{n} \end{matrix} ] ,

i.e. the matrix with row vectors \overline{η}_{1}, …, \overline{η}_{m}. We note that, by commutativity of ∨, the simple inequation \overline{a} ≤ \overline{\overline{B}}, where \overline{\overline{B}} is any matrix obtained by permuting the rows of \overline{\overline{C}}, represents exactly the same simple inequation as \overline{a} ≤ \overline{\overline{C}}, viz. the inequation \overline{a} ≤ U, where U = \{\overline{c}_{1}, …, \overline{c}_{k}\} and the \overline{c}_{i} (i ∈ [k]) are the row vectors of \overline{\overline{C}}. Similarly any permutation of the column vectors of \overline{\overline{C}} combined with a corresponding permutation of the entries of \overline{a} yields a simple inequation that holds in N iff \overline{a} ≤ \overline{\overline{C}} does. (Any instantiation matrix should be similarly permuted as well.) The weight of \overline{\overline{C}}, notation |\overline{\overline{C}}|, is defined as the sum of its entries.

Notation: In the remainder of this paper, \overline{a} and \overline{\overline{C}} will denote a row vector in ℕ^{1×m} and a matrix in ℕ^{k×m}, respectively.

Now we have the following corollaries of Lemma 4.6.

Corollary 4.7 Let p be a prime number. If p > max\{|\overline{a}|, |\overline{\overline{C}}|\} then the following holds. For all L_{1}, …, L_{m} ∈ P_{f}(ℕ^{p}),

\begin{matrix}∀(\overline{v}_{1}, …, \overline{v}_{m}) ∈ L_{1} × … × L_{m}. \\ \{a^{1}\overline{v}_{1} + … + a^{m}\overline{v}_{m}\} ⪯_{p} \{c_{1}^{1}\overline{v}_{1} + … + c_{1}^{m}\overline{v}_{m}, ; ⋮ ; c_{k}^{1}\overline{v}_{1} + … + c_{k}^{m}\overline{v}_{m}\} \end{matrix}

implies

a^{1}L_{1} + … + a^{m}L_{m} ⪯_{p} c_{1}^{1}L_{1} + … + c_{1}^{m}L_{m} ; ∪ ; ⋮ ; ∪ ; c_{k}^{1}L_{1} + … + c_{k}^{m}L_{m} .

Proof: Follows directly from Lemma 4.6(2). □

The next result will play a key role in the proof of Thm. 4.9 to follow. Corollary 4.8 Assume that \overline{a} ≤ \overline{\overline{C}} holds and is irredundant. Then A_{p} |̸= \overline{a} ≤ \overline{\overline{C}}, where p is a prime number with |\overline{a}| < p and |\overline{\overline{C}}| < p, iff there is an instantiation matrix \overline{\overline{η}} ∈ ℕ^{m×p}, such that

1. \overline{a} · \overline{\overline{η}} has weight p and at least two non-zero coefficients, and

2. \overline{c}_{j} · \overline{\overline{η}} has weight p and exactly one non-zero coefficient for j ∈ [k].

Proof: We prove the two implications separately.

• ‘Only If Implication’: We establish that each condition is met in

turn.

1. Assume that \overline{a} ≤ \overline{\overline{C}} holds in N, and therefore in CI_{f}(ℕ^{p}) (Theorem 3.5), but not in A_{p}. Then, as |\overline{a}| < p and |\overline{\overline{C}}| < p, for some

L_{1}, …, L_{m} ∈ P_{f}(ℕ^{p}),

\overline{a} · [ L_{1} ; ⋮ ; L_{m} ] ≤ \overline{\overline{C}} · [ L_{1} ; ⋮ ; L_{m} ]

but

\overline{a} · [ L_{1} ; ⋮ ; L_{m} ] ⪯̸_{p} \overline{\overline{C}} · [ L_{1} ; ⋮ ; L_{m} ]

where \overline{\overline{C}}·[ L_{1} ; ⋮ ; L_{m} ] has the obvious meaning in P_{f}(ℕ^{p}). By Cor. 4.7

there is a (\overline{η}_{1}, …, \overline{η}_{m}) ∈ L_{1} × … × L_{m} such that

\{\overline{a} · [ \overline{η}_{1} ; ⋮ ; \overline{η}_{m} ]\} ≤ \{ \overline{c}_{1} · [ \overline{η}_{1} ; ⋮ ; \overline{η}_{m} ] , ; ⋮ ; \overline{c}_{k} · [ \overline{η}_{1} ; ⋮ ; \overline{η}_{m} ] \}

but

\{\overline{a} · [ \overline{η}_{1} ; ⋮ ; \overline{η}_{m} ]\} ⪯̸_{p} \{ \overline{c}_{1} · [ \overline{η}_{1} ; ⋮ ; \overline{η}_{m} ] , ; ⋮ ; \overline{c}_{k} · [ \overline{η}_{1} ; ⋮ ; \overline{η}_{m} ] \} .

Let \overline{\overline{η}} = [ \overline{η}_{1} ; ⋮ ; \overline{η}_{m} ]. First we note that if \overline{a} · \overline{\overline{η}} is p-ok then, by

definition of ⪯_{p},

\{\overline{a} · \overline{\overline{η}}\} ⪯_{p} \{\overline{c}_{j} · \overline{\overline{η}} : j ∈ [k]\}

which contradicts our assumption. Thus we may conclude that \overline{a}·\overline{\overline{η}} is not p-ok. Next we note that if |\overline{a}·\overline{\overline{η}}| > p then, by Lemma 4.5, |\{\overline{c}_{j} · \overline{\overline{η}} : j ∈ [k]\}| > p and therefore

\{\overline{a} · \overline{\overline{η}}\} ⪯_{p} \{\overline{c}_{j} · \overline{\overline{η}} : j ∈ [k]\} ,

again a contradiction to our assumption. Thus we are left with the case where |\overline{a} · \overline{\overline{η}}| = p and \overline{a} · \overline{\overline{η}} has at least two non-zero coefficients.

2. By Cor. 3.6, since \overline{a} ≤ \overline{\overline{C}} holds in CI_{f}(ℕ^{p}), we may infer that

\overline{a} ≤ λ_{1}\overline{c}_{1} + … + λ_{k}\overline{c}_{k} ,

where, as \overline{a} ≤ \overline{\overline{C}} is irredundant, λ_{1}, …, λ_{k} > 0 and λ_{1}+…+λ_{m} = 1. By associativity of matrix multiplication we have that

\overline{a} · \overline{\overline{η}} ≤ λ_{1}(\overline{c}_{1} · \overline{\overline{η}}) + … + λ_{k}(\overline{c}_{k} · \overline{\overline{η}})

which in turn implies

p = |\overline{a} · \overline{\overline{η}}| ≤
|λ_{1}(\overline{c}_{1} · \overline{\overline{η}})| + … + |λ_{k}(\overline{c}_{k} · \overline{\overline{η}})| =
λ_{1}|\overline{c}_{1} · \overline{\overline{η}}| + … + λ_{k}|\overline{c}_{k} · \overline{\overline{η}}| .

As by the analysis at point 1 of the proof |\overline{c}_{j} · \overline{\overline{η}}| ≤ p, for j ∈ [k], this implies that |\overline{c}_{j} · \overline{\overline{η}}| = p for j ∈ [k]. Thus, as every \overline{c}_{j} · \overline{\overline{η}} is p-ok, it must have exactly one non-zero coefficient for every j ∈ [k].

• ‘If Implication”: Take an instantiation matrix \overline{\overline{η}} ∈ ℕ^{m×p} that satisfies the proviso of this statement. Let x_{1} = J_{1} = [[\{\overline{η_{1}}\}]]_{n}, …, x_{m} = J_{m} = [[\{\overline{η_{m}}\}]]_{n}. Then it is easy to check that

a^{1}J_{1} + … + a^{m}J_{m} = ⊤

but that

c_{j}^{1}J_{1} + … + c_{j}^{m}J_{m} ≠ ⊤ for j ∈ [k]

and therefore

⋁_{j∈[k]} c_{j}^{1}J_{1} + … + c_{j}^{m}J_{m} ≠ ⊤ .

Thus the inequation \overline{a} ≤ \overline{\overline{C}} does not hold in A_{p}. □

Note that if \overline{\overline{η}} is an instantiation matrix satisfying points 1–2 in the above statement, then so does any matrix obtained by permuting the columns of \overline{\overline{η}}.

Using the previous result, we are now in a position to show the following theorem, which is the key to the proof of Propn. 4.2 and of Thm. 4.1.

Theorem 4.9 If \overline{a} ≤ \overline{\overline{C}} is irredundant and holds in N, then A_{p} |̸= \overline{a} ≤ \overline{\overline{C}} for at most one prime number p > max\{|\overline{a}|, |\overline{\overline{C}}|\}.

Proof: Assume that \overline{a} = (a^{1}, …, a^{m}) ∈ ℕ^{1×m} and \overline{\overline{C}} = (c_{j}^{i})_{j≤k}^{i≤m} ∈ ℕ^{k×m}

(i.e. the inequation \overline{a} ≤ \overline{\overline{C}} contains at most m variables) and that N ⊧ \overline{a} ≤ \overline{\overline{C}}. Assume furthermore that the statement of the theorem does not hold and that m is the smallest number of variables for which it fails; we shall show that this leads to a contradiction. So suppose that N ⊧ \overline{a} ≤ \overline{\overline{C}} but that A_{p} |̸= \overline{a} ≤ \overline{\overline{C}} and A_{q} |̸= \overline{a} ≤ \overline{\overline{C}}, where p and q are prime and max\{|\overline{a}|, |\overline{\overline{C}}|\} < p < q. First we note that we may assume that a^{i} > 0 for i ∈ [m], or else we could immediately reduce the number of variables in the equation under consideration. Since \overline{a} ≤ \overline{\overline{C}} holds in N, this implies that each column of \overline{\overline{C}} is non-zero. We now continue with the proof as follows: First we use the assumption A_{p} |̸= \overline{a} ≤ \overline{\overline{C}} and Corollary 4.8 to analyze the structure of \overline{a} and \overline{\overline{C}}. Then we argue that the result of this analysis contradicts our second assumption, viz. the failure of the inequation \overline{a} ≤ \overline{\overline{C}} in A_{q}.

As A_{p} |̸= \overline{a} ≤ \overline{\overline{C}}, by Corollary 4.8 there is an instantiation matrix \overline{\overline{η}} = (η_{i}^{r})_{i≤m}^{r≤p} ∈ ℕ^{m,p}, such that

• \overline{a} · \overline{\overline{η}} has weight p and at least two non-zero coefficients and

• \overline{c}_{j} ·\overline{\overline{η}} has weight p and exactly one non-zero coefficient, for every j ∈ [k].

By minimality of m, we may furthermore assume that each row of \overline{\overline{η}} contains a non-zero entry.

By rearranging the order of the rows of \overline{\overline{C}} (i.e. the order of the terms that occur on the right-hand side of the simple equation) and of the columns of \overline{\overline{η}}, we may assume that there is a 0 < k_{0} ≤ k such that

1. \overline{c}_{j} · \overline{\overline{η}} = (p, 0, …, 0) for j ∈ [k_{0}] and

2. \overline{c}_{j} · \overline{\overline{η}} = (0, l_{j}^{2}, …, l_{j}^{m}) for k_{0} < j ≤ k, where exactly one of the l_{j}^{i} is non-zero for 2 ≤ i ≤ m.

By rearranging the columns of \overline{\overline{C}} and correspondingly the order of the entries of \overline{a} and \overline{\overline{η}} (i.e. the order of the variables that occur in the equation), we may assume that there is an m_{0} ∈ [m] such that if j ≤ k_{0} then c_{j}^{i} = 0 for all i > m_{0}. Therefore we may suppose that \overline{\overline{C}} looks as follows:

\overline{\overline{C}} = [ \begin{matrix}\begin{matrix}c_{1}^{1} … c_{1}^{m_{0}} \\ ⋮ & ⋮ \\ c_{k_{0}}^{1} … c_{k_{0}}^{m_{0}} \end{matrix} & \overline{\overline{O}}_{1} \\ \overline{\overline{O}}_{2} & ? \end{matrix} ]  (1)

where \overline{\overline{O}}_{1} and \overline{\overline{O}}_{2} are (possibly empty) 0-matrices (i.e., matrices whose entries are all 0) and ? just means that this part of the matrix is unknown. Recall that, as previously observed, some of the c_{j}^{i} (i ∈ [m_{0}], j ∈ [k_{0}]) may be 0, but no column in the upper left corner of \overline{\overline{C}} is identically 0.

We claim that k_{0} < k and m_{0} < m, and therefore that \overline{\overline{O}}_{1} and \overline{\overline{O}}_{2} are both non-trivial. To see that this claim holds, note that, by 1.-2. above, \overline{\overline{η}} has the form

\overline{\overline{η}} = [ \begin{matrix}η_{1}^{1} ; ⋮ ; η_{m_{0}}^{1} & \overline{\overline{O}} \\ ? & ? \end{matrix} ]

where \overline{\overline{O}} is a 0-matrix. This follows because if some of the columns of the

matrix to the right of the first column (the one that starts with [ η_{1}^{1} ; ⋮ ; η_{m_{0}}^{1} ])

has a non-zero entry above the horizontal solid line, at least one of the \overline{c}_{j} · \overline{\overline{η}}, j ∈ [k_{0}], is going to have more than one non-zero entry. Since the rows of \overline{\overline{η}} are non-zero, we have that η_{j}^{1} ≠ 0 for every j ∈ [m_{0}]. Using this fact it is not difficult to see that, as claimed, the cases where either k_{0} = k or m_{0} = m cannot occur. Indeed, if m_{0} = m then \overline{\overline{η}} has only one non-zero column and consequently \overline{a}·\overline{\overline{η}} cannot have two non-zero coefficients. Moreover, if k_{0} = k and m_{0} < m then the right hand side of the inequation does not contain the variables x_{i}, with m_{0} < i ≤ m, whereas, by assumption, the left hand side does—a contradiction to the fact that the inequation \overline{a} ≤ \overline{\overline{C}} holds in N. We may therefore assume that k_{0} < k and m_{0} < m.

Now we recall from Cor. 3.6 that, since \overline{a} ≤ \overline{\overline{C}} is an irredundant inequation that holds in N, there is a sequence of real numbers λ_{i}, i ∈ [k], such that

\overline{a} ≤ (λ_{1}\overline{c}_{1} + … + λ_{k_{0}} \overline{c}_{k_{0}}) + (λ_{k_{0}+1}\overline{c}_{k_{0}+1} + … + λ_{k}\overline{c}_{k}) ,

where λ_{i} > 0 for i ∈ [k] and λ_{1} + … + λ_{k} ≤ 1. Next let

\overline{a}_{1} = (a^{1}, …, a^{m_{0}}, 0, …, 0)  and
\overline{a}_{2} = (0, …, 0, a^{m_{0}+1}, …, a^{m}) .

Then \overline{a} = \overline{a}_{1} + \overline{a}_{2} and

\begin{matrix}\overline{a} · \overline{\overline{η}} = \overline{a}_{1} · \overline{\overline{η}} + \overline{a}_{2} · \overline{\overline{η}} ≤ \\ (λ_{1}\overline{c}_{1} · \overline{\overline{η}} + … + λ_{k_{0}} \overline{c}_{k_{0}} · \overline{\overline{η}}) + (λ_{k_{0}+1}\overline{c}_{k_{0}+1} · \overline{\overline{η}} + … + λ_{k}\overline{c}_{k} · \overline{\overline{η}}) . \end{matrix}

By multiplying with \overline{δ}_{p} = (1, ..., 1) ∈ ℕ^{p}, and therefore getting the weight, we have:

p = (\overline{a} · \overline{\overline{η}}) · \overline{δ}_{p} = (\overline{a}_{1} · \overline{\overline{η}}) · \overline{δ}_{p} + (\overline{a}_{2} · \overline{\overline{η}}) · \overline{δ}_{p} ≤
λ_{1}(\overline{c}_{1} · \overline{\overline{η}}) · \overline{δ}_{p} + … + λ_{k}(\overline{c}_{k} · \overline{\overline{η}}) · \overline{δ}_{p} =
λ_{1}|\overline{c}_{1} · \overline{\overline{η}}| + … + λ_{k}|\overline{c}_{k} · \overline{\overline{η}}| =
λ_{1}p + … + λ_{k}p ≤ p .

Thus these last two inequalities must be equalities, and

p = (\overline{a} · \overline{\overline{η}}) · \overline{δ}_{p} = (λ_{1} + … + λ_{k})p .

Furthermore, because of the special structure of the coordinates of the vectors \overline{a}_{1}, \overline{a}_{2}, \overline{c}_{1}, ..., \overline{c}_{k}, we must have that

\overline{a}_{1} ≤ λ_{1}\overline{c}_{1} + ... + λ_{k_{0}} \overline{c}_{k_{0}}

and

\overline{a}_{2} ≤ λ_{k_{0}+1}\overline{c}_{k_{0}+1} + ... + λ_{k}\overline{c}_{k}

and therefore, using similar reasoning as above,

(\overline{a}_{1} · \overline{\overline{η}}) · \overline{δ}_{p} ≤ (λ_{1} + … + λ_{k_{0}})p

and

(\overline{a}_{2} · \overline{\overline{η}}) · \overline{δ}_{p} ≤ (λ_{k_{0}+1} + … + λ_{k})p .

From above we know that both the left hand sides and the right hand sides of these inequalities sum up to p; therefore these two inequalities must be equalities. Thus we have proven that

n_{p} = (\overline{a}_{1} · \overline{\overline{η}}) · \overline{δ}_{p} = λp ,

where λ = λ_{1} + … + λ_{k_{0}} and n_{p} ∈ ℕ. Note that, as k_{0} < k and λ_{i} > 0 (i ∈ [k]), it holds that λ < 1. Hence we have that n_{p} < p.

In a similar way, using the form of \overline{\overline{C}} in (1) and the fact that q > p, N ⊧ \overline{a} ≤ \overline{\overline{C}} and A_{q} |̸= \overline{a} ≤ \overline{\overline{C}}, we may conclude that there is a \overline{\overline{γ}} ∈ ℕ^{m×q} such that

n_{q} = (\overline{a}_{1} · \overline{\overline{γ}}) · \overline{δ}_{q} = λq .

This in turn implies that \frac{n_{p}}{p} = \frac{n_{q}}{q} or equivalently n_{p} ·q = n_{q} ·p, contradicting our assumption that n_{p} < p, n_{q} < q and p and q are different primes. We may therefore conclude that no such minimal number of variables m exists and consequently that the statement of the theorem holds. This completes the proof of the theorem. □

Prop. 4.2 follows immediately from the above result, completing the proof of the non-existence of a finite equational axiomatization for the two-variable fragment of the equational theory of the algebra N.

Remark 4.1 Using our results, it is easy to show that the reduct (ℕ, ∨, +) of N is also not finitely based, and that the two variable fragment of its equational theory has no finite equational axiomatization.

Remark 4.2 As a further corollary of Thm 4.1, we obtain that the equational theory of the algebra (ℕ, ∨, +, 0, 1) is also not finitely based. To see this, note that whenever an equation holds in (ℕ, ∨, +, 0, 1) and one side contains an occurrence of the symbol 1, then so does the other side. Let E be an axiom system for (ℕ, ∨, +, 0, 1), and let E_{0} denote the subset of E consisting of all the equations not containing occurrences of the constant 1. In light of the above observation, E_{0} is an axiom system for the reduct N of (ℕ, ∨, +, 0, 1). Thus the existence of a finite basis for the algebra (ℕ, ∨, +, 0, 1) would contradict Thm. 4.1.

In similar fashion, it is easy to prove that the two variable fragment of the equational theory of the algebra (ℕ, ∨, +, 0, 1) has no finite equational axiomatization.

5 An Application to Process Algebra

We now offer an application of the results we have developed in this paper to the field of process algebra. (The interested reader is referred to [2] for a textbook presentation of this field of research.)

We begin by presenting the language of Basic Process Algebra (BPA)

[3] (over a singleton set of actions) with the empty process [10] and its operational semantics.

The Syntax We assume a countably infinite set Var of process variables, with typical element x. We use a to denote the only action symbol that may be used in process terms.

The language (BPA_{ε}) of Basic Process Algebra with the empty process and action a is given by the following BNF grammar:

P ::= ε | a | x | P + P | P · P .

The set of closed terms, i.e., terms that do not contain occurrences of process variables, is denoted by T(BPA_{ε}). We shall use P, Q to range over (BPA_{ε}). A closed substitution is a mapping from process variables to closed terms in the language (BPA_{ε}). For every term P and closed substitution σ, the closed term obtained by replacing every occurrence of a variable x in P with the closed term σ(x) will be written P σ.

Operational Semantics and Trace Equivalence The operational semantics for the language of closed terms T(BPA_{ε}) is defined by the transition rules in Table 1 from [2]. These rules define transitions P →^{a} P′ to express that term P can evolve into term P′ by the execution of action a, and transitions P √ to express that term P can terminate successfully.

\overline{a →^{a} ϵ}  \overline{ϵ√}

\frac{P √}{P + Q√} \frac{P →^{a} P′}{P + Q →^{a} P′} \frac{Q√}{P + Q√} \frac{Q →^{a} Q′}{P + Q →^{a} Q′}

\frac{P √ Q√}{P · Q√} \frac{P √ Q →^{a} Q′}{P · Q →^{a} Q′}  \frac{P →^{a} P′}{P · Q →^{a} P′ · Q}

Table 1: Transition Rules for T(BPA_{ε}).

For n ≥ 0, we write P →^{a^{n}} P′ iff there exist terms P_{0}, …, P_{n} such that P = P_{0} →^{a} P_{1} →^{a} ⋯ P_{n−1} →^{a} P_{n} = P′. In that case, we say that a^{n} is a trace of term P [6]. For terms P, Q ∈ T(BPA_{ε}), we write P ≃ Q iff P and Q afford the same traces. Note that the collection of traces of a term is non-empty and prefix-closed. Moreover, since a is the only action, it is completely determined by the longest sequence it contains. This is the key to the proof of the following result.

Proposition 5.1 The relation ≃ is preserved by the operators in the signature of (BPA_{ε}).

In light of Propn. 5.1, we can construct the quotient algebra

T = (T(BPA_{ε})/≃, ·, +, ε, a)

of closed (BPA_{ε})-terms modulo ≃. That is, for P, Q ∈ (BPA_{ε}),

T ⊧ P = Q iff (for all closed substitutions σ : P σ ≃ Qσ) .

The equational theory of T will be written Eq(T). Our order of business in the remainder of this paper will be to show the following result to the effect that there is no finite equational axiomatization of the algebra T, i.e., of trace equivalence over the language T(BPA_{ε}).

Theorem 5.1 The algebra T is not finitely based. In particular, no finite subset of Eq(T) proves all the equations in two variables that hold in T.

To prove the above theorem, note that T is isomorphic to the algebra (ℕ, ∨, +, 0, 1), if we interpret summation over ℕ as ·, ∨ as +, and the constants 0 and 1 as ε and a, respectively. (An isomorphism would simply map the congruence class of term P to the length of the longest trace P affords.) Therefore the claim follows immediately from Remark 4.2.

Remark 5.1 As a corollary of the observations in Remark 4.1, similar results can be proven mutatis mutandis for trace equivalence over the language of Basic Process Algebra (over a singleton set of actions) without the empty process.

References

[1] L. Aceto, Z. Ésik, and A. Ingólfsdóttir, The Max-Sum Algebra of the Natural Numbers has no Finite Equational Basis, Technical Report 99-1-001, Department of Computer Science, The University of Aizu, 1999.

[2] J. Baeten and W. Weijland, Process Algebra, Cambridge Tracts in Theoretical Computer Science 18, Cambridge University Press, 1990.

[3] J. Bergstra and J. Klop, Fixed point semantics in process algebras, Report IW 206, Mathematisch Centrum, Amsterdam, 1982.

[4] S. Burris and H. P. Sankappanavar, A Course in Universal Algebra, Springer-Verlag, New York, 1981.

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

[6] C. Hoare, Communicating Sequential Processes, Prentice-Hall International, Englewood Cliffs, 1985.

[7] G. McNulty, A field guide to equational logic, J. Symbolic Computation, 14 (1992), pp. 371–397.

[8] W. Taylor, Equational logic, in Contributions to universal algebra, North-Holland Publishing Co., Amsterdam, 1977, pp. 465–501. Proceedings of the Colloquium held in Szeged, 1975. Colloquia Mathematica Societatis János Bolyai, vol. 17.

[9] , Equational logic, in [5], Appendix 4, pp. 378–400.

[10] J. Vrancken, The algebra of communicating processes with empty process, Theoretical Comput. Sci., 177(1997), pp. 287–328.

Recent BRICS Report Series Publications

RS-99-22 Luca Aceto, Zoltán Ésik, and Anna Ingólfsdóttir. On the Two-Variable Fragment of the Equational Theory of the Max-Sum Algebra of the Natural Numbers. August 1999. 22 pp.

RS-99-21 Olivier Danvy. An Extensional Characterization of Lambda-Lifting and Lambda-Dropping. August 1999. 13 pp. Extended version of an article to appear in Fourth Fuji International Symposium on Functional and Logic Programming, FLOPS ’99 Proceedings (Tsukuba, Japan, November 11–13, 1999). This report supersedes the earlier report BRICS RS-98-2.

RS-99-20 Ulrich Kohlenbach. A Note on Spector’s Quantifier-Free Rule of Extensionality. August 1999. 5 pp. To appear in Archive for Mathematical Logic.

RS-99-19 Marcin Jurdziński and Mogens Nielsen. Hereditary History Preserving Bisimilarity is Undecidable. June 1999. 18 pp.

RS-99-18 M. Oliver Möller and Harald Rueß. Solving Bit-Vector Equations of Fixed and Non-Fixed Size. June 1999. 18 pp. Revised version of an article appearing under the title Solving Bit-Vector Equations in Gopalakrishnan and Windley, editors, Formal Methods in Computer-Aided Design: Second International Conference, FMCAD ’98 Proceedings, LNCS 1522, 1998, pages 36–48.

RS-99-17 Andrzej Filinski. A Semantic Account of Type-Directed Partial Evaluation. June 1999. To appear in Nadathur, editor, International Conference on Principles and Practice of Declarative Programming, PPDP99 ’99 Proceedings, LNCS, 1999.

RS-99-16 Rune B. Lyngsø and Christian N. S. Pedersen. Protein Folding in the 2D HP Model. June 1999. 15 pp.

RS-99-15 Rune B. Lyngsø, Michael Zuker, and Christian N. S. Pedersen. An Improved Algorithm for RNA Secondary Structure Prediction. May 1999. 24 pp. An alloy of two articles appearing in Istrail, Pevzner and Waterman, editors, Third Annual International Conference on Computational Molecular Biology, RE-COMB 99 Proceedings, 1999, pages 260–267, and Bioinformatics, 15, 1999.