Better answers to real questions

Better answers to real questions

Accepted Manuscript Better answers to real questions Marek Košta, Thomas Sturm, Andreas Dolzmann PII: DOI: Reference: S0747-7171(15)00071-1 http://...

425KB Sizes 2 Downloads 18 Views

Accepted Manuscript Better answers to real questions

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 quantifier elimination generalizes the concept of regular quantifier elimination by providing in addition answers, which are descriptions of possible assignments for the quantified variables. Implementations of extended quantifier 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 infinitesimal and infinite numbers, which are hard to interpret in practice. We introduce here a post-processing procedure to convert, for fixed 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 significantly improves the quality of the results.

1. Introduction We consider existential problems over the reals. Extended quantifier elimination generalizes the concept of regular quantifier elimination by providing in addition answers, which are descriptions of possible assignments for the quantified variables (Weispfenning, 1994a, 1997b). Implementations of extended quantifier 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 infinitesimal and infinite 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 fixed 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 quantifier elimination problems from the scientific 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 quantifier elimination. In Section 3 we give an introduction of virtual substitution for extended quantifier elimination for the quadratic case to the extent necessary to understand how nonstandard values enter the answers and what information is available for fixing 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 quantified 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 quantifier 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 scientific literature where the application of extended quantifier elimination to various problems from planning, modeling, science, and engineering had yielded nonstandard answers. In all cases we can efficiently fix 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 significantly 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 Quantifier 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 first-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 quantifier elimination applied to ϕ yields an extended quantifier 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 quantifier-free Tarski formulas such that R |= ϕ ←→ k k i=1 βi . In other words, i=1 βi is a regular quantifier elimination result for ϕ, and extended quantifier elimination generalizes regular quantifier 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 quantifier 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 quantifier elimination result we can derive a regular quantifier elimination result (a = 0 ∧ 4a + 3 ≥ 0) ∨ (a ≤ 0 ∧ 3a2 − 3a − 4 ≤ 0), which can be simplified 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 quantifier elimination result, the first 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 first 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 first 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 different 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 first row happen to work as well. This shows that the conditions are sufficient but not necessary for the answers to be valid. 3

Although we are focusing on the reals here, it is noteworthy that extended quantifier elimination is an established concept, which exists also for a variety of other important algebraic theories including the linear theory of valued fields (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 finite 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 quantified variable x via a virtual substitution [x // e]. The γ are quantifier-free Tarski formulas serving as substitution guards. Equation (1) formally describes regular quantifier elimination of one quantifier ∃x from ϕ. For the elimination of several quantifiers, one assumes without loss of generality that the formula is prenex and processes the prenex quantifier 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 sufficiently precise to understand our main contribution here. For a more thorough introduction into the theory of quantifier 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 quantifier elimination from the virtual substitution procedure. Later, in Section 3.2, we generalize to formulas containing also strict inequalities. While with regular quantifier elimination the techniques used in the course of the generalization to strict inequalities remain completely transparent to the user, with extended quantifier 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 fixed 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 fixed 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 finite 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 quantifier-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 quantifier-free L-formulas: [x // t] : atomic L-formulas → quantifier-free L-formulas Note that when there is more than one quantifier, it is crucial to obtain Lformulas in (1) in order to be able to proceed with the respective next quantifier. 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 first-order symbol “=.”

5

Let us now apply these ideas to derive an extended quantifier elimination procedure for several existential quantifiers 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 simplification 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 quantifier from ∃xψ(x, u). Recall from the beginning of the previous Section 3.1 how we considered fixed interpretation u = a ∈ Rm causing the set S = { c ∈ R | R |= ψ(c, a) } to be a finite 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 infinitesimal number, i.e., 0 < ε < x for all 0 < x ∈ R. Then for a strict constraint as defined in (4) we use four test points √ −fi1 ± Δi ± ε. 2fi2 As an optimization, it suffices 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 quantifier 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 quantifier 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 first, 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 definitions 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 final 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 quantifier 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 fixed real interpretations of the parameter a there are positive real choices for ε1 , ε2 so that the answers satisfy ψ. Infinitesimals introduced at different stages of the elimination are indexed accordingly. It is noteworthy that they have to be chosen differently in general: Fixing a = −2 in the example, it is easy to see that ε1 has to be chosen different 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 quantifier elimination were left alone with results as in (7) and the corresponding difficulties. Nevertheless, there is a considerable record of applications of extended quantifier 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 unfixed parameters it is not possible in general to determine suitable real choices for nonstandard symbols: Proposition 1 (No Standard Answers for Unfixed Parameters). Consider the formula ϕ = ∃x(a < x < 1) and the nonstandard extended quantifier elimination result   x = 1 − ε1 a<1 .   a<1 x = 1 − ε1 There is no standard choice ε1 ∈ R such that is an extended quantifier elimination result for ϕ as well. Proof. Assume for a contradiction that ε1 ∈ R is a suitable choice. Then by definition of extended quantifier 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 quantifier 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 fixing 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 difference whether the parameters are fixed after extended quantifier 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 quantifier elimination result is “false,” then the extended quantifier elimination result is [ ], i.e., empty. If the result is “true,” then we assume for simplicity that the extended quantifier 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 first-order logic, there is a real closed field R∗ where the interpretation of ε is a positive infinitesimal and ∞ = ε−1 . The L-restriction of R∗ is a proper extension field 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 finite 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 finite union of intervals and points. Hence there is a0 ∈ R, such that ]a0 , ∞[ ⊆ T . Lemma 3. Consider a quantifier-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 defined and an arbitrary but fixed 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 quantifier-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 quantifier-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 specification (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 defining polynomials and open isolating intervals with rational bounds. Given k ∈ {1, . . . , n}, it suffices 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 . Define ϕ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 definitions it is sufficient 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 define furthermore ξ(xk , . . . , xn ) ξ  (xk )

=

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

=

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

Lemma 3 applied to the quantifier-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  sufficiently 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 finitely many refinements 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 find 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 quantifier elimination results ϕk . In practice, there are arguments for saving these ϕk during the extended quantifier elimination run. Consider, e.g., the following common optimization: Whenever some ϕk heuristically simplifies 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 infinitesimals occur only in expressions of the form xi = xi+1 − ε we introduce an artificial 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 first step is fixing 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 Refining the isolating interval ]−1, 1[ of αh to ]− 32 , 32 [ we find 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 Refining the isolating interval ]− 16 , 16 [ of αx to ]− 256 , 256 [ we find 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 final 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 quantifier 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 quantifier elimination express using EQRs like:   true a=∞ x = arbitrary1 . For applying Theorem 5 such arbitrary variables have to be replaced with arbitrary but fixed 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 quantified variables. Among the heuristics for decreasing these degrees there is an observation, which was essentially made already by Weispfenning (1997a), and which was refined 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 quantifier-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 quantifiers. Recall that we are considering existential problems of the form ϕ(u1 , . . . , um ) = ∃xn . . . ∃x1 ψ(x1 , . . . , xn , u1 , . . . , um ). As a first 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 quantifier ∃ˆ xi imposes a trivial elimination problem. Strictly following the virtual substitution framework, one would not simply drop those quantifiers ∃ˆ 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 quantifier ˆ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 define √ ˆ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 floor function is applied to make the definition 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 quantifier ∃ˆ x1 . Intuitively, for the elimination of ∃ˆ one hard plus one trivial elimination step to two nontrivial elimination steps. The termination of quantifier elimination with shadow quantifiers follows from the termination of the underlying quantifier elimination method plus the fact that there are only finitely many shadow quantifiers for each regular quantifier. To keep the notation simple, we will in the sequel not formally introduce shadow quantifiers for all quantifiers. 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 specification (a) or the specification (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 artificial 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 find 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 quantifier 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 quantifier 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 affecting 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 final α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 modified BSD license.2 Technically, our implementation is an extension of Redlog’s extended quantifier 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 quantifier elimination that have been documented in the scientific literature. In each case we are going to briefly explain the underlying problem, recompute the solutions with nonstandard answers, and finally 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 differ 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 quantifier 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 quantifiers:

∃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 quantifier 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 quantifier-free description one concrete image. The remaining part of the

of 200 input formula fixes i = 100 to be the image of the origin of the cuboid. 59 , 59 Extended quantifier 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 quantifier 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 fixes ∞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 quantifier elimination is used to decide whether a geometrical object can be moved from an initial to a final 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 fixes ε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 identification of Hopf bifurcations in vector fields 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 field, El Kahoui and Weber (2000) introduced a method, which automatically generates first-order Tarski formulas describing the existence of a Hopf bifurcation in terms of the parameters. Then real quantifier elimination is applied to obtain corresponding necessary and sufficient conditions. For efficiency reasons, one often existentially quantifies all parameters

21

and applies extended quantifier 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 fixes ∞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 firstly analyzed with symbolic methods by Gatermann et al. (2005, Example 2.1). We adopt here the first-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 fill more than 16 pages in this document. √ Our method fixes ∞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 quantifier elimination to the sizing of a BJT amplifier. 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 fixes ∞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 difference between their conflict 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 fixes ε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 quantifier elimination as a general concept, and focused on virtual substitution as one possible method for its realization. Successful applications of extended quantifier 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 fixed parameters the present work resolves this issue by providing a complete post-processing method for fixing all answers to standard real numbers. We have implemented our method, and applied it to various extended quantifier 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 significantly contribute to the overall computation time. Recall from our discussion in Section 6 on finding 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 quantifier elimination methods as a theory solver in the context of Satisfiability Modulo Theory (SMT) solving (Nieuwenhuis et al., 2006), in particular when combining several theories in a Nelson–Oppen (1979) style, one is specifically interested in avoiding identical answers for different 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 finds 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 infinitesimals and infinities without fixing 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 infinitesimal ε1 could be replaced, e.g., with 1−a 2 yielding a standard extended quantifier 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 quantifier 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. Simplification of quantifier-free formulae over ordered fields. 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 quantifier 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 quantifier 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. Efficient 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 fields, 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. Conflict 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 quantifier 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 quantifier elimination. THE Computer Journal 36, 450–462. Nelson, G., Oppen, D.C., 1979. Simplification 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 quantification in a first-order context, in: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (Eds.), Computer Algebra in Scientific 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 Quantifier 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 offsetting and blending of solids, in: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (Eds.), Computer Algebra in Scientific Computing. Proceedings of the CASC 2000. Springer, Berlin, pp. 367–382. Sturm, T., 2000b. Linear problems in valued fields. Journal of Symbolic Computation 30, 207–219. Sturm, T., Tiwari, A., 2011. Verification and synthesis using real quantifier 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. Quantifier elimination in term algebras. The case of finite languages, in: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (Eds.), Computer Algebra in Scientific 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 quantified 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 fields. 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. Quantifier elimination for real algebra—the cubic case, in: Proceedings of the ISSAC 1994. ACM Press, pp. 258–263. Weispfenning, V., 1997a. Quantifier 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 quantifier 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