Cylindrical Decomposition for Systems Transcendental in the First Variable

Adam Strzebonski

Wolfram Research Inc.
100 Trade Centre Dr.
Champaign, IL 61820
U.S.A.

adams@wolfram.com
http://members.wolfram.com/adams

Abstract

The CAD algorithm [Collins 1975] is the best currently known algorithm for solving many classes of problems related to systems of real polynomial equations and inequalities. It not only allows elimination of quantifiers, but also provides an explicit description of the solution sets in terms of real algebraic functions.

In [Achatz, McCallum and Weispfenning 2008] the CAD algorithm is extended to solve decision problems for systems of real equations and inequalities that are exponential-polynomial in the first variable and polynomial in the remaining variables. In this talk we take this idea further and show how to compute full cylindrical descriptions of solution sets for systems involving more general functions of the first variable. More precisely, the algorithm presented here applies to systems of equations and inequalities polynomial in x,(Subscript[f, 1])(x),…,(Subscript[f, m])(x),(Subscript[y, 1]),…,(Subscript[y, n]), where (Subscript[f, 1])(x),…,(Subscript[f, m])(x) are real univariate functions continuous in their domains. The algorithm succeeds whenever it can solve a certain set of univariate equations that are polynomial in x,(Subscript[f, 1])(x),…,(Subscript[f, m])(x). In particular, the algorithm applies when there exists a real root isolation algorithm for functions from the algebra ℚ[x,(Subscript[f, 1])(x),…,(Subscript[f, m])(x)], which is the case, for instance, when  (Subscript[f, 1])(x),…,(Subscript[f, m])(x) are real exp-log functions [Strzebonski 2008].

Definitions

A subfield K⊆ℝ is a real computable field iff field operations, comparison and approximation to arbitrary accuracy can be performed algorithmically in K.

A continuous univariate function f:ℝ⊇D(f)→ℝ is finitely solvable over a real computable field K iff:
• D(f)=((Subscript[a, 1]),(Subscript[b, 1]))⋃…⋃((Subscript[a, l]),(Subscript[b, l])),
• (f^(-1))(0)=((Subscript[c, 1]),(Subscript[d, 1]))⋃…⋃((Subscript[c, m]),(Subscript[d, m]))⋃{(Subscript[r, 1]),…,(Subscript[r, n])},
• There is an algorithm which computes (Subscript[a, i]),(Subscript[b, i]),(Subscript[c, j]),(Subscript[d, j]),(Subscript[r, k])∈K⋃{-∞,∞}.

An algebra A of continuous univariate functions is finitely solvable over K iff each element of A is finitely solvable over K.

A formula 

S(x,(Subscript[y, 1]),…,(Subscript[y, n]))=(Underscript[∨, 1≤i≤k])(Underscript[∧, 1≤j≤l])(Subscript[g, i,j])(x,(Subscript[y, 1]),…,(Subscript[y, n]))(Subscript[⋄, i,j])0

where each (Subscript[⋄, i,j]) is one of <, ≤, >, ≥, =, or ≠, is a system of equations and inequalities finitely solvable in x and polynomial in (Subscript[y, 1]),…,(Subscript[y, n]) iff there exist:
• a real computable field K, 
• an algebra A of univariate functions finitely solvable over K, 
• functions (Subscript[f, 1]),…,(Subscript[f, m])∈A,
• polynomials (Subscript[p, i,j])∈ℚ[x,(Subscript[t, 1]),…,(Subscript[t, m]),(Subscript[y, 1]),…,(Subscript[y, n])] such that 
(Subscript[g, i,j])(x,(Subscript[y, 1]),…,(Subscript[y, n]))=(Subscript[p, i,j])(x,(Subscript[f, 1])(x),…,(Subscript[f, m])(x),(Subscript[y, 1]),…,(Subscript[y, n])).

Let F={(Subscript[F, i]):i∈ℕ,(Subscript[F, i])⊆𝒞((ℝ^i),(OverBar[ℝ]))}, where 𝒞((ℝ^i),(OverBar[ℝ])) is the set of continuous functions ϕ:(ℝ^i)⊇D(ϕ)→ℝ⋃{-∞,∞}. Cells with bounds in F are defined recursively as follows:
• A cell in ℝ is a point {r} or an open interval ((Subscript[r, 1]),(Subscript[r, 2])), where r,(Subscript[r, 1]),(Subscript[r, 2])∈(Subscript[F, 0]),
• A cell in (ℝ^(k+1)) has the form
{((Subscript[a, 1]),…,(Subscript[a, k]),(Subscript[a, k+1])):((Subscript[a, 1]),…,(Subscript[a, k]))∈(Subscript[C, k])∧(Subscript[a, k+1])=r((Subscript[a, 1]),…,(Subscript[a, k]))} or
{((Subscript[a, 1]),…,(Subscript[a, k]),(Subscript[a, k+1])):((Subscript[a, 1]),…,(Subscript[a, k]))∈(Subscript[C, k])∧(Subscript[r, 1])((Subscript[a, 1]),…,(Subscript[a, k]))<(Subscript[a, k+1])<(Subscript[r, 2])((Subscript[a, 1]),…,(Subscript[a, k]))}
where (Subscript[C, k]) is a cell in (ℝ^k) and r,(Subscript[r, 1]),(Subscript[r, 2])∈(Subscript[F, k]).

For a polynomial p∈ℚ[(Subscript[x, 1]),…,(Subscript[x, k]),z], let (Subscript[Root, z,k])p((Subscript[x, 1]),…,(Subscript[x, k]),z):(ℝ^k)⊇D→ℝ denote the function which gives the k-th real root of p((Subscript[x, 1]),…,(Subscript[x, k]),z) considered as a univariate polynomial in z (roots are counted with multiplicities). D is the set of points ((Subscript[x, 1]),…,(Subscript[x, k])) for which p has at least k real roots.

Let (Subscript[𝒞, alg])((ℝ^k),(OverBar[ℝ])) denote the set of continuous algebraic functions, i.e. restrictions of functions (Subscript[Root, z,k])p((Subscript[x, 1]),…,(Subscript[x, k]),z) to sets on which the functions are continuous, extended by constant functions -∞ and ∞.

Cylindrical Decomposition Algorithm

Let us use the notation of the MouseOver a system of equations and inequalities finitely solvable in x and polynomial in (Subscript[y, 1]),…,(Subscript[y, n]).

Input: A system S of equations and inequalities finitely solvable in x and polynomial in (Subscript[y, 1]),…,(Subscript[y, n]). 
Output: A decomposition of the solution set of S into a finite union of disjoint cells with bounds in F, where (Subscript[F, 0])⊆K⋃{c:ϕ∈A,ϕ(c)=0}⋃{-∞,∞} and (Subscript[F, i])⊆{α(x,(Subscript[f, 1])(x),…,(Subscript[f, m])(x),(Subscript[y, 1]),…,(Subscript[y, i-1])):α∈(Subscript[𝒞, alg])((ℝ^(m+i)),(OverBar[ℝ]))}.

Outline of the algorithm

• Find the common domain D of  (Subscript[f, 1]),…,(Subscript[f, m]).
• Use the variant of the cylindrical algebraic decomposition algorithm given in [Strzebonski 2006] to find a description of the solution set of the system

S'(x,(Subscript[t, 1]),…,(Subscript[t, m]),(Subscript[y, 1]),…,(Subscript[y, n]))=(Underscript[∨, 1≤i≤k])(Underscript[∧, 1≤j≤l])(Subscript[p, i,j])(x,(Subscript[t, 1]),…,(Subscript[t, m]),(Subscript[y, 1]),…,(Subscript[y, n]))(Subscript[⋄, i,j])0

as a finite number of disjoint cells with bounds in (Subscript[𝒞, alg])((ℝ^k),(OverBar[ℝ])). It suffices to construct only the set C of cells whose projection on ℝ intersects D.
• Let P be the set of all polynomials p(x,(Subscript[t, 1]),…,(Subscript[t, k-1]),z), with 1≤k≤m, such that (Subscript[Root, z,s])p appears in the description of C.
• Set F:={p(x,(Subscript[f, 1])(x),…,(Subscript[f, k])(x)):p∈P}⊆A.
• Let (Subscript[C, 1]) be the set of projections of elements of C on ℝ, and let U:=(⋃_((Subscript[c, 1])∈(Subscript[C, 1])))(Subscript[c, 1])⋂D. Find the set R of all distinct roots of elements of F in U.
• Let (Subscript[C, R]) be a decomposition of U into disjoint open intervals and points consistent with R and (Subscript[C, 1]), i.e. if (a,b)∈(Subscript[C, R]) then (a,b)⊆(Subscript[c, 1]) for some (Subscript[c, 1])∈(Subscript[C, 1]) and (a,b)⋂R=∅. Let C':={c⋂((Subscript[c, R])×(ℝ^(m+n))):c∈C∧(Subscript[c, R])∈(Subscript[C, R])}.
• Replace (Subscript[t, 1]),…,(Subscript[t, m]) with (Subscript[f, 1])(x),…,(Subscript[f, m])(x) in equations and inequalities describing the elements of C'. Note that each of the obtained equations and inequalities of the form
(Subscript[f, k])(x)⋄(Subscript[Root, z,s])p(x,(Subscript[f, 1])(x),…,(Subscript[f, k-1])(x),z)				(1)
where each ⋄ is one of <, ≤, >, ≥, =, or ≠, is either always true or always false on each element of (Subscript[C, R]). Replace all such equations and inequalities with their truth values. Computing the truth values does not require zero testing for nonalgebraic elements of K. [Let c'=c⋂((Subscript[c, R])×(ℝ^(m+n))) and let a be a sample point in (Subscript[c, R]). From the construction of (Subscript[C, R]) we know whether a is a root of p(x,(Subscript[f, 1])(x),…,(Subscript[f, k])(x)). From the construction of C we know the real root structure of p on c. Using methods of [Strzebonski 2006] we can then find arbitrarily accurate validated approximations of (Subscript[Root, z,s])p(a,(Subscript[f, 1])(a),…,(Subscript[f, k-1])(a),z). This, combined with the knowledge of whether (Subscript[f, k])(a) is equal to one of the roots of p allows to decide the truth value of (1).]
• Return the cell descriptions that did not reduce to false.

As shown in [Strzebonski 2008], exp-log functions form a finitely solvable algebra over the field of real elementary constants, hence the algorithm applies to systems of equations and inequalities exp-log in x and polynomial in (Subscript[y, 1]),…,(Subscript[y, n]). (The zero testing algorithm for elementary constants relies on Schanuel' s conjecture for proof of termination.)

Example

Find a cylindrical decomposition for (e^x) (y^3)+y log(x)>3x.

(Subscript[f, 1])=E^x;
(Subscript[f, 2])=Log[x];

Find a common domain of (Subscript[f, 1]) and (Subscript[f, 2]).

𝔇=Reduce[Element[(Subscript[f, 1])|(Subscript[f, 2]),Reals],x,Reals]

Find a cylindrical algebraic decomposition of S'(x,(Subscript[t, 1]),(Subscript[t, 2]),y)=(Subscript[t, 1])(y^3)+(Subscript[t, 2])y>3x with x restricted to 𝔇.

ℭ=CylindricalDecomposition[(Subscript[t, 1])(y^3)+(Subscript[t, 2])y>3x&&𝔇,{x,(Subscript[t, 1]),(Subscript[t, 2]),y}]

Find bounds on (Subscript[t, 1]) and (Subscript[t, 2]).

t1bds=Cases[ℭ,(Less|LessEqual|Greater|GreaterEqual)[(Subscript[t, 1]),b_]->b,∞]//Union

t2bds=Cases[ℭ,(Less|LessEqual|Greater|GreaterEqual)[(Subscript[t, 2]),b_]->b,∞]//Union

Set F:={p(x,(Subscript[f, 1])(x),…,(Subscript[f, k])(x)):p∈P}⊆A.

F={(Subscript[t, 1]),(Subscript[t, 2]),4 ((#1)^3)+243 (x^2) (Subscript[t, 1])&[(Subscript[t, 2])]}/.{(Subscript[t, 1])->(Subscript[f, 1]),(Subscript[t, 2])->(Subscript[f, 2])}

Find roots of F in U=𝔇.

red=Reduce[Or@@Thread[F==0]&&𝔇,x,Reals]

r=red[[2,2]]

Let (Subscript[ℭ, R])={(0,r),{r},(r,1),{1},(1,∞)} be a decomposition of U into disjoint open intervals and points consistent with R={r,1} and (Subscript[ℭ, 1])=U.

Let ℭ':={c⋂((Subscript[c, R])×(ℝ^(m+n))):c∈ℭ∧(Subscript[c, R])∈(Subscript[ℭ, R])}. ℭ has the form x>0∧Φ , hence the description of ℭ' has the form (0<x<r∧Φ)∨(x=r∧Φ)∨(r<x<1∧Φ)∨(x=1∧Φ)∨(x>1∧Φ).

Replace (Subscript[t, 1]),…,(Subscript[t, m]) with (Subscript[f, 1])(x),…,(Subscript[f, m])(x) in equations and inequalities describing the elements of C'.

Ψ=ℭ[[2]]/.{(Subscript[t, 1])->(Subscript[f, 1]),(Subscript[t, 2])->(Subscript[f, 2])}

Find equations and inequalities in Ψ that depend only on x.

(Subscript[Ψ, x])=Select[Union[Flatten[Ψ/.{And->List,Or->List}]],FreeQ[#,y]&]

Evaluate (Subscript[Ψ, x]) for x∈(0,r):

(Subscript[Ψ, 1])=(Subscript[Ψ, x])/.x->1/10

The first term of the answer.

(Subscript[ans, 1])=0<x<r&&(Ψ/.Thread[(Subscript[Ψ, x])->(Subscript[Ψ, 1])])

Evaluate (Subscript[Ψ, x]) for x=r. [For simplicity, we use a numeric approximation here. The  actual implementation of the algorithm uses an exact method described in the previous slide.]

(Subscript[Ψ, 2])=(Subscript[Ψ, x])/.x->N[r,100]

The second term of the answer.

(Subscript[ans, 2])=x==r&&(Ψ/.Thread[(Subscript[Ψ, x])->(Subscript[Ψ, 2])])

Evaluate (Subscript[Ψ, x]) for x∈(r,1):

(Subscript[Ψ, 3])=(Subscript[Ψ, x])/.x->1/2

The third term of the answer.

(Subscript[ans, 3])=r<x<1&&(Ψ/.Thread[(Subscript[Ψ, x])->(Subscript[Ψ, 3])])

Evaluate (Subscript[Ψ, x]) for x=1:

(Subscript[Ψ, 4])=(Subscript[Ψ, x])/.x->1

The fourth term of the answer.

(Subscript[ans, 4])=x==1&&(Ψ/.Thread[(Subscript[Ψ, x])->(Subscript[Ψ, 4])])

Evaluate (Subscript[Ψ, x]) for x∈(1,∞):

(Subscript[Ψ, 5])=(Subscript[Ψ, x])/.x->2

The fifth term of the answer.

(Subscript[ans, 5])=x>1&&(Ψ/.Thread[(Subscript[Ψ, x])->(Subscript[Ψ, 5])])

Full answer.

ans=(Subscript[ans, 1])||(Subscript[ans, 2])||(Subscript[ans, 3])||(Subscript[ans, 4])||(Subscript[ans, 5])

The answer using the built-in implementation of the algorithm. It is easy to see that the answers are equivalent.

Reduce[E^x y^3+Log[x]y>3x, {x,y},Reals]

Examples: Quantified exp-log formulas

Reduce[(Subscript[∀, b])(Subscript[∃, a])(a^2) (x^3)==Exp[x]+a (b^2) ((x^2)-1),{x},Reals]

Reduce[(Subscript[∃, a])a (x^3)==Exp[x]+(a^2),{x},Reals]

Reduce[(Subscript[∃, a])(a (x^2)+Sinh[(x^2)+1] (a^2)-1≥0&&(x^2)+(a^2)≤1),x,Reals]

More examples

Reduce[Sin[x-Cos[x]] (y^3)-x==1&&(x^2)+(y^2)≤1,{x,y},Reals]

Reduce[(y^3)-Cos[x] y+2 (x^2) Sin[(x^2)-1]>0&&(x^2)+((Cos[x])^2)≤2,{x,y},Reals]

Reduce[Erf[x-Cos[x+1]] (y^2)-x y z==1&&(x^2)+(y^2)+(z^2)≤3,{x,y,z},Reals]

Reduce[(y^4)-Gamma[x+2] y-y-3 ArcSin[(x/3)]>-2&&(1/2)<x<(5/2),{x,y},Reals]