Kozen D.C. Theory of Computation

Подождите немного. Документ загружается.

Complexity of Decidable Theories 137

Proof. This is a standard back-and-forth argument. Pick the ﬁrst element

D in some enumeration of D that is not among the a

,0≤ i ≤ k − 1, and

call it a

. It lies in some relation to all the a

;thatis,foreacha

,either

or a

. Because E is dense and has no endpoints, there must

exist an element b

that lies in the same relationship to the b

,0≤ i ≤ k−1.

Pick the ﬁrst such b

in some enumeration of E and set f(a

)=b

.We

have extended the domain of f by one and preserved the fact that it is a

local isomorphism.

Now do the same thing from the other side: pick the ﬁrst unmatched

element b

k+1

of E and ﬁnd an element a

k+1

of D to match with it (that

is, make f(a

k+1

)=b

k+1

) preserving local isomorphism. Go back and forth

like this forever. Every element of D and E is eventually matched with

something on the other side, so we get an isomorphism. 2

A Decision Procedure

Let D be a dense linear order without endpoints. (By the result of the

previous section, we might as well take D to be Q.) To decide the sentence

∃x ∀y ∃zx<y∧ (x ≥ z ∨ y = z),

for example, it suﬃces to pick an arbitrary point a ∈ D andthencheck

whether

∀y ∃za<y∧ (a ≥ z ∨ y = z). (21.1)

It does not matter which a is chosen, because all such a look the same: by

Theorem 21.1, for every a, a



∈ D, there is an automorphism of D mapping

a to a



. Now to check (21.1), we wish to check whether for all b ∈ D,

∃za<b∧ (a ≥ z ∨ b = z). (21.2)

However, there are essentially only three choices for b: either less than a,

equal to a, or greater than a.Ifwepickanyb

, b

,andb

representing

these three respective possibilities respectively, then any other pair (a



)

of elements of D looks like one of (a, b

), (a, b

), or (a, b

). Therefore it

suﬃces to check (21.2) for b ∈{b

}. Finally, to eliminate the last

quantiﬁer ∃z in (21.2), we pick a c ∈ D in one of ﬁnitely many ways. For

(a, b

), because b

<a, there are essentially ﬁve ways to pick c:either

c<b

, c = b

, b

<c<a, c = a,orc>a.For(a, b

), there are essentially

three ways to pick c,andfor(a, b

)thereareﬁve.

Once we have chosen three elements a, b, c ∈ D and know their relative

order in D, we have enough information to determine the truth or falsity

of the quantiﬁer-free part

a<b∧ (a ≥ c ∨ b = c). (21.3)

138 Lecture 21

We did not really need to pick out actual elements a, b, c of D.Wecould

do the whole procedure symbolically. Deﬁne a linear arrangement of the

variables x

,... ,x

to be a list of the variables x

,... ,x

in some order,

with either < or = in between each adjacent pair. The linear arrangements

will be the board positions of our game.

A linear arrangement determines for each pair i, j ∈{1,... ,k} whether

, x

= x

,orx

by transitivity. It therefore determines the

truth of all atomic formulas x

≤ x

and x

= x

. These in turn determine

the truth of any quantiﬁer-free formula with variables among x

,... ,x

For a linear arrangement α of x

,... ,x

and a quantiﬁer-free formula

ϕ with all free variables among x

,... ,x

,wewrite

α |= ϕ (21.4)

if ϕ is true under arrangement α.

We now extend the relation |= of (21.4) to formulas ϕ with quantiﬁers.

For any linear arrangement α of x

,... ,x

,letmove(α)bethesetof

arrangements β of x

,... ,x

k+1

obtained from α by inserting x

k+1

all possible ways. The set move(α) could be as large as 2k + 1 or as small

as 3, depending on how many equal signs (=) appear in α.

For a formula of the form

∃x

k+1

k+2

··· Q

ψ(x

,... ,x

k+1

,... ,x

where ψ is quantiﬁer-free and contains only variables among x

,... ,x

and for α a linear arrangement of x

,... ,x

, deﬁne

α |= ∃x

k+1

k+2

··· Q

ψ(x

,... ,x

k+1

,... ,x

)

if there exists a β ∈ move(α) such that

β |= Q

k+2

··· Q

ψ(x

,... ,x

k+1

,... ,x

Similarly, deﬁne

α |= ∀x

k+1

k+2

··· Q

ψ(x

,... ,x

k+1

,... ,x

)

if for all β ∈ move(α),

β |= Q

k+2

··· Q

ψ(x

,... ,x

k+1

,... ,x

The basis of this inductive deﬁnition is given by (21.4).

Let α

be the null arrangement, and let ϕ be a prenex formula of the

form

··· Q

ψ(x

,... ,x

where ψ is quantiﬁer-free. It is not diﬃcult to show by induction that

|= ϕ iﬀ ϕ is true in all dense linear orders without endpoints. This gives

Complexity of Decidable Theories 139

an alternating polynomial-time algorithm for the theory of dense linear

order without endpoints, as follows. The initial process will attempt to

check whether

|= Q

··· Q

ψ(x

,... ,x

Subsequently, a process attempting to check whether

α |= ∃x

k+1

k+2

··· Q

ψ(x

,... ,x

)

will produce all β ∈ move(α) using existential branching, and for each such

β, check whether

β |= Q

k+2

··· Q

ψ(x

,... ,x

To check whether

α |= ∀x

k+1

k+2

··· Q

ψ(x

,... ,x

universal branching is used. Once all quantiﬁers are eliminated, the truth

of the quantiﬁer-free part is easily determined from the arrangement of

,... ,x

in polynomial time.

We have given an alternating polynomial-time algorithm for deciding

the ﬁrst-order theory of dense linear orders without endpoints. The theory

is also PSPACE-hard, as is any nontrivial ﬁrst-order theory (Miscellaneous

Exercise 49). We have shown

Theorem 21.2 The ﬁrst-order theory of dense linear order without endpoints is PSPACE -

complete.

Lecture 22

Complexity of the Theory of Real Addition

Among Alfred Tarski’s many signiﬁcant achievements, one of the most im-

portant was showing the decidability of Th(R, +, ·, =), the ﬁrst-order the-

ory of reals with addition and multiplication. This is often called the theory

of real closed ﬁelds. This result stands in stark contrast to the undecidabil-

ity of number theory Th(N, +, ·, =).

In the next two lectures, we show that the weaker theory of real addition

Th(R, +, ≤), the ﬁrst-order theory of the real numbers with addition + and

order ≤, is complete for the complexity class STA(∗, 2

O(n)

,n).

We have not included a constant for the real number 0 in the language,

but it is deﬁnable: it is the unique x such that ∀yx+ y = y.Theidentity

relation = is also deﬁnable: x = y iﬀ x ≤ y ∧ y ≤ x. The element 1 is not

deﬁnable, but any positive element is as good as 1 in this theory, because for

any a>0, the map x → ax is an isomorphism of the structure (R, +, ≤).

This says that R  ϕ(1) iﬀ R  ∃zz>0 ∧ϕ(z), so we might as well assume

that the constant 1 is in the language.

Ferrante and Rackoﬀ [40] showed that the theory is decidable in expo-

nential space, or STA(∗, 2

O(n)

, ∗). Fischer and Rabin [42] showed that the

theory is hard for NEXPTIME ,orSTA(∗, 2

O(n)

, Σ1). These arguments are

given in [63]. Berman [14] improved both the upper and lower bounds and

showed that the exact complexity is STA(∗, 2

O(n)

,n). We prove the upper

bound in this lecture and the lower bound in Lecture 23.

Complexity of the Theory of Real Addition 141

Extend the ﬁrst-order language to allow multiplication by rational con-

stants. Thus we now allow statements such as ∀x ∃y

y ≤

. It suﬃces

to show the upper bound for this extended language.

Deﬁnition 22.1 An integer aﬃne function is a function f : R

→ R deﬁned by a linear

polynomial with integer coeﬃcients:

f(x

,... ,x

)=c



i=1

for some c

,... ,c

∈ Z. For such functions, deﬁne

#f # =

max

i=0

Let A

be the set of all aﬃne functions f : R

→ R with integer

coeﬃcients, and let A

def

= {f ∈ A

|#f #≤m}.

As with the theory of dense linear order without endpoints, we partition

the set of all k-tuples of reals into ﬁnitely many equivalence classes that

determine the formulas that a given k-tuple satisﬁes.

Deﬁnition 22.2 For a, b ∈ R

, deﬁne

a ≡

def

⇐⇒ ∀f ∈ A

sign(f (a)) = sign(f (b)),

where

sign(x)

def

⎧

⎨

⎩

−1 if x<0,

0 if x =0,

1 if x>0.

Equivalently, a ≡

b iﬀ a = a

,... ,a

and b = b

,... ,b

satisfy the same

linear inequalities



≤ c

with integer coeﬃcients c

of absolute value

at most m.

Unlike the theory of dense linear order, the deﬁnition here depends on

a parameter m, which will determine the size of constants and quantiﬁer

depth of formulas on which two ≡

-equivalent k-tuples are guaranteed to

agree. For more complex formulas, we need to take larger m. Note that the

equivalence relation ≡

is ﬁner (equates fewer elements) for larger values

of m.

The following lemma is used inductively to eliminate one quantiﬁer.

Lemma 22.3 Let a, b ∈ R

.Ifa ≡

b, then for all a



∈ R there exists b



∈ R such that

a, a



≡

k+1

b, b



142 Lecture 22

Proof. Suppose a ≡

b.Leta



∈ R be arbitrary. We would like to ﬁnd



∈ R such that for any f ∈ A

and |c|≤m,

sign(f (a)+ca



)=sign(f(b)+cb



), (22.1)

or equivalently,

sign(a



+ f(a)/c)=sign(b



+ f(b)/c), (22.2)

assuming c =0(ifc = 0 then (22.1) is immediate from the assumption

a ≡

b). Now (22.2) is equivalent to the assertion that



≤−

f(a)

⇔ b



≤−

f(b)

In order to show the existence of such a b



for an arbitrarily chosen a



,it

suﬃces to show that the numbers f(a)/c for all aﬃne functions f ∈ A

and nonzero c such that |c|≤m lie in the same order on the real line as the

corresponding numbers f(b)/c. This occurs if and only if for all f,g ∈ A

and nonzero c, d such that |c|, |d|≤m,

f(a)

≤

g(a)

⇔

f(b)

≤

g(b)

or in other words,

sign(df (a) −cg(a)) = sign(df (b) − cg(b)). (22.3)

But the aﬃne function

h(x)=df (x) − cg(x)

satisﬁes #h#≤2m

, so (22.3) follows from the assumption a ≡

b. 2

Let σ be an ≡

-equivalence class and and τ an ≡

k+1

-equivalence

class. We say that τ is consistent with σ if there exist a ∈ R

and a



∈ R

such that a ∈ σ and a, a



∈ τ .

Lemma 22.4 Let a ∈ R

and σ the ≡

-equivalence class of a.Theset

{(a, f(a)/c) | f ∈ A

, |c|≤2m

}

contains a representative of every ≡

k+1

-equivalence class consistent with

σ.

Complexity of the Theory of Real Addition 143

Proof. Let a



∈ R.Thena, a



≡

k+1

a, b



iﬀ for all nonzero c such that

|c|≤m and f ∈ A

sign(ca



+ f(a)) = sign(cb



+ f(a));

in other words, a



≤−f(a)/c iﬀ b



≤−f(a)/c. This says that all ≡

k+1

equivalence classes are represented by a, a



,wherea



is either

(i) a rational number f(a)/c for |c|≤m and f ∈ A

;

(ii) a rational number contained in an interval strictly between adjacent

rational numbers f (a)/c and g(a)/d for |c|, |d|≤m, c, d =0,and

f,g ∈ A

;or

(iii) a rational number strictly less than the smallest rational number of

the form f(a)/c for |c|≤m and f ∈ A

, or strictly greater than the

largest such rational number.

For (i), take a



= f(a)/c. For (ii), take the midpoint of the interval:



(f(a)/c + g(a)/d)=

f(a)d + g(a)c

2cd

Letting h(a)=f(a)d + g(a)c,wehaveh ∈ A

2m +1

and |2cd|≤2m

.For

(iii), take a



= f (a)/c −1=(f (a) −c)/c or a



= f (a)/c +1=(f(a)+c)/c.

Let us say a formula with variables x = x

,... ,x

is in reduced form

if it is in prenex form and all atomic formulas are linear inequalities of

the form f(x) ≥ 0 for some aﬃne function f with integer coeﬃents. Any

formula can be put into reduced form eﬃciently and without signiﬁcant

increase in size, so we assume henceforth that all formulas are of this form.

Deﬁne

r(0,)

def

= r(n +1,)

def

=2r(n, )

It follows inductively that r(n, )=2

−1



, which is 2

O(n+log log )

.Thus

a number whose absolute value is bounded by r(n, ) can be written down

in binary with exponentially many bits.

Lemma 22.5 If a, b ∈ R

and a ≡

r(n, )

b, then for any formula ϕ(x) in reduced form

with free variables x = x

,... ,x

and at most n quantiﬁers such that all

integer constants are of size at most ,

R  ϕ(a) ⇔ R  ϕ(b).

144 Lecture 22

Proof. The proof is by induction on the structure of the formula. For

atomic formulas, the result is immediate from the deﬁnition of ≡



.For

formulas of the form ϕ ∧ ψ, the argument is by straightforward appeal to

the induction hypothesis for the simpler formulas ϕ and ψ:

R  ϕ(a) ∧ ψ(a)

⇔ R  ϕ(a)andR  ψ(a)

⇔ R  ϕ(b)andR  ψ(b)

⇔ R  ϕ(b) ∧ ψ(b).

The argument for the other propositional operators is equally straight-

forward. Finally, for formulas ∃xϕ(a, x), suppose R  ∃xϕ(a, x), and let



∈ R be such that R  ϕ(a, a



). By Lemma 22.3, there exists b



such that

a, a



≡

k+1

r(n − 1,)

b, b



and by the induction hypothesis, R  ϕ(b, b



), thus

R  ∃xϕ(b, x).

The case where the leading quantiﬁer is ∀ is similar. 2

Theorem 22.6 Th(R, +, ≤) ∈ STA(∗, 2

O(n)

,n).

Proof. We describe an alternating Turing machine that accepts the set

of true formulas of the theory of real addition. The machine M runs in time

and makes n alternations on formulas of length n.

The ﬁrst step is to put the formula into reduced form. This can be done

in polynomial time and entails no signiﬁcant increase in size. Let n and 

be the quantiﬁer depth and maximum absolute value of a constant in the

formula, respectively.

Suppose the ﬁrst quantiﬁer is ∃x

. Using existential branching, choose

a rational number a

= d/c,where|c|, |d|≤r(n, ). If the ﬁrst quantiﬁer is

∀, do the same thing with universal branching. By the bound on |c| and |d|,

this takes exponential time. By Lemma 22.4, the leaves of the computation

tree have a representative of each ≡

r(n, )

-equivalence class.

We eliminate the second quantiﬁer Q

by choosing f ∈ A

r(n − 1,)

and

c such that |c|≤r(n − 1,) either existentially or universally according as

is ∃ or ∀, respectively, and let a

= f(a

)/c. By Lemma 22.4, the leaves

of the computation tree have a representative a

of each ≡

r(n − 1,)

equivalence class consistent with the ≡

r(n, )

-equivalence class of a

Continuing in this fashion, after eliminating all quantiﬁers, we have

chosen a sequence a = a

,... ,a

representing some ≡



-equivalence class.

Complexity of the Theory of Real Addition 145

We then evaluate the quantiﬁer-free part of the formula on a,whichtakes

exponential time.

The correctness of this alternating algorithm follows from Lemma 22.5.

Lecture 23

Lower Bound for the Theory of Real Addition

Last time we proved that Th(R, +, ≤), the theory of real addition, is con-

tained in the complexity class STA(∗, 2

O(1)

,n). In this lecture we show

that the theory is hard for this complexity class as well. We actually only

show hardness for STA(∗, 2

O(1)

, Σ1) = NEXPTIME,asmostofthemain

ideas are already contained there. This result is originally due to Fischer

and Rabin [42], and the improvement to STA(∗, 2

O(1)

,n) is due to Berman

[14].

The idea is to encode full arithmetic—addition and multiplication—on

integers up to a certain magnitude with short formulas of Th(R, +, ≤).

The language does not contain a predicate that picks out the integers,

and there is no way to deﬁne such a predicate. Quantiﬁers range over reals,

andwehavenowayofsaying“x is an integer” in general. However, we can

say that “x is an integer in the range 0 ≤ x ≤ n” for any large constant n.

In fact, the formula

x =0 ∨ x =1 ∨ x =1+1 ∨ ··· ∨ x =1+···+1



 

(23.1)

does this, albeit very ineﬃciently. We can even encode multiplication on

integers in this range in the same way, just by writing down the multipli-

cation table. However, this is too ineﬃcient an encoding to get a decent

lower complexity bound.