Search problems in T22
Toshiyasu Arai (Chiba) Jan. 21, 2011
Abstract
In this talk we will introduce a class of search problems, called nested Polynomial Local Search(nPLS) problems to characterize TFNP(T22).
1 Search problems: TFNP
Consider the language of the bounded arithmetic with function symbols for polytime computable functions, and let R(x, y) be a Σb0-formula(literal) in this language.
For a polynomial p, suppose
N |= ∀x∃y < 2p(|x|) R(x, y).
The related search problem, TFNP [Megiddo-Papadimitriou1991] is, given x, to find a witness y such that R(x, y).
Let T be a bounded arithmetic. The problem is to character- ize the class of search problems, denoted TFNP(T ), such that T proves its totality,
T # ∀x∃y < 2p(|x|) R(x, y)
and thereby to characterize Σb1-definable (multivalued) functions in T .
S2i+1 ≡Σb
i+1 T
i
2 = basic axioms+induction axioms for Σbi-formulas. [Buss-Kraj´ıˇcek1994] proved that TFNP(T21) = PLS, Polyno- mial Local Search problems. A problem P of PLS consists in polytime computable predicates and functions F, i, N, c:
1. F (x) = {s : F (x, s)} (search space, feasible points) s ∈ F (x) → |s| ≤ d(|x|) with a polynomial d.
2. initial point function i(x) ∈ F (x). 3. neighborhood function N (x, s)
s ∈ F (x) → N (x, s) ∈ F (x). 4. cost function c(x, s)
N(x, s) = s ∨ c(x, N (x, s)) < c(x, s). An s is a solution of the instance x iff
s ∈ F (x) ∧ N (x, s) = s.
T21 # ∀x∃s < 2d(|x|)[s ∈ F (x) ∧ N (x, s) = s]
T21 # there exists an s ∈ F (x) with a (globally) minimal cost. Next let us consider TFNP(T22).
• colored PLS problems[Kraj´ıˇcek-Skelly-Thapen2007]
• 2-turn games[Skelly-Thapen∞]
• Πp1-PLS problems with Πp0-goals[Beckmann-Buss∞1], [Beckmann-Buss∞2]
• nPLS
2 nested PLS
In an nPLS the neighborhood function is replaced by a polytime predicate N (x, s, t) such that the set of neighbors {t : N (x, s, t)} is exponentially large. In other words, given (x and) s, to find a t s.t.
s →N t(:⇔ N (x, s, t))
is another search problem S(x, s), which is generated by s.
For a solution y of S(x, s), a result extracting function Ux,s(y) computes a neighbor t to s:
y →N y ⇒ s →N Ux,s(y) = t
An nPLS problem P = -d; S, T , N ; N, i, t, c, S, U, rk. where d(x) is a polynomial, and other ingredients are polytime com- putable.
1. S(x, s) and T (x, s, t) for sources and targets, resp. with a polynomial bound d.
S(x) = {s : S(x, s)} and T (x) = !{T (x, s) : s ∈ S(x)} with T (x, s) = {t : T (x, s, t)}
N (x, s, y, z) for neighborhoods.
2. N (x, s, y), i(x), t(x, s), c(x, s), S(x, s, y), U (x, s, y, z) and rk(x, s) for neighborhoods of rank zero, initial source, initial target, cost, generated source, extracted result and rank.
Table 1: nPLS sources s targets T (x, s)
i(x)
s t(x, s) y →N U(x, s, y, z) →N · · · →N u S(x, s, y) solution z →N z
• row s : a search problem in the search space T (x, s) (higher rows are search problems in higher ranks).
• Given a y ∈ T (x, s), generate a lower rank source S(x, s, y) and search a solution z of the problem S(x, s, y) to get a neigh- bor U (x, s, y, z) of y in a lower cost.
• Continue this search to find a solution u of the problem s.
If s is not the highest rank problem, then extract a result from the solution u to find a neighbor of a higher rank target, and so forth.
1. y →N z for y, z ∈ T (x, s) designates N (x, s, y, z).
rk(x, s) > 0∧y ∈ T (x, s) ⇒ y →N y∨rk(x, S(x, s, y)) < rk(x, s) 2.
rk(x, s) > 0 ∧ z →N z for S(x, s, y) ⇒ y →N U(x, s, y, z) 3.
y →N z ⇒ y = z ∨ c(x, y) > c(x, z)
Let P be an nPLS. Then we write
y = P(x) :⇔ N (x, i(x), y, y).
Lemma 2.1 Let P = -d; S, T , N ; N, i, t, c, S, U, rk. be an nPLS in S21. Then
T22 # ∀x∃y < 2d(|x|)[y = P(x)].
Proof. Argue in T22. We show by induction on the ranks a that
∀s ∈ S(x)∃y ∈ T (x, s)[rk(x, s) ≤ a ⇒ y →N y] (1) First consider the case a = 0. Then (1) is equivalent to the totality of a PLS problem, which is provable in T1.
Now suppose that (1) holds for any b < a and a > 0, and assume that s ∈ S(x) and rk(x, s) = a.
Let c be the minimal cost of the targets in T (x, s):
c := min{c : ∃y < 2d(|x|)[y ∈ T (x, s) ∧ c(x, y) = c]}.
Pick a y ∈ T (x, s) such that c(x, y) = c. We claim that y →N y. Assume y →N z. Then either y = z or c(x, y) > c(x, z). The minimality of c forces us to have y = z.
It remains to show the existence of a u such that y →N u. By IH find a solution z ∈ T (x, S(x, s, y)) of the problem S(x, s, y) in lower rank, z →N z. Then y →N U(x, s, y, z).
!
3 NP search problems in T22
Theorem 3.1 If T22 # ∀x∃y R(x, y) for a polytime computable R, then we can find an nPLS P in S21 such that
S21 # y = P(x) → R(x, U0(y))
for a polytime computable result extracting function U0.
Suppose a T22-derivation of a Σb1-formula ∃y < t(x) R(x, y) is given.
Formulate T22 in a one-sided sequent calculus, in which
Γ, A(0) Γ, x /< s0, ¬B(a, x), A(a + 1) Γ, x /< s0, ¬B(t, x)
Γ (Σb2-ind)
for Σb2-formula A(a) ≡ ∃x < s0 B(a, x) where B(a, x) is a Πb1- formula. By a Πb0-formula or a Σb0-formula we mean a literal.
By eliminating cut inferences partially, we can assume that any formula occurring in the derivation is a Σb2-formula.
Now pick a binary numeral ¯x arbitrarily, and substitute ¯x for the parameter x in the end-formula ∃y < t(x) R(x, y). Moreover unfold the inference rules (Σb2-ind) using cut inferences:
· · · Γ, ¬B(¯n) · · · (n < s0) ∃x < s0B(x), Γ
Γ (Σb2-cut)
Unfold the combination of inference rules for bounded universal quantifiers followed by ones for bounded existential quantifiers to the following:
· · · Γ, ∃x < s0∀y < s1 L(x, y), L(t, ¯n) · · · (n < s1)
Γ, ∃x < s0∀y < s1 L(x, y) (Σ
b2)
This results essentially in a propositional derivation D of ∃y < t(¯x) R(¯x, y). Inference rules in D are (Σb2-cut), (Σb2) and (Σb1)
Γ, ∃x < t L(x), L(s) (s < t)
Γ, ∃x < t L(x) (Σ
b1)
s a closed term such that s < t is true.
Each upper sequent contains its lower sequent. (2) There occurs no free variable in D. Initial sequents in D are
Γ, L for true literals L.
Let d be a polynomial such that the size of D(the number of occurrences of symbols in D) is bounded by 2d(|x|), and the depth of D is bounded by d(|x|).
Each sequent in D consists of Σb2, Σb1 and Σb0(literals) sentences: Γ = Γ(Σb2), Γ(Σb1), Γ(Σb0)
where Γ(Σbk) ⊆ Σbk for k = 1, 2.
Let T (D) ⊂ <ωω denote a naked tree of D. kb : T (D) 2 σ 3→ kb(x, σ), which is compatible with the Kleene-Brouwer ordering
<KB on T (D):
σ, τ ∈ T (D) & σ <KB τ ⇒ kb(x, σ) < kb(x, τ ) (3)
Seqσ for σ ∈ D(T ) denotes the sequent situated at the node σ. Let σ be a node in the tree T (D) such that
Seqσ contains no true literal. (4) Let us view such a node σ as a search problem in searching a witness for a Σb1-formula in Seqσ(Σb1). S(x) consists in left upper sequents of (Σb2-cut) σ with (4) and the bottom ∅.
The algorithm is based on the following simple observation.
Proposition 3.2 Let σ be a node in the tree T (D) enjoying the condition (4). Then there exists a τ ⊇ σ on the rightmost branch in the upper part of σ such that either Seqτ is a lower sequent of a (Σb1) whose auxiliary formula is true, or Seqτ is a lower sequent of a (Σb2). Moreover the lowest such node τ = t(x, σ) is polytime computable.
Three cases to consider according to the principal formula A ≡
∃x < t B(x) of the lowest τ = t(x, σ). λ denotes the vanishing point of the principal formula.
1. A is the end-formula ∃y < t(¯x) R(¯x, y). Then we are done, and the value of its witnessing term s is a witness sought.
2.
S(x, σ, τ ) := κ <KB σ
· · · κ : Γ, ¬B(¯n) · · ·
· · · A, ∆0, L(¯n, m¯ ) · · ·
τ : A, ∆0 (Σb2) A,.... Γ
λ : Γ (Σb2-cut)
σ : Seq.... σ
κ is another search problem i.e., enjoys the condition (4) since for any ρ with λ ⊇ ρ ⊃ σ Seqρ is either a right upper sequent of a (Σb2-cut) or an upper sequent of a (Σb1) with a false auxiliary formula.
Proposition 3.3 In the above figures, κ <KB σ
and σ 3→ κ = S(x, σ, τ ) is a polytime computable map.
3. A ≡ ¬B(¯p) ≡ ∃y < s¬L(¯p, y) of a λ : (Σb2-cut). τ is a solution for σ = λ ∗ -p. = S(x, σ0, τ0) for a problem σ0 with λ ∗ -p. <KB σ0. τ0 ∈ T (x, σ0) and L(¯p, n) is a false literal.¯ If ¬B(¯p) /∈ Seqσ0(Σb1), then
A,∆0,¬L(¯p,n)¯ τ : A, ∆0 (Σ
b 1) ....
· · · λ ∗ -p. : Γ, ¬B(¯p) · · · (p < t0)
· · · τ0 ∗ -n. : ∃x < t0B(x), Γ0, L(¯p,n) · · · (n < s)¯ τ0 : ∃x < t0B(x), Γ0 (Σ
b 2) ....
∃x < t0B(x), Γ
λ : Γ (Σ
b
2-cut)
The solution n of the problem λ ∗ -p. : Γ, ¬B(¯p) tells the problem σ0 where to proceed. Namely go to the n-th path τ0 ∗ -n. : ∃x < t0B(x), Γ0, L(¯p, n¯), and then climb up to the node τ → U(x, σ , τ , τ) := t(x, τ ∗ -n.).
If ¬B(¯p) ∈ Seqσ0(Σb1), then n is a witness of the problem σ0, and U (x, σ0, τ0, τ) := τ .
Now let us define an nPLS problem d, S, t, S and U as above. P = -d; S, T , N ; N, i, t, c, S, U, rk..
1. τ ∈ T (x, σ) iff σ, τ ∈ T (D), σ ∈ S(x), and
(a) either σ ⊆ τ , Seqτ is a lower sequent of a (Σb2), and the path from σ to τ is in the rightmost branch of the upper part of σ, or
(b) Seqτ is a lower sequent of a (Σb1) such that its auxiliary formula is true, and its principal formula is in Seq .
2. For τ ∈ T (x, σ), c(x, τ ) denotes the depth of τ in the finite tree T (D) if Seqτ is a lower sequent of a (Σb2). Otherwise put c(x, s) = 0.
3. For τ, ρ ∈ T (x, σ), N (x, σ, τ, ρ) iff one of the following two holds:
(a) Seqτ is a lower sequent of a (Σb2), and if Seqρ is a lower sequent of a (Σb2), then τ ⊂ ρ.
(b) Seqτ is a lower sequent of a (Σb1), and τ = ρ. 4. rk(x, σ) = kb(x, σ) in (3).
5. i(x) = ∅.
Assume N (x, i(x), τ, τ ). Then τ is a (Σb1) witnessing the end- formula of D. Therefore the value U0(τ ) of its witnessing term realizes Theorem 3.1.
For future works, the approach in this talk could be extended to characterize the Σb1-definable functions in T2k for any k ≥ 2 by introducing classes of search problems of higher order PLS.
References
[Beckmann-Buss∞1] Beckmann, A. and Buss, S. R. : Polynomial local search in the polynomial hierarchy and witnessing in fragments of bounded arithmetic, submitted
[Beckmann-Buss∞2] Beckmann, A. and Buss, S. R. : Characterising definable search problems in bounded arithmetic via proof notations, submitted
[Buss2004] Buss, S. R.: Bounded arithmetic and constant depth Frege proofs, In: Kraj´ıˇcek, J (ed.) Complexity of Computations and Proofs (Quaderni di matematica, vol. 13), 153-174 (2004)
[Buss-Kraj´ıˇcek1994] Buss, S. R. and Kraj´ıˇcek, J.: An application of Boolean complexity to separation problems in bounded arithmetic, In Proc. London Math. Society 69, pp. 1-21, (1994)
[Kraj´ıˇcek-Skelly-Thapen2007] Kraj´ıˇcek, J., Skelly, A. and Thapen, N.: NP search problems in low frag- ments of bounded arithmetic, Jour. Symb. Logic 72, 649-672 (2007)
[Megiddo-Papadimitriou1991] Megiddo, N. and Papadimitriou, C. H. : A note on total functions, exis- tence theorems, and computational complexity, Theor. Comp. Sci. 81, 317-324(1991)
[Skelly-Thapen∞] Skelly, A. and Thapen, N.: The provable total search problems of bounded arithmetic, Typeset manuscript, 2007
