Kozen D.C. Theory of Computation

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

Lower Bound for the Theory of Real Addition 147

To get the lower complexity bound we want, we show how to encode

full arithmetic on integers in the range 0 ≤ x<2

with formulas of length

O(n). This allows us to manipulate bit strings of length 2

with short

formulas and index into them to extract their bits, which in turn allows

us to describe computation histories of exponential-time machines, thereby

encoding the halting problem for such machines.

Constructing Short Formulas for Large Integers

We make use of a trick due to Fischer and Rabin [42] for constructing

short formulas for full arithmetic on large integers. We illustrate the trick

by constructing a formula of length O(n)thatsaysx =2

. We actually

construct inductively a formula ψ

(x, z)thatsaysx =2

z.Thenx =2

is expressed by ψ

(x, 1).

Here is an inductive construction that produces formulas that are ex-

ponentially smaller than (23.1), although still too big:

(x, z)

def

⇐⇒ x = z + z, (23.2)

n+1

(x, z)

def

⇐⇒ ∃yψ

(x, y) ∧ ψ

(y, z). (23.3)

Note that we have used only addition +, thus the ψ

are syntactically

correct. Under this deﬁnition, the ψ

express the desired property:

(x, z) ⇔ x = z + z ⇔ x =2

and by induction,

n+1

(x, z) ⇔∃yψ

(x, y) ∧ ψ

(y, z)

⇔∃yx=2

y ∧ y =2

⇔ x =2

n+1

The problem is that ψ

appears twice in the inductive deﬁnition (23.3) of

n+1

, so the length of ψ

n+1

is roughly twice the length of ψ

.Thusthe

formulas ψ

grow exponentially with n.

Here is where the trick comes in. We use universal quantiﬁcation to

write ψ

n+1

with only one occurrence of ψ

. Instead of the deﬁnition (23.3),

we take

n+1

(x, z)

def

⇐⇒

∃y ∀u ∀v ((u = x ∧ v = y) ∨ (u = y ∧ v = z)) → ψ

(u, v).

This says the same thing, but now ψ

n+1

contains only one occurrence of

, so its length is that of ψ

plus a constant. Thus the formulas ψ

grow

only linearly with n.

148 Lecture 23

Encoding Multiplication

Let

def

= {z | z is an integer and 0 ≤ z<2

We now show how to construct a formula of length O(n)thatsays,“z ∈ I

and x = yz.” The basis is given by:

mult

(x, y, z)

def

⇐⇒ (z =0∧ x =0)∨ (z =1∧ x = y). (23.4)

Before we give the induction step, let us prove a motivating lemma.

Lemma 23.1 I

n+1

= {z

+ z

| z

∈ I

, 1 ≤ i ≤ 4}.

Proof. (⊇) The sum of four integers in the range 0 ≤ z

< 2

must be

an integer and cannot be less than 0 nor more than

− 1)(2

− 1) + (2

− 1) = 2

n+1

− 1.

( ⊆)If0≤ z<2

n+1

, and if we divide z by 2

using

integer division with remainder, we obtain z =2

q + r,0≤ q<2

,and

0 ≤ r<2

.Thus

z =(2

− 1)q + q + r.

This gives us a way of deﬁning mult

n+1

inductively in terms of mult

By Lemma 23.1,

z ∈ I

n+1

∧ x = yz

⇔∃z

∃z



i=1

∈ I

∧ z = z

+ z

∧ x = yz

+ yz

⇔∃z

∃z

∃s ∃t ∃u ∃v ∃wz= s + z

+ z

∧ x = u + v + w

∧



i=1

∈ I

∧ s = z

∧ t = yz

∧ u = tz

∧ v = yz

∧ w = yz

⇔∃z

∃z

∃s ∃t ∃u ∃v ∃wz= s + z

+ z

∧ x = u + v + w

∧ mult

(s, z

) ∧ mult

(t, y, z

) ∧ mult

(u, t, z

)

∧ mult

(v, y, z

) ∧ mult

(w, y, z

The last of these formulas is semantically correct but way too large, because

it involves ﬁve occurrences of mult

; however, we can combine these into

Lower Bound for the Theory of Real Addition 149

one occurrence using the Fischer–Rabin trick. We deﬁne mult

n+1

(x, y, z)

to be the resulting formula.

Once we have deﬁned mult

, we can express membership in the set I

with the formula

(x)

def

⇐⇒ mult

(x, 1,x).

Bitstring Manipulation

Once we know how to deﬁne and manipulate large integers with short

formulas, we are on our way to manipulating long bitstrings. Here are

some useful formulas that will help us with this task.

• Integer division with remainder: “y, q, r ∈ I

, q is the quotient and r

the remainder obtained when dividing x by y”=“y, q, r ∈ I

∧ x =

yq + r ∧ 0 ≤ r<y”:

intdiv

(x, y, q, r)

def

⇐⇒ I

(q) ∧ I

(r) ∧∃u mult

(u, q, y)

∧ x = u + r ∧ 0 ≤ r<y

rem

(x, y, r)

def

⇐⇒ ∃q intdiv

(x, y, q, r).

• “x, y ∈ I

and y divides x”:

div

(y, x)

def

⇐⇒ rem

(x, y, 0).

• “x ∈ I

and x is even”:

even

(x)

def

⇐⇒ div

(2,x).

Here 2 is an abbreviation for 1 + 1.

• “p ∈ I

and p is prime”:

prime

(p)

def

⇐⇒ I

(p) ∧∀z div

(z,p) → (z =1 ∨ z = p).

• “y has no odd factors less than 2

except 1”:

power2

(y)

def

⇐⇒ ∀z div

(z,y) → (z =1 ∨ even

(z)).

For numb ers y ∈ I

,thissaysthaty is a power of 2.

150 Lecture 23

• “x, y ∈ I

, y is a power of two, say 2

,andthekth bit of the binary

representation of x is 1”:

bit

(x, y)

def

⇐⇒ I

(x) ∧ I

(y) ∧ power2

(y)

∧∀q ∀r (intdiv

(x, y, q, r) →¬even

(q)).

Here is an explanation of the formula bit

(x, y). Suppose x and y are num-

bers satisfying bit

(x, y). Because y is a power of two, its binary represen-

tation consists of a 1 followed by a string of zeros. The formula bit

(x, y)

is true precisely when x’s bit in the same position as the 1 in y is 1. We

get hold of this bit in x by dividing x by y using integer division; the quo-

tient q and remainder r are the binary numbers illustrated. The bit we are

interested in is 1 iﬀ q is odd.

y = 1000000000000

x = 11011001



 

010001011011

  

This formula is useful for treating numbers as bit strings of exponential

length and indexing into them with other numbers to extract bits.

Now we can use this capability to write a formula ϕ

M,x

(w)thatex-

presses the fact that w is a bitstring of exponential length encoding an

accepting computation history of a nondeterministic exponential-time-

bounded Turing machine M on input x.ThenM accepts x iﬀ R 

∃wϕ

M,x

(w). The accepting computation history is a sequence of expo-

nentially many conﬁgurations of M beginning with the start conﬁguration

on input x and ending with an accepting conﬁguration such that each suc-

cessive conﬁguration follows from the previous according to the transition

rules of M. A string of exponential length is used as a yardstick to compare

corresponding bits of adjacent conﬁgurations. The construction of ϕ

M,x

(w)

is fairly standard using the tools we have provided; for a detailed account,

see the proof of G¨odel’s incompleteness theorem as given in Lectures 38

and 39 of [76]. The only diﬀerence here is that because of the bound on the

length of strings we can talk about, we can only encode accepting compu-

tation histories of Turing machines running in exponential time.

Lecture 24

Lower Bound for Integer Addition

The theory of integer addition, Th(Z, +, ≤), also known as Presburger arith-

metic, is complete for the complexity class STA(∗, 2

O(1)

,n)—one expo-

nential up from Th(R, +, ≤). In this lecture we describe how to obtain the

lower bound.

The decidability of Presburger arithmetic is due to Presburger [98]. The

precise upper and lower bounds are due to Berman [14], based on work of

Fischer and Rabin [42], Cooper [33], Oppen [91], and Ferrante and Rackoﬀ

[41].

As with Th(R, +, ≤), the trick is to encode full arithmetic—addition and

multiplication—on large integers with short formulas. Intepreting integers

as bit strings, this enables us to describe accepting computation histories

of time-bounded Turing machines.

The main diﬀerence between Th(Z, +, ≤) and Th(R, +, ≤) is that quan-

tiﬁers in Th(Z, +, ≤) range over Z,sowedonothavetoencodethisaswe

did with Th(R, +, ≤). This allows us to encode full arithmetic on integers

in the range 0 ≤ x<2

with formulas of length O(n), which in turn

allows us to encode computation histories of Turing machines running in

double-exponential time.

152 Lecture 24

Encoding Huge Numbers

Recall from Lecture 23 the deﬁnition

= {z | z is an integer and 0 ≤ z<2

Let





p∈I

p prime

the product of all the primes less than 2

. By [51, Theorem 414, p. 341],



≥ 2

for some constant c>0; so for n ≥ 1+loglog

, 

≥ 2

n−1

We can deﬁne the number 

with a short formula:

(x)

def

⇐⇒ x ≥ 1 ∧∀p (prime

(p) → div

(p, x))

∧∀y ≥ 1(∀p (prime

(p) → div

(p, y))) → x ≤ y.

In other words, 

is the least positive integer divisible by all primes less

than 2

. Once we have deﬁned 

,wecansaythatx is an integer in the

range 0 ≤ x<

by just saying ∃L

() ∧ 0 ≤ x<.Herewearealso

using the fact that variables range over integers, which was not true with

Th(R, +, ≤).

Chinese Remaindering

The Chinese remainder theorem (Theorem B.1) says that we can do arith-

metic on numbers modulo 

by doing arithmetic on their remainders mod-

ulo primes less than 2

We can express that r is the remainder of x modulo a prime p<2

with the predicate rem

(x, p, r) deﬁned in Lecture 23. However, to get the

higher complexity bound, we must amend the deﬁnition slightly to avoid

saying anything about the size of x. We therefore redeﬁne

intdiv

(x, y, q, r)

def

⇐⇒ ∃u mult

(u, q, y) ∧ x = u + r ∧ 0 ≤ r<y. (24.1)

Here we are taking advantage of the fact that quantiﬁers range over integers,

so that we do not have to include the predicates I

(q)andI

(r). We also

amend the deﬁnition of bit

(x, y) to replace the subexpression I

(x) ∧

(y)withx<

∧ y<

. The deﬁnitions of the other predicates—

rem

(x, y, r), div

(y, x), and so on—are the same. The inductive deﬁnition

of mult

(u, q, y) given in Lecture 23 constrains y to be in I

, but does not

say anything about u and q.Thusintdiv

(x, y, q, r), deﬁned as in (24.1),

says nothing about the size of x or q.Consequently,div

(y, x), although

constraining y to be in I

, says nothing about x.

Lower Bound for Integer Addition 153

Write x ≡ y (mod p)ifx and y are congruent modulo p;thatis,ifp

divides x − y. The Chinese remainder theorem says that x ≡ yz (mod 

)

iﬀ for all primes p<2

, x ≡ yz (mod p). For p<2

, we can express

x ≡ yz (mod p)usingmult

and div

mult

mod

(x, y, z, p)

def

⇐⇒ ∃u ∃v mult

(u, y, v) ∧ div

(p, x − u) ∧ div

(p, z − v).

This does not place any size constraints on x, y,orz, because mult

does

not care how big its ﬁrst two arguments are (it does care how big its third

argument is, which is why we need the v), and div

does not care how big

its second argument is. Also, we have used the subtraction operator in the

above deﬁnition, but we can express subtraction because we can express

addition:

z = x − y

def

⇐⇒ x = y + z.

We can now deﬁne a multiplication predicate that expresses x ≡

yz (mod 

mult



(x, y, z)

def

⇐⇒ ∀p prime

(p) → mult

mod

(x, y, z, p).

This is all the machinery we need to do full arithmetic on numbers in

the range 0 ≤ x ≤ 2

with formulas of length O(n). The rest of the

construction is the same as in Lecture 23.

Lecture 25

Automata on Inﬁnite Strings and S1S

Here is a logical theory that is decidable, but not in elementary time;that

is, not in any time bounded by a stack of exponentials

of any ﬁxed height. It is the monadic second-order theory of successor

(S1S). This is the set of true statements about the natural numbers

ω = {0, 1, 2,...} expressible in a language with a symbol s for the suc-

cessor function and allowing quantiﬁcation over elements and subsets of

ω.Thetermsecond-order refers to the fact that we allow quantiﬁcation

over relations, not just individual elements. The term monadic means that

we allow quantiﬁcation only over sets (monadic or unary relations). If we

allow quantiﬁcation over dyadic (binary) relations, the theory becomes un-

decidable. The theory S1S was originally shown to be decidable by B¨uchi

[23, 24]. The result was generalized to the monadic second-order theory of

n successors (SnS) by Rabin [99].

The structure in question is (ω,s, ∈), where ω is the set of natural

numbers, s is the successor function x → x+1, and ∈⊆ω ×2

is the usual

membership relation between elements and sets. The variables x,y,z,...

range over elements and X,Y,Z,... range over sets, and quantiﬁcation is

allowed over both types of variables.

Here are some predicates deﬁnable in this language.

Automata on Inﬁnite Strings and S1S 155

• “x = y”: ∀Xx∈ X ↔ y ∈ X.

• “X ⊆ Y ”: ∀xx∈ X → x ∈ Y .

• “X = Y ”: X ⊆ Y ∧ Y ⊆ X.

• “x = 0”: ∀y ¬(x = sy); in other words, x has no predecessor.

• “x = 1”: x = s0. Because we can deﬁne 0, we can use 0 informally as

if it were a symbol in the language.

• “x ≤ y”:

∀X (x ∈ X ∧(∀zz∈ X → sz ∈ X)) → y ∈ X.

In other words, any set X that contains x and is closed under suc-

cessor also contains y.

• “X is ﬁnite”: ∃x ∀yy∈ X → y ≤ x.

Automata on Inﬁnite Strings

We prove the decidability of S1S using automata on inﬁnite strings. We

deﬁne three types of such automata, namely B¨uchi, Rabin ,andMuller.

These automata are similar in most respects, but diﬀer in the form of their

acceptance conditions.

Let Σ be a ﬁnite alphabet, and let Σ

denote the set of inﬁnite strings

··· over Σ. If |Σ|≥2, then Σ

is uncountable—it contains as many

elements as there are real numbers. These are the inputs to our automata.

A nondeterministic B¨uchi automaton is a structure

M =(Q, Σ,δ,s,F),

where Q is a ﬁnite set of states, δ ⊆ Q × Σ × Q is the transition relation,

s ∈ Q is the start state, and F ⊆ Q is the set of accept states.

The transition (p, a, q) ∈ δ means that M can move from state p to

state q under input symbol a.ThemachineM is deterministic if δ is single-

valued; that is, if it is equivalent to a function δ : Q × Σ → Q.

A run of M on input a

···∈Σ

is a sequence q

···∈Q

such

that

• q

= s;

• (q

i+1

) ∈ δ, i ≥ 0.

156 Lecture 25

If M is deterministic, there is a unique run on each input string. If M is

nondeterministic, there could be anywhere from zero to uncountably many

runs on a given input string.

The IO set of a run σ, denoted IO(σ), is the set of states of Q that

appear in σ inﬁnitely often. Formally, if σ = q

···,then

IO(σ)

def

= {q ∈ Q | q = q

for inﬁnitely many i},

or equivalently,

IO(σ)

def



n≥0

| i ≥ n}.

ArunofaB¨uchi automaton is an accepting run if its IO set intersects

F ; that is, if IO(σ)∩F = ∅.Astringisaccepted by M if it has an accepting

run. The set of strings in Σ

accepted by M, denoted L(M), is the set of

strings that have accepting runs:

L(M)

def

= {x ∈ Σ

| there is a run σ of M on x such that

IO(σ) ∩ F = ∅}.

Example 25.1 Here is a deterministic B¨uchi automaton that accepts the set

{x ∈{a, b, c}

| every a is followed sometime later by a b}

= c

+(a + b + c)

∗

b(b + c)

+((a + c)

∗

b, c

a, c

ssg











(The short arrow indicates the start state and a circle around a state indi-

cates that it is an accept state.) 2

Example 25.2 Here is a nondeterministic B¨uchi automaton that accepts the set (0+1)

∗

the set of inﬁnite strings over the alphabet {0, 1} with only ﬁnitely many

occurrences of 1.

0, 1

ssg









This was the original deﬁnition used by B¨uchi to prove that S1S is decid-

able. Unfortunately, the acceptance condition is not quite general enough

for our needs, because it turns out that nondeterministic and determinis-

tic B¨uchi automata are not equivalent. For example, the set of Example

25.2 is not accepted by any deterministic B¨uchi automaton (Homework 8,

Exercise 1).