- Email: [email protected]

Marek Košta, Thomas Sturm, Andreas Dolzmann

PII: DOI: Reference:

S0747-7171(15)00071-1 http://dx.doi.org/10.1016/j.jsc.2015.07.002 YJSCO 1607

To appear in:

Journal of Symbolic Computation

Received date: Accepted date:

27 September 2014 8 July 2015

Please cite this article in press as: Košta, M., et al. Better answers to real questions. J. Symb. Comput. (2016), http://dx.doi.org/10.1016/j.jsc.2015.07.002

This is a PDF file of an unedited manuscript that has been accepted for publication. As a service to our customers we are providing this early version of the manuscript. The manuscript will undergo copyediting, typesetting, and review of the resulting proof before it is published in its final form. Please note that during the production process errors may be discovered which could affect the content, and all legal disclaimers that apply to the journal pertain.

Better Answers to Real Questions Marek Koˇstaa , Thomas Sturma , Andreas Dolzmannb a Max-Planck-Institut b Leibniz-Zentrum

f¨ ur Informatik, 66123 Saarbr¨ ucken, Germany f¨ ur Informatik, 66123 Saarbr¨ ucken, Germany

Abstract We consider existential problems over the reals. Extended quantiﬁer elimination generalizes the concept of regular quantiﬁer elimination by providing in addition answers, which are descriptions of possible assignments for the quantiﬁed variables. Implementations of extended quantiﬁer elimination for the quadratic case via virtual substitution have been successfully applied to various problems in science and engineering. So far, the answers produced by these implementations included inﬁnitesimal and inﬁnite numbers, which are hard to interpret in practice. We introduce here a post-processing procedure to convert, for ﬁxed parameters, all answers into standard real numbers. The relevance of our procedure is demonstrated by application of our implementation to various examples from the literature, where it signiﬁcantly improves the quality of the results.

1. Introduction We consider existential problems over the reals. Extended quantiﬁer elimination generalizes the concept of regular quantiﬁer elimination by providing in addition answers, which are descriptions of possible assignments for the quantiﬁed variables (Weispfenning, 1994a, 1997b). Implementations of extended quantiﬁer elimination (Dolzmann and Sturm, 1997a, 1999; Dolzmann et al., 1998a) for the quadratic case via virtual substitution (Weispfenning, 1988, 1994b, 1997a; Loos and Weispfenning, 1993; Dolzmann et al., 1999) have been successfully applied to various problems in science and engineering (Sturm and Weispfenning, 1997b,a; Dolzmann et al., 1998b; Sturm, 1999a,b, 2000a; Weispfenning, 2001; Sturm and Weber, 2008; Sturm et al., 2009; Sturm and Tiwari, 2011; Weber et al., 2011; Errami et al., 2011, 2013, 2015). So far, the answers produced by these implementations included inﬁnitesimal and inﬁnite numbers, which are hard to interpret in practice. This has been explicitly criticized in the literature, e.g., by Collard (2003). In the present article, we introduce a complete post-processing procedure to convert, for ﬁxed values Email addresses: [email protected] (Marek Koˇsta), [email protected] (Thomas Sturm), [email protected] (Andreas Dolzmann)

Preprint submitted to Journal of Symbolic Computation

July 17, 2015

of parameters, all answers into standard real numbers. We furthermore demonstrate the successful application of an implementation of our method within Redlog (Dolzmann and Sturm, 1997a) to a number of extended quantiﬁer elimination problems from the scientiﬁc literature including computational geometry (Sturm and Weispfenning, 1997a), motion planning (Weispfenning, 2001), bifurcation analysis for models of genetic circuits and for mass action (Sturm and Weber, 2008; Sturm et al., 2009), and sizing of electrical networks (Sturm, 1999b). The plan of the paper is as follows: In Section 2 we make ourselves familiar with the concept of extended quantiﬁer elimination. In Section 3 we give an introduction of virtual substitution for extended quantiﬁer elimination for the quadratic case to the extent necessary to understand how nonstandard values enter the answers and what information is available for ﬁxing them to standard values. Section 4 is the technical core; we describe and prove our method and illustrate it by discussing one example in detail. In Section 5 we revisit degree shifts for reducing the degree of quantiﬁed variables before their elimination, which heuristically pushes the limits of our implementation beyond the quadratic case (Weispfenning, 1997a; Dolzmann et al., 1998b). We re-interpret these degree shifts as quantiﬁer eliminations by virtual substitution. This allows us in Section 6 to generalize our method to cover also possible degree shifts during elimination. In Section 7 we revisit examples from the scientiﬁc literature where the application of extended quantiﬁer elimination to various problems from planning, modeling, science, and engineering had yielded nonstandard answers. In all cases we can eﬃciently ﬁx all nonstandard symbols to standard values using our implementation of the method as it was introduced in Section 4 and generalized in Section 6. This signiﬁcantly improves the quality of the results from a practical point of view. Finally, in Section 8 we summarize our results and discuss possible extensions of our method. 2. The Concept of Extended Quantiﬁer Elimination For our purposes here, we restrict ourselves to existential problems ϕ(u1 , . . . , um ) = ∃xn . . . ∃x1 ψ(x1 , . . . , xn , u1 , . . . , um ) with parameters u = (u1 , . . . , um ) in the Tarski language L = (0, 1, +, −, ·, ≤ , <, ≥, >, =) interpreted in the Tarski algebra (R, 0, 1, +, −, ·, ≤, <, ≥, >, =). As usual in algebraic model theory, the symbol “=” and its interpretation as equality is part of ﬁrst-order logic so that it does not occur explicitly in the language L. Without loss of generality, ψ is an ∧-∨-combination of atomic constraints, and we agree that all right hand sides of the atomic constraints are 0. Extended quantiﬁer elimination applied to ϕ yields an extended quantiﬁer elimination result (EQR) as follows: ⎤ ⎡ x1 = e11 (u) ... xn = e1n (u) β1 (u) ⎥ ⎢ .. .. .. .. ⎦. ⎣ . . . . βk (u)

x1 = ek1 (u)

... 2

xn = ekn (u)

The conditions βi (u) are quantiﬁer-free Tarski formulas such that R |= ϕ ←→ k k i=1 βi . In other words, i=1 βi is a regular quantiﬁer elimination result for ϕ, and extended quantiﬁer elimination generalizes regular quantiﬁer elimination. The answers ei (u) are terms in an extension language of the Tarski language. For a ∈ Rm , if ϕ(a) holds, then at least one βi (a) holds, and so does ψ(ei (a), a). We agree that “false” never occurs as a condition. If ϕ itself is equivalent to “false,” we possibly obtain the empty EQR [ ]. As an example, consider the input formula ϕ = ∃x∃yψ,

ψ = ay + 3x2 + 4x ≤ a ∧ x ≥ a ≥ y.

A possible extended quantiﬁer elimination result for ϕ is given by ⎡ y = −3a − 3 x=a a = 0 ∧ 4a + 3 ≥ 0 ⎢ √ ⎢ −3a2 + 3a + 4 − 2 ⎣ y=a x= a ≤ 0 ∧ 3a2 − 3a − 4 ≤ 0 3

⎤ ⎥ ⎥. ⎦

From this extended quantiﬁer elimination result we can derive a regular quantiﬁer elimination result (a = 0 ∧ 4a + 3 ≥ 0) ∨ (a ≤ 0 ∧ 3a2 − 3a − 4 ≤ 0), which can be simpliﬁed to a ≥ 0 ∨ 3a2 − 3a − 4 ≤ 0. Hence, ϕ holds if and only if a ≥ α, where α ≈ −0.758306 is the smaller root of 3a2 − 3a − 4. In the extended quantiﬁer elimination result, the ﬁrst row covers the case that −0.75 ≤ a and a = 0, while the second row covers α ≤ a ≤ 0. Let us consider some particular interpretations of a: • For a = 2, the condition in the ﬁrst row holds, and the corresponding answers yield x = 2 and y = −9. In fact, these three values satisfy ψ. The condition in the second row, in contrast, does not hold. If we plug a = 2 into the corresponding answers anyway, then we obtain a negative argument for the square root, which cannot be interpreted over the reals. • For α < a = −0.7525 < −0.75, the condition in the second row holds, and √ the corresponding answers yield x = 6997−800 and y = −0.7525. Again, 1200 these three values satisfy ψ. Now the condition in the ﬁrst row does not hold. If we plug a = −0.7525 into the corresponding answers anyway, then we obtain x = −0.7525 and y = −0.7425, which does not satisfy ψ. • For a = −0.5, both conditions hold and yield two diﬀerent sets of val√ , y = −0.5, ues satisfying ψ, viz. x = −0.5, y = −1.5 and x = 7−4 6 respectively. • For a = 0 only the condition in the second row holds, but the answers in the ﬁrst row happen to work as well. This shows that the conditions are suﬃcient but not necessary for the answers to be valid. 3

Although we are focusing on the reals here, it is noteworthy that extended quantiﬁer elimination is an established concept, which exists also for a variety of other important algebraic theories including the linear theory of valued ﬁelds (Sturm, 2000b), Presburger Arithmetic (Lasaruk and Sturm, 2007), initial Boolean algebras (Seidl and Sturm, 2003; Sturm and Zengler, 2010), and certain term algebras (Sturm and Weispfenning, 2002). 3. The Method of Virtual Substitution Given ϕ(u) = ∃xψ(x, u), we compute a ﬁnite elimination set

γ ∧ ψ[x // e]. E = . . . , γ(u), e(u) , . . . , such that ∃xψ ←→

(1)

(γ,e)∈E

In the elimination set E the e(u) are elimination terms substituted for the quantiﬁed variable x via a virtual substitution [x // e]. The γ are quantiﬁer-free Tarski formulas serving as substitution guards. Equation (1) formally describes regular quantiﬁer elimination of one quantiﬁer ∃x from ϕ. For the elimination of several quantiﬁers, one assumes without loss of generality that the formula is prenex and processes the prenex quantiﬁer block from the inside to the outside. We are now going to give an idea of the exact shape and computation of elimination sets that is suﬃciently precise to understand our main contribution here. For a more thorough introduction into the theory of quantiﬁer elimination by virtual substitution we refer to the original publications by Weispfenning (1988, 1994b, 1997a), Loos and Weispfenning (1993), and Dolzmann et al. (1999). In Section 3.1 we restrict ourselves to input formulas ϕ not containing any strict inequalities “<,” “>,” or “=.” In that course it will become clear how exactly we derive extended quantiﬁer elimination from the virtual substitution procedure. Later, in Section 3.2, we generalize to formulas containing also strict inequalities. While with regular quantiﬁer elimination the techniques used in the course of the generalization to strict inequalities remain completely transparent to the user, with extended quantiﬁer elimination they leave visible traces in the answers by possibly introducing certain nonstandard elements, which do not have a straightforward interpretation over the reals. The purpose of this paper is to convert these answers to standard real numbers, given ﬁxed real values for the parameters. 3.1. Virtual Substitution for Weak Inequalities Recall that our constraints are normalized such that their right hand sides are 0. Assume that all occurrences of x in ϕ(u) = ∃xψ(x, u) are at most quadratic. Consider ﬁxed real interpretations u = a ∈ Rm for all parameters. Then all constraints in ψ(x, a) become univariate, and the set { c ∈ R | R |= ψ(c, a) } is a ﬁnite union of real intervals, where the interval endpoints are zeros of the univariate left hand side polynomials.

4

Our goal is to include at least one such interval endpoint into our elimination set E: For each constraint f2 (u)x2 + f1 (u)x + f0 (u) 0 with ∈ {=, ≤, ≥} and discriminant Δ = f12 − 4f2 f0 we add to E three pairs (γ, e) as follows: f2 = 0 ∧ Δ ≥ 0,

√ −f1 + Δ , 2f2

√ −f1 − Δ f2 = 0 ∧ Δ ≥ 0, , 2f2

f2 = 0 ∧ f1 = 0, −

f0 . f1

In order to obtain a quantiﬁer-free equivalent for ϕ, such pairs have to be plugged into ϕ according to (1). To start with, note that the substitution guards γ make the substitution terms e meaningful by ensuring that denominators are not zero and that arguments of square roots are not negative. Next, observe that our elimination terms e are not terms in the Tarski language as they contain division as well as root symbols. It is one central idea of the virtual substitution approach that the substitution operator does not map L-terms to L-terms but atomic L-formulas to quantiﬁer-free L-formulas: [x // t] : atomic L-formulas → quantiﬁer-free L-formulas Note that when there is more than one quantiﬁer, it is crucial to obtain Lformulas in (1) in order to be able to proceed with the respective next quantiﬁer. To give an impression of virtual substitution, we describe here the substitu√ g +g g tion (f = 0)[x // 1 g24 3 ] of a root expression √ g 1 + g2 g3 , g4

gi ∈ Z[u]

into an equation f = 0, where f ∈ Z[u][x] of arbitrary degree: It is easy to see that there are g1∗ , g2∗ , g4∗ such that √ √ g ∗ + g2∗ g3 g1 + g2 g3 = 1 f g4 g4∗ is again a root expression. Using this intermediate result, we transform as follows:1 √ g1∗ + g2∗ g3 √ =0 = ˙ g1∗ + g2∗ g3 = 0 ∗ g4

√ = ˙ |g1∗ | = |g2∗ g3 | ∧ sgn(g1∗ ) = sgn(g2∗ ) ∨ sgn(g1∗ ) = sgn(g2∗ ) = 0 = ˙

g1∗ 2 − g2∗ 2 g3 = 0 ∧ g1∗ g2∗ ≤ 0.

Technical details and formal descriptions of virtual substitutions for all our relations have been given by Weispfenning (1997a). 1 For

clarity we use “=” ˙ to distinguish equality from the ﬁrst-order symbol “=.”

5

Let us now apply these ideas to derive an extended quantiﬁer elimination procedure for several existential quantiﬁers via virtual substitution. Given ∃xn . . . ∃x1 ψ(x1 , . . . , xn , u1 , . . . , um ), our intended result is a scheme as described in Section 2: ⎡ β1 (u) x1 = e11 (u) ... xn = e1n (u) ⎢ .. .. .. . .. ⎣ . . . x1 = ek1 (u) ... xn = ekn (u) βk (u)

⎤ ⎥ ⎦.

We successively apply (1) to x1 , . . . , xn using elimination sets E1 (x2 , . . . , xn , u), . . . , En (u), respectively, to obtain β1 , . . . , βk as follows:

··· γn ∧ · · · ∧ γ1 ∧ ψ[x1 // e1 ] · · · [xn // en ] . (2) (γ ,e )∈E (γ ,e )∈E n

n

n

1

1

1

βi (u)

The index i of βi describes one choice (γn , en ), . . . , (γ1 , e1 ) from the Cartesian product En × · · · × E1 . In practice, the βi obtained this way undergo sophisticated simpliﬁcation methods such as those described by Dolzmann and Sturm (1997b). Recall from the previous section that βi which become “false” are ignored. It is important to understand that for the computation of the βi we are using exclusively virtual substitution. The corresponding ei (u), in contrast, are obtained from en (u), en−1 (xn , u), . . . , e1 (x2 , . . . , xn , u) via regular back-substitution of terms: ei,n = en ,

ei,n−1 = en−1 [xn /ei,n ],

ei,1 = e1 [x1 /ei,2 ] . . . [xn /ei,n ].

(3)

Formally, that back-substitution takes place in a suitable extension language of L possibly creating objects like √ 3 5u1 − u2 − 2 u1 + , 2 which are not L-terms or even root expressions. Regular back-substitution is thus suitable for obtaining the ei but not for the βi . Vice versa, virtual substitution requires atomic formulas as input. Thus it is suitable for obtaining the βi while for the ei it is not applicable at all. Virtual substitution and regular term substitution are independent concepts, which complement each other. 3.2. Virtual Substitution with Strict Inequalities Let us return to the elimination of a single quantiﬁer from ∃xψ(x, u). Recall from the beginning of the previous Section 3.1 how we considered ﬁxed interpretation u = a ∈ Rm causing the set S = { c ∈ R | R |= ψ(c, a) } to be a ﬁnite union of intervals. When considering in addition strict inequalities, the intervals in S are possibly open. Consequently, for a strict constraint ψi (x, u) = ˙ fi2 (u)x2i + fi1 (u)xi + fi0 (u) i 0, 6

i ∈ {=, <, >},

(4)

contained in ψ(x, u) we cannot use the zeros zi (u) of its left hand side but need a point from inside the corresponding interval. The established approach for strict inequalities uses nonstandard extensions of R: Let ε ∈ R∗ ⊃ R be a positive inﬁnitesimal number, i.e., 0 < ε < x for all 0 < x ∈ R. Then for a strict constraint as deﬁned in (4) we use four test points √ −fi1 ± Δi ± ε. 2fi2 As an optimization, it suﬃces to consider only upper bounds using −ε. For solution sets that are unbounded from above we have to add only one more point ∞ := 1/ε ∈ R∗ for the entire problem. In early versions of virtual substitution methods for the linear case, Weispfenning (1988) used arithmetic means 12 (zi + zj ) for all pairs (ψi , ψj ) of strict constraints. However, the size of the elimination set then grows quadratically in the number of constraints. Furthermore, one cannot apply the above-mentioned optimization to ignore all lower bounds. In experiments with early implementations this turned out to be critical for the practical performance of the method (Burhenne, 1990; Loos and Weispfenning, 1993). For the quadratic case, there is an even more fundamental obstacle. Arithmetic means −gj1 ± Δj 1 −gi1 ± Δi (5) + 2 2gi2 2gj2 g ∗ +g ∗

√

Δ∗

of root expressions are themselves not root expression of the form 1 g2∗ , so 3 that Weispfenning’s (1997a) virtual substitution rules sketched in the previous Section 3.1 are not applicable at all. From a theoretical point of view, it easily follows from the existence of real quantiﬁer elimination that suitable virtual substitutions for arithmetic means of the form (5) exist. However, the practical applicability of this approach is quite questionable so that it has never been explicitly studied. Let us return to our approach with non-standard expressions. For the application of the elimination set as described in (1) and thus for the computation of the βi with extended quantiﬁer elimination, both ε and ∞ are equivalently translated into the Tarski language L via virtual substitution. For instance, let t be a standard term. Then ˙ (x3 + x2 − x − 1 < 0)[x // t − ε] = (x3 + x2 − x − 1 < 0 ∨ (x3 + x2 − x − 1 = 0 ∧ (3x2 + 2x − 1 > 0 ∨ (3x2 + 2x − 1 = 0 ∧ (6x + 2 < 0 ∨ (6x + 2 = 0 ∧ 6 > 0))))))[x // t]. The principal idea becomes clear when noticing that 3x2 + 2x − 1, 6x + 2, and 6 are the ﬁrst, second, and third derivatives of x3 + x2 − x − 1, respectively. In a subsequent step, t is virtually substituted for x as discussed in the previous section. For the substitution of ∞ we have, e.g., (ax2 + bx + c < 0)[x // ∞] = ˙ a < 0 ∨ (a = 0 ∧ b < 0) ∨ (a = 0 ∧ b = 0 ∧ c < 0). 7

Again, precise deﬁnitions and proofs for all relevant cases have been given by Weispfenning (1997a). When performing regular back-substitution of terms on the side of the ei , nonstandard symbols cannot be removed but are propagated along the way. In the ﬁnal result a single answer ei can even contain several of such nonstandard symbols. For example, on input of ϕ = ∃x∃yψ,

ψ= ˙ ay + 3x2 + 4x < 0 ∧ x > y > a

we obtain a nonstandard extended quantiﬁer elimination result: ⎡ −a − 3ε1 − 4 −a − 3ε1 − 3ε2 − 4 x= y= a+4<0 ⎣ 3 3 a<0∧a+4>0 y = −ε1 − ε2 x = −ε1

(6) ⎤ ⎦.

(7) Given such answers containing nonstandard symbols, it is not hard to nonconstructively prove from the elimination procedure that for ﬁxed real interpretations of the parameter a there are positive real choices for ε1 , ε2 so that the answers satisfy ψ. Inﬁnitesimals introduced at diﬀerent stages of the elimination are indexed accordingly. It is noteworthy that they have to be chosen diﬀerently in general: Fixing a = −2 in the example, it is easy to see that ε1 has to be chosen diﬀerent from ε2 because otherwise we would obtain y = 2x, which together with a = −2 does not satisfy ay + 3x2 + 4x < 0. Until now users of extended quantiﬁer elimination were left alone with results as in (7) and the corresponding diﬃculties. Nevertheless, there is a considerable record of applications of extended quantiﬁer elimination in the literature. We are going to discuss some of these with our examples in Section 7. We conclude this section with the important observation that for unﬁxed parameters it is not possible in general to determine suitable real choices for nonstandard symbols: Proposition 1 (No Standard Answers for Unﬁxed Parameters). Consider the formula ϕ = ∃x(a < x < 1) and the nonstandard extended quantiﬁer elimination result x = 1 − ε1 a<1 . a<1 x = 1 − ε1 There is no standard choice ε1 ∈ R such that is an extended quantiﬁer elimination result for ϕ as well. Proof. Assume for a contradiction that ε1 ∈ R is a suitable choice. Then by deﬁnition of extended quantiﬁer elimination it follows for all a ∈ ]−∞, 1[ that a < 1 − ε1 < 1, in particular ε1 > 0. On the other hand, for a0 = 1 − ε21 we have a0 ∈ ]−∞, 1[ and 1 − ε1 < a0 < 1, a contradiction. 4. Elimination of Nonstandard Symbols from Answers Given an extended quantiﬁer elimination result and prescribed values for all parameters, our goal is to compute answers containing only standard real 8

numbers. For instance, given (6) and (7) and ﬁxing a = −2 we are going to obtain 9 1 . y=− x=− true 256 32 From the point-of-view of our method, it makes no diﬀerence whether the parameters are ﬁxed after extended quantiﬁer elimination or in advance. For the sake of a concise description, we are thus going to consider w.l.o.g. existential decision problems from now on. Recall that if the regular quantiﬁer elimination result is “false,” then the extended quantiﬁer elimination result is [ ], i.e., empty. If the result is “true,” then we assume for simplicity that the extended quantiﬁer elimination result contains only one row, like true x1 = e1,1 ... xn = e1,n . (8) Recall from (3) in Section 3.1 that here the e1,1 , . . . , e1,n have been obtained from elimination terms e1 , . . . , en via regular back-substitution. Our method, however, is going to use not these back-substituted answers but the original elimination terms. In addition, it is going to use the substitution guards γ1 , . . . , γn corresponding to those elimination terms. Hence the input for our method is not an EQR like in (8) but a pre-EQR as follows: true x1 = e1 (x2 , . . . , xn ) ... xn−1 = en−1 (xn ) xn = en () . γ1 (x2 , . . . , xn ) ... γn−1 (xn ) γn () Lemma 2 (Semantics of Virtual Substitution). Let ϕ(x1 , . . . , xn ) be a Tarski formula, and let a2 , . . . , an ∈ R. (i) Assume that R |= ϕ[x1 // x2 − ε](a2 , . . . , an ). Then there is ε0 ∈ R, 0 < ε0 , such that for all ε ∈ R, 0 < ε < ε0 , we have R |= ϕ(a2 − ε, a2 , . . . , an ). (ii) Assume that R |= ϕ[x1 // ∞](a2 , . . . , an ). Then there is a0 ∈ R, such that for all a1 ∈ R, a0 < a1 , we have R |= ϕ(a1 , a2 , . . . , an ). In particular, the set T = { a ∈ R | 0 < a and R |= ϕ(a, a2 , . . . , an ) } is unbounded from above. Proof. Consider Lε = L∪{ε, ∞}. Using the compactness theorem for ﬁrst-order logic, there is a real closed ﬁeld R∗ where the interpretation of ε is a positive inﬁnitesimal and ∞ = ε−1 . The L-restriction of R∗ is a proper extension ﬁeld of R and, by the Tarski principle, elementary equivalent to R. Formally, R∗ |L ⊃ R and R∗ |L ∼ = R. (i) Using R ∼ = R∗ |L and expanding to R∗ it follows from R |= ϕ[x1 // x2 − ε](a2 , . . . , an ) that also R∗ |= ϕ[x1 // x2 − ε](a2 , . . . , an ). It has been discussed by Loos and Weispfenning (1993) and Weispfenning (1997a) that for our a2 , . . . , an ∈ R the virtual substitution of ε has the following property: R∗ |= ϕ[x1 // x2 − ε](a2 , . . . , an ) ←→ ϕ[x1 /x2 − ε](a2 , . . . , an ). 9

It follows that R∗ |= ϕ[x1 /x2 − ε](a2 , . . . , an ). Let n ∈ N \ {0}. Then we can conclude R∗ |= ψ[x0 /ε](a2 , . . . , an ), where ψ = (0 < x0 ∧ nx0 < 1 ∧ ϕ)[x1 /x2 − x0 ]. Now we can generalize R∗ |= ∃x0 ψ(a2 , . . . , an ). Since ε does not occur anymore, we restrict from R∗ to R∗ |L and then use the elementary equivalence to obtain R |= ∃x0 ψ(a2 , . . . , an ). We have just shown that for any n ∈ N \ {0} there exists a0 ∈ R, 0 < a0 < n1 , such that R |= ϕ(a2 − a0 , a2 , . . . , an ). It follows that inf S = 0, where S = { a ∈ R | 0 < a and R |= ϕ(a2 − a, a2 , . . . , an ) } ⊆ R. On the other hand, S is a semialgebraic set and thus a ﬁnite union of intervals and points. Hence there is ε0 ∈ R, 0 < ε0 , such that ]0, ε0 [ ⊆ S. (ii) The argument is essentially the same as in (i) above: We conclude that R∗ |= ϕ[x1 // ∞](a2 , . . . , an ). According to Loos and Weispfenning (1993) and Weispfenning (1997a) we know that R∗ |= ϕ[x1 // ∞](a2 , . . . , an ) ←→ ϕ[x1 /∞](a2 , . . . , an ) so that for n ∈ N we can conclude R∗ |= ψ[x0 /∞](a2 , . . . , an ), where ψ = (n < x0 ∧ ϕ)[x1 /x0 ]. Again, we generalize, restrict, and apply elementary equivalence to obtain R |= ∃x0 ψ(a2 , . . . , an ). We thus know that for any n ∈ N there exists a0 ∈ R, n < a0 , such that R |= ϕ(a0 , a2 , . . . , an ). It follows that the set T is unbounded from above. On the other hand, T is a semialgebraic set and thus a ﬁnite union of intervals and points. Hence there is a0 ∈ R, such that ]a0 , ∞[ ⊆ T . Lemma 3. Consider a quantiﬁer-free Tarski formula ψ(x1 , . . .√, xn ). Assume a +b c that for each i ∈ {2, . . . , n} we have a root expression ei = i dii i with ai , bi , ci , di ∈ Z[xi+1 , . . . , xn ]. Assume furthermore that R |= ψ −→ ci ≥ 0 ∧ di = 0, en ]. Then and let αi ∈ R be the interpretation of ei = ei [xi+1 /e i+1 ] . . . [xn / { α ∈ R | R |= ψ[x2 // e2 ] . . . [xn // e n ](α) } = { α ∈ R | R |= ψ(α, α2 , . . . , αn ) }. √ √ and −1 Proof. Consider L = L∪{ , −1 } and the L -expansion R of R where have the usual semantics if deﬁned and an arbitrary but ﬁxed value otherwise. Let ν =√(f 0), where f ∈ Z[x, u1 , . . . , um ], ∈ {=, =, <, ≤, ≥, >}, and let e = a+bd c , where a, b, c, d ∈ Z[u1 , . . . , um ]. Let s ∈ Rm such that c(s) ≥ 0 and d(s) = 0. Then according to Weispfenning (1997a) the following holds for s ∈ Rm : R |= (ν[x // e] ←→ ν[x/e])(s).

10

For our formula ψ and all α ∈ R we obtain en ] ←→ ψ)(α, α2 , . . . , αn ). R |= (ψ[x2 // e2 ] . . . [xn // e n ] ←→ ψ[x2 /e2 ] . . . [xn / It follows that R |= (ψ[x2 // e2 ] . . . [xn // e n ] ←→ ψ)(α, α2 , . . . , αn ) for all α ∈ R. Lemma 4 (Commutation of Virtual Substitutions). Consider a quantiﬁer-free √ a +b c Tarski formula ψ(x1 , . . . , xn ). Let e1 = 1 d11 1 , with a1 , b1 , c1 , d1 ∈ Z, a +b

√

c

c1 ≥ 0, d1 = 0. Furthermore, let i ∈ {2, . . . , n}, let ei = i dii i with ai , bi , ci , di ∈ Z[xi+1 , . . . , xn ], and let γi (xi+1 , . . . , xn ) be a quantiﬁer-free formula such that R |= γi −→ ci ≥ 0 ∧ di = 0. Then R |= (γi ∧ ψ)[xi // ei ][x1 // e1 ] ←→ (γi ∧ ψ)[x1 // e1 ][xi // ei ]. Proof. Let L , R be as in the proof of Lemma 3. Recall the equivalence R |= (ν[x // e] ←→ ν[x/e])(s) and observe that, on the other hand, if R |= (ci < 0)(s) or R |= (di = 0)(s) for s ∈ Rn−i , then R |= (γi ∧ ψ ←→ false)(s). It follows that R |= (γi ∧ ψ)[xi // ei ][x1 // e1 ]

←→ ←→ ←→

(γi ∧ ψ)[xi /ei ][x1 /e1 ] (γi ∧ ψ)[x1 /e1 ][xi /ei ] (γi ∧ ψ)[x1 // e1 ][xi // ei ].

√ and −1 , we can conSince virtual substitution eliminates all occurrences of clude that R |= (γi ∧ ψ)[xi // ei ][x1 // e1 ] ←→ (γi ∧ ψ)[x1 // e1 ][xi // ei ]. Theorem 5 (Computation of Standard Answers). Consider a closed Tarski formula ϕ = ∃xn . . . ∃x1 ψ(x1 , . . . , xn ). Assume that true x1 = e1 ... xn = e n γ1 ... γn is a pre-EQR for ϕ such that each ei is of one of the following forms: (a) a root expression

√ a+b c , d

where a, b, c, d ∈ Z[xi+1 , . . . , xn ],

(b) ∞, (c) xi+1 − ε. Then we can compute root expressions e1 , . . . , e n meeting the speciﬁcation (a) above and γ1 , . . . , γ n such that the following is a pre-EQR for ϕ as well: x1 = e1 ... xn = e true n . (9) γ1 ... γ n

11

Proof. For the sake of the proof, we are going to show that in addition to the required e1 , . . . , e n and γ1 , . . . , γ n we can compute real algebraic numbers α1 , . . . , αn for the values of e1 , . . . , e n after back-substitution. We represent these real algebraic numbers as pairs of univariate deﬁning polynomials and open isolating intervals with rational bounds. Given k ∈ {1, . . . , n}, it suﬃces to show that from xk = ek xk+1 = e ... xn = e true x1 = e1 . . . k+1 n γ1 . . . γk γ ... γ k+1 n and αk+1 , . . . , αn we can compute suitable ek , γ k , and αk . Deﬁne ϕk (xk , . . . , xn ) ϕk+1 (xk+1 , . . . , xn ) and observe that true

and

=

(γk−1 ∧ · · · ∧ γ1 ∧ ψ)[x1 // e1 ] . . . [xk−1 // ek−1 ],

=

(γk ∧ ϕk )[xk // ek ],

xk+1 = e k+1 γ k+1

xk = ek γk

xk+1 = e k+1 γ k+1

true

... ...

... ...

xn = e n γ n

xn = e n γ n

(10)

(11)

are pre-EQRs for ∃xn . . . ∃xk ϕk and ∃xn . . . ∃xk+1 ϕk+1 , respectively. On the k , basis of these deﬁnitions it is suﬃcient for our proof to compute suitable ek , γ and αk such that xk = ek xk+1 = e ... xn = e true k+1 n γ k γ ... γ k+1 n is a pre-EQR for ∃xn . . . ∃xk ϕk as well. We deﬁne furthermore ξ(xk , . . . , xn ) ξ (xk )

=

γ n ∧ ··· ∧ γ k+1 ∧ ϕk ,

=

ξ[xk+1 // e k+1 ] . . . [xn // e n ].

Lemma 3 applied to the quantiﬁer-free formula ξ, the root expressions e k+1 , . . . , e n , and the real algebraic numbers αk+1 , . . . , αn yields { r ∈ R | R |= ξ (r) } = { r ∈ R | R |= ξ(r, αk+1 , . . . , αn ) }.

(12)

We distinguish three cases depending on the type of ek . a +b

√

c

(a) We have ek = k dkk k , and γk equals dk = 0 ∧ ck ≥ 0. We set ek = ek and γ k = γk . Since (11) is a pre-EQR for ∃xn . . . ∃xk+1 ϕk+1 and αk+1 , . . . , αn correspond to the values of e k+1 , . . . , e n after back-substitution, we have R |= ϕk+1 (αk+1 , . . . , αn ). It follows that in particular R |= γk (αk+1 , . . . , αn ) and furthermore R |= (dk = 0)(αk+1 , . . . , αn ) and R |= (ck ≥ 0)(αk+1 , . . . , αn ). This allows us to compute αk = ek (αk+1 , . . . , αk ) from ak , bk , ck , dk , αk+1 , . . . , αn . 12

(b) We have ek = ∞, and γk is “true.” Since (10) is a pre-EQR for formula ∃xn . . . ∃xk ϕk we have R |= ξ[xk // ∞][xk+1 // e k+1 ] . . . [xn // e n ]. Using the fact that αk+1 , . . . , αn are real algebraic numbers corresponding to the values of e k+1 , . . . , e n after back-substitution we conclude that R |= ξ[xk // ∞](αk+1 , . . . , αn ). Lemma 2(ii) now guarantees that the set { r ∈ R | R |= ξ(r, αk+1 , . . . , αn ) } is unbounded from above. Thus by (12) the set { r ∈ R | R |= ξ (r) } is unbounded from above as well. Using well-known bounds (Akritas, 2009) on the roots of the univariate polynomials contained in √ ξ , we compute a p p+0 0 suﬃciently large q ∈ Q satisfying ξ . We set ek = and construct q k = true. Then a corresponding real algebraic number αk , and we set γ R |= ( γk ∧ ξ )[xk // ek ], and n − k applications of Lemma 4 yield R |= ( γn ∧ · · · ∧ γ k ∧ ϕk )[xk // ek ][xk+1 // e k+1 ] . . . [xn // e n ]. (c) We have ek = xk+1 − ε, and γk is “true.” Similarly to case (b), we observe that (10) is a pre-EQR for ∃xn . . . ∃xk ϕk and obtain R |= ξ[xk // xk+1 − ε][xk+1 // e k+1 ] . . . [xn // e n ], and conclude that R |= ξ[xk // xk+1 − ε](αk+1 , . . . , αn ). Lemma 2(i) now guarantees the existence of some ε0 ∈ R, 0 < ε0 , such that R |= ξ(αk+1 − ε, αk+1 , . . . , αn )

for

0 < ε < ε0 .

By (12) it follows that R |= ξ (αk+1 − ε) for all 0 < ε < ε0 . Therefore, after ﬁnitely many reﬁnements of the isolating interval pq , u of αk+1 we obtain √

R |= ξ pq . We set ek = p+0q 0 and construct a corresponding real algebraic number, and we set γ k = true. Exactly as in case (b), R |= ( γk ∧ξ )[xk // ek ], and n − k applications of Lemma 4 yield R |= ( γn ∧ · · · ∧ γ k ∧ ϕk )[xk // ek ][xk+1 // e k+1 ] . . . [xn // e n ]. Note that instead of using the lower bound ﬁnd a satisfying integer.

p q

one can heuristically try and

A careful inspection of our proof reveals that in all cases γ k = γk . However, this is going to change in Corollary 7, which generalizes our theorem. Notice that the constructive proof of Theorem 5 suggests to recompute the intermediate quantiﬁer elimination results ϕk . In practice, there are arguments for saving these ϕk during the extended quantiﬁer elimination run. Consider, e.g., the following common optimization: Whenever some ϕk heuristically simpliﬁes to a disjunction ϕk,1 ∨ · · · ∨ ϕk,s , then the virtual substitution procedure would treat each ϕk,j separately, i.e., like originating from several elimination set elements. In general, in the course of the application of Theorem 5 such transformations cannot be reconstructed exclusively from the pre-EQR. 13

Illustrating Examples We are going to illustrate Theorem 5 by means of two examples. Example 1 We revisit our example given in (6) for the choice a = −2. For this choice, (6) specializes to ϕ = ∃x∃yψ,

ψ= ˙ −2y + 3x2 + 4x < 0 ∧ x > y > −2,

and the second row of the EQR (7) before back-substitution becomes true y =x−ε x = −ε . To meet the requirement of the theorem that inﬁnitesimals occur only in expressions of the form xi = xi+1 − ε we introduce an artiﬁcial variable h, which leads to the following pre-EQR to start with: y =x−ε x=h−ε h=0 true . (13) true true true Following the proof of the theorem, we compute ϕ1 (y, x, h) ϕ2 (x, h) ϕ3 (h)

= ˙

−2y + 3x2 + 4x < 0 ∧ x > y > −2,

= ˙ true ∧ ϕ1 [y // x − ε] = ˙ true ∧ x + 2 > 0 ∧ 3x2 + 2x < 0, = ˙ = ˙

true ∧ true ∧ ϕ2 [x // h − ε] true ∧ true ∧ h + 2 > 0 ∧ (h = 0 ∨ 3h2 + 2h < 0).

As in the theorem, we proceed from the right to the left, i.e., our ﬁrst step is ﬁxing h and computing a respective algebraic number αh . Since h = 0, we are in case (a), and true h=0 true is a pre-EQR for ∃hϕ3 . We set αh to 0, which is formally represented as the only root of ζ ∈ Z[ζ] in the interval ]−1, 1[. We continue with x = h − ε, which is case (c). Now true x=h−ε h=0 true true is a pre-EQR for ∃h∃xϕ2 . For ξ = true ∧ ϕ2 we obtain R |= ξ[x // h − ε][h // 0] and conclude that R |= ξ[x // h − ε](0). Lemma 2(i) guarantees that there exists ε0 ∈ R with 0 < ε0 such that for all ε ∈ R with 0 < ε < ε0 we have R |= ξ(αh − ε, αh ). It follows that for all ε ∈ R with 0 < ε < ε0 also R |= ξ (αh − ε), where ˙ true ∧ true ∧ x + 2 > 0 ∧ 3x2 + 2x < 0. ξ = ξ[h // 0] = 14

1 1 1 Reﬁning the isolating interval ]−1, 1[ of αh to ]− 32 , 32 [ we ﬁnd that R |= ξ (− 32 ). 1 We replace x = h − ε with the standard answer x = − 32 , which is a root expression, and we compute a corresponding real algebraic number αx as the only 1 1 , 16 [. root of 32ζ + 1 in the interval ]− 16 The last answer to consider is y = x − ε, which is again case (c). Now 1 true y =x−ε x = − 32 h=0 true true true

is a pre-EQR for ∃h∃x∃yϕ1 . Analogously to the previous step we obtain ξ = true ∧ true ∧ ϕ1 and ξ

= = ˙

1 ξ[x // − 32 ][h // 0] true ∧ true ∧ −2048y − 125 < 0 ∧ −32y − 1 > 0 ∧ y + 2 > 0.

1 1 9 9 Reﬁning the isolating interval ]− 16 , 16 [ of αx to ]− 256 , 256 [ we ﬁnd that R |= 9 9 , which is a ξ (− 256 ). We replace y = x − ε with the standard answer y = − 256 root expression, and we compute a corresponding real algebraic number αy as 5 5 , 128 [. In our ﬁnal output pre-EQR the only root of 256ζ +9 in the interval ]− 128 we delete the answer h = 0 as h does not occur in the input formula: 9 1 true y = − 256 x = − 32 . true true

Example 2 Our second example addresses a rather straightforward but interesting generalization of extended quantiﬁer elimination, which we have not discussed so far: Consider the valid sentence ∃x∃a(x − a < 0). After elimination of ∃a we essentially obtain ∃x(true). Our theoretical framework would now compute an elimination set {(true, ∞)} for x and obtain a corresponding answer x = ∞. In practice, however, we recognize that x can be chosen arbitrarily, which implementations of extended quantiﬁer elimination express using EQRs like: true a=∞ x = arbitrary1 . For applying Theorem 5 such arbitrary variables have to be replaced with arbitrary but ﬁxed answers that are interpretable in the context of the condition “true.” It is easy to see that this is not a limitation of the theorem but a semantic consequence similar to the observation in Proposition 1. Choosing, e.g., arbitrary1 as 2 and using Theorem 5 we compute ϕ1

= ˙

x−a<0

ϕ2

= ˙ = ˙

true ∧ ϕ1 [a // ∞] true ∧ true.

For the answer x = 2, we are in case (a), where we only have to compute a suitable αx representing 2. Next, for a = ∞, we are in case (b) and obtain ξ = ˙ true ∧ 2 − a < 0. 15

Using, e.g., the Cauchy bound 1 + max 21 = 3 of a − 2, we replace a = ∞ with the standard answer a = 3 + 1 = 4, which is a root expression. This yields the standard EQR true a=4 x=2 . Choosing, in contrast, arbitrary1 as 3 we obtain the bound 1 + max 31 = 4 and thus true a=5 x=3 . 5. Degree Shifts by Virtual Substitution We have already discussed that the feasibility of the virtual substitution method strongly depends on the degrees of the quantiﬁed variables. Among the heuristics for decreasing these degrees there is an observation, which was essentially made already by Weispfenning (1997a), and which was reﬁned and named degree shift by Dolzmann et al. (1998b). The following lemma restates the result by Dolzmann et al.: Lemma 6 (Degree Shift). Consider a quantiﬁer-free Tarski formula ψ. Let g be the gcd of all exponents of x in ψ. We divide all exponents of x in ψ by g yielding ψ . If g is odd, we have ∃xψ ←→ ∃xψ , if g is even we have ∃xψ ←→ ∃x(x ≥ 0 ∧ ψ ). For g > 1 this reduces the degree of x in ψ. In order to obtain larger gcds and hence a better degree reduction, we may in advance “adjust” the degree n > 0 of x in polynomials of the form xn f , where x does not occur in f as follows: In equations and disequations, n may be equivalently replaced by any m > 0. In ordering inequalities we may choose any m > 0 of the same parity as n. We now want to reanalyze this result as a special case of virtual substitution. For this, we have to slightly generalize the framework by introducing shadow quantiﬁers. Recall that we are considering existential problems of the form ϕ(u1 , . . . , um ) = ∃xn . . . ∃x1 ψ(x1 , . . . , xn , u1 , . . . , um ). As a ﬁrst step we now switch to the equivalent problem ϕ(u ˆ 1 , . . . , um ) = ∃ˆ xn ∃xn . . . ∃ˆ x1 ∃x1 ψ(x1 , . . . , xn , u1 , . . . , um ), ˆn } ∩ {x1 , . . . , xn , u1 , . . . , um } = ∅. That is, the variables x ˆi do where {ˆ x1 , . . . , x not occur in ψ. Consequently, proceeding with the elimination as discussed in Section 3, each shadow quantiﬁer ∃ˆ xi imposes a trivial elimination problem. Strictly following the virtual substitution framework, one would not simply drop those quantiﬁers ∃ˆ xi but eliminate them via trivial elimination sets like {(true, 0)}. Notice that one cannot use ∅ as an elimination set here be cause ∅ = false. Furthermore, from the point of view of extended quantiﬁer ˆn . elimination the use of {(true, 0)} formally provides answers also for x ˆ1 , . . . , x

16

Consider now w.l.o.g. the elimination of ∃x1 , and assume that we are in the situation of Lemma 6, where g > 1 is the gcd of the, possibly adjusted, degrees of x1 in ψ. We use an elimination set that depends on the parity of g: ! E= γ, g x ˆ1 , where γ is x1 ≥ 0 if g is even and “true” otherwise. Of course, we have to deﬁne √ ˆ1 for x1 within ψ: a suitable virtual substitution of g x # $ k k " " max(j,g) j g g aj x1 0 x1 // x ˆ1 = aj x ˆ1 0 , j=1

j=1

where a1 , . . . , ak ∈ Z[x2 , . . . , xn , u1 , . . . , um ] and ∈ {=, =, <, ≤, ≥, >}. The ﬂoor function is applied to make the deﬁnition complete; with our elimination sets we will always have divisibility g | max(j, g). The max operator takes care of possible degree adjustments made for the computation of E. Observe that in contrast to the elimination sets studied so far we introduce here a variable x ˆ1 which was not present in ψ before. That variable is bound by x1 ∃x1 we switch from shadow quantiﬁer ∃ˆ x1 . Intuitively, for the elimination of ∃ˆ one hard plus one trivial elimination step to two nontrivial elimination steps. The termination of quantiﬁer elimination with shadow quantiﬁers follows from the termination of the underlying quantiﬁer elimination method plus the fact that there are only ﬁnitely many shadow quantiﬁers for each regular quantiﬁer. To keep the notation simple, we will in the sequel not formally introduce shadow quantiﬁers for all quantiﬁers. Instead, our procedure will silently assume their presence whenever it performs a degree shift. In the corresponding pre√ ˆi , which cannot EQR this can be recognized by assignments of the form xi = g x come into existence otherwise. 6. Generalizations and Extensions of Our Method In this section we generalize Theorem 5 to admit more general pre-EQRs as input. Furthermore, we discuss heuristics for obtaining rational numbers or even integers instead of root expressions in our standard answers. Corollary 7 (Generalized Computation of Standard Answers). Consider a closed Tarski formula ϕ = ∃xn . . . ∃x1 ψ(x1 , . . . , xn ). Assume that the following is a pre-EQR for ϕ: x1 = e1 ... xn = e n true γ1 ... γn such that each ei is of one of the following forms: (a)

√ a+b c , d

where a, b, c, d ∈ Z[xi+1 , . . . , xn ], 17

(b)

√ a+b c d

± ε, where a, b, c, d ∈ Z[xi+1 , . . . , xn ],

(c) ±∞, √ (d) g xi+1 , where g ∈ N \ {0}, where as usual “±” denotes “+” or “−.” Then we can compute root expressions e1 , . . . , e n each meeting either the speciﬁcation (a) or the speciﬁcation (d) above and γ1 , . . . , γ n such that the following is a pre-EQR for ϕ as well: x1 = e1 ... xn = e true n . γ1 ... γ n √

Proof. From a theoretical point of view, the treatment of ei = a+bd c − ε can be reduced to Theorem 5 via the introduction of artiﬁcial variables as we did for our example in (13) above. From a practical point of view, it is not hard to see how to algorithmically treat such expressions directly. Notice that then our corrected answer ei will generally be a rational number. As already mentioned in the proof of Theorem 5(c), one might heuristically even ﬁnd an integer. In γ = true. both cases the possibly non-trivial guard γi has to be replaced by √ √ i Next, the treatment of a+bd c + ε and −∞ in analogy to a+bd c − ε and ∞, respectively, is straightforward. Finally, having obtained algebraic numbers for xi+1 , . . . , xn , one can com√ pute an algebraic number also for g xi+1 with g ∈ N \ {0}. The proofs for both Theorem 5 and Corollary 7 are constructive. Recall that the ordering of the variables within the given pre-EQR is such that quantiﬁer elimination has taken place from the left to the right, while the construction of the standard answers proceeds from the right to the left. Consider the computation of ek for some ek . Here, the quantiﬁer elimination direction mentioned above has played an important role in our proofs: Although ek+1 , . . . , en have been replaced with e k+1 , . . . , e n , the expression ek is still valid. Taking that idea a bit further, we may replace ek with any valid expression without aﬀecting the validity of either e1 , . . . , ek−1 or e k+1 , . . . , e n. In fact, it is sometimes possible to convert a root expression ek into a rational number or even an integer as follows: Before processing ek , we check whether changing it to one of ek ± ε yields a valid pre-EQR for ϕ as well. This can be done by means of the virtual substitution ( γn ∧ · · · ∧ γ k+1 ∧ γk ∧ · · · ∧ γ1 ∧ ψ) [x1 // e1 ] . . . [xk−1 // ek−1 ][xk // ek ± ε][xk+1 // e k+1 ] . . . [xn // e n ]. In the positive case, we process ek ± ε instead of ek . In terms of the proofs of Theorem 5 and Corollary 7 this leads to the cases (c) and (b), respectively, where we generally obtain rational solutions ek and heuristically even integers. Finally, it is quite helpful in general to recognize rational numbers among all occurring real algebraic numbers. This holds in particular for the ﬁnal αn , 18

. . . , α1 , as they correspond to the values of the back-substituted e n , . . . , e1 , which may be complicated nested root expressions. For this one can use the following lemma. Lemma 8 (Rational Algebraic Numbers). Consider a real algebraic number

a0 , . . . , an ∈ Z, a0 > 0, l, u ∈ Q, l > 0. α = an xn + · · · + a0 , ]l, u[ a , where Assume furthermore that u0 , al0 ∩ Z = {z}. Then α ∈ Q if and only if α = az0 . Proof. Let α ∈ Q. From l > 0 it follows that α > 0, say α = pq , where p, q ∈ Z, p > 0, q > 0. Using the Gaussian Lemma this admits the following factorization for suitable b0 , . . . , bn−1 ∈ Z: n "

ai xi = (qx − p) ·

i=0

n−1 "

bi x i .

i=0

a0 0p It follows that a0 = −b0 p, and we obtain α = −b −b0 q = −b0 q . On the other a0 a0 a0 hand, l < −b0 q < u, which is equivalent to u < −b0 q < l , and it follows that a0 = az0 . The converse implication is obvious. −b0 q = z. Together α = −b 0q

The lemma can be straightforwardly generalized to arbitrary intervals ]l, u[. 7. Implementation and Application Examples We have implemented our method in Redlog, which is a part of the computer algebra system Reduce. Reduce is freely available under a modiﬁed BSD license.2 Technically, our implementation is an extension of Redlog’s extended quantiﬁer elimination rlqea by a switch rlqestdans, which toggles the computation of standard answers. In the following subsections we are going to revisit a number of applications of extended quantiﬁer elimination that have been documented in the scientiﬁc literature. In each case we are going to brieﬂy explain the underlying problem, recompute the solutions with nonstandard answers, and ﬁnally compute solutions with standard answers using our approach as described in this article. Since Redlog is very actively developed and improved, and the considered applications date back up to more than 15 years, the nonstandard answers obtained here partly diﬀer from those reported in the literature. Of course, in such cases both variants are correct. All computations have been carried out with the CSL version of Reduce, revision 2465, using 4 GB RAM on a 2.4 GHz Intel Xeon E5-4640 running 64 bit Debian Linux 7.3. 2 http://reduce-algebra.sourceforge.net

19

7.1. Computational Geometry Besides many standard problems from computational geometry, Sturm and Weispfenning (1997a) consider in their Example 10 the reconstruction of a cuboid wireframe from a photography taken from the origin along the x3 -axis with a lens of focal length 5. The answers obtained by extended quantiﬁer elimination is going to describe vectors e1 , e2 , e3 ∈ R3 generating the cuboid together with a vector v ∈ R3 describing its translation from the origin. The input formula, which contains in addition points i ∈ R2 on the camera sensor, contains 15 quantiﬁers:

∃e1 ∃e2 ∃e3 ∃v∀i (ι ←→ π0 ) ∧ ∃k(59kv = (100, 200, 295k + 295)) . The formula ι (e1 , e2 , e3 , v, i), which has been obtained by regular quantiﬁer elimination earlier, generically describes that a point i lies in the image of a cuboid generated by e1 , e2 , e3 , and translated by v. The formula π0 (i) is a quantiﬁer-free description one concrete image. The remaining part of the

of 200 input formula ﬁxes i = 100 to be the image of the origin of the cuboid. 59 , 59 Extended quantiﬁer elimination yields “true” if and only if π0 is a picture of a cuboid at all. In the positive case, the answers will provide suitable vectors e1 , e2 , e3 , and v. For π0 as considered by Sturm and Weispfenning (1997a) in Example 10, the extended quantiﬁer elimination yields “true” together with the following nonstandard answers: 7∞1 5∞1 −24∞1 , , e2 = ∞1 , 2∞1 , , e1 = 5∞1 , 2 2 5 −109∞1 53∞1 ∞1 59∞1 + 20 e3 = , , , v = 5∞1 , 10∞1 , . 65 26 2 4 Our method ﬁxes ∞1 = 1, which yields the following standard answers: 7 5 24 e1 = 5, , , e2 = 1, 2, − , 2 2 5 79 109 53 1 , , , v = 5, 10, . e3 = − 65 26 2 4 The entire computation takes 189 s, of which the computation of the standard answers takes less than 1 ms. 7.2. Motion Planning Weispfenning (2001) has studied motion planning problems in dimension two. Both the object to be moved and the free space between given obstacles are semilinear sets. Extended quantiﬁer elimination is used to decide whether a geometrical object can be moved from an initial to a ﬁnal destination in at most n moves, where the trajectory of each move is a line segment. In the positive case, the answers describe the coordinates u1 , . . . , un ∈ R2 of the object after 20

Table 1: Summary of nonstandard answers and computation times for motion planning examples considered by Weispfenning (2001).

Example 6.4 6.8 6.9

u1 (5 − ε1 , 5 − ε1 ) (0, 3 + ε1 ) (0, 3 + ε1 )

u2

5 − ε1 , −2ε21 +1 (3 − ε1 , 6)

u3 9 2

9, (7, 6)

(3 − ε1 , 6)

time 0.06 s 9.5 s 0.28 s

Table 2: Summary of standard answers for motion planning examples considered by Weispfenning (2001). In all cases the time spent for the computation of ε1 was less than 1 ms.

Example 6.4 6.8 6.9

ε1 3 16

1 1

u1

77 77 16 , 16 (0, 4) (0, 4)

u2

77 5 16 , 16 (2, 6) (2, 6)

u3 9, 92 (7, 6)

each of the n moves. Accordingly, the input formulas contain 2n variables in the prenex existential block. We have applied our answer correction to three of the examples discussed by Weispfenning (2001). For the concrete input formulas and pictures of the scenery we refer to that publication. For Example 6.4, we obtain the following nonstandard answers: −2ε1 + 1 9 , u3 = 9, . u1 = (5 − ε1 , 5 − ε1 ) , u2 = 5 − ε1 , 2 2 3 Our method ﬁxes ε1 = 16 , which yields the following standard answers: 9 77 77 77 5 u1 = , , , u2 = , u3 = 9, . 16 16 16 16 2

The entire computation takes 60 ms, of which the computation of the standard answers takes less than 1 ms. Tables 1 and 2 summarize these results along with the two other examples. 7.3. Models of Genetic Circuits Recently, symbolic methods for the identiﬁcation of Hopf bifurcations in vector ﬁelds arising from biological networks or chemical reaction networks have received considerable attention in the literature (Sturm and Weber, 2008; Sturm et al., 2009; Errami et al., 2011; Weber et al., 2011; Errami et al., 2013). Given a polynomial vector ﬁeld, El Kahoui and Weber (2000) introduced a method, which automatically generates ﬁrst-order Tarski formulas describing the existence of a Hopf bifurcation in terms of the parameters. Then real quantiﬁer elimination is applied to obtain corresponding necessary and suﬃcient conditions. For eﬃciency reasons, one often existentially quantiﬁes all parameters

21

and applies extended quantiﬁer elimination. In the positive case, the answers provide one set of parameter values giving rise to a Hopf bifurcation. Based on models introduced by Boulier et al. (2007), Sturm and Weber (2008) and Sturm et al. (2009) used the approach sketched above to automatically derive the existence of Hopf bifurcations for the gene regulatory network controlling the circadian clock of a certain unicellular green alga. The input formula is ∃(0 < v1 ∧ 0 < v3 ∧ 0 < v2 ∧ 0 < ϑ ∧ 0 < γ0 ∧ 0 < μ ∧ 0 < δ ∧ 0 < α ∧ ϑ · (γ0 − v1 − v1 v39 ) = 0 ∧ λ1 v1 + γ0 μ − v2 = 0 ∧ 9α(γ0 − v1 − v1 v39 ) + δ(v2 − v3 ) = 0 ∧ 0 < ϑδ + ϑv39 δ + 9λ1 ϑv1 v38 δ ∧ 162ϑv317 αv1 + 162ϑαv1 v38 + 162αv1 v38 δ + ϑ + 2ϑv39 δ + ϑ2 v318 δ + ϑv39 + 2ϑδ + 81αv1 v38 ϑδ + 81αv1 v317 ϑδ + δ 2 + ϑδ 2 + ϑ2 δ + ϑ2 + 2ϑ2 v39 + ϑ2 v318 + 6561α2 v12 v316 + 2ϑ2 v39 δ + δ + 81αv1 v38 + ϑv39 δ 2 − 9λ1 ϑv1 v38 δ = 0), for which we obtain the following nonstandard answers: γ0

=

√ √ √ 8 9 ∞2 19 ∞3 +16 9 ∞2 10 ∞3 +8 9 ∞2 ∞3 , 729∞21 ∞32 +1458∞21 ∞22 +729∞21 ∞2 −486∞1 ∞22 ∞3 −486∞1 ∞2 ∞3 +9∞2 ∞23

μ

=

729∞21 ∞32 +1458∞21 ∞22 +729∞21 ∞2 −486∞1 ∞22 ∞3 −486∞1 ∞2 ∞3 +∞2 ∞23 −8∞23 , 8∞22 ∞3 +16∞2 ∞3 +8∞3

ϑ

=

v1

=

v2

=

−6561∞41 ∞42 −26244∞41 ∞32 −39366∞41 ∞22 −26244∞41 ∞2 −6561∞41 +4374∞31 ∞32 ∞3 +13122∞31 ∞22 ∞3 +13122∞31 ∞2 ∞3 +4374∞31 ∞3 −54∞1 ∞2 ∞33 −54∞1 ∞33 +∞43

6561∞41 ∞52 +32805∞41 ∞42 +65610∞41 ∞32 +65610∞41 ∞22 +32805∞41 ∞2 +6561∞41 −8748∞31 ∞42 ∞3 −34992∞31 ∞32 ∞3 −52488∞31 ∞22 ∞3 −34992∞31 ∞2 ∞3 −8748∞31 ∞3 +3078∞21 ∞32 ∞23 +9234∞21 ∞22 ∞23 +9234∞21 ∞2 ∞23 +3078∞21 ∞23 −108∞1 ∞22 ∞33 −216∞1 ∞2 ∞33 −108∞1 ∞33 +∞2 ∞43 +∞43

,

√ √ 8 9 ∞2 10 ∞3 +8 9 ∞2 ∞3 , 729∞21 ∞32 +1458∞21 ∞22 +729∞21 ∞2 −486∞1 ∞22 ∞3 −486∞1 ∞2 ∞3 +9∞2 ∞23

√ 9

∞2 ,

v3 =

√ 9

∞2 ,

α = ∞1 ,

Our method ﬁxes ∞1 = 1, ∞2 following standard solution: √ 69984800 · 9 9 , μ= γ0 = 616061191401 √ 6998480 · 9 9 v1 = , v2 = 616061191401 α = 1,

δ = 1,

λ1 = ∞3 .

= 9, and ∞3 = 87481, which yields the 3827162521 , 69984800 √ 9

9,

δ = 1,

ϑ= v3 =

7652917261 , 76056937210 √ 9

9,

λ1 = 87481.

The entire computation takes 370 ms, of which the computation of the standard answers takes 140 ms. 22

7.4. Mass Action Systems We are now going to discuss another example about Hopf bifurcation. This time, the considered system is a chemical reaction system, viz. the famous and well-studied phosphofructokinase reaction. It has been ﬁrstly analyzed with symbolic methods by Gatermann et al. (2005, Example 2.1). We adopt here the ﬁrst-order formulation discussed by Sturm and Weber (2008) and Sturm et al. (2009) following the approach sketched in the previous subsection. We obtain nonstandard answers of the following form: k21 = K21 (∞1 , ∞2 , ∞3 , ∞4 , ε1 ), k46 = K46 (∞1 , ∞2 , ∞3 , ∞4 , ∞5 , ε1 ), k56 = K56 (∞1 , ∞2 , ∞3 , ∞4 , ∞5 , ε1 ), v2 = V2 (∞1 , ∞2 , ∞3 , ∞4 , ∞5 , ε1 ),

k34 = ∞1 , k64 = ∞5 , ∞2 ∞4 v1 = , ∞1 v 3 = ∞4 .

k43 = ∞2 , k65 = ∞3 ,

The nonstandard terms K21 , . . . , K56 , V2 are so large that we cannot explicitly display them here. To give an idea, K46 would ﬁll more than 16 pages in this document. √ Our method ﬁxes ∞1 = ∞2 = ∞3 = ∞4 = 1, ∞5 = 20, and ε1 = 2( 2 − 1), which yields the following standard solution: k21 = 3, √

k34 = 1,

k43 = 1,

k46 =

k64 = 20,

k65 = 1,

3457 + 1 , √ 8 − 3457 + 159 , k56 = √ 6 − 3457 + 159 v2 = , 24

v1 = 1, v3 = 1.

The entire computation takes 13.2 s, of which the computation of the standard answers takes 0.1 s. 7.5. Sizing of Electrical Networks Sturm (1999b, Section 5) has applied generic quantiﬁer elimination to the sizing of a BJT ampliﬁer. Description of a circuit is given as a set of operating point equations E1 and a set of AC conditions E2 . For the concrete equations we refer to the mentioned publication. The system E1 ∧ E2 has to be solved w.r.t. the main variables M = {r1 , . . . , r8 , c3 } in terms of parameter variables P = {vcc , ahigh , alow , p, zin , zout }. Fixing values of the parameters to vcc = 3, ahigh = 3, alow = 2, p = 12, zin = 5, zout = 5,

23

the answers contain one nonstandard term: r1 =

4457058395 , 5180672

r4 = −

r2 =

4457058395 , 2590336

4182864929375836679 , 128066211840000

r7 = 5,

r8 =

r3 = −

r5 = ∞1 ,

r6 =

25509595605337086755 , 20836792295619328

4457058395 , 1295168

282999424999 , 804520000

c3 =

647584 . 13371175185

Our method ﬁxes ∞1 = 1, which yields a standard answer for r5 . The entire computation takes less than 2 ms, of which the computation of the standard answer takes less than 1 ms. 7.6. A Linear Feasibility Example Korovin et al. (2009, Section 9) have considered a small linear existential problem to demonstrate the diﬀerence between their conﬂict resolution method and the Fourier–Motzkin elimination method. The following are nonstandard answers for that problem computed by Redlog: x1 = − x4 =

8 , 13

−302 − 195ε1 + 65ε2 , 130

Our method ﬁxes ε1 = answers: x1 = −

8 , 13

1 65

x2 =

1 − 65ε1 , 65

x5 =

−30 + 26ε2 . 39

and ε2 =

x2 = 0,

1 13 ,

x3 = −1,

x3 =

−14 + 13ε2 , 13

which yields the following standard x4 = −

30 , 13

x5 = −

28 . 39

The entire computation takes 3 ms, of which the computation of the standard answers takes less than 1 ms. 8. Conclusions and Future Work We have introduced extended quantiﬁer elimination as a general concept, and focused on virtual substitution as one possible method for its realization. Successful applications of extended quantiﬁer elimination via virtual substitution have been documented in the literature over the past two decades. One problem there was that the answers obtained via virtual substitution in general contain nonstandard symbols, which can be hard to interpret. For ﬁxed parameters the present work resolves this issue by providing a complete post-processing method for ﬁxing all answers to standard real numbers. We have implemented our method, and applied it to various extended quantiﬁer elimination problems from the literature. In these experiments we have generally obtained standard answers that are meaningful in terms of the modeled problems. In most cases 24

our post-processing method does not signiﬁcantly contribute to the overall computation time. Recall from our discussion in Section 6 on ﬁnding integer and rational answers that there is often a considerable degree of freedom in the choice of standard answers. In future this can be further exploited in many interesting ways: For instance, using extended quantiﬁer elimination methods as a theory solver in the context of Satisﬁability Modulo Theory (SMT) solving (Nieuwenhuis et al., 2006), in particular when combining several theories in a Nelson–Oppen (1979) style, one is speciﬁcally interested in avoiding identical answers for diﬀerent variables. Alternatively, one can try to identify certain variables, which might be interesting in certain contexts. As another option, there is only a small step to automatically generating for a given pre-EQR code for an interactive procedure that suggests ranges and ﬁnds possible choices for certain variables in cooperation with the user. In cooperation projects with researchers from the sciences we have had the experience that those researchers often have a surprisingly precise idea about reasonable choices for certain variables. A theoretically way more challenging step would be the generalization of our method to the parametric case. Recall that Proposition 1 has shown that it is not possible in general to determine real standard values for inﬁnitesimals and inﬁnities without ﬁxing values for the parameters beforehand. Nevertheless, it might well be possible to devise on the basis of our work here a complete method for symbolically replacing nonstandard symbols with standard terms. In the example in Proposition 1 the inﬁnitesimal ε1 could be replaced, e.g., with 1−a 2 yielding a standard extended quantiﬁer elimination result. Acknowledgments This research was supported in part by the German Transregional Collaborative Research Center SFB/TR 14 AVACS and by the DFG/ANR Programme Blanc Project STU 483/2-1 SMArT. References Akritas, A.G., 2009. Linear and quadratic complexity bounds on the values of the positive roots of polynomials. Journal of Universal Computer Science 15, 523–537. ¨ upl¨ Boulier, F., Lefranc, M., Lemaire, F., Morant, P.E., Urg¨ u, A., 2007. On proving the absence of oscillations in models of genetic circuits, in: Anai, H., Horimoto, K., Kutsia, T. (Eds.), Proceedings of Algebraic Biology 2007. volume 4545 of LNCS, pp. 66–80. Burhenne, K.D., 1990. Implementierung eines Algorithmus zur Quantorenelimination fur lineare reelle Probleme. Diplomarbeit. Universit¨ at Passau. Germany. Collard, J.F., 2003. Reasoning About Program Transformations. Springer. 25

Dolzmann, A., Gloor, O., Sturm, T., 1998a. Approaches to parallel quantiﬁer elimination, in: Gloor, O. (Ed.), Proceedings of the ISSAC 98. ACM Press, pp. 88–95. Dolzmann, A., Sturm, T., 1997a. Redlog: Computer algebra meets computer logic. ACM SIGSAM Bulletin 31, 2–9. Dolzmann, A., Sturm, T., 1997b. Simpliﬁcation of quantiﬁer-free formulae over ordered ﬁelds. Journal of Symbolic Computation 24, 209–231. Dolzmann, A., Sturm, T., 1999. Redlog User Manual, 2nd Edition. Technical Report MIP-9905. FMI, Universit¨ at Passau. Germany. Dolzmann, A., Sturm, T., Weispfenning, V., 1998b. A new approach for automatic theorem proving in real geometry. Journal of Automated Reasoning 21, 357–380. Dolzmann, A., Sturm, T., Weispfenning, V., 1999. Real quantiﬁer elimination in practice, in: Matzat, B.H., Greuel, G.M., Hiss, G. (Eds.), Algorithmic Algebra and Number Theory. Springer, pp. 221–247. El Kahoui, M., Weber, A., 2000. Deciding Hopf bifurcations by quantiﬁer elimination in a software component architecture. Journal of Symbolic Computation 30, 161–179. Errami, H., Eiswirth, M., Grigoriev, D., Seiler, W.M., Sturm, T., Weber, A., 2013. Eﬃcient methods to compute Hopf bifurcations in chemical reaction networks using reaction coordinates, in: Proceedings of the CASC 2013. volume 8136 of LNCS, pp. 88–99. Errami, H., Eiswirth, M., Grigoriev, D., Seiler, W.M., Sturm, T., Weber, A., 2015. Detection of Hopf bifurcations in chemical reaction networks using convex coordinates. Journal of Computational Physics 291, 279–302. Errami, H., Sturm, T., Weber, A., 2011. Algorithmic aspects of Muldowney’s extension of the Bendixson-Dulac criterion for polynomial vector ﬁelds, in: Vassiliev, N.N. (Ed.), Polynomial Computer Algebra, The Euler International Mathematical Institute, St. Petersburg, Russia. pp. 25–28. Gatermann, K., Eiswirth, M., Sensse, A., 2005. Toric ideals and graph theory to analyze Hopf bifurcations in mass action systems. Journal of Symbolic Computation 40, 1361–1382. Korovin, K., Tsiskaridze, N., Voronkov, A., 2009. Conﬂict resolution, in: Gent, I.P. (Ed.), Principles and Practice of Constraint Programming – CP 2009. volume 5732 of LNCS, pp. 509–523. Lasaruk, A., Sturm, T., 2007. Weak quantiﬁer elimination for the full linear theory of the integers. A uniform generalization of Presburger arithmetic. Applicable Algebra in Engineering, Communication and Computing 18, 545– 574. 26

Loos, R., Weispfenning, V., 1993. Applying linear quantiﬁer elimination. THE Computer Journal 36, 450–462. Nelson, G., Oppen, D.C., 1979. Simpliﬁcation by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1, 245– 257. Nieuwenhuis, R., Oliveras, A., Tinelli, C., 2006. Solving SAT and SAT modulo theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). Journal of the ACM 53, 937–977. Seidl, A.M., Sturm, T., 2003. Boolean quantiﬁcation in a ﬁrst-order context, in: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (Eds.), Computer Algebra in Scientiﬁc Computing. Proceedings of the CASC 2003. Institut f¨ ur Informatik, Technische Universit¨ at M¨ unchen, M¨ unchen, Germany, pp. 329–345. Sturm, T., 1999a. Real Quantiﬁer Elimination in Geometry. Doctoral dissertation. Universit¨ at Passau. Germany. Sturm, T., 1999b. Reasoning over networks by symbolic methods. Applicable Algebra in Engineering, Communication and Computing 10, 79–96. Sturm, T., 2000a. An algebraic approach to oﬀsetting and blending of solids, in: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (Eds.), Computer Algebra in Scientiﬁc Computing. Proceedings of the CASC 2000. Springer, Berlin, pp. 367–382. Sturm, T., 2000b. Linear problems in valued ﬁelds. Journal of Symbolic Computation 30, 207–219. Sturm, T., Tiwari, A., 2011. Veriﬁcation and synthesis using real quantiﬁer elimination, in: Proceedings of the ISSAC 2011. ACM Press, pp. 329–336. Sturm, T., Weber, A., 2008. Investigating generic methods to solve Hopf bifurcation problems in algebraic biology, in: Horimoto, K. (Ed.), Proceedings of Algebraic Biology 2008. volume 5147 of LNCS, pp. 200–215. Sturm, T., Weber, A., Abdel-Rahman, E.O., El Kahoui, M., 2009. Investigating algebraic and logical algorithms to solve Hopf bifurcation problems in algebraic biology. Mathematics in Computer Science 2, 493–515. Sturm, T., Weispfenning, V., 1997a. Computational geometry problems in REDLOG, in: Wang, D. (Ed.), Automated Deduction in Geometry. volume 1360 of LNAI, pp. 58–86. Sturm, T., Weispfenning, V., 1997b. Rounding and blending of solids by a real elimination method, in: Sydow, A. (Ed.), Proceedings of the IMACS 97. Wissenschaft & Technik Verlag, Berlin. volume 2, pp. 727–732.

27

Sturm, T., Weispfenning, V., 2002. Quantiﬁer elimination in term algebras. The case of ﬁnite languages, in: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (Eds.), Computer Algebra in Scientiﬁc Computing. Proceedings of the CASC 2002. Institut f¨ ur Informatik, Technische Universit¨ at M¨ unchen, Garching, Germany, pp. 285–300. Sturm, T., Zengler, C., 2010. Parametric quantiﬁed SAT solving, in: Watt, S.M. (Ed.), Proceedings of the ISSAC 2010. ACM Press, pp. 77–84. Weber, A., Sturm, T., Abdel-Rahman, E.O., 2011. Algorithmic global criteria for excluding oscillations. Bulletin of Mathematical Biology 73, 899–916. Weispfenning, V., 1988. The complexity of linear problems in ﬁelds. Journal of Symbolic Computation 5, 3–27. Weispfenning, V., 1994a. Parametric Linear and Quadratic Optimization by Elimination. Technical Report MIP-9404. Universit¨at Passau. Germany. Weispfenning, V., 1994b. Quantiﬁer elimination for real algebra—the cubic case, in: Proceedings of the ISSAC 1994. ACM Press, pp. 258–263. Weispfenning, V., 1997a. Quantiﬁer elimination for real algebra—the quadratic case and beyond. Applicable Algebra in Engineering Communication and Computing 8, 85–101. Weispfenning, V., 1997b. Simulation and optimization by quantiﬁer elimination. Journal of Symbolic Computation 24, 189–208. Weispfenning, V., 2001. Semilinear motion planning in REDLOG. Applicable Algebra in Engineering, Communication and Computing 12, 455–475.

28