We study function elimination for Arithmetical Logics. We propose a method allowing substitution of functions appearing in a given formula with functions with less arity. We prove the correctness of the method and we use it to show the decidability of the satisfiability problem for two classes of formulae allowing linear and polynomial terms.
A branch of First Order Logics are Arithmetical Logics. Arithmetical Logics consider quantified formulae where variables are either reals or integers, and where functions in {+, •} and relations in {<, =, >, ≤, ≥} are used.
The satisfiability problem deals with the existence of a valuation for variables, functions and predicates s.t. a given formula is true under that valuation. This problem is in general undecidable if one considers polynomial formulae on integer variables (see [23]). Different classes are considered to avoid such difficulty, and several techniques can be used to prove decidability (see [4]). One of these techniques is based on the quantifier elimination approach. Given a formula with a quantified variable, the quantifier elimination deals with the problem of finding an equivalent formula without quantifiers.
The results of this paper are the following ones: we prove that quantifier elimination for formulae with functions cannot exist; we introduce a technique that permits to decrease the arity of a certain function; we use the technique proposed to prove the decidability of the satisfiability problem for two subclasses of formulae in the set of formulae with prefixes in (∃ * ∀) * . The two classes (the first one allowing real polynomial terms and the second one mixed linear terms) are sufficient to describe the theories of sets and strings.
The paper is organized as follows: in Section 2 we review some base notions and results on Arithmetical Logics. In Section 3 we show the function elimination method and the two decidable classes are defined in Section 4. In Section 5 we use our method to model sets and in Section 6 we discuss related works and draw some conclusions.
Let us assume a set of function symbols F ranged over by a, b, . . . together with an arity mapping ar : F → IN. If ar(a) = 0 then a is called a real variable. We will usually use x, y, . . . to denote real variables.
A valuation over F is a mapping v : F → (IR IN → IR) that assigns a function v(a) : IR ar(a) → IR to each function symbol a. Notice that v(x) is a constant for each variable x. The set of all valuations over F is denoted by V. For a valuation v ∈ V, a function symbol a and a function f : IR ar(a) → IR, we denote with v[f /a] the valuation s.t. v[f /a](a) = f and v[f /a](b) = v(b) for all b = a. Definition 1. The set T of polynomial terms with rational coefficients, ranged over by τ , is defined inductively by:
where q ∈ Q and a ∈ F . The terms in T generated without using the multiplication τ 1 • τ 2 are called linear terms.
When we use real variables in terms, we usually write x for x(). For instance, we will write x + 3 for x() + 3. We assume a function ID : T → 2 F that, applied to a term τ ∈ T , returns the set of the function symbols appearing in τ .
Example 1. Let ar(a) = ar(b) = 1 and x, y be two real variables. If τ 1 is the term 4 9
For a term τ ∈ T and a valuation v ∈ V, we denote with [τ ] v the value of τ under the valuation v, more precisely:
The set Φ of quantified formulae over T is defined inductively by: φ
where τ, τ ∈ T , ∼∈ {<, ≤, =, ≥, >} and a ∈ F . Conjunction, implication and universal quantification can be easily derived. We say that φ is linear iff for each τ ∼ τ and int(τ ) appearing in φ, it holds that τ, τ are linear terms.
For a quantified formula φ ∈ Φ and a valuation v ∈ V, we write v |= φ if v satisfies φ. The relation |= is defined as follows:
For a formula φ ∈ Φ, we denote with φ the set of valuations in V that satisfy φ, formally φ = {v ∈ V | v |= φ}. Two formulae φ 1 and φ 2 are equivalent iff φ 1 = φ 2 . We denote with true the formula 0 = 0 and with false the formula ¬true. So, true, false are in Φ. Notice that false = ∅ and true = V. Moreover, with Free(φ) we denote the set of real variables and functions symbols non-quantified in φ, and with Bnd(φ) we denote the set of real variables and functions symbols quantified in φ. We assume, without loss of generality, that the sets Free(φ) and Bnd(φ) are always disjoint.
Example 2. Let x, y be two real variables, and a, b be two function symbols with ar(a) = 1 and ar(b) = 2. We give some properties that can be expressed in Φ:
-The function a assumes only integer values: ∀x.int(a(x)).
-The function a reaches x: ∃y.a(y) = x.
-The minimum of a is in position x: ∀y.a(y) ≥ a(x).
-The function a is binary: ∀x.a(x) = 0 ∨ a(x) = 1.
-The function a is monotone: ∀x, y.x ≤ y ⇒ a(x) ≤ a(y).
Given two terms τ 1 , τ 2 ∈ T , with φ[τ 1 := τ 2 ] we denote the formula obtained by replacing all occurrences of τ 1 in φ with τ 2 . Moreover, if a is a function symbol in F , let App(a, φ) denote the set of terms a(τ 1 , . . . , τ ar(a) ) appearing in φ.
called the set of universal quantification prefixes, and Q = {∃a., ∀a. | a ∈ F } * is called the set of quantification prefixes.
For instance, ∃a.∃b. is in E and ∃a.∀b. is in Q. From now on, without loss of generality we consider formulae of the form Q.φ where Q ∈ Q, and Bnd(φ) = ∅. Definition 4. A quantified formula φ ∈ Φ is satisfiable iff φ = ∅. The satisfiability problem for φ ∈ Φ consists in answering if φ is satisfiable.
The satisfiability problem is in general undecidable if one considers quantified polynomial formulae on integer variables (see [23]). Different classes of formulae have been considered to avoid such a difficulty. For quantified linear formulae on real and integer variables (without function symbols a with ar(a) > 0), the satisfiability problem is decidable (see [34]). In fact, in this case quantifiers can be eliminated through quantifier elimination, which consists in transforming a formula ∃x.φ where Bnd(φ) = ∅ into an equivalent formula φ s.t. Bnd(φ ) = ∅. For instance, ∃x.5 < x∧x < y can be transformed into the equivalent formula 5 < y. In general, quantifier elimination does not hold if one considers also functions (see [7] and [16] for example). The problem is that the variables appearing in the scope of some functions cannot be eliminated. The following proposition states that quantifier elimination cannot work, in general, for the formulae in Φ.
Proposition 1. Let φ be the formula ∀x . 0 ≤ x < y ⇒ a(x) = 0. There is no formula φ ∈ Φ with Bnd(φ ) = ∅ equivalent to φ.
For a formula ∃a.φ with Bnd(φ) = ∅, we say that a is an uninterpretated function. The satisfiability of such a formula is decidable. In fact, by following [30], one can get a formula φ equivalent to ∃a.φ by substituting each occurrence a(τ 1 , . . . , τ ar(a) ) in φ with a real variable x, provided φ is updated in a suitable way that, however, does not require to introduce any function with arity > 0. Then, since the φ so obtained does not contain functions with arity > 0, its satisfiability is decidable according to [34]. For instance, ∃a.a(4) ≤ a(k) can be turned into ∃x.∃y.x ≤ y ∧ ((4 = k) ⇒ (x = y)). The challenge is to extend this method to formulae not in the form ∃a.φ with Bnd(φ) = ∅. This is immediate for formulae of the form ∃a.∃x.φ with Bnd(φ) = ∅, since such a formula is equivalent to ∃x.∃a.φ, which can be transformed to ∃x.φ , to which quantifier elimination applies. The difficulty is in the formulae of the form ∃a.∀x.φ and ∀a.∃x.φ. In next section we consider the case ∃a.∀x.φ since ∀a.∃x.φ = ¬∃a.∀x.¬φ.
In this section we give two results showing under which circumstances a function in a quantified formula in Φ can be replaced by a function with less arguments. If, by iteratively applying these substitutions, we transform each function into a real variable, then satisfiability follows from results in [32] and [34].
First of all we investigate when all occurrences in a formula φ of a function a can be substituted by occurrences of a function b that applies to a subset of the arguments of a (Theorem 1 below).
, and v(y) = v (y) for all y = x.
For instance, the terms x 3 +a(z)•z 2 and 3•x+2 are determined by x, whereas the terms x 2 and a(x) are not determined by x.
Proposition 2. It is decidable to check whether τ is determined by x. Definition 6. Let a ∈ F , S ⊆ {1, . . . , ar(a)} with S = ∅, x be a real variable and φ ∈ Φ. We say that a is S-fixed on x in φ iff:
for each i ∈ S and a(τ 1 , . . . , τ ar(a) ) ∈ App(a, φ), it holds that x ∈ ID(τ i ); for each i ∈ S, there exists a term τi determined by x s.t. ID(τ i ) ⊆ Free(φ) ∪ {x} and, for all a(τ 1 , . . . , τ ar(a) ) ∈ App(a, φ), it holds that τ i = τi .
Informally, a is S-fixed on x in φ iff for all terms of the form a(τ 1 , . . . , τ ar(a) ) appearing in φ, the real variable x appears in all and only the terms τ i with i ∈ S and, for each i ∈ S, the respective term τ i is unique and determined by x. This implies that, for each c, c ∈ IR with c = c , the values of the argument terms τ i with i ∈ S to which a is applied in φ Now we investigate when a given term a(τ 1 , . . . , τ ar(a) ) in App(a, φ) can be replaced by a term a (τ 1 , . . . , τ j−1 , τ j+1 , . . . τ ar(a) ). The idea is to generalize to arbitrary functions the technique proposed in [30] to replace uninterpreted functions with functions with less arguments.
Let φ ∈ Φ and a ∈ F . With EQ(a, φ) we denote the formula a(τ1,...,τ ar(a) )
a(τ 1 ,...,τ ar(a) ) ∈ App(a, φ)
i∈[1,ar(a)]
expressing that if two arbitrary occurrences of a in φ are applied to argument terms with the same values, then the resulting values are equal.
Example 5. Let φ r be as the formula in Ex. 4. Then EQ(b , φ r ) is equivalent to
In [2] it is proved that the formula ∃f.∀y.P (y, f (y)), with P a predicate, is equivalent to ∀y.∃x.P (y, x). We apply the same strategy to formulae in Φ.
We can now apply Th. 1 to function symbol b , which is now {1}-fixed on x, thus obtaining the equivalent formula ∀y.∃w.∃t.∀x.∃s.∃a.∀z.a(z
By applying Th. 2 to term a(0) we get the equivalent formula ∀y.∃w.∃t.∀x.∃s.∃a.∃a .∀z.a(z
By applying Th. 1 to function symbol a, which is {1}-fixed on z, we obtain the equivalent formula ∀y.∃w.∃t.∀x.∃s.∃a .∀z.∃a .a
which has no function with arity > 0. Therefore its satisfiability is decidable. The formula above is equivalent to the original formula φ r in Ex. 3.
The following result is a generalization of Th. 2. 4 The sets Φ L and Φ P In this section we characterize the subset of formulae in Φ for which we can prove that satisfiability is decidable by means of Theorems 1 and 2.
For a formula φ ∈ Φ, we say that the variable x is in the scope of function a iff there is a term a(τ i , . . . , τ r(f ) ) ∈ App(a, φ) s.t. x appears in some τ i .
We say that φ ∈ Φ is a basic formula iff it has the form Q.φ , where Q ∈ Q, Bnd(φ ) = ∅ and no function symbol a with ar(a) > 1 is universally quantified by Q. Hence, for some φ with Bnd(φ ) = ∅, E 1 , . . . , E n+1 in E (recall that ε ∈ E), and real variables x 1 , . . . , x n , a basic formula has the form
For a basic formula ∃a.E 1 .∀x 1 . . . . E n .∀x n .E n+1 .φ, the following definition gives a condition ensuring that, by iteratively applying Th. 1, all occurrences of a(τ 1 , . . . , τ ar(a) ) ∈ App(a, φ) can be substituted by terms a (τ i1 , . . . , τ im ) s.t. no universally quantified variable x i is in the scope of a . Definition 7. Given the basic-formula φ = ∃a.E 1 .∀x 1 . . . . E n .∀x n .E n+1 .φ , let j be the maximal index in {1, . . . , n} s.t. x j is in the scope of a. Then we say that a is a sequenced-function, denoted as S-function for short, iff for each index i ∈ {1, . . . , j} there exists a set of indexes S xi = ∅ s.t. a is S xi -fixed on x i in φ. Moreover, for each term a(τ 1 , . . . , τ ar(a) ) ∈ App(a, φ ), for all argument terms τ h we have either:
-ID(τ h ) ⊆ Free(φ), or x l ∈ ID(τ h ) for some l ∈ {1, . . . , j}.
The idea behind Def. 7 is that φ = ∃a.E 1 .∀x 1 . . . . E n .∀x n .E n+1 .φ can be mapped through j application of Th. 1 to an equivalent formula of the form E 1 .∀x 1 . . . . E j .∀x j ∃a .E j+1 .∀x j+1 . . . E n .∀x n .E n+1 .φ , where all occurrences of a(τ 1 , . . . , τ ar(a) ) ∈ App(a, φ ) have been replaced by occurrences of a (τ i1 , . . . , τ im ) in φ s.t. no universally quantified x i is in the scope of a .
Example 7. The formula ∃b.∀x.∃a.∀y. x < y ⇒ a < b(y) does not respect Def. 7, since y is in the scope of b and b is not {1}-fixed on x. Since b is not {1}-fixed on x, we cannot apply Th. 1 to b and x and the formula cannot be transformed by applying Th. 1.
The formula ∃a.∃c.∀x.∀y. x < y ⇒ a(x) < c(y, x) respects Def. 7, since a is {1}-fixed on x and c is {2}-fixed on x and {1}-fixed on y. By applying Th. 1 to a and x we get the equivalent formula ∃c.∀x.∃a .∀y. x < y ⇒ a < c(y, x). Then, by applying Th. 1 to c and x we get the equivalent formula ∀x.∃a .∃c .∀y. x < y ⇒ a < c (y). Finally, by applying Th. 1 to c and y, we get the formula ∀x.∃a .∀y.∃c . x < y ⇒ a < c with only real variables.
Our aim is now to formally define a sequenced formula as a formula in Φ in which all functions are sequenced functions. For the basic formula φ of the form E 1 .∀x 1 . . . . E n .∀x n .E n+1 .φ , we denote with Ex(i, φ) the set of existentially quantified function symbols that occur in E i . Formally, we define Ex(i, φ) = {a 1 , . . . , a m } if E i has the form ∃a 1 .∃a 2 . . . ∃a m ; in particular we define Ex(1, φ) = {a i | a i is existentially quantified in E 1 } ∪ Free(φ). Definition 8. The set of sequenced-formulae, S-formulae for short, is the least set closed under disjunction and conjunction that contains the basic formula E 1 .∀x 1 . . . . E n .∀x n .E n+1 .φ with a ∈ Ex(i, φ) for some i = 1, . . . , n + 1 iff a is an S-function for the subformula ∃a.E i .∀x i . . . E n .∀x n .E n+1 .φ.
With Φ L we denote the set of S-formulae that are linear. With Φ P we denote the set of S-formulae φ s.t. no occurrence of predicate int( ) appears. For instance, all formulae in Ex. 2 but the first, are in Φ L . Moreover, the formula in Ex. 3 and the first formula of Ex. 2 are in Φ P . Proposition 3. For each S-formula φ, there exists a S-formula φ disjunction of basic formulae that is equivalent to φ.
From now on we suppose that each formula is of the form as in Proposition 3. As a result of Def. 7 and Def. 8, if φ is an S-formula, then each value assumed by a function symbol a, that as to be an S-function, can be related with itself and a fixed finite set of values assumed by a, whichever is its arity. The following theorem proves that satisfiability is decidable for formulae in Φ L and Φ P .
Theorem 3. The satisfiability problem is decidable for Φ L and Φ P .
We now aim to show that the sets Φ L and Φ P of S-formulae are the biggest decidable classes. In other terms, all requirements of Def. 7, and so of Def. 8, are necessary to ensure that satisfiability is decidable. The result of [7] can be used to prove that, if we relax the definition of S-formulae, the satisfiability problem for Φ L and Φ P is undecidable. In fact, [7] uses functions to calculate the satisfiability of formula with polynomial terms and integer variables.
Firstly we focus on Φ L . For instance, we can consider the generic polynomial term τ •h, where τ is a linear term and h is an integer variable. Let φ (sol,τ,h) be the linear formula int(sol)∧sol = a(τ +h)∧a(τ +1) = τ ∧∀ l ∈ [τ +1, τ +h] . a(l+1) = a(l) + τ. Notice that this formula is not an S-formula, since function symbol a is not S l -fixed on l,
The value τ • h is equal to the integer value assumed by the variable sol which satisfies φ (sol,τ,h) . In fact, sol = a(τ +h) = a(τ +h−1)+τ = a(τ +h−2
By applying this technique recursively, a value of a polynomial term τ can be easily written as an integer value assumed by a variable which satisfies a linear formula. For instance, τ • h 1 • h 2 can be written as sol 1 • h 2 , where sol 1 satisfies the formula φ (sol1,τ,h1) . Now sol 1 is trivially a linear term, and hence, τ • h 1 • h 2 is equal to the value of sol 2 of the valuations which satisfy φ (sol1,τ,h1) ∧φ (sol2,sol1,h2) . As a consequence, a polynomial formula τ ∼ 0 can be written as an equivalent linear formula. Hence the satisfiability problem for Φ L is undecidable if we relax the definition of S-functions and, consequently, of S-formulae, by removing the S-fixed property.
We now take on the case of Φ P . The satisfiability of a formula with polynomial terms and real variables is decidable. But we can use the functions to force a real variable to be an integer. For instance, let τ ∼ 0 be a formula on integer variables; we can write a formula φ, with no occurrences of predicate int( ), s.t. τ ∼ 0 is satisfiable iff φ is.
Let {k 1 , . . . , k n } be the integer variables which appear in τ , and {x 1 , . . . , x n } be a set of real variables. Let
It is sufficient to consider as the formula φ the following formula:
We notice that, as in the previous case, function symbol a, which expresses the integer part of a real variable, is not an S-function, since it is not S y -fixed on y in φ. Thus, φ ∈ Φ P . We are going to show that, for each v |= φ, if x i is positive, then a(x i ) = x i iff x i is a natural. If this holds, then the satisfiability problem for φ is undecidable and therefore we cannot relax the definition of S-formula without loosing decidability.
Let us suppose that v |= φ and a(x i ) = x i , then there exist ∈ [0, 1) and k ∈ IN s.t. v(a(x)) = v(a( )) + k. But, for each y < 1, it holds that a(y) = 0, and therefore v(a( )
. Hence a(x) = x. Now it is obvious that if x i is negative, then it is an integer iff a(−x i ) = −x i . So we can conclude as above that satisfiability is not decidable for formulae not in Φ P .
Examples studied above, show that requirements of Def. 7, and so of Def. 8, are necessary to ensure that satisfiability is decidable. Thus, the sets Φ L and Φ P are the biggest decidable classes.
5 Modeling sets with Φ L and Φ P The sets of formulae Φ L and Φ P are sufficient to model sets and strings.
In the following we show how to write classical operators and properties on sets of integers and reals, where A and B are sets of n-tuples.
-A = {(x 1 , . . . , x n ) | φ} where φ is a formula with only real variable, can be expressed with the formula ∀x 1 . . . . ∀x n .a A (x 1 , . . . , [1,n] x j = y i j -|A| ≥ k can be expressed by the formula
We note that the formulae above are closed on conjunction and disjunction.
This last formula is in Φ P , and therefore the satisfiability is decidable.
In the example above we have considered sets of reals where formulae to express properties are polynomial. If one wants to consider also integers one must restrict to linear formulae.
This last formula is in Φ L , and therefore the satisfiability is decidable.
We have proved that, in the framework of Arithmetical Logics, quantifier elimination for formulae with functions cannot exist, and hence we have defined a technique for decreasing the arity of functions appearing in a given formulae. We have proved the correctness of the method and we have used it to prove the decidability of the satisfiability problem for two classes of formulae. These classes have sufficient power to model theories as those of sets and strings.
In the literature several classes and methods have been studied. In [4] the decidable classes are surveyed. First of all, the paper considers classes that are subclasses of first order logics (hence no predicates and functions can be quantified). In [26] formulae with prefixes in ∃ * ∀ * and without functions are considered. Formulae with prefixes in ∃ * ∀ 2 ∃ * and without functions and equality predicates are tackled in [11], [24] and [27]. Formulae without equality predicate, and with unary predicate and functions are studied in [19] and [12]. In [22] and [13] prefixes in ∃ * ∀∃ * for formulae without equality predicates are considered, and in [14] existential quantified formulae are tackled. Finally universal quantified formulae with unary predicates and at most one unary function are studied in [3]. For all these classes, the finite model property is decidable, i.e. it is decidable to check whether there exists a model with a given finite complexity satisfying a given formula. The classes we define have a decidable result for generic model, moreover also quantifications on functions are considered. We do not consider predicates but these can be simulated by a function that can assume values in the set {0, 1}, where 0 represents f alse, and 1 represents true.
Monadic second order formulae are studied in [25] (see [15] and [33] for surveys). More precisely, a second order logic is defined (with unary predicates and at most one unary function) for which the satisfiability problem is decidable. There are several differences between this logic and those we consider. First of all, we have general arity but restrictions on the quantifications of variables and functions. Moreover, we consider reals and integers. In [25] only the natural field is considered (in [28] it is proved that the satisfiability problem for monadic second order logic on real field is undecidable). Finally we consider polynomial and general linear formulae, instead of formulae of the form x < y as done in [25]. The class defined in [29] contains the set of second order formulae with prefixes in ∃ * ∀∃ * , with predicates and one function. The classes we consider have a similar prefix, but the other differences shown for the class in [25] still hold.
Hence we must compare our classes with the classes allowing real and integer variables. Decidability results in this framework in usually given by a quantifier elimination technique. In [9] quantifier elimination for formulae which are linear and which contain real variables is studied. In [32] Tarski considers the general case of polynomial formulae on real variables. In the case of integer variables, if one considers linear formulae without quantifier on integer variables, then the satisfiability is decidable (see [36] and [18]). If one deals with First Order Logic on Linear Formulae with Integer Variables (called Presburger Arithmetic), [8] offers a quantifier elimination algorithm which is given by introducing equivalences modulo a natural value. In [10] it is shown that it is decidable in double-exponential time. These first studies were directed to prove decidability. In recent years such quantifier elimination procedure has turned out to allow important applications e.g. in simulation and optimization, control theory and applied computational geometry ( [1], [5], [6], [17] and [35]). Hence improvements to the efficiency of the algorithms are done in [20] and [31]. When one tackles formulae with mixed integer and real variables, techniques of quantifier elimination given for real field still hold. Conversely, these techniques do not hold for the case of integer variables. In [34], a quantifier algorithm for mixed variables is proposed. In this case, together with equivalences modulo a natural value, a function which gives the integer part of a real value is considered. All the classes mentioned consider first order logics without functions symbols. Hence they are subclasses of Φ L and Φ P . For formulae with exponential functions, which our logics cannot express, quantifier elimination exists for some cases (see [21]).
The satisfiability problem for High Order Arithmetical Logics (where function are quantifiable) is undecidable (due to the already mentioned undecidability result holding for polynomial formulae on integer variables). This bad result holds also if one considers linear formulae (see [7] and [16]). If uninterpreted functions are considered with linear formulae then the decidability holds [30]. It is immediate to see that the classes defined in this paper extend the class of uninterpreted functions by simply considering formulae of the form ∃a.∀x.φ.