ファイル置き場 Sendai Logic Homepage 101203eguchi

Tohoku University, December 3, 2010

Towards a Theory of Bounded Arithmetic for

Polynomial Space Functions.

Naohi Eguchi

(School of Information Science, JAIST) joint work with Toshiyasu Arai

(Graduate School of Science, Chiba University)

Outline

• Complexity classes defined by Turing machines:

P ⊆ NP = Σ^P₁ ⊆ Σ^P₂ ⊆ · · · ⊆ PSPACE. FP ⊆ _✷^P_{1 ⊆ ✷}^P₂ ⊆ · · · ⊆ FPSPACE.

Outline

• Complexity classes defined by Turing machines:

P ⊆ NP = Σ^P₁ ⊆ Σ^P₂ ⊆ · · · ⊆ PSPACE. FP ⊆ _✷^P_{1 ⊆ ✷}^P₂ ⊆ · · · ⊆ FPSPACE.

• Proof-theoretic characterizations (S. Buss, ’86): FP _{⊆ ✷}^P_{1 ⊆ ✷}^P₂ ⊆ · · · ⊆ FPSPACE.

S₂¹ ⊆ S₂² ⊆ S₂³ ⊆ · · · ⊆ U₂¹.

Outline

• Complexity classes defined by Turing machines:

P ⊆ NP = Σ^P₁ ⊆ Σ^P₂ ⊆ · · · ⊆ PSPACE. FP ⊆ _✷^P_{1 ⊆ ✷}^P₂ ⊆ · · · ⊆ FPSPACE.

• Proof-theoretic characterizations (S. Buss, ’86): FP _{⊆ ✷}^P_{1 ⊆ ✷}^P₂ ⊆ · · · ⊆ FPSPACE.

S₂¹ ⊆ S₂² ⊆ S₂³ ⊆ · · · ⊆ U₂¹.

• Recursion-theoretic characterizations:

F_P F_PSPACE

C (A. Cobham ’64) _U (K. Ueno ’05)

Outline

• Complexity classes defined by Turing machines:

P ⊆ NP = Σ^P₁ ⊆ Σ^P₂ ⊆ · · · ⊆ PSPACE. FP ⊆ _✷^P_{1 ⊆ ✷}^P₂ ⊆ · · · ⊆ FPSPACE.

• Proof-theoretic characterizations (S. Buss, ’86): FP _{⊆ ✷}^P_{1 ⊆ ✷}^P₂ ⊆ · · · ⊆ FPSPACE.

S₂¹ ⊆ S₂² ⊆ S₂³ ⊆ · · · ⊆ U₂¹.

• Recursion-theoretic characterizations:

F_P F_PSPACE

C (A. Cobham ’64) _U (K. Ueno ’05)

S₂¹ This talk

Contents 1. Complexity classes

2. Bounded arithmetic

(Proof-theoretic characterizations) 3. Function algebras

(Recursion-theoretic characterizations) 4. Main results

5. Conclusion

Complexity classes _{P, PSPACE}

P: the class of polynomial time acceptable words. NP: the non-determinisitic counterpart of P.

Σ^P_i (i > 1): the i-th level of the polytime hierarchy. PSPACE: the class of poly-space acceptable words.

Complexity classes _{P, PSPACE}

P: the class of polynomial time acceptable words. NP: the non-determinisitic counterpart of P.

Σ^P_i (i > 1): the i-th level of the polytime hierarchy. PSPACE: the class of poly-space acceptable words. Well kown:

P ⊆ NP = Σ^P₁ ⊆ Σ^P₂ ⊆ · · · ⊆ PSPACE.

Complexity classes _{P, PSPACE}

P: the class of polynomial time acceptable words. NP: the non-determinisitic counterpart of P.

Σ^P_i (i > 1): the i-th level of the polytime hierarchy. PSPACE: the class of poly-space acceptable words. Well kown:

P ⊆ NP = Σ^P₁ ⊆ Σ^P₂ ⊆ · · · ⊆ PSPACE. Open:

P(NP = Σ^P₁(Σ^P₂( · · · (PSPACE? In particular, P ( PSPACE?

Complexity classes _{FP, FPSPACE}

Definition

• ^{FP = ∪}_k^{{f : Nk} → N | f ( ⃗m) is computable by a deterministic Turing machine in a step

bounded by a polynomial in max | ⃗m|}

• ^{FPSPACE = ∪}_k^{{f : Nk} → N | f ( ⃗m) is

computable by a deterministic Turing machine in a space bounded by a polynomial in max | ⃗m|}

Complexity classes _{FP, FPSPACE}

Definition

• ^{FP = ∪}_k^{{f : Nk} → N | f ( ⃗m) is computable by a deterministic Turing machine in a step

bounded by a polynomial in max | ⃗m|}

• ^{FPSPACE = ∪}_k^{{f : Nk} → N | f ( ⃗m) is

computable by a deterministic Turing machine in a space bounded by a polynomial in max | ⃗m|} Fact P = PSPACE ⇐⇒ FP = FPSPACE.

Contents 1. Complexity classes

2. Bounded arithmetic

(Proof-theoretic characterizations) 3. Function algebras

(Recursion-theoretic characterizations) 4. Main results

5. Conclusion

Bounded arithmetic What’s bounded arithmetic

• 1st order theories of bounded arithmetic are essentially very weak fragments of PA.

Bounded arithmetic What’s bounded arithmetic

• 1st order theories of bounded arithmetic are essentially very weak fragments of PA.

• No concreat notions of bounded arithmetic.

• However, ^{T ̸⊢ 2x ↓} for any reasonable theory T of bounded arithmetic.

Bounded arithmetic What’s bounded arithmetic

• 1st order theories of bounded arithmetic are essentially very weak fragments of PA.

• No concreat notions of bounded arithmetic.

• However, ^{T ̸⊢ 2x ↓} for any reasonable theory T of bounded arithmetic.

• Hence, bounded arithmetic can be closely related to complexity classes since

2^x ̸∈ FP, 2^x ̸∈ FPSPACE (initiated by R. Prikh).

Bounded arithmetic _Σ^b_{i -formulas}

Definition ^（Σ^b_i -formulas^） For i > 1, A ∈ Σ^b_i

⇔ A ≡ (∃x1 ⁶ t1)(∀x2 ⁶ t2) · · · (Qxi ⁶ ti)A^′ where A^′ contains only (Qx 6 |t|) quantifiers.

Bounded arithmetic _Σ^b_{i -formulas}

Definition ^（Σ^b_i -formulas^） For i > 1, A ∈ Σ^b_i

⇔ A ≡ (∃x1 ⁶ t1)(∀x2 ⁶ t2) · · · (Qxi ⁶ ti)A^′ where A^′ contains only (Qx 6 |t|) quantifiers.

• Σ^bi is closed under (∀x 6 |t|):

∀x 6 |a|∃y 6 bA(x, y)

→ ∃w 6 t(a, b)∀x 6 |a|A(x, β(x, w)).

Bounded arithmetic _Σ^b_{i -formulas}

Definition ^（Σ^b_i -formulas^） For i > 1, A ∈ Σ^b_i

⇔ A ≡ (∃x1 ⁶ t1)(∀x2 ⁶ t2) · · · (Qxi ⁶ ti)A^′ where A^′ contains only (Qx 6 |t|) quantifiers.

• Σ^bi is closed under (∀x 6 |t|):

∀x 6 |a|∃y 6 bA(x, y)

→ ∃w 6 t(a, b)∀x 6 |a|A(x, β(x, w)).

• However, Σ^bi ^{is not} closed under (∀x 6 t).

Bounded arithmetic S. Buss’s theories Definition Let Φ: a class of formulas, A ∈ Φ.

(Φ-IND):

A(0) ∧ ∀x(A(x) → A(x + 1)) → ∀xA(x), (Φ-PIND):

A(0) ∧ ∀x(A(⌊x/2⌋) → A(x)) → ∀xA(x), Let i > 1.

1. S₂ⁱ := BASIC + Σ^b_i -PIND. 2. T₂ⁱ := BASIC + Σ^b_i -IND.

Bounded arithmetic S. Buss’s theories Definition Let Φ: a class of formulas, A ∈ Φ.

(Φ-IND):

A(0) ∧ ∀x(A(x) → A(x + 1)) → ∀xA(x), (Φ-PIND):

A(0) ∧ ∀x(A(⌊x/2⌋) → A(x)) → ∀xA(x), Let i > 1.

1. S₂ⁱ := BASIC + Σ^b_i -PIND. 2. T₂ⁱ := BASIC + Σ^b_i -IND.

Theorem ^（Buss ’86^） S₂ⁱ ⊆ T₂ⁱ ⊆ S₂ⁱ⁺¹(i > 1).

Bounded arithmetic _Σ^b_i -definable functions Definition Let Φ: a class of formulas,

T : a theory of bounded arithmetic. f is Φ-definable in T

if there exists Af ∈ Φ such that

1. ∀n, m ∈ N, f (⃗n) = m ⇐⇒ N |= Af (⃗n, m). 2. T ⊢ ∀⃗x∃!yAf (⃗x, y).

Bounded arithmetic _Σ^b_i -definable functions Definition Let Φ: a class of formulas,

T : a theory of bounded arithmetic. f is Φ-definable in T

if there exists Af ∈ Φ such that

1. ∀n, m ∈ N, f (⃗n) = m ⇐⇒ N |= Af (⃗n, m). 2. T ⊢ ∀⃗x∃!yAf (⃗x, y).

Theorem ^（Buss ’86^）

1. f ∈ FP ⇔ f is Σ^b₁-definable in S₂¹.

2. f ∈ ✷^p_i ^{⇔ f is Σb}i -definable in S₂ⁱ (i > 1).

Contents 1. Complexity classes

2. Bounded arithmetic

(Proof-theoretic characterizations) 3. Function algebras

(Recursion-theoretic characterizations) 4. Main results

5. Conclusion

Function algebras Cobham’s class Definition C is the smallest class containing

O(⃗x) = 0, I_j^k(⃗x) = xj, C0(x) = 2x, C1(x) = 2x + 1, #(x, y) = 2^|x|·|y| and closed under composition and

bounded recursion on notation (BRN): f (0, ⃗x) = g(⃗x),

f (Ci(y), ⃗x) = hi(y, ⃗x, f (y, ⃗x)) (i = 0, 1), f (y, ⃗x) 6 j(y, ⃗x).

Function algebras Cobham’s class Definition C is the smallest class containing

O(⃗x) = 0, I_j^k(⃗x) = xj, C0(x) = 2x, C1(x) = 2x + 1, #(x, y) = 2^|x|·|y| and closed under composition and

bounded recursion on notation (BRN): f (0, ⃗x) = g(⃗x),

f (Ci(y), ⃗x) = hi(y, ⃗x, f (y, ⃗x)) (i = 0, 1), f (y, ⃗x) 6 j(y, ⃗x).

Theorem ^（Cobham ’64^） C = FP.

Function algebras _Σ^b₁-definablity (revisited) Theorem f ∈ C ⇔ f is Σ^b₁-definable in S₂¹.

(⇒): Straightforward (by induction over f ∈ C). Important:

Σ^b₁ is closed under (∀x 6 |t|).

Function algebras _Σ^b₁-definablity (revisited) Theorem f ∈ C ⇔ f is Σ^b₁-definable in S₂¹.

(⇒): Straightforward (by induction over f ∈ C). Important:

Σ^b₁ is closed under (∀x 6 |t|). This enables S₂¹:

to Σ^b₁-define f in case f is defined by BRN.

Function algebras _Σ^b₁-definablity (revisited) Theorem f ∈ C ⇔ f is Σ^b₁-definable in S₂¹.

(⇒): Straightforward (by induction over f ∈ C). Important:

Σ^b₁ is closed under (∀x 6 |t|). This enables S₂¹:

to Σ^b₁-define f in case f is defined by BRN. (⇐): Harder than (⇒).

Function algebras Witnessing method Theorem f ∈ C ⇔ f is Σ^b₁-definable in S₂¹.

(⇐): Shown by witnessing method. Lemma ^（Witnessing Lemma^）

Let Ai: Σ^b₁-formula ∃xBi(x) (1 6 i 6 k + l).

Suppose: S₂¹ ⊢ A1, . . . , Ak ⇒ Ak+1, . . . , Ak+l. Then there exist f1, . . . , fl ∈ C such that

S₂¹ ⊢ B1(x1), . . . , Bk(xk) ⇒

Bk+1(f1(⃗x)), . . . , Bk+l(fl(⃗x)).

Function algebras Witnessing method Theorem f ∈ C ⇔ f is Σ^b₁-definable in S₂¹.

(⇐): Shown by witnessing method. Lemma ^（Witnessing Lemma^）

Let Ai: Σ^b₁-formula ∃xBi(x) (1 6 i 6 k + l).

Suppose: S₂¹ ⊢ A1, . . . , Ak ⇒ Ak+1, . . . , Ak+l. Then there exist f1, . . . , fl ∈ C such that

S₂¹ ⊢ B1(x1), . . . , Bk(xk) ⇒

Bk+1(f1(⃗x)), . . . , Bk+l(fl(⃗x)).

Function algebras Ueno’s class Definition U is the smallest class containing

O, I_j^k, C0, C1, #,

and closed under composition, BRN and bounded recursion (BR):

f (0, ⃗x) = g(⃗x),

f (y + 1, ⃗x) = h(y, ⃗x, f (y, ⃗x)), f (y, ⃗x) 6 j(y, ⃗x).

Function algebras Ueno’s class Definition U is the smallest class containing

O, I_j^k, C0, C1, #,

and closed under composition, BRN and bounded recursion (BR):

f (0, ⃗x) = g(⃗x),

f (y + 1, ⃗x) = h(y, ⃗x, f (y, ⃗x)), f (y, ⃗x) 6 j(y, ⃗x).

Theorem ^（Ueno ’05^） U = FPSPACE.

Corollary FP = FPSPACE ⇔ FP is closed under BR.

Contents 1. Complexity classes

2. Bounded arithmetic

(Proof-theoretic characterizations) 3. Function algebras

(Recursion-theoretic characterizations) 4. Main results

5. Conclusion

Main results _Σ^seq_{1 , T2}^1,seq

We introduce:

1. a new class Σ^seq₁ (⊇ ^∪_i Σ^b_i ), 2. a new theory T₂^1,seq (⊇ ^∪_i S₂ⁱ )

s.t.

Conjecture f ∈ U ⇔ f is Σ^seq₁ -definable in T₂^1,seq.

Main results _Σ^seq_{1 , T2}^1,seq

We introduce:

1. a new class Σ^seq₁ (⊇ ^∪_i Σ^b_i ), 2. a new theory T₂^1,seq (⊇ ^∪_i S₂ⁱ )

s.t.

Conjecture f ∈ U ⇔ f is Σ^seq₁ -definable in T₂^1,seq.

• (⇒): already presented at Proof Theory Meeting 2009.

• (⇐): still unfinished, but almost finished.

Main results _Σ^seq_{1 , T2}^1,seq

We introduce:

1. a new class Σ^seq₁ (⊇ ^∪_i Σ^b_i ), 2. a new theory T₂^1,seq (⊇ ^∪_i S₂ⁱ )

s.t.

Theorem f ∈ U ⇔ f is Σ^seq₁ -definable in T₂^1,seq.

• (⇒): already presented at Proof Theory Meeting 2009.

• (⇐): still unfinished, but almost finished.

Main results _Σ^seq_{1 -formulas}

Extend the language by adding function symbols β, Len, . . . and variables X, Y, Z, . . . of higher types. 1. Each X encodes a sequence of exponential length. 2. Each element of X has a polynomial growth-rate.

Main results _Σ^seq_{1 -formulas}

Extend the language by adding function symbols β, Len, . . . and variables X, Y, Z, . . . of higher types. 1. Each X encodes a sequence of exponential length. 2. Each element of X has a polynomial growth-rate.

Definition ^（Σ^seq₁ -formulas^） 1. Σ^seq₀ := ^∪_i Σ^b_i .

2. A ∈ Σ^seq₀ ⇒ (∃X^6t,6s)A ∈ Σ^seq₁ , where

Main results _Σ^seq_{1 -formulas}

Extend the language by adding function symbols β, Len, . . . and variables X, Y, Z, . . . of higher types. 1. Each X encodes a sequence of exponential length. 2. Each element of X has a polynomial growth-rate.

Definition ^（Σ^seq₁ -formulas^） 1. Σ^seq₀ := ^∪_i Σ^b_i .

2. A ∈ Σ^seq₀ ⇒ (∃X^6t,6s)A ∈ Σ^seq₁ , where (∃X^6t,6s)A denotes

∃_X(∀j < Len(X))β(j, X) 6 t ^∧ Len(X) 6 s ^{∧ A}.

Main results _{Theory T2}^1,seq

Definition

T₂^1,seq := BASIC + BASIC^seq + Σ^seq₁ -IND.

Main results _{Theory T2}^1,seq

Definition

T₂^1,seq := BASIC + BASIC^seq + Σ^seq₁ -IND.

Theorem f ∈ U ⇔ f is Σ^seq₁ -definable in T₂^1,seq. (⇒): Straightforward (by induction over f ∈ U ). Important:

Σ^seq₁ is closed under (∀x 6 t) in contrast to Σ^b_i .

Main results _{Theory T2}^1,seq

Definition

T₂^1,seq := BASIC + BASIC^seq + Σ^seq₁ -IND.

Theorem f ∈ U ⇔ f is Σ^seq₁ -definable in T₂^1,seq. (⇒): Straightforward (by induction over f ∈ U ). Important:

Σ^seq₁ is closed under (∀x 6 t) in contrast to Σ^b_i . This enables T₂^1,seq:

to Σ^seq₁ -define f in case f is defined by BR.

Main results _Difficulty

Theorem f ∈ U ⇔ f is Σ^seq₁ -definable in T₂^1,seq. (⇐): Much harder than (⇒).

Difficulty:

Σ^seq₁ -formulas are not witnessed by functions from U

Main results _Difficulty

Theorem f ∈ U ⇔ f is Σ^seq₁ -definable in T₂^1,seq. (⇐): Much harder than (⇒).

Difficulty:

Σ^seq₁ -formulas are not witnessed by functions from U

• since the witness of a Σ^seq1 -formula (∃X^6t,6s)A does not range over N.

• Hence, the witnessing method does not work.

Main results _Difficulty

Theorem f ∈ U ⇔ f is Σ^seq₁ -definable in T₂^1,seq. (⇐): Much harder than (⇒).

Difficulty:

Σ^seq₁ -formulas are not witnessed by functions from U

• since the witness of a Σ^seq1 -formula (∃X^6t,6s)A does not range over N.

• Hence, the witnessing method does not work.

Solution: Extend U to a class U^seq of functions on sequences on N.

Main results Important lemmas Lemma ^（Witnessing Lemma^）

Let Ai: Σ^seq₁ -formula ∃XBi(X) (1 6 i 6 k + l). Suppose:

T₂^1,seq ⊢ A1, . . . , Ak ⇒ Ak+1, . . . , Ak+l. Then there exist F1, . . . , Fl ∈ U^seq such that T₂^1,seq ⊢ B1(X1), . . . , Bk(Xk) ⇒

Bk+1(F1( ⃗X)), . . . , Bk+l(Fl( ⃗X)).

Main results Important lemmas Lemma ^（Witnessing Lemma^）

Let Ai: Σ^seq₁ -formula ∃XBi(X) (1 6 i 6 k + l). Suppose:

T₂^1,seq ⊢ A1, . . . , Ak ⇒ Ak+1, . . . , Ak+l. Then there exist F1, . . . , Fl ∈ U^seq such that T₂^1,seq ⊢ B1(X1), . . . , Bk(Xk) ⇒

Bk+1(F1( ⃗X)), . . . , Bk+l(Fl( ⃗X)).

Main results Important lemmas Lemma ^（Witnessing Lemma^）

Let Ai: Σ^seq₁ -formula ∃XBi(X) (1 6 i 6 k + l). Suppose:

T₂^1,seq ⊢ A1, . . . , Ak ⇒ Ak+1, . . . , Ak+l. Then there exist F1, . . . , Fl ∈ U^seq such that T₂^1,seq ⊢ B1(X1), . . . , Bk(Xk) ⇒

Bk+1(F1( ⃗X)), . . . , Bk+l(Fl( ⃗X)). Lemma For every F ∈ U^seq, there exists f ∈ U such that β(y, F (⃗x)) = f (⃗x, y).

Conclusion _Summary

We introduced:

a new class Σ^seq₁ and a higher type extension T₂^1,seq of 1st order theories of bounded arithmetic such that

• f ∈ F^{PSPACE ⇔ f is Σseq}1 -definable in T₂^1,seq.

• F^P ⊆ ✷^P1 ⊆ ✷^P2 ⊆ · · · ⊆ FPSPACE. S₂¹ ⊆ S₂² ⊆ S₂³ ⊆ · · · ⊆ T₂^1,seq.

•

FP FPSPACE

C (A. Cobham ’64) _U (K. Ueno ’05)

S₂¹ T₂^1,seq

Conclusion Future works 1. Connections to a 2nd order theory U₂¹ of bounded arithmetic (S. Buss) which captures FPSPACE, or a 3-sorted theory W₁¹ of Cook style bounded

arithmetic (A. Skelley) which caputures F_PSPACE. 2. Characterizations of smaller classes on space

complexity, e.g., linear space, logarithmic space, ....

3. Applications: What can be formalized in T₂^1,seq nicely?