# Deciding whether the ordering is necessary in a Presburger formula.

Introduction

Presburger arithmetic is the fragment of arithmetic concerning the integers with addition and order. Presburger's supervisor considered the decidability of this fragment too modest a result to deserve a Ph.D. degree and he accepted it only as a Master's Thesis in 1928. Looking at the number of citations, we may say that history revised this depreciative judgment long ago. There still remains, at least as far as we can see, some confusion concerning the domain of the structure: Z or N? with or without the order relation? (the main popular mathematical web sites disagree on that respect). The original paper deals with the additive group of positive and negative integers with no binary relation, but in a final remark of the original communication, the author asserts that the same result, namely quantifier elimination, holds when the structure is enriched with the binary relation "<". In [1], which is the main reference on the subject, Presburger arithmetic is defined as the elementary theory of integers with equality, addition and having 0 and 1 as constant symbols and "<" as binary predicate, see also [20]. On the other hand, the majority of the "modern" papers referring to Presburger arithmetic is concerned with the natural numbers where the order relation is unnecessary as it is first-order expressible in (N; +}.

The origin of the present work is the simple remark that concerning the set of integers Z, the binary relation matters. Here we study the decidability of the definability in the structure (Z; +, 0,1} which we call the weak Presburger arithmetic, for a given relation defined in (Z; +, <, 0,1}. We show that it is indeed recursively decidable and we prove this result by revisiting the notion of linear subsets introduced by Ginsburg and Spanier [9]; [10]; [11]; [12]) in the sixties for n-ary relations on N. Other problems of definability in substructures of Presburger arithmetic introduced in [15] have been solved positively in [4]: given a formula in the Presburger arithmetic, it is recursively decidable whether or not it can be expressed in the structure with domain Z (resp. N) and with the unique predicates of the form x - y > a and x > a for all a [member of] Z (resp. a [member of] N).

Despite its simplicity, Presburger arithmetic is central in many areas of theoretical and applied computer science. From a theoretical point of view, it has many remarkable properties: 1) it admits quantifier elimination [1]; [19]; [20] and therefore it is decidable, 2) given a formula on the expansion of the structure obtained by adding the function which to each integer assigns the maximal power of 2 which divides it, it is decidable whether or not it is definable by a Presburger formula over N, [18]; the claim of a polynomial time algorithm can be found in [17]. Moreover, there is a strong and old connection between language theory, Presburger definable sets and rational relations on Z and N dating back to the sixties [2]; [7]; [9]. The concept is also widely used in many application areas, such as program analysis and model-checking and more specifically timed automata since it models infinite systems, see for example [3].

The paper is organized as follows. Section 1 recalls known results which are necessary for the rest of the paper, essentially around the notion of linear sets in Zn. Section 2 investigates the closure properties of the linear sets. This allows us to give in Section 3 a characterization of the subsets of Zn which are definable in the weak Presburger arithmetic, along with a decision procedure.

1 Preliminaries

1.1 Variants of Presburger arithmetic

In this paper we deal with first-order languages with equality, i.e., the signature of a structure implicitly contains the symbol "= ". As observed in the introduction, a source of confusion is the lack of agreement in the definition of Presburger arithmetic itself. We make the convention of calling weak Presburger arithmetic the structure [Z.sup.W] = (Z; +; 0,1} originally studied in [19] (see also [21] for an English translation and commentary), while with Z we mean the (standard) Presburger arithmetic (Z; +, <, 0,1}. Observe that the predicate <, as restriction of the order on Z to N, is already definable in (N; +}. These structures are decidable in the sense that given a closed formula, it is recursively decidable whether or not it holds in that structure. In particular [Z.sup.W] admits quantifier elimination in the augmented language with the additional unary functional symbol "- " and the (recursive) set of binary relations {[=.sub.m]}m[member of]N\{0,1}, having the usual meaning of opposite and modulo. As for Z, quantifier elimination is obtained in the same augmented language enriched with the binary relation <.

1.2 Logical definability

Here we are concerned with the definability issue. Consider a structure D with domain D and a first-order formula on this structure, say [PHI]([x.sub.1],..., [x.sub.n]), where [x.sub.1],..., [x.sub.n] are its free variables. Then the n-ary relation R defined by [PHI] is the set of n-tuples (a1,... ,an) such that </> holds true when the variable [x.sub.i] is assigned the value [a.sub.i], i.e., R = {(a1,..., an) e Dn | D = {([a.sub.1],..., [a.sub.n])}. A relation is D-definable or simply definable when the structure is understood, if it can be defined by a first-order formula on D.

The following is the main result on the integer arithmetic without multiplication. It proves that it admits quantifier elimination and it is due to Presburger, cf. [19].

Theorem 1.1 (Presburger) A subset X of [Z.sup.n] is Z-definable if and only if it is a Boolean combination of relations defined by predicates of the form

t <t' and t = t' (mod b) (1)

where t and t' are linear expressions on the integer variables [x.sub.i] of the form [a.sub.0] + [SIGMA.sup.n].sub.i]=1 [x.sub.i] with [a.sub.i][x.sub.i] [member of] Z, and b [member of] N, b > 1 .

A subset X of [Z.sup.n] is [Z.sup.W]-definable if and only if it is a Boolean combination of relations defined as in(1) where the binary relation < is replaced by the equality.

1.3 Linear sets

The following definitions could be given for arbitrary finitely generated commutative monoids but we are mainly interested in the free commutative group [Z.sup.n]. We consider it as a subset of the Q-vector space [Q.sup.n] and view its elements as row vectors. The operation of addition is extended from elements to subsets: if X, Y [subset or equal to] [Z.sup.n], then the sum X + Y [subset or equal to] [Z.sup.n] is the set of all sums x + y where x [member of] X and y [membe of] Y. When X is a singleton {x} we simply write x+Y. Given x in [Z.sub.n], the expression Nx represents the subset of all vectors nx where n range over N and similarly for Zx. For example, Zx + Zy represents the subgroup generated by the vectors x and y. We extend also the matricial notation to subsets, e.g., if A is an (n x p)-matrix with integer or rational entries, then [Q.sub.n] A stands for the set of all p-row vectors of the form xA for some n-row vector x [member of] [Q.sub.n].

We now briefly recall the classical theory of the linear and semilinear subsets of [Z.sub.n] as exposed in [7]. Definition 1.2 A subset of [Z.sub.n] is N-linear if it is of the form

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]. (2)

It is N-simple if the vectors bj are linearly independent as vectors of [Q.sub.n]. It is N-semilinear if it is a finite union of linear sets.

Ginsburg and Spanier proved [11] the following equivalent statements for Nn, but it can readily be seen to hold for [Z.sub.n]. Together with Theorem 1.1, it can be interpreted as saying that the first-order definable sets in (Z; +, 0,1, <} are exactly the rational subsets of [Z.sub.n]. Actually Eilenberg and Schutzenberger in [7], and independently Ito in [14], strengthened the third condition by proving that the simple sets may be assumed disjoint.

Theorem 1.3 Given a subset X of [Z.sub.n], the following assertions are equivalent:

1. X is first-order definable in Z;

2. X is N-semilinear;

3. X is a finite union of N-simple sets.

Furthermore, each of the specifications can be effectively transformed into another.

When dealing with a linear subset, this result allows us to assume that it is given as a finite union of simple subsets.

The following notion of dimension will be useful in the sequel. It is defined on linear sets but extended to arbitrary sets in a natural way.

Definition 1.4 The dimension of the simple set a + [[SIGMA].sup.m.sub.i]=1 [Nb.sub.i] is the integer m. More generally, the dimension of an arbitrary nonempty subset X [subset or equal to] [Z.sub.n] is the minimum integer m, denoted dim(X), such that X is included in a finite union of simple sets of dimension at most m. The dimension of the empty set is equal to -1.

Observe that the dimension of a finite union of simple sets does not depend on the specific expression which defines it. This is seen by observing that an expression of a simple set of dimension m as a finite union of simple sets contains a simple set of dimension m and no simple set of dimension greater than m and that equality dim(A [union] B) = max{dim(A), dim(B)} holds. Indeed, since dimension is a nondecreasing operator, we have dim(A [union] B) [greater than or equal to] dim(A) and dim(A [union] B) [greater than or equal to] dim(B) and therefore dim(A [union] B) [greater than or equal to] max{dim(A), dim(B)}. The other direction is trivial. As a result we have the following proposition.

Proposition 1.5 Given a subset X [subset or equal to] [Z.sub.n] specified by some first-order formula in Z and some integer 0 [less than or equal to] d [less than or equal to] n, it is recursively decidable whether or not it has dimension at most d.

Proof: Indeed, using Ginsburg and Spanier's construction in ([11], Theorem 1.3.), an expression as a finite union of simple sets for X can be effectively computed from the first-order formula specifying it. A simple inspection suffices to determine whether or not the linear sets composing it have dimension less than or equal to d.

1.4 Z-linear sets

We now extend the notion of N-linear subsets defined in Section 1.3 to Z-linear subsets by allowing the coefficients of expression (2) to be in Z.

Definition 1.6 A subset of [Z.sub.n] is Z-linear if it is of the form

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]. (3)

The notions of Z-simple and Z-semilinear sets are defined with the obvious modifications of Definition 1.2.

There exists a notion which is halfway between that of simple and that of arbitrary disjoint unions of simple sets. We use the standard geometric notion of translation, restricted to [Z.sub.n], which is a mapping of the form x [right arrow] a + x for some given vector a [member of] [Z.sub.n]. A translate of a subset is its image in a translation.

Definition 1.7 A subset is quasi-simple if it is a finite union of translates of a given simple set S. This is equivalent to saying that it is a set of the form A + S, where A [subset or equal to] [Z.sub.n] is finite and S is a subgroup of [Z.sub.n]. The set S is called template.

Clearly, a finite union of Z-linear subsets is also a finite union of N-linear subsets.

Proposition 1.8 Every Z-linear subset of [Z.sub.n] is a finite union N-linear subsets.

Proof: Indeed, a Z-linear subset as in expression (3) is equal to the union of all [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] where ([member of.sub.1],..., [member of.sub.k]) ranges over the set {[[+ or -]1}.sup.k].

The converse does not hold, e.g., the subset N is not expressible as a finite union of Z-linear subsets (this is a direct consequence of Theorem 1.1 and Theorem 1.3 but can be worked out directly too).

2 Closure properties

2.1 Properties of Z-linear sets

Our decidability result is based on the equivalence between definable subsets in the structure [Z.sup.W] and the family of finite unions of subset differences of Z-semilinear subsets, see subsection 2.2. This characterization is obtained by a careful study of the closure properties of the family of Z-linear sets carried out here.

We will show that the class of Z-linear sets enjoys many properties such as closure under finite sum as defined in subsection 1.3, projection, direct product and even more interestingly intersection, making it a more robust family than the family of N-linear sets since N-linear sets are not closed under intersection. On the opposite, the family of N-semilinear sets is more robust than that of Z-semilinear sets, in fact while the first is closed under all Boolean operations, the second is not. The sets belonging to the Boolean closure of the Z-linear sets have a more complex representation (see Theorem 3.1).

We start with a property which shows how different the N- and the Z-linear subsets are. In the case of the nonnegative integers, every linear set is a finite disjoint union of simple sets. For Z, we have a stronger property which is a direct consequence of a classical algebraic result.

Proposition 2.1 Every Z-linear set is Z-simple.

Proof: Consider the set X = a + [[SIGMA].sup.m.sub.i]=1 [Zb.sub.i], with [b.sub.i] [member of] [Z.sub.n] for 1 [less than or equal to] i [less than or equal to] m. It suffices to consider the case where a is null. Then X is a subgroup of [Z.sub.n] and therefore it is free, ([16], Theorem 4, (I,[section]9))), i.e., there exists h [less than or equal to] n linearly independent vectors [b'.sub.i] [member of] [Z.sub.n] such that X = [[SIGMA].sup.h.sub.i]=1 Z[b'.sub.i].

Using standard manipulations we get the following proposition.

Proposition 2.2 The family of Z-linear sets is closed under projection, direct product and finite sum.

Observe that N-linear sets are closed under direct product and finite sum but they are not closed under projection. Indeed, consider the N-linear (actually N-simple) set N(2,1) + N(3,1). Its projection onto the first component is the set {0} [union] {n | n [greater than or equal to] 2}.

The following is a kind of closure property under composition.

Proposition 2.3 Let X = a + [[SIGMA].sup.p.sub.i] =1 [Zb.sub.i] [subset or equal to] [Z.sub.n] and Y = c [[SIGMA].sup.m.sub.j]=1 [Zd.sub.j] [subset or equal to] Z be two Z-linear subsets. Then the set

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] (4)

is Z-linear.

Proof: Indeed, denote by B the (p x n)-matrix consisting of the p row-vectors [b.sub.i] and by D the (m x p)matrix consisting of the m row-vectors [d.sub.j]. Then the set defined in (4) is equal to

a + (c + [Z.sup.m]D)B = (a + cB) + [Z.sup.m](DB)

The intersection of two N-linear subsets is a finite union of N-linear subsets, not necessarily an N-linear subset. Here we have a stronger property: the intersection of two Z-linear subsets is a Z-linear subset. We prove this result by resorting to a different approach from that in [7] which is purely combinatorial and proceeds by induction on the dimension of the space while we make use of a classical theorem of linear algebra. We recall that [GL.sub.n] (Z) represents the unimodular group which consists of all the invertible n x n-matrices with entries in Z. We denote by rank(A) the rank of the matrix A.

Theorem 2.4 (Smith normal form ([6], [section]2.4.4)) Let A [member of] [Z.sub.nxm] be an integer matrix of rank s. Then there exist two unique invertible matrices U [member of] [GL.sub.n](Z) and V [member of] [GL.sub.m](Z), such that
```A'= UAV = (D   0
0   0)
```

where D = ([d.sub.jj]) [member of] [Z.sup.sxs] is an integer square diagonal matrix such that [d.sub.jj] divides [d.sub.ii], for 1 [less than or equal to] i [less than or equal to] j [less than or equal to] s.

The matrix A' is called the Smith normal form of A. The following is a preparatory result.

Proposition 2.5 Given A e [Z.sub.nxm] and b e [Z.sub.n], the set of solutions in [Z.sup.m] of the linear system Ax = b is a Z-simple set of dimension m - rank(A).

Proof: Let rank(A) = s and A' = UAV be the Smith normal form of A. The given system is equivalent to [UAVV.sup.-1]x = Ub. Setting [V.sup.-1]x = y and Ub = b', the set of solutions of A'y = b' is the Z-simple set [S.sup.'] = c + [[SIGMA].sup.m.sub.i=s+1] [Ze.sub.i], where [C.sub.j] = [b.sup.'.sub.j]/[a.sub.jj] for 1 [less than or equal to] j [less than or equal to] s and [C.sub.j] =0 for s < j [less than or equal to] m and the [e.sub.i] are the vectors of the canonical basis (observe that the system admits solutions in [Z.sub.m] if and only if [a.sub.jj] divides [b.sup.'.sub.j], for 1 [less than or equal to] j [less than or equal to] s). Then the set of solutions of the equation Ax = b is equal to S = VS', and so if [??] = Vc and [??.sub.j] = [V.sub.ej], we have S = [??] + [[[SIGMA].sup.m.sub.i]=s+1 Z[[??].sub.i]. Because V is unimodular, the vectors [[??].sub.i] are again linearly independent, so the set has dimension equal to m - rank(A).

Consequently, we have the following theorem.

Theorem 2.6 If P and Q are Z-simple sets of [Z.sub.n] of dimension p and q respectively, then P [intersection] Q is a Zsimple set of dimension less than or equal to min{p, q}. Furthermore, an expression for this intersection can be computed effectively.

Proof: Let P = a + [[SIGMA].supsub.i]=1 [Zb.sub.i] and Q = c + [[SIGMA].supq.sub.j]=1 [Zb.sub.i] be two Z-simple sets in [Z.sub.n] with p [less than or equal to] q and suppose that P [intersection] Q [not equal to] 0. Let us consider the linear system [[[SIGMA].sup.p.sub.i]=1 [b.sub.i][x.sub.i] + [[SIGMA].sup.p+q.sub.i=p+1] [d.sub.i]-q[x.sub.i] = c - a and let S be its set of solutions in [Z.sup.p+q]. Then S is a Z-simple set in [Z.sup.p+q] and so, its projection T on the first p components is a Z-linear set in [Z.sup.p], say T = e + [[SIGMA].supl.sub.i=1],[Zf.sub.i] for some e, [f.sub.i] [member of] [Z.sup.p] and l [less than or equal to] p. Considering the first p components of S, we have the following expression for P [intersection] Q:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

It then suffices to apply Proposition 2.3. Concerning the complexity of the computation, it directly follows from the fact that Smith normal form of A can be computed in polynomial time, see [22].

We now turn to the union operation. Its is clear that the union of two Z-simple sets in [Z.sub.n] is not necessarily simple, e.g., in Z, the singletons {0} and {1} are simple but their union is not. However, when the simple sets have maximal dimension, i.e., when their dimension equals n, the union is almost simple. This is expressed rigorously in the next result.

Proposition 2.7 Every finite union of Z-simple sets of maximal dimension is a Z-quasi-simple set. Proof: Let S [subset or equal to] [Z.sub.n] be a Z-semilinear set of the form

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

where for all 1 [less than or equal to] i [less than or equal to] m, [X.sub.i] = [a.sup.(i)] + [SIGMA.sup.n].sub.j]=1 [Zb.sub.i]j) is a Z-simple set. Since for each fixed i = 1, ..., m, the vectors [b.sup.i].sub.j], 1 [less than or equal to] j [less than or equal to] n, are linearly independent, these vectors generate a subgroup of [Z.sub.n] of finite index. In particular [X.sub.i] -[a.sup.(i)] is the inverse image of the unit of a finite commutative group. In other words there exists a surjective morphism [[phi].sub.i] of [Z.sub.n] into a finite commutative group [G.sub.i] such that [X.sub.i] = [[phi].sup.-1.sub.i]([[phi].sub.i]([a.sup.(j)])). Consider the morphism 92 of [Z.sub.n] into the direct product [G.sub.i] x ... x [G.sub.m] defined by [phi]>(u) = ..., [[phi].sub.m](w)) and set K = {x [member of] G1 x ... x [G.sub.m] | [x.sub.i] = [phi.sub.i]([a.sup.(i)]) for some 1 [less than or equal to] i [less than or equal to] m}. Then S = [[phi].sup.-1](K), which means that S is a union of cosets of the subgroup (e) where e is the unit of the direct product [G.sub.1] x ... x [G.sub.m]. ?

The following proposition expresses also an interesting property.

Proposition 2.8 Let S, T be Z-simple sets in [Z.sub.n]. If dim(S) = dim(T) and T [subset or equal to] S, then X = S \ T is a Z-quasi-simple set with template T.

Proof: Let dim(S) = dim(T) = m [less than or equal to] n, then S = a + [[SIGMA].supm.sub.i=1] [Zb.sub.i] and T = c + jm=1 [Zb.sub.i], with a, c, [b.sub.i], [d.sub.i] [member of] [Z.sub.n] for 1 [less than or equal to] i [less than or equal to] m. From T [subset or equal to] S we have c = a + [[SIGMA].supm].sub.i=1]] [[gamma].sub.i][b.sub.i], so

S = c + [[SIGMA].supm].sub.i=1](- [[gamma].sub.i])[b.sub.i] + [[SIGMA].supm].sub.i=1] [Zb.sub.i] = c + [[SIGMA].supm].sub.i=1](Z -[[gamma].sub.i])[b.sub.i] = c + [[SIGMA].supm].sub.i=1] [Zb.sub.i]. (5)

Observing that for A, B [subset or equal to] [Z.sub.n], v e [Z.sub.n], we have (A + v) n (B + v) = (A [intersection] B) + v, we can suppose without loss of generality that c = 0, so that S = [[SIGMA].supm].sub.i=1] [Zb.sub.i] and T = [[SIGMA].supm.sub.i=1] [Zb.sub.i]. Then S and T are additive groups of finite index and moreover T is a subgroup of S, so S \ T can be written as a finite union of cosets of T, which completes the proof.

Corollary 2.9 Let S and T be Z-simple sets of maximal dimension n in [Z.sub.n]. Then X = S \ T is a Z-quasi-simple set of dimension n with template T.

Proof: Observe that S \ T = S \ (S n T). From Theorem 2.6, S n T is again a Z-simple set of dimension n. Then ( S [intersection] T) [subset or equal to] S holds so that we can apply Proposition 2.8. ?

The following proposition provides us with a remarkable family of Z-simple sets which are the traces of the affine Q-spaces in [Z.sub.n].

Proposition 2.10 Let H = a + [[SIGMA].supp].sub.i=1] [Qb.sub.j] [subset or equal to] [Q.sub.n] with 0 < p < n and a, bj e [Z.sub.n], i = 1, ... ,p. Then [H.sup.'] = H [intersection] [Z.sub.n] is a Z-simple set of [Z.sub.n] of the same dimension as that of H. Moreover a Z-simple expression for [H.sup.'] is effectively computable.

Proof: Without loss of generality we can suppose that 0 e H and that dim(H) = p < n holds so that H = QpA, where A is the (p x n)-matrix whose rows are the p vectors bj. From Theorem 2.4 there exist two integer invertible matrices U [member of] [GL.sub.p] (Z) and V [member of] [GL.sub.n] (Z) such that

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE ASCII.]

where all the coefficients dj are integers. Since U and V are invertible we have

[Q.sup.p][U.sup.-1]A'[V.sup.-1] [intersection] [Z.sub.n]V[V.sup.-1] = ([Q.sup.p][U.sup.-1A'] [intersection] [Z.sup.n]V)[V.sup.-1], and, from the unimodularity of U and V, [Z.sub.n]V = [Z.sub.n] and [Q.sup.p][U.sup.-1] = [Q.sup.p]. Furthermore, we clearly have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE ASCII.]

so we we obtain

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE ASCII.]

Denote by [V.sup.'] the matrix obtain from [V.sup.-1] by substituting 0 for all entries in the last n - p rows, we finally

get:

[Q.sup.p]A [intersection] [Z.sub.n] = [Z.sup.p][V.sup.'],

which completes the proof.

As a rephrasing of the previous proposition we obtain the following result which involves a notion of saturation.

Corollary 2.11 For all Z-simple sets X = a + [[SIGMA].supp].sub.i=1] [Zb.sub.i], the set

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

is Z-simple and has the same dimension as X.

2.2 Boolean closure

The previous results show that the Z-linear subsets enjoy stronger closure properties than the N-linear subsets but that they still fail to form a Boolean algebra. As the family of finite unions of N-linear sets is closed under the Boolean operations, we may wonder whether or not so is the family of finite unions of Z-linear subsets. This is not so and here is how it can be seen. Consider the singleton {0} in Z. Its complement cannot be expressed as a finite union of Z-linear subsets. Indeed, such a finite union would consist of a finite subset of Z and, by Proposition 2.7, a union of cosets of a subgroup of the form pZ, i.e., it would be cofinite if and only if it were equal to Z, contradiction. So, we are led to consider the family of finite unions of differences of Z-semilinear sets.

Definition 2.12 We denote by F the family of finite unions of subsets of the form A \ B where A and B are Z-semilinear sets.

We shall see that F is the Boolean closure of the Z-linear subsets. In the meantime, we show that these subsets may be written in different relatively simple ways.

Proposition 2.13 Let X [subset or equal to] [Z.sub.n]. Then the following conditions are equivalent:

(i) the set X belongs to F;

(ii) the set X is a finite union of subsets of the form

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

where [T.sub.1] , ... , [T.sub.m] and [S.sub.1] , ... , [S.sub.m] are Z-simple sets and [T.sub.i] [subset or equal to] [S.sub.i] for 1 [less than or equal to] i [less than or equal to] m;

(iii) the set X is a finite union of subsets of the form

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

where [T.sub.1] , ... , [T.sub.m] and S are Z-simple sets and [T.sub.i] [subset or equal to] S for 1 [less than or equal to] i [less than or equal to] m;

(iv) the set X is a finite union of subsets of the form

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

where [T.sub.1], ... , [T.sub.m] and S are Z-simple sets anddim ([T.sub.i]) < dim(S), for 1 [less than or equal to] i [less than or equal to] m. Proof: We prove that condition (i) implies (ii). It suffices to start with a subset of the form

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

where the sets [S.sub.1],..., [S.sub.1], [T.sub.1], ..., [T.sub.m] are Z-simple. Applying the three rules of set differences (X [union] Y)

Z = (X \ Z\ [intersection] (Y\Z\, X\ (YUZ\ = (X \ Y\ [intersection] (X \ Z) = (X \ Y\ \ Z and X \ (Y [union] X\ = (X \ Y\ the subset defined in (9) becomes

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

so the first implication is proved.

Now let us prove that condition (ii) implies condition (iii). It suffices to start with a subset of the form

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] (10)

where the sets [S.sub.1],..., [S.sub.m], [T.sub.1], ..., [T.sub.m] are Z-simple and [T.sub.i] [subset or equal to] [S.sub.i] for all 1 [less than or equal to] i [less than or equal to] m. Then the set in (10) can be written as

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

where [T.sup'.sub.i] = [T.sub.i] [intersection] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] . Observe that the set [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] is Z-simple by Theorem 2.6 and that so is each of the sets Tj' for the same reason.

To prove the implication from condition (iii) to condition (iv), it suffices to show that each Z-linear subsets [T.sub.i] may be furthermore assumed of dimension less than s where s = dim(S). Indeed, after possible renumbering of the sets [T.sub.i], we may assume that the p first of them are of dimension s and that the remaining are of lesser dimension. Write

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] (11)

By Proposition 2.8 the set i ((... (S \ [T.sub.1]\) \ ...) [T.sub.p]) is a finite union of Z-simple set of dimension s, say [S.sub.1],..., Sr. Since the set difference distributes over the union the above expression (11) is the union over i j = 1,..., r of the subsets

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

which completes the verification of this implication. The implication from condition (iv) to condition (i) is trivial. ?

We are now in a position to prove the main result of this section.

Theorem 2.14 The family F is an effective Boolean algebra, i.e., given two subsets X, Y [subset or equal to] [Z.sub.n] specified as in Definition 2.12, there exists a procedure that computes the specification of the subsets X [union] Y, X [union] Y and [Z.sub.n] \ X.

Proof: Since F is defined as a collection of finite unions of sets, in order to prove the closure under complement we first have to prove the closure under intersection. Remembering that intersection distributes over union, it suffices to consider intersections of the form P [intersection] Q with

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

where all the sets S, [S.sup.'], [T.sub.1], ..., [T.sub.l], [T.sub.1], ..., [T.sup.'.sub.m] are Z-simple. Applying the general set theoretical equivalence (X \ Y) [intersection] (Z \ T) = (X [intersection] Z) \ (Y [union] T), we obtain

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

and then applying Theorem2.6 to S [intersection] [S.sup.'], we get the required form for the intersection P n Q. Concerning the complement, and due to the fact that F is trivially closed under union and, as we have proved, also intersection, is suffices to consider the complement of the set

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

defined as above. Then its complement [bar.P] can be equivalently written as

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

namely in the required form.

Effectiveness follows from Theorem 2.6 since intersection between Z-simple sets is the only real operation we have to perform. ?

We can interpret the previous result as a bound for nested Boolean operations, in the sense that no matter what Boolean combination of Z-simple sets, it can be always written in such way that its derivation tree has no more than three levels.

For our decision procedure we will need more detailed information about Boolean operations between sets belonging to the family F. In particular we can be more precise when simple subsets of maximal dimension are involved.

Proposition 2.15 Let X a subset of [Z.sub.n] such that

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] (12)

where the [S.sub.1] , ... , [S.sub.m] are Z-simple of maximal dimension n, each [T.sub.1] , ... , [T.sub.m] belongs to the family F and is included into a finite union of Z-simple of dimension strictly less than n. Moreover if we have that [T.sub.i] [subset or equal to] [S.sub.i] for all 1 [less than or equal to] i [less than or equal to] n, then X can be written in the form

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

where T belongs to the family F and is included in a finite union of Z-simple sets of dimension strictly less than n.

Observe that we may not assume that T is a finite union of simple sets of dimension less than n, even if this is true for all sets Tj. Indeed, consider for example the set X defined as

X = ([S.sub.1] \ [T.sub.1]) [intersection] ([S.sub.2] \ [T.sub.2]),

where

[S.sub.1] = [Z.sup.2], [T.sub.1] = Z x {0},

[S.sup.2] = 2Z x Z, [T.sub.2] = {0} x Z.

Then

X = [Z.sup.2] \ ((N \ {0}) x {0} [union] (-N \ {0}) x {0}) = [Z.sup.2] \ ((Z \ {0}) x {0}), and we already know that the set ((Z {0}) x {0}) is not Z-semilinear.

Proof: Without loss of generality we can suppose n = 2. Then from set theoretical rules, we have the equivalence

([S.sub.1] \ [T.sub.1]\ [union] ([S.sub.2] \ [T.sub.2]\ = ([S.sub.1] [union] [S.sub.2]\ \ (([bar.S.sub.2][intersection] [T.sub.1]u ([bar.S.sub.1] [intersection] [T.sub.2]\ [union] ([T.sub.1] [intersection] [T.sub.2]\).

From Proposition 2.7 it follows that [S.sub.1] [union] [S.sub.2] is a Z-quasi-simple set of maximal dimension n. From Proposition 2.8, the subsets [S.sub.1] and [S.sub.2] are again Z-quasi-simple. Finally from Theorem 2.6 it follows that the union of the last three terms of the above expression is included into a finite union of Z-simple sets of dimension less than n and moreover belongs to F as an immediate consequence of Theorem 2.14.

3 The weak Presburger arithmetic

3.1 Definable sets in the weak Presburger arithmetic

We are now in a position to prove the main result of this section which gives an algebraic characterization of the [Z.sup.W]-definable sets.

Theorem 3.1 The family F coincides with the family of [Z.sup.W]-definable sets.

Proof: Since F is the Boolean closure of the family of Z-simple sets, in order to prove that each element of F is [Z.sup.W]-definable, it suffices to prove that an arbitrary Z-simple set

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

is [Z.sup.W]-definable. Denote by [a.sub.j] and [b.sub.ij] respectively the j-th component of the vectors a and [b.sub.i]. For simplicity, identify assignments of variables with variables themselves. Then ([x.sub.1], ... , [x.sub.n]) belongs to X if and only if the variables [x.sub.1], ..., [x.sub.n] satisfy the formula [phi] with

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

We now prove the converse. To that order, we use Presburger's elimination of quantifiers which asserts that every formula [phi]([x.sub.1], ..., [x.sub.n]) with n free variables is equivalent to a Boolean combination of formulas of the form [[SIGMA].supn.sub.i=1] [a.sub.i][x.sub.i] + b = 0 and of the form [[SIGMA].supn][.sub.i=1] [a.sub.i][x.sub.i] [[equivalent to].sub.m] b, with aj, b [member of] Z. Concerning the first type of predicate, Proposition 2.5 where the matrix A is reduced to a unique row, guarantees that the set of solutions is linear. As for the second type, we prove by induction on n that it defines a Z-semilinear set. For n = 1, we get ax [[not equal to].sub.m] b. If the equation ax = b has no solution in the finite cyclic group Z/mZ, then the relation defined by [phi] is empty. Otherwise, let 0 [less than or equal to] [c.sub.1] < ... < [c.sub.s] < m be the set of solutions in Z/mZ (we identify the nonnegative integers less than m with their natural image in the group Z/mZ). Then the formula [phi] defines the subset of integers x such that x = c + mZ, for some c [member of] {[c.sub.1],..., [c.sub.s]}, i.e., the Z-semilinear set

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

Now let n > 1. The condition [[SIGMA].supn][.sub.=1] [a.sub.i][x.sub.i] [equivalent to] m b is equivalent to the disjunction

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

By induction hypothesis, the subformula [[SIGMA]=1 [a.sub.i][x.sub.i] [[equivalent to].sub. m] j defines a Z-semilinear subset, say [T.sub.j] [subset or equal to] [Z.sup.n-1], and an[x.sub.n] =m (b - j), as proved above, another Z-semilinear subset, say [R.sub.j] [subset or equal to] Z. Because of Proposition 2.2, the family of finite union of Z-simple sets is closed under direct product, so the relation is equal to

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

The last result asserts, loosely speaking, that a Presburger (resp. weak Presburger) definable subset of [Z.sub.n] included in a simple set, is a Presburger (resp. weak Presburger) definable subset of that subspace.

Proposition 3.2 Let X = a + [[SIGMA].supp]=1 [Zb.sub.i] [subset or equal to] [Z.sub.n] be a simple set and let t : X [right arrow] [Z.sup.p] be the mapping of X onto Zp which assigns to each a + [[SIGMA].supp].sub.=1] [lambda].sub.i].sub.b.i] the element ([[lambda].sub.1], ..., [[lambda].sub.p]) [member of] [Z.sup.p].

Then a subset Y of X is Z-definable (resp. [Z.sup.W]-definable) if and only if the set t (Y) is Z-definable (resp. [Z.sup.W] -definable).

Proof: Observe that the function t is well-defined since the vectors bj are linearly independent. Now, if [phi]([x.sub.1], ..., [x.sub.n]) is a Z- (resp. [Z.sup.W]-) formula defining a subset Y [subset or equal to] X, then the subset t(Y) is defined by the Z- (resp. [Z.sup.W] -) formula

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

where [a.sub.j] and [b.sub.ij] represent the j-th component of the vectors a and [b.sub.i]. Conversely, if for some subset Y of X the set [tau] (Y) is definable by some Z- (resp. [Z.sup.W]-) formula [psi] ..., (y.sub.1] [y.sub.p]), then Y is definable by the Z- (resp. [Z.sup.W]-) formula

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

3.2 Decidability of weak Presburger logic in Presburger logic

We recall that the problem of deciding whether or not a relation definable in Buchi arithmetic can be actually defined in Presburger arithmetic has been positively answered in [18]. Here instead of considering Presburger arithmetic with a superstructure, we consider it with a substructure: we prove that it is decidable whether or not a given formula of the structure (Z; +, <, 0,1} is equivalent to some formula in the structure (Z; +, 0,1}.

The procedure for deciding weak Presburger definability proceeds by induction on the dimension of the subsets. To that purpose, we introduce the following notation. Let X and Y be two subsets of [Z.sub.n]. If dim(X) = dim(Y) = k > 0, we write X ~ Y if the symmetric difference XAY = X \ Y [union] Y \ X has dimension less than k. Otherwise, i.e., if dim(X), dim(Y) [less than or equal to] 0, we put X ~ Y if and only if X = Y. The relation is clearly an equivalence relation and plays an important role in our decision procedure.

3.2.1 A special case

Our decision procedure relies on the following structural characterization of the Z-definable subsets of maximal dimension. The general case, i.e., when no assumption is made on the dimension, is, as we shall see, a reduction to this special case. Therefore, the following theorem can be considered as the crux of the algorithm. Given an N-simple set S = a + [[SIGMA].supm][.sub.i=1] Nbj we denote by [S.sup.Z] the Z-simple set a + [[[SIGMA].sup.m][.sub.i=1] [Zb.sub.i] and we extend this notation to finite unions of N-simple sets. Also we denote by [S.sup.Q] the Z-simple sets (a + [[SIGMA].supm].sub.i=1] [Qb.sub.i]) n [Z.sub.n], cf. Corollary 2.11.

Theorem 3.3 Let X [subset or equal to] [Z.sub.n] be a Z-definable set,

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

where the sets [Y.sub.i] are N-simple sets of dimension n and where T is a finite union of N-simple sets of dimension less than n.

Set P = ([[union].sup.m][.sub.i=1] [Y.sup.Z].sub.i]. Then X is [Z.sup.W]-definable if, and only if, the sets X \ P and P \ X are ZW-definable subsets ofdimension less than n.

Proof: The subset P is clearly [Z.sup.W]-definable. Now we have

X = (X \ P\ [union] (P \ (P \ X)\ (13)

which shows that the condition is sufficient. Let us prove that it is necessary.

If X is [Z.sup.W]-definable so are X \ P and P \ X. Since (13) always holds, it suffices to prove that X \ P and P \ X are of dimension less than n and since X \ P [subset or equal to] T holds, we prove that P \ X has dimension

less that n. Because of propositions 2.13 and 2.15, we can isolate all the simple sets of dimension n and write

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE ASCII.]

where A [subset or eqaul to] [Z.sub.n] is finite, the vectors [d.sub.j] are linearly independent and Q and R are [Z.sup.W]-definable sets of

dimension less than n. For all i = 1, ..., m, set [Y.sub.i] = [a.sup.(i)] + [[SIGMA].supn].sub.j=1] where the [b.sup.(i)].sub.j]) are linearly independent. Now we prove

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] (14)

Clearly, if we take a vector in A + [[SIGMA].supn].sub.j=1] [Zb.sub.i] not belonging to R [union] T (which is contained in R [union] [T.sup.Z], that is, a finite union of Z-simple sets of dimension less than n), it must belong to one of the [Y.sub.i], and thus to [U.sup.m].sub.=1] ([a.sup.(i)] + [[SIGMA].supn.sub.j=1] [Zb.sub.i]j)).

Conversely, consider one of the sets [Y.sub.i], namely Y= a +[[SIGMA].supn.sub.j=1]N[b.sub.j] (we drop the upper indices to simplify the notation). We observe that Q is in particular Z-definable, so Q = [U.sub.1[less than or equal to]i [less than or equal to]l][Q.sub.i], where every [Q.sub.i] is a N-simple set of dimension less than n. Set

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE ASCII.]

(recall the definition of [Q.sup.Z] before the theorem) which, by Corollary 2.11, is a finite union of simple sets of dimension less than n.

Now we show by induction on j that the set

[W.sub.j] = (a + [Zb.sub.1] + ... [Zb.sub.j-1] + [Nb.sub.j] +... + [Nb.sub.n]) \ U

is included in A + [[SIGMA].supn].sub.j=1] [Zb.sub.j]. The case j = [less than or equal to] is obvious, so we suppose 1 < j [less than or equal to] n. By induction hypothesis, for every h < j we have [W.sub.h] [subset or equal to] (A + [[SIGMA].supn.sub.j=1] [Zb.sub.i]). Consider a vector v [member of] [W.sub.j] and observe that the line v + [Nb.sub.j] intersects a subset QZ in at most one point so that its intersection with U is a finite set. Indeed, set [Q.sub.i] = c + [[SIGMA].sub.k] [Ne.sub.k] and assume that for two integers [alpha],[beta] [member of] Z we have that v + [alpha].sub.bj] and v + /[[beta].sub.j] belong to c + [SIGMA.sub.k] [Q.sub.ek]- This implies that [b.sub.j] belongs to the Q-vector space generated by the vectors ek, so that v [member of] (c + [[SIGMA].sub.k] [Q.sub.ek]) [intersection] [Z.sup.n] = [Q.sup.Z.sub.i], contradiction.

Consequently, for every sufficiently large integer s, we have v + [sb.sub.j] = [a.sub.s] + [SIGMA.sup.n].sub.i=1] [[lambda].sup.i].sub.s][d.sub.i], where [a.sub.s] [member of] A and [lambda].sup.(i).sub.s] [member of] Z. Since A is finite, so there exists [s.sub.1] [member of] N and 0 [less than or equal to] r [less than or equal to] |A| such that [a.sub.s1] = [a.sub.s1]+r. By computing v + ([lambda].sup.(i).sub.s] + r)[b.sub.j] - (v + [s.sub.1][b.sub.j]), we obtain [rb.sub.j] = [[SIGMA].supn.sub.i]=1 [[mu].sup.(i).sub.r][d.sub.i], where [[mu].sub.r] = [[lambda].sub.s1]+r [lambda].sub.s1]. Now for all integers s let m [member of] Z and 0 [less than or equal to] [r.sup.'] [less than or equal to] r be such that s = [s.sub.1] H mr H [r.sup.'], then we have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

Now we have X ~ (A + [[[SIGMA].sup.n.sub.j=1] [Zb.sub.i]) ~ P which completes the proof.

3.2.2 The procedure

The procedure solves the following decision problem:

Input: a Z-definable set X given as a finite union of N-simple sets

Question: decide whether or not the set X is [Z.sup.W]-definable and, in the affirmative case, give a representation as a Boolean combination of Z-simple sets.

We cannot directly use Theorem 3.3, because it requires that the finite union has an N-simple subset of maximal dimension. We thus proceed as follows. The set X [subset or eqaul to] [Z.sub.n] is given as a union of sets of the form

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] (15)

We use an induction on dim(X) = max{[r.sub.i] | 1 [less than or equal to] i [less than or equal to] m}. When this dimension is at most 0 the answer is "yes". Assume thus that d = dim(X) > 0. Set [H.sub.i] = [X.sup.Q.sub.i] for 1 [less than or equal to] i [less than or equal to] m and observe that it is Z-simple by Corollary 2.11, thus [Z.sup.W]-definable by Theorem 3.1. Suppose, after possibly changing some indices, that [H.sub.1], ..., [H.sub.p], p [less than or equal to] m, are the maximal elements for the subset inclusion, of the collection of sets {[H.sub.i] | 1 [less than or equal to] i [less than or equal to] m}. We claim that X is [Z.sup.W]-definable if and only if every intersection X [intersection] [H.sub.i], 1 [less than or equal] i < p, is [Z.sup.W]-definable. Indeed, this is clearly necessary since [H.sub.i] is [Z.sup.W]-definable. Conversely, if every X [intersection] [H.sub.i] is [Z.sup.W]-definable, because each [X.sub.j] is a subset of [H.sub.i] for some 1 [less than or equal] i [less than or equal to] p, i.e, because of the inclusion X [subset or eqaul to] \Jp=1 [H.sub.i] holds, we have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.] (15)

For each [H.sub.i] of dimension less than d, we call the procedure recursively. If one of these calls returns "no", then the procedure returns "no" and stops. Now, for each [H.sub.i] of dimension d we call the procedure recursively as described below and we return "yes" if all these calls return "yes". We now explain how we treat each [H.sub.i], denoted H for simplification. Write H = a + [[SIGMA].supd][.sub.j=1] [Zc.sub.j] where the [cj.sub.s] are a set of vectors generating H freely. Let t : H - Zd be the mapping which assigns the d-tuple ([lambda].sub.1], ..., [[lambda].sub.d]) [member of] [Z.sup.d] to the element a + -d=1 Aja,. By Proposition 3.2, for all Y [subset or equal to] H we have: Y is [Z.sup.W]-definable if, and only if, t(Y) is ZW-definable. Let I be the set of indices 1 [less than or equal to] j [less than or equal to] m such that [X.sub.j] [subset or eqaul to] H has dimension d and let T be the union of all other Xjs included in H. Then we have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

so that every t([X.sub.j]) for j [member of] I, has maximal dimension in t(H) = [Z.sup.d]. Then we are in the conditions of Theorem 3.3 and it suffices to check the equivalence

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII.]

which is decidable by Proposition 1.5 since it involves Boolean operations on N-semilinear subsets. If the equivalence does not hold, then the procedure returns "no" and stops. Otherwise we call the procedure recursively with t(X [intersection] H) \ P and P \ (P t(X [intersection] H)) where P = \J t(Xj)Z.

Considering Ginsburg and Spanier's construction, the previous procedure has the following consequence.

Theorem 3.4 Given a first-order formula over (Z; +, <, 0,1} it is recursively decidable whether or not it is expressible in (Z; +, 0,1}.

4 Further works

We have presented an algorithm based on an algebraic characterization of the sets of integers that can be expressed in first order logic with the binary function of sum and the constants 0 and 1. We did not tackle the problem of evaluating the complexity of the algorithm (which is probably nonelementary as written) nor that of the problem. Concerning the former, we think that even more elementary issues should be addressed first relative to the constructions of Ginsburg and Spanier to which we have alluded at several instances. Little has been undertaken since their publications. For example, Huynh proved in [13] that inequality of two finite unions of N-linear sets is log-complete in [[SIGMA].supS.sub.2], but other questions remain unsettled: the intersection of two N-linear sets is a finite union of N-linear sets, but we ignore the size of the output as a function of the size of the two N-linear sets. This leaves room for further research which might simplify or improve the present results.

received March 30 2009, revised August 26 2009, accepted January 14 2010.

References

[1] Paul Bernays and David Hilbert. Grundlagen der MathematikI, chapter 7, pages 368-377. SpringerVerlag, Berlin, 2nd edition, 1970.

[2] Alexis Bes. A survey of arithmetical definability. Bullettin of the Belgian Mathematical Society. Simon Stevin, suppl.:1-54, 2001.

[3] Veronique Bruyere, Emmanuel Dall'Olio, and Jean-Francois Raskin. Durations, parametric model-checking in timed automata with presburger arithmetic. In STACS, pages 687-698, 2003.

[4] Christian Choffrut. Deciding whether a relation defined in Presburger logic can be defined in weaker logics. Theoretical Informatics and Applications, 42:121-135, 2008.

[5] Christian Choffrut and Achille Frigeri. Definable sets in weak Presburger arithmetic. In G. F. Italiano etal., editor, Theoretical Computer Science, 10th Italian Conference, ICTCS 2007, pages 175-186, 2007.

[6] Henri Cohen. A Course in Computational Algebraic Number Theory, volume 138 of Graduate Texts in Mathematics. Springer-Verlag, 1993.

[7] Samuel Eilenberg and Marcel-Paul Schutzenberger. Rational sets in commutative monoids. Journal of Algebra, 13:173-191, 1969.

[8] Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, New York, 1972.

[9] Seymour Ginsburg and Edwin H. Spanier. Bounded ALGOL-like languages. Transactions of the American Mathematical Society, 113:333-368, 1964.

[10] Seymour Ginsburg and Edwin H. Spanier. Bounded regular sets. Proceedings of the American Mathematical Society, 17:1043-1049, 1966.

[11] Seymour Ginsburg and Edwin H. Spanier. Semigroups, Presburger formulas, and languages. Pacific Journal of Mathematics, 16:285-296, 1966.

[12] Seymour Ginsburg and Edwin H. Spanier. AFL with the semilinear property. Journal of Computer and System Science, 5:365-396, 1971.

[13] T.-D. Huynh. The complexity of semilinear sets. In ICALP, pages 324-337, 1980.

[14] Ryuichi Ito. Every semilinear set is a finite union of disjoint linear sets. Journal of Computer and System Sciences, 3:221-231, 1969.

[15] Manolis Koubarakis. Complexity results for first-order theories of temporal constraints. In Jon Doyle et al., editor, Proceedings of the 4th International Conference on Principles of Knowledge Representation and Reasoning, pages 379-390, 1994.

[16] Serge Lang. Algebra. Addinson Wesley, 1965.

[17] Jerome Leroux. A polynomial time Presburger criterion and synthesis for number decision diagrams. In Proceedings of the 20th IEEE Symposium on Logic in Computer Science, pages 147-156, 2005.

[18] Andrei Al'bertovich Muchnik. The definable criterion for definability in Presburger arithmetic and its applications. Theoretical Computer Science, 290:1433-1444, 2003.

[19] Mojzesz Presburger. Uber die Vollstandigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Sprawozdanie z I Kongresu matematykow krajow slowianskich, Warszawa 1929 (Comptes-rendus du I Congres des Mathematiciens des Pays Slaves, Varsovie 1929), pages 92-101, and an unnumbered addendum after page 394, Warsaw, 1930.

[20] Craig Smorymki. Logical Number Theory I, chapter III, pages 307-329. Universitext. Springer Verlag, Berlin, 1991.

[21] Ryan Stansifer. Presburger's article on integer arithmetic: Remarks and translation. Technical Report TR84-639, Cornell University, Computer Science Department, http://ecommons.library.cornell.edu/ handle/1813/64 7 8, September 1984.

[22] Arne Storjohann. Near optimal algorithms for computing Smith normal forms of integer matrices. In Y. N. Lakshman, editor, Proceedings of the 1996 International Symposium on Symbolic and Algebraic Computation, ISSAC '96, pages 1-8. ACM Press, 1996.

Christian Choffrut (1) and Achille Frigeri (2)

(1) L.I.A.F.A., University Paris 7, 2 Pl. Jussieu - 75 251 Paris Cedex - France (2) Dipartimento di Matematica, Politecnico di Milano & LIAFA, University Paris 7 via Bonardi, 9 - 20133 Milano, Italia ([dagger]) A preliminary version of these results was published in the proceedings of the Conference ICTCS 2007, held in Rom, Italy, 2007, (5)