Deciding Linear-Trigonometric Problems (Theory and Application in Computer Algebra)

(1)

Deciding

Linear-Trigonometric

Problems

FUJITSU LABORATORIES LTD

穴井

宏和

(Hirokazu

ANAI)

$*$

universit\"at

$\mathrm{P}\mathrm{a}\mathrm{S}\mathrm{S}\mathrm{a}\mathrm{u}$

Volker WEISPFENNING\dagger

Abstract

In thispaper, wepresentadecision procedure forcertainlinear-trigonometric problems for the reals andintegersformalizedinasuitable first-order language. Theinputs arerestrictedto formulas,

whereall butoneofthequantified variablesoccurlinearly andat mostoneoccursbothlinearlyand

in a specific trigonometric function. Moreoverwe allow in addition the integer-part operation in formulas. Besides ordinary quantifiers, we allow also countingquantifiers. Furthermore we also determine the qualitativestructureof the connectedcomponentsofthesatisfactionsetofthemixed linear-trigonometric variable. We alsoconsiderthedecision ofthese problems in subfields ofthe

real algebraic numbers.

1 Introduction

Decision and quantifier elimination methods for the real numbers as ordered field have a

large variety of applications in mathematics, computer science, and industrial engineering (see

$e.g$. $[3,25])$. In particular, many engineering and industrial applications

can

be reduced to the

QEproblems containingtrigonometricfunctions(see [9, 6]).

Unfortunately, the general first-order theory of the real numbers with sine or cosine and

the constant $\pi$ is undecidable: this is because the zeros of sine function are exactly the integer

multiples of$\pi$. As a consequence one can code Hilbert’s tenth problem in existential formulas

$\mathrm{i}\mathrm{n}\mathrm{v}\mathrm{o}]\mathrm{v}\mathrm{i}\mathrm{n}\mathrm{g}+,$

$-,$$\cdot$, the sinefunction andtheconstants $0,1,$$\pi$ (compare [13]). In fact as remarked

already in [19] even the first-order theory ofthe real numbers with sine (without the constant

$\pi)$ is undecidable, since one can code the first-order theory ofrational numbers in this theory

by representing rational numbers as quotients of arbitrary

zeros

of the sine function. In the

special case, where the quantified variables of the given formula split into purely polynomial

ones

andpurelytrigonometric

ones

the decisionproblemand the quantifiereliminationproblem

can

be reducedto the theory of real numbers as ordered field. It suffices to replace for apurely

trigonometricvariable$x$theterms $\sin(x)$ and$\cos(x)$ bynewvariables $u,$$v$, respectively, with the

additional relation $u^{2}+v^{2}=1$ _{(compare [7,}4,_5]). Theintroduction oftwo

new

variables inplace

of

one

trigonometric variables creates, however, serious problems in practical computational

complexity. A

more

efficient alternative

was

_proposed,

by Pau et al.; it adapts Collins’ CAD

*[email protected]

(2)

method [2] to the trigonometric case [12]. And trigonometric problems of special types have

been studied byD.Richardson by avariety of approaches [14, 15, 16, 17].

Here we consider the decision problem for a fragment of the full first-order theory of the

reals

as

ordered field with

one

specific trigonometric function. In contrast to the special case,

wherequantified variables

are

separated into polynomial and trigonometric variables,

we

allow

one

mixedquantified variable$x$ occurringboth in the trigonometric functionand in linear

poly-nomials. All other quantified variables $x_{i}$ may

occur

only linearly. Parameters

may occur

in

arbitrary degree. We

assume moreover

that the mixed variable $x$ is quantified last (i.e.

outer-most) inthegiven formula. Closed formulas of this restrictedtype

are

called normal. Wepresent

an decision procedure for normal formulas. The procedurehas certain parallels in its approach

tothe decision procedure for linear-exponential problems announced in [26]. In fact bya simple

coding trickwe could also allow awhole block of quantifierswith respect to mixed variables in

place of

a

single mixedvariable.

Both extend also to the mixed real-integer case, $i.e$, to formulas, where terms may involve

the integer-part operation and henceimplicitly quantifiers

over

the integers. Our resultsmay be

viewed

as

afirst step towards decidable classes ofproblemswith mixed algebraic-trigonometric

real andintegervariables thataremotivatedbythe study ofcontroltheoryofhybridsystems [8].

The proofs involve real and mixedreal-integerlinear quantifier elimination [21, 23, 10, 27],

elementary analysis, the idea of checking the real satisfiability of formulas by finitely many

symbolic test points, and Lindemann’s theorem from transcendental number theory in orderto

decide relations between constant terms. In contrast to the purely linear

case

considered in

$[10, 27]$ the_testpointsconsideredherehaveno straightforward mathematicalrepresentation. We

inventasymbolic notationforthem,and show,howto sortthesepoints intheirnatural order,and

how to evaluate the sign of other terms at these symbolically represented points in an indirect

manner.

We also solve the decision problem for normal formulas, where quantifiers range

over

an

arbitrary subfield$F$of the field of real algebraic numbers. In contrast topurely linearproblems,

mixed linear-trigonometric problems mayhave different truth values overthe reals and over$F$.

Besides ordinary quantifiers, we mayalso allowcounting quantifiers.

In contrast to the general decision procedure for the first order theory of the reals as

ex-ponential field that relies on Schanuel’s conjecture [11], we require no open conjecture from

transcendence theory. Instead we use only Lindemann’s theorem and the transcendency of$\pi$ in

orderto decide relations betweenconstants.

Theclassicaltheorem of Lindemann(see [18],page 70)asserts that the values of thecomplex

exponential functionfor

non-zero

complex algebraic arguments

are

transcendental. As

a

conse-quence acorresponding assertion holds forreal trigonometric functions

as

well. This is seen

as

follows: Call areal orcomplex function $f(z)$ is stronglytranscendental(withexceptional point

$p)$ if for all real

or

complex numbers $(z\neq p)$ it is not the case thatboth $z$ and $f(z)$ are

alge-braic. Then by Lindemann’s theorem $e^{z}$ is strongly transcendental with exceptionalpoint $0$. As

an immediate consequence we see that the real logarithm $\ln(x)$ is strongly transcendental with

exceptionalpoint 1.

Next weclaim that the real sinus and cosinus functions are stronglytranscendental with

ex-ceptional point $0$. Indeed $e^{ix}=\cos(x)+i\sin(x)$ and $\cos^{2}(x)+\sin^{2}(X)=1$. So if _$\cos(x)$

is algebraic, then by the second equation $\sin(x)$ is algebraic; since $i$ is algebraic, this implies

that $i\sin(x)$, and hence $e^{ix}$ is algebraic. By Lindemann’s theorem this implies that _$ix$, and

(3)

$\arcsin(X)$

are

also strongly transcendental with exceptionalpoint 1 and $0$, respectively. In order

to

see

that the real tangent function is strongly transcendental with exceptionalpoint $0$,

we

use

thewell-known formula forthe arcustangent: $\arctan(x)=-\frac{i}{2}\ln(\frac{1+ix}{1-ix})$. It shows thatfor

alge-braic $x\neq 0\arctan(X)$ is transcendental. As

a

consequence $\arctan(x)$ and$tan(X)$

are

strongly

transcendental with exceptional point $0$. In a similar way

one

sees that the real arcuscotangent

function and hencethe real cotangent function are strongly transcendental without exceptional

point.

2 The

formal framework

Let $F$ be an arbitrary subfield $F$ of the field of real algebraic numbers. We consider the

following fragment $L$ ofa first-order language for the real numbers. Let $x$ be a distinguished

variable. Lineartermsareexpressions of the form $s:=cx+ \sum_{i=1}^{n}C_{i}X_{i}+c_{0}$with$c;c_{i}\in F$. The

trigonometric term is

an

expressions of the form $t:=trig(ax+b)$, where trig denotes a real

trigonometric function sine, cosine or tangent, and $a(\neq 0),$ $b$ are fixed elements of$F$. Atomic

formulas are equations or inequalities of the form $s=0,$ $s=t,$$s<t,$$t<s$, where $s$ is a

lineartermand$t$isantrigonometricterm. Arbitraryformulas

are

obtained fromatomic formulas

as usual in first order logic, $i.e$. by iterated application ofthe propositional operations $\mathrm{A},$ $,$$\neg$

andquantifiers $\exists x,$$\exists x_{i},$$\forall X,$ $\forall x_{i}$ with respectto the variable_$x$

or

to

some

$x_{i}$. Every formula can

be rewritten equivalently in prenex normal form. If all

occurrences

of $x$ in a formula $\varphi$ are

quantified, then $\varphi$ is a closed

formula.

In the natural interpretation of formulas over the real

numbers,_every closed formula is eithertrue orfalse. We call aclosed formula $\varphi$ normal ifit is

prenexand either doesnotcontainthevariable$x$orthe quantifier$\exists x$or$\forall x$binding_$x$isoutermost

in theprefix of$\varphi$. Ourgoal is a decision procedure for normal formulas in $L$ i.e. an algorithm

that takes normal formulas in $L$ as inputs and Output the truth value ofthe input formula over

the reals. This goal is analogoustothat in [22] foralmost linearinteger problems.

In fact we could allow in normal formulas a whole block of quantifiers referring to mixed

variables, say$y_{1},$ $\ldots$

,

$y_{m}$ in placeofasingle mixedvariable$x$. Thentrigonometric terms would

beoftheform trig$(a_{0}+a_{1}y_{1}+.. . a_{m}y_{m})$ forfixedreal constants$a_{0},$

. .

${ }$ ,$a_{m}$. Suchaformula

$\exists y_{1}\ldots\exists ymQ1x_{1}\ldots Qnxn(\psi)$ witharbitrary quantifiers $Q_{i}$ canbe equivalently replacedby the

followingnormalformula

$\exists x\exists y_{1}\ldots\exists y_{m}Q_{1}X1\cdots Qn^{X}n$($x=a_{0}+a_{1}y_{1}+\ldots a_{m}y_{m}$ A $\psi’$),

where$\psi’$ results from$\psi$by replacingeach

occurence

oftrig$(a0+a_{1}y_{1}+\ldots a_{m}y_{m})$ by trig_$(x)$.

In fact we will consider also formulas in an extended sense, where we admit besides the

“ordinary” quantifiers $\exists,$$\forall$alsothe“counting quantifiers” $\exists\leq n,$$\exists^{n},$$\exists\geq n,$ $\exists\leq\infty,$$\exists^{\infty}$ interpreted

as

“thereexistatmost $n$, exactly$n$,atleast$n$, only finitely

many,

infinitely many”, respectively for

$n\in \mathrm{N}$. Formulas,closedformulas, normalformulasinthis extended

sense

willbe referredtoas

formulas,closed formulas, normalformulas with countingquantifiers. Notice thatthe first three

types ofcountingquantifiers are definable using ordinary quantifiers, while the lasttwo are not

definable in this way.

Let $\varphi:=Qx(\psi(x))$ be a normal formula ($Q$ a quantifier $\exists$ or $\forall$). Let

$\psi_{1}$ result from $\psi$

by replacing the trigonometric term trig$(ax+b)$ by a

new

variable $z$. Then $\psi_{1}$ is a linear

formula in the

sense

of $[21, 10]$. So by linear _real _quantifier elimination, $\psi_{1}$ is equivalent to a

(4)

$\psi_{2}$ bybacksubstitution of the trigonometric term $t=trig(ax+b)$ for _$z$. Then _{$\varphi’:=Qx(\psi_{3})$}

is

a

normal formula with only

one

quantifierthat is equivalent to $\varphi$. Notice that rational linear

combinations oftrigonometric terms can be rewritten as arational multiple of a trigonometric

term. Sobydividing byrational constants theatomic formulas of$\varphi’$ canassumedtobe normal.

For normal formulas with counting quantifiers one can argue similarly, using linear

elimi-nation by test points. So for example

a

counting quantifier $\exists^{\infty}x_{i}(\sigma(X_{i}))$

can

be eliminated by

restrictingthe disjunction

over

testtermsused forthe elimination of the quantifier $\exists x_{i}(\sigma(X_{i}))$ to

test terms of the form $s\pm\epsilon$, where $s$is alinearterm.

So the problem of deciding the truth value of normal formulas is reduced to normal input

formulas of the form $Qx(\psi)$, where $\psi$ is quantifier-free. Moreover by passing to the negation

-ifnecessary-we may

assume

that $Q$ is an existential quantifier. So it suffices to decide such

univariatenormal formulaswith a single existential quantifier $\exists x$

over

the reals. In factwe will

do

more:

Incase thetruth value of$\exists x(\psi)$ is ‘true’,

we

will provide a sample point $r\in \mathbb{R}$for $x$.

In fact if$M$ isthe set of reals satisfying $\psi(x)$, then we will determine the numberofconnected

components of$M$ and their types as anon-empty intervals $[b, c],$$(b, c),$ $[b, c)$ or $(b, c]$.

As a consequence we canalso inan obviousway decidea univariatenormal formula$Qx(\psi)$

with quantifier-free$\psi$, where$Q$ isacounting quantifier.

3 Geometric

properties of

trigonometric

functions

and

straight

lines

In ordertostudy the solutions ofequationsandinequalitiesbetweenstraightlines and

trigono-metric functions,we nowconsiderfunctionsof the type$f(x)=trig(x)-(cx+d)$,andfocus

on

the caseoftrig$(x)=\cos(x)$ or trig$(x)=\sin(x)$_. _{In the}_following, we _only _{deal with} _the

case

of$\cos(x)$ because thecase of$\sin(x)$ is very analogous tothat of$\cos(x)$. Let the basic intervals

for be $\mathcal{I}_{n}:=(-\frac{\pi}{2}+n\pi, -\frac{\pi}{2}+(n+1)\pi)$ for $n\in$ N. For any straight line $y=cx+d$ the

equation $\cos(x)=cx+d$has at most two solutionsinthe interval$\mathcal{I}_{n}$. We denote thesesolutions

(iftheyexist) by $\xi_{n,1}$ and$\xi_{n,2}$.

Definition 1 Consider the equation $\cos(x)=cx+d$ with real numbers $c,$$d$ andassume that

are analogous.

Lemma2 Considerthe equation $\cos(x)=cx+d$ with real numbers $c,$$d$. Then the following

hold:

1.

_If

$c=0and|d|<1$, then theequation has infinitely many solutions.

$If1>d\geq 0$thenthe solutionsare$\xi_{n,1},\xi_{n,2},$ $where- \frac{\pi}{2}+n\pi\leq\xi_{n,1}<\xi_{n,2}\leq-\frac{\pi}{2}+(n+1)\pi$

for

alleven integer$n$. Moreover$\cos(x)\geq cx+d$

for

$\xi_{n,1}\leq x\leq\xi_{n,2}$, otherwise _$\cos(x)<$

$cx+d$ in$\mathcal{I}_{n}$.

If $0>d>-1$

then the solutionsare $\xi_{n,1},\xi_{n,2}$ where $- \frac{\pi}{2}+n\pi\leq\xi_{n,1}<\xi_{n,2}\leq-\frac{\pi}{2}+$

$d=1$.

3.

_If

$c=0$ and $|d|>1$, then the equation has no solution. Moreover $\cos(x)>cx+d$

for

$d<-1,$ $\cos(X)<cx+d$

for

$d<1$.

4. $If|c|\geq 1$ then the equation has exactlyone solution $\xi$. When $c\geq 1$ then $\cos(x)\geq cx+d$

for

$x\leq\xi,$ $\cos(X)<cx+d$

for

_$x>\xi$. And when $c\leq-1$ then $\cos(x)\geq cx+d$

for

$x\geq\xi$_, $\cos(x)<cx+d$

for

$x<\xi$.

5.

_If

$0<c<1$

then thefollowing cases occurin the positive domain where $m,$$n$are integers

$s.t$. $m<n.\cdot$

(i) $If- \frac{\pi}{2}+2m\pi<x_{0}<-\frac{\pi}{2}+(2m+1)\pi and-\frac{\pi}{2}+2n\pi<x_{+1}<2n\pi$ then the equation

has the solutions $\xi_{2m,1}<\xi_{2m+2,1}<\xi_{2m+,2}<\cdots<\xi_{2n-2,1}<\xi_{2n-2},2$.

Moreover $\cos(x)\geq cx+d$

for

$x_{0}\leq x\leq\xi_{2m,1},$ $\cos(x)<cx+d$

for

$\xi_{2m,1}<x<$

Moreover $\cos(x)<cx+d$

for

$x_{0}<x<\xi_{2m+2,1},$ $\cos(x)\geq cx+d$

for

$\xi_{2m+2,1}\leq$

$x\leq\xi_{2m+2,2},$ $\cdots,$ $\cos(x)\geq cx+d$

for

$\xi_{2n-2,1}\leq x\leq\xi_{2n-2},2,$ $\cos(x)<cx+d$

for

$\xi_{2n-2,2}\leq x_{+1}$.

(vi) $If- \frac{\pi}{2}+(2m+2)\pi<x_{0}<-\frac{\pi}{2}+(2m+2)\pi$ and$2n \pi<x_{+1}<-\frac{\pi}{2}+(2n+1)\pi$then

theequationhas the solutions$\xi_{2m+2,1}<\xi_{2m+2,2}<,$ $..<\xi_{2n-2},1<\xi_{2n-2}$_}$2<\xi_{2n,1}<$

$\xi_{2n,2}$,

Moreover $\cos(x)<cx+d$

_for

$x_{0}<x<\xi_{2m+2,1},$ $\cos(x)\geq cx+d$

for

$\xi_{2m+2,1}\leq$

$x\leq\xi_{2m+2,2},$ $\cdots,$ $\cos(x)\geq cx+d$

for

$\xi_{2n-2},1\leq x\leq\xi_{2n-2},2,$ $\cos(x)<cx+d$

for

$\xi_{2n-2},2<x<\xi_{2n,1},$ $\cos(x)\geq cx+d$

for

$\xi_{2n,1}\leq x\leq\xi_{2n,2},$ $\cos(x)<cx+d$

for

$\xi_{2n,2}<x\leq x_{+1}$.

Forthe negative domain wehavean analogouscasedistinction.

6. _{$If- l<c<0$}

then wehave analogous subcasesas incase5.

(6)

4 Decision Procedures for

univariate

formulas

In this section we decide thevalidity ofunivariateclosed normal formulas inthelanguage $L$

ofthe form $\exists x(\psi)$, where $\psi$ is a quantifier-free. In view ofthe results in the section 2 this will

solvethe general decision problems for normal formulas.

Let the input formula $\varphi$ be of the form $\exists x(\psi(X))$, where $\psi$ is quantifier-free. The only

trigonometric termoccurring in$\psi$is trig$(ax+b)$where_$a,$ $b$

are

elementsof$F$and$a\neq 0$. By the

linear substitution$x\vdasharrow a^{-1}x-a^{-}1b,$ $\varphi$is equivalentto$\exists x(\psi;)$, where$\psi’:=\psi(a^{-1}x-a^{-1}b))$.

Notice that the only trigonometric term occuring in $\psi’$ is trig$(x)$. So $\psi’$ is a propositional

combination ofatomicformulas

$\alpha_{i}:=c_{i}x+d_{i}\rho_{i}trig(X)$ or $c_{i}x+d_{i}\rho_{i}0$ (1)

with$i\in I,$ $\rho_{i}\in\{=, <, >\}$. Let$s$be $2\pi$plusthe maximal absolute value ofthe domainbounds

ofall lines $c_{i}x+d_{i}$ with $c_{i}\neq 0$ occurring in $\psi’$ and ofthe first components of all intersection

points between all lines $y=c_{i}x+d_{i}$ and $y=c_{j}’x+d_{j}’$ with $ci\neq 0$ orwith $c_{j}\neq 0$. Consider

onlythe region $[-s, s]$. Forevery atomic formula$\alpha_{i}$ in$\psi’$, the set $M_{\alpha_{i}}$ of reals defined by it in

$[-s, s]$ consists ofone interval

or

finitely manydisjoint intervals described in lemma2. So the

set$M_{\psi’}$ of realsin $[-s, s]$ definedby$\psi’$ isafinite unionofintervals,whoseendpointsareamong

solutions ofthe equations

$c_{i}x+d_{i}=trig(x)$ or $c_{i}x+d_{i}=0$ (2)

obtained from the atomicformulas $\alpha_{i}$ in (1).

Lemma3

_If

$\exists x(\psi’)$ holds in$\mathbb{R}$

, thenitholds in $[-s, s]$.

ProofThisis animmediateconsequencefrom the definition of$s$ and lemma2. 1

Let$p_{1}<p_{2}<\ldots<p_{n}$ be the solutions of the equations (2) ordered in increasingorder. Then

the truth value of each atomic formula $\alpha_{j}$ of

$\psi’$ and hence of $\psi’$ remains invariant in each of

the intervals $(-\infty,p_{1}),$ $(p_{1},p_{2}),$ $..\mathrm{x}$

,

$(p_{n-1},p_{n}),$ $(p_{n}.\infty)$. So following the ideas in [10] in the

present context, it suffices to determine the truth value of each $\alpha_{i}$ at the test$\mathrm{P}^{\mathrm{o}\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}s}-,pi$, and

$p_{i}+\epsilon$, where $\epsilon$ is a positive infinitesimal. From the result of these evaluations one can then

determine the truth-value of$\psi’$ at all these points, andthus determine the structure ofthe setof

real values $x$ for which $\psi’(X)$ holds. In particularone can then decide, whetherornot $\varphi$ holds.

Moreprecisely,

one

obtains the exact numberofconnectedcomponents of the setofreal values

$x$forwhich$\psi’(X)$ holds.

Twoproblems arise inthis procedure:

1. First,

one

needsto determine the order relations between the solutions ofthe equations (2).

2. Second,

one

mustbe able toevaluate all atomic formulas$\alpha_{j}$ of$\psi’$ atthese solutions,closely

tothe right ofthese solutions, and $\mathrm{a}\mathrm{t}-s$.

In contrast to the purely linear situation in [10], the solutions of the equations $c_{i}x+d_{i}$ $=$

$trig(x)(i\in I)$ are no longer given in a standard mathematical notation. So the evaluation of

$\alpha_{j}$ at or closely to theright ofthese solutions has to be done in a roundabout way. It turns out

that both problems can be

overcome

by

case

distinctions following lemma 2 and evaluation of

(7)

The nexttwolemmasspecifythedetailsdepending

on

the

cases

specified inlemma2.

More-over, herewealsorestrict tothe

case

oftrig$(x)=\cos(x)$_.

Lemma 4 Let $\ell$ and $\ell’$ be a distinct straight lines

defined

by $y=cx+d$ and $y=c’x+d’$,

respectively, where$C,$$C^{J}d,$$d’\in F$. Let$D$ be the interval $[-t, t]$ where

$t:= \max$

{

$- \frac{\pi}{2}+(n+1)\pi|n\in \mathrm{N}$ and $- \frac{\pi}{2}+n\pi<s$

}.

$Let \mathcal{I}_{2n}=(-\frac{\pi}{2}+2n\pi, -\frac{\pi}{2}+(2n+1)\pi)$

for

integers$n$. Wedenoteas

before

by$\xi_{2n,1}<\xi_{2n,2}$ the

potential solutions

_of

theequation$\cos(x)=cx+d$ in$\mathcal{I}_{2n}\cap D$. Similarly wedenote by_{$\xi_{2n,1}’<$}

$\xi_{2n,2}’$ the potential solutions

of

the equation $\cos(x)=c’x+d’$ in$\mathcal{I}_{2n}\cap D$. We let $(\alpha, \beta)\in F^{2}$

denote thepotential intersection point

_of

the lines $\ell$ and$\ell’$. Notice that

$\xi_{2n,1},$ $\xi_{2n,2},$ $\xi’2n,1’\xi_{2n}^{;},2$

are all

_{different from}

$\alpha$, since $\cos(x)$ is strongly transcendental.

If

the line $cx+d>0$ in an

interval, then itiscalledpositive in the interval.

If

one

_of

the two lines $\ell$ and $\ell’$ has no intersection point with

$\cos(x)$, the ordering

of

the

solutions$\xi_{i,j}$ are obvious

from

lemma 2. Hencewe only consider thecases where both two lines

have atleast one solution with $\cos(x)$ in $\mathcal{I}_{2n}$. Then the order relation among the solutions $\xi_{i,j}$

aredecidedas

_follows:

1.

_If

the two lines $\ell$ and $\ell’$ are bothpositive and have intersection points with

$\cos(x)$ in $\mathcal{I}_{2n}$,

then let $\xi_{2n,1},$ $\xi_{2n},2$ be the intersection points with $\cos(x)$

for

the line $\ell$ and

$\xi_{2n,1}’,$$\xi’2n,2$ be

those

_for

the line $\ell’$. (Note that the case where _{$\cos(\alpha)=\beta$} is impossible, since

$\cos(x)$ is

stronglytranscendental.)

$(a)$

Ifthere

is no intersectionpoint$of\ell$and$\ell’$ with

$\alpha$in$\mathcal{I}_{2n}$ ortheintersection point$(\alpha, \beta)$has

$\alpha$ in$\mathcal{I}_{2n}$ and$\cos(\alpha)<\beta$, then wehave _{$\xi_{2n,1}’<\xi_{2n,1}<\xi_{2n,2}<\xi_{2n,2}’$}

for

$c(2n\pi)+d>$

$c>c’$.

2.

_If

the line$\ell$ is positive and has intersection points with

$\cos(x)$ in $\mathcal{I}_{2n}$ and$\ell’$ has an

intersec-tion point$(\gamma, 0)$ withthe$x$-axis in $\mathcal{I}_{2n}$, let_{$\xi_{2n,1},$ $\xi_{2}n,2$} be the intersection pointswith $\cos(x)$

for

the line$\ell$and

$\xi_{2n,1}’$ be that

for

the line

1’.

(The casewhere the line$\ell’$ is positive and has

intersection pointswith $\cos(x)$ in $\mathcal{I}_{2n}$ and$\ell$ has an intersection point _{$(\gamma, 0)$} with the x-axis

respectively, let$\xi_{2n,1}$ be theintersection point with$\cos(x)$

for

theline$\ell$and

$\xi_{2n,1}’$ be

thatfor

the line$\ell’$.

$(a)$

If

there isno intersection point

of

$\ell$ and$\ell’$ with

$\alpha$ in $\mathcal{I}_{2n}$ orthe intersection point $(\alpha, \beta)$

(8)

$i$.

If

$c,$$c’>0$ then $\xi_{2n,1}<\xi_{2n,1}’$

$occu\gamma.\cdot$

$i$.

If

$c,$$c’>0$ then $\xi_{2n,1}’<\xi_{2n,1}$

for

$c(- \frac{\pi}{2}+2n\pi)+d>c’(-\frac{\pi}{2}+2n\pi)+d’$ and

$\xi_{2n,1}<\xi_{2n,1}’$

for

$c(- \frac{\pi}{2}+2n\pi)+d<c’(-\frac{\pi}{2}+2n\pi)+d’$.

$ii$.

If

_$c,$$c’<0$ then _{$\xi_{2n,1}<\xi_{2n,1}’$}

for

_{$c(- \frac{\pi}{2}+2(n+1)\pi)+d>c’(-\frac{\pi}{2}+2(n+1)\pi)+d’$}

and$\xi_{2n,1}’<\xi_{2n,1}$

for

$c(- \frac{\pi}{2}+2(n+1)\pi)+d<c’(-\frac{\pi}{2}+2(n+1)\pi)+d’$. $iii$.

If

$cc’<0$ then $\xi_{2n,1}<\xi_{2n,1}’$

for

$c<0,$$c’>0$ and$\xi_{2n,1}’<\xi_{2n,1}$

for

$c>0,$$c’<0$.

The interval$\mathcal{I}_{2n+1}$

for

aninteger$n$ istreatedin analogousway tothe interval$\mathcal{I}_{2n}$.

Lemma5 Let $\xi_{2n,1}<\xi_{2n,2}$ be the potential solutions

of

the equation $cx+d=\cos(x)$ in

$\mathcal{I}_{2n}\cap D$. Let the potential intersection point

of

two lines$\ell$ and

1’

be _{$(\alpha, \beta)$}. We only consider

the caseswhere both twolines haveatleastonesolution with$\cos(x)$ in$\mathcal{I}_{2n}\cap D$. Then the order

relation between$c’\xi 2n,i+d’$ and$\cos(\xi 2n,i)\mathcal{I}_{2}n$ isdecidedas

follows:

1.

_If

the two lines$\ell$and1’ arebothpositive on$\mathcal{I}_{2n}$ and have intersection pointswith $\cos(x)$ in

$\mathcal{I}_{2n}$, then let_{$\xi_{2n,1},$ $\xi_{2}n,2$} bethe intersectionpoints with $\cos(x)$

for

the line$\ell$.

$(a)$

If

there isno intersectionpoint

of

1 and1’ with $\alpha$ in $\mathcal{I}_{2n}$ orthe intersectionpoint $(\alpha, \beta)$ has$\alpha$ in$\mathcal{I}_{2n}$ and$\cos(\alpha)<\beta$, then wehave $c’\xi_{2n},1+d’<\cos(\xi 2n,1),$ $C’(\xi_{2n,1}+\epsilon)+d’<$

$\cos(\xi_{2}n,1),$ $c’\xi_{2n},2+d’<\cos(\xi 2n,2),$ $c^{J}(\xi 2n,2+\epsilon)+dJ<\cos(\xi_{2}n,2)$,

for

$c(2n\pi)+d>$

$c’(2n\pi)+d’$ and$c’\xi_{2n},1+d’>\cos(\xi_{2}n,1),$ $c’(\xi_{2}n,1+\epsilon)+d’>\cos(\xi 2n,1),$$c\xi\prime 2n,2+d’>$

$\cos(\xi_{22}n,),$ $c(;\xi 2n,2+\epsilon)+d’>\cos(\xi_{2n,2})$

for

$c(2n\pi)+d<c’(2n\pi)+d’$.

$(b)$

there isno intersection point

of

$\ell$and$\ell’$ with

$c,$$c’>0$ then $c’\xi_{2n,1}+d’>\cos(\xi_{2n},1),$ $C^{;}(\xi_{2n,1}+\epsilon)+d’>\cos(\xi_{2n,1})$

for

$c(- \frac{\pi}{2}+$

$2n \pi)+d>c’(\frac{\pi}{2}+2n\pi)+d’$ and $c’\xi_{2}n,1+d’<\cos(\xi_{2n,1}),$ $c’(\xi_{2}n,1+\epsilon)+d’<$

$\cos(\xi_{2n,1})$

for

$c(- \frac{\pi}{2}+2n\pi)+d<c’(\frac{\pi}{2}+2n\pi)+d’$. $ii$.

If

occurring in $\psi’$ are real algebraic numbers in $F$ and _$\cos(x)$ is strongly transcendental we can

decide equations and order inequalities between the elements of $F$ and between the values of

$\cos(x)$for$x\in F$. Then all thecasedistinctionsmadeinthe twoproceedinglemmascan_be

eval-uated algorithmically. Sowe can determinealgorithmicallytheexactnumber of real solutions of

everyequation arising from

an

atomic subformulaof$\psi’$. Next

we

can orderall these solutions by

the first lemma. Bythesecond lemmawe can evaluate the truth value ofeveryatomicsubformula

of$\psi’$ and hence of$\psi’$ at all thesepoints in $[-s, s]$, and closely to the right of all these points.

Fromtheseevaluations we obtainimmediately thenumber ofnon-empty connectedcomponents

of theset$M_{\psi’}$, andmoreoverthe type ofintervals thatthese componentsconstitute in increasing

order.

5 The mixed real-integer

case

In this section we consider a considerable extension of linear-exponential problems given

by

an

extension of the concept ofterm used

so

far. We admit as

new

operation symbol in

our

extension language the integer-part operation [-] (compare [27]). Similar as in the language

(10)

addition, scalar multiplication by rational constants and the integer-part operation. Notice that

these operations maybe nested in an arbitrary way. Atomic formulas in the extended

sense

can

be equivalently

expressedby the extended formula$\exists x$($x=[x]$ A

$\varphi$). So the problems that

can

be expressed by

normal formulasinthe extended

sense

are

now

mixed real-integer linear-trigonometric problems.

We are now going to describe

a

decision procedure

_for

normal

_formulas

in the extended

sense: By an argument similarto the one in section 2

we can

use the mixed real-integer linear

quantifier eliminationof[27] toreduce the decision problem fornormal formulasto the

case

of

normal formulaswithjust one existential quantifier

$\exists x(-s\leq x\leq s\wedge\psi(x))$ (3)

where $\psi(x)$ is quantifier-free. From the givenbound $S$

we can

compute an integer bound$T$ for

the absolutevalues of all extendedtermsand subterms$t(x)$ occurring in $\psi(x)\mathrm{f}\mathrm{o}\mathrm{r}-S\leq x\leq S$.

Next, we successively eliminate all

occurrences

ofthe integer-part operation from (3): Let $[t]$

be aninnermost

occurrence

ofinteger-partoperation in $\psi(x)$. We write $\psi(x)$

as

$\tau([t])$. Then(3)

is equivalent to $_{i=-T}^{T}\exists x$(_{$-s\leq x\leq S$} A _{$i\mathrm{l}\leq t(x)<(i+1)1$} _A _$\tau(i1)$) This decreases

the number of

occurrences

ofthe integerpart operation by

one.

By iteration oftheprocedureall

occurrences

of theintegerpart operation canbe eliminatedfrom thegiven formula. Atthispoint

theresulting formulacanbe decidedas in section4.

6 The

Tangent

case

So far the trigonometric function in normal formulas was essentially the sine

or

the cosine

function. Whathappens ifwereplace this functionby the tangent function?

The obvious changes are the following: $tan(X)$ is defined only for $x \neq\frac{\pi}{2}+n\pi$ forinteger

$n,$ $tan(X)$ has period $\pi$, and $tan(X)$ is unbounded. We extend$tan(X)$ to

a

total function on

IR

by setting $tan( \frac{\pi}{2}+n\pi)=0$. Sothe new tasksare thefollowing:

1. Compute the real zeros of the functions $f_{\mathrm{c},d}(x):=tan(X)+cx+d$where $c,$$d\in F$ and

determine the sign of$f_{c,d}(x)$ infinitesimallyto theright ofthese

zeros.

2. Eliminate the

occurrence

of the integer part operation from an univariate extended normal

formulas.

For the first task we note to begin with that in each basic interval $\mathcal{I}_{n}$ the function _{$f_{c,d}(x)$}

has exactly one zero, with the possible exception ofthe interval $\mathcal{I}_{m}$ containing the $\mathrm{z}\mathrm{e}\mathrm{r}\mathrm{o}-d/c$

of the line $cx+d$ in case $c\neq 0$. In the exceptional interval $\mathcal{I}_{m}$ the function has exactly one

zero if$c>-1$, or $c=-1$ and $d=0$, or$c<-1$ and the values of$tan( \pm acos(\frac{1}{\sqrt{-c}}+m\pi))$

have the same sign, and exactly three zeros otherwise. This follows from the following facts:

$f_{c,d(X)}’=(\cos(x\mathrm{I})^{-2}+c>0$ for $c>-1$. For $c<-1,$ $f_{c,d}’(X)$ has exactly two real zeros $\pm acos(\frac{1}{\sqrt{-c}}+n\pi)$ in each ofthe intervals$\mathcal{I}_{n}$. By the strong transcendence of$tan(X),$ _{$f_{c,d}(x)$}

(11)

has

a

multiple

zero

iff$c=-1$ and $d=0$. Using these facts

we

can

solve the first task similarly

as

in section 4. As

a consequence we can

decidenormalformulas with trig$(x)=tan(X)$.

We do not know how to solve the second task, since $tan(X)$ is unbounded. Instead

we

modify thetangent function by truncating its values at

some

fixedpositive integer $k$

as

follows:

Put $tan_{k}(x)=tan(X)$; if $|tan(X)|\leq k,$ $tan_{k}(x)=-k$ for$tan(X)<-k,$ $tan_{k(X})=k$ for

$tan(X)>k$. Thenthe second taskcanbe solved similarly

as

insection 6. So foreach fixed $k$we

obtain

a

decisionprocedure for extendednormalformulas withtrig$(x)=tan_{k}(x)$.

Again these decision procedures

can

be modified

as

indicated before for quantifiers ranging

over

a subfield of the field ofreal algebraic numbers.

7 Deciding linear-trigonometric problems

over

subfields

So far we have consideredthe decision problemfor (extended) normal formulas, where all

quantifiers range

over

the field of real numbers. It is well-known that the truth value of linear

formulas does not change when quantifiers are restricted to an arbitrary subfield of the reals

[10]. By [27] the same applies to mixed real-integer linear fornulas. For linear-trigonometric

problems thereis, however, abig differencebetweenvalidity in$\mathbb{R}$andin somesubfield_$F$of the

real algebraicnumbers: Consider forexample the normal formula $\exists x(\cos(X)=x)$. Inthe reals

this formula is true, since the equation $\cos(x)=x$ has a unique real solution $\xi$ in the interval

$(0, \pi/2)$. By the strong trancendency of $\cos(x)$ this solution is transcendental, and hence the

formulaisfalsein $F$.

So

over

$F$theelimination oflinear variables from(extended)normal formulas remainsvalid,

while thedecision ofunivariate normalformulas involvinga trigonometricfunction in section 4

maybecome incorrect.

In the following

we

sketch a modified decision algorithm that will be valid for arbitrary

subfields $F$ ofthe field of real algebraic numbers. As remarked aboveit suffices to modify the

decisionofunivariatenormal formulas $\exists x(\psi(x)$. Sincethe decision works bysubstituting finitely

many test points, it suffices to delete all test point that

are

not in $F$. These are exactly the test

points of the form$\xi_{n,i}$ arising

as zeros

offunctions $f(x)=trig(x)+cx+d$ differentfrom

zero.

Notice, however,thatwe keepall the testpointof theform$\xi_{n,i}+\epsilon$, since they couldbe replaced

byanelement of$F$.

Thusinourexample $\exists x(\cos(X)=x)$ thedecisioninthereal lineuses astest$\mathrm{p}\mathrm{o}\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}-1-2\pi$,

the solution $\xi$ ofthe equation $\cos(x)=x$, and the point $\xi+\epsilon$ for a positive infinitesimal $\epsilon$,

whereas in $F$ the testpoint $\xi$ is dropped. Hence the result of the decision is “true” in the reals

and“false” in$F$.

Remark

6

(Complexity of the decisionproblem) The complexity

_of

the decision problem

_for

(extended)normal

_formulas

hasnotbeen determinedyetexactly. We expectourdecision method

torun in doubly exponential time

_for

non-extended normal

_formulas

andin exponential time

_for

(12)

8 Conclusions

We have shown that the decision problem forseveral classes offormulas involving real and

integervariables, linear polynomials and a trigonometric function is decidable. This is in

con-trast to theundecidability of the full elementarytheory of the reals with

a

specifictrigonometric

function. The formulas may involve

one

mixed linear-trigonometric variable and several

lin-ear

variables. The decision method

uses

linear quantifier elimination and a symbolic test point

method. It is quite explicit and implementable. Variants of it work

over

subfields of the real

algebraic numbers. In its approach it is similar to the decision method for linear-exponential

problems announced in [26]. We expect that theapproach

can

be generalizedto formulas

involv-ing larger classes ofelementary functions.

Our decision method

can

be construed

as

a modified quantifier elimination method, when

the coefficients of terms

are

taken as parameters. Notice, however, that in this

case

the output

formula willno longer benormal,but will include

more

complicatedterms.

References

[1] BAREISS, E. Sylvester’s identity and multistep integer preserving Gaussian elimination.

Mathematics

_of

Computation 22 (1968),

565-578.

[2] COLLINS, G. E. Quantifier Elimination

_for

Real ClosedFields by Cylindrical Algebraic

Decomposition, LNCS 32. Springer Verlag, 1975.

[3] DOLZMANN, A., STURM, T., AND WEISPFENNING, V. Real quantifier elimination in

practice. Technical ReportMIP-9720, FMI, Universit\"at Passau,D-94030Passau, Germany,

Dec. 1997.

[4] GUTIERREZ, J., AND RECIO, T. Advanceson thesimplification ofsine-cosine equations.

J. Symbolic Computation26, 1 (1998), 31-71.

[5] HONG, H., AND SCHICHO, J. Algorithmsfortrigonometric

curves

(simplification,

implic-itization,parameterization). J. Symbolic Computation26, 3 (1998), 279-300.

[6] JIRSTRAND, M. Nonlinear control system design by quantifier elimination. J. Symbolic

Computation24, 2 (Aug. 1997),

137-152.

[7] KOVA’CS, P. Computer algebra in robot-kinematics. In Proceeding

of

the

work-shop: “Computer Algebra in Science and Engineering”, Bielefeld, Aug’94 (Singapore,

1994),World Scientific,pp.

303-316.

[8] LAFFERRIERE, G., PAPPAS, G. J., AND YOVINE, S. Decidable hybrid systems. Tech.

rep., VERIMAG, Univ. ofGrenoble, 1998.

[$9_{\mathrm{J}}^{\rceil}$ LISKA, R., AND STEINBERG, S. Applying quantifier elimination to stability analysis of

difference schemes. The ComputerJournal36, 5 (Oct. 1993),

497-503.

[10] Loos, R., ANDWEISPFENNING,V. Applying linear quantifier elimination. The Computer

Journal36, 5 (1993),

450-462.

Special issueoncomputational quantifier elimination.

[11] MACINTYRE, A., AND WILKIE, A. On the decidability ofthe real exponential field. In

(13)

[12] PAU, P., AND SCHICHO, J. Quantifier elimination fortrigonometricpolynomials by

cylin-drical trigonometric decomposition. RISC-Linz Technical Report(submitted to Journal

_of

Symbolic Computation(1999).

[13] RICHARDSON, D. Some undecidable problems involving elementary functions of a real

Symbolic

Computation5, 1-2 (Feb.-Apr. 1988), 3-27.

[22] WEISPFENNING, V. The complexity ofalmost linear Diophantine problems. Journal

_of

Symbolic Computation 10,5 (Nov. 1990), 395-403.

[23] WEISPFENNING, V. Existential equivalence ofordered abelian groups with parameters.

_for

Mathematical Logic29 (1990),_237-248.

[24] WEISPFENNING, V. Parametriclinear andquadraticoptimizationby elimination. Technical

ReportMIP-9404, FMI, Universit\"at Passau, D-94030 Passau, _{Germany, Apr.} _1994.

[25] WEISPFENNING, V. Simulation and optimization by quantifier elimination. Journal

_of

Symbolic Computation24, 2 (Aug. 1997), 189-208. Special issue on applications of

quan-tifier elimination.

[26] WEISPFENNING, V. Deciding linear-exponential problems. Poster presentation at

IS-SAC’99, Vancouver,July 1999.

[27] WEISPFENNING, V. Mixedreal-integer linear quantifierelimination. In ISSAC’99(1999),