Padding

If P = NP, then EXP = NEXP and E = NE Arora and Barak, Section 2.6: collapses of polynomial classes translate upwards, by the padding argument of Book Book. The proof pads instances until a slow nondeterministic machine is fast in the length of the padded instance, decides the padded problem deterministically, and pays for writing the padding.

Timed reductions

The general timed-reduction API lives in Complexity.Computability.Complexity.Classes.Time. In particular, Cslib.Complexity.preimage_mem_DTIME computes a reduction and then tidily decides its output; the padding arguments below apply this API to their padded instances. The unconditional deterministic exponential-padding lemma Cslib.Complexity.setOf_mem_E_of_computableTidilyInPolyTime_pad lives in Complexity.Computability.Complexity.Classes.EXP.

The padded problem

A nondeterministic machine ntm decides A within time t. The padded problem Turing.MultiTapeNTM.padded ntm c consists of the bit words x such that some c * |x| coins encode an accepting computation of ntm on the word unframe x framed at the start of x, read as coins of the choice table (Turing.MultiTapeNTM.checkChoices). The general certificate characterization Turing.MultiTapeNTM.DecidesInTime.mem_iff_exists_checkChoices lives with checkChoices in Complexity.Computability.Complexity.Classes.NP.Nondeterministic. The padded problem is in NP with respect to encBits by definition: checking the coins is polynomial-time. If every computation path on enc a with at least t a steps has halted, and c * |x| is at least M * t a for the number M of actions, the padded word x = frame (enc a) ++ u is in the padded problem exactly when a ∈ A (Turing.MultiTapeNTM.DecidesInTime.frame_append_mem_padded_iff).

The translation lemma

If NP ⊆ P for problems on bit words, and t n is computable in unary from any word of length n within time O(T n), then NTIME t ⊆ ⋃ d, DTIME ((n + T n + 1) ^ d) (Cslib.Complexity.NTIME_subset_iUnion_DTIME_of_NP_subset_P): the padded problem with padding t n is decided in time polynomial in n + t n. For t n = 2 ^ f n with f computable in unary in polynomial time and n ≤ f n, 2 ^ f n is computed in unary by doubling, within time O((f n + 1) * 2 ^ f n) using the quantitative machine API (Turing.MultiTapeTM.ComputableTidilyInO.unary_two_pow), and NTIME (2 ^ f n) ⊆ ⋃ d, DTIME (2 ^ (d * f n)) (Cslib.Complexity.NTIME_two_pow_subset_iUnion_DTIME_of_NP_subset_P). With f n = (k + 1) * n and f n = n ^ (k + 1) this gives NE ⊆ E and NEXP ⊆ EXP.

The hypothesis is NP ⊆ P for problems on bit words, under encBits; the conclusions hold for problems on any type, under any encoding.

The unconditional pullback lemmas Cslib.Complexity.preimage_mem_NTIME_of_mem_NP and Cslib.Complexity.preimage_pad_mem_NEXP compose a timed deterministic map with an NP verifier; exponential padding yields an NEXP decider without a collapse hypothesis.

Main definitions

• Turing.MultiTapeNTM.checkPadded: the verifier of padded instances.
• Turing.MultiTapeNTM.padded: the padded problem of a nondeterministic machine.

Main results

• Cslib.Complexity.preimage_mem_NTIME_of_mem_NP, Cslib.Complexity.preimage_pad_mem_NEXP: unconditional timed pullback of NP, including exponentially padded inputs.
• Turing.MultiTapeNTM.padded_mem_NP, Turing.MultiTapeNTM.DecidesInTime.frame_append_mem_padded_iff: the padded problem is in NP, and decides the original problem on padded instances.
• Cslib.Complexity.NTIME_subset_iUnion_DTIME_of_NP_subset_P: the translation lemma.
• Cslib.Complexity.NEXP_subset_EXP_of_NP_subset_P, Cslib.Complexity.EXP_eq_NEXP_of_P_eq_NP: if P = NP, then EXP = NEXP.
• Cslib.Complexity.NE_subset_E_of_NP_subset_P, Cslib.Complexity.E_eq_NE_of_P_eq_NP: if P = NP, then E = NE.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• R. V. Book, Comparing complexity classes

noncomputable def Turing.MultiTapeNTM.checkPadded {k : ℕ} {State : Type} [Finite State] (ntm : MultiTapeNTM k Bool State) (x : List Bool × List Bool) : Bool

The verifier of padded instances. It accepts when the certificate, read as coins of the choice table, replays a computation path of ntm on the word framed at the start of the instance that halts with output [true]; the rest of the instance is padding.

theorem Turing.MultiTapeNTM.computableTidilyInPolyTime_checkPadded {k : ℕ} {State : Type} [Finite State] (ntm : MultiTapeNTM k Bool State) : MultiTapeTM.ComputableTidilyInPolyTime ntm.checkPadded (MultiTapeTM.encPair MultiTapeTM.encBits MultiTapeTM.encBits) MultiTapeTM.encBool

Checking a padded instance is polynomial-time.

def Turing.MultiTapeNTM.padded {k : ℕ} {State : Type} [Finite State] (ntm : MultiTapeNTM k Bool State) (c : ℕ) : Set (List Bool)

The padded problem of ntm: the bit words x such that some c * |x| coins encode an accepting computation of ntm on the word unframe x framed at the start of x.

theorem Turing.MultiTapeNTM.padded_mem_NP {k : ℕ} {State : Type} [Finite State] (ntm : MultiTapeNTM k Bool State) (c : ℕ) : ntm.padded c ∈ Cslib.Complexity.NP MultiTapeTM.encBits

The padded problem is in NP, with certificates of length c * |x|.

theorem Turing.MultiTapeNTM.DecidesInTime.frame_append_mem_padded_iff {k : ℕ} {State : Type} [Finite State] {α : Type} {enc : α ↪ List Bool} {ntm : MultiTapeNTM k Bool State} {A : Set α} {t : α → ℕ} (h : ntm.DecidesInTime enc A t) {a : α} {c : ℕ} {u : List Bool} (hc : Nat.card (Action k Bool State) * t a ≤ c * (MultiTapeTM.frame (enc a) ++ u).length) : MultiTapeTM.frame (enc a) ++ u ∈ ntm.padded c ↔ a ∈ A

Padded instances. If ntm decides A within t, then the padded word frame (enc a) ++ u is in the padded problem of ntm with c coins per bit exactly when a ∈ A, as soon as c * |frame (enc a) ++ u| is at least M * t a, for the number M of actions.

The translation lemma

theorem Cslib.Complexity.NTIME_subset_iUnion_DTIME_of_NP_subset_P {α : Type} {enc : α ↪ List Bool} (hNP : NP Turing.MultiTapeTM.encBits ⊆ P Turing.MultiTapeTM.encBits) {t T : ℕ → ℕ} {S : List Bool → ℕ} (hpad : Turing.MultiTapeTM.ComputableTidilyInO (fun (x : List Bool) => t x.length) Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encUnary (fun (x : List Bool) => T x.length) S) : NTIME enc t ⊆ ⋃ (d : ℕ), DTIME enc fun (n : ℕ) => (n + T n + 1) ^ d

The translation lemma. If NP ⊆ P for problems on bit words, and t n is computable in unary from any word of length n within time O(T n), then every problem decidable by a nondeterministic machine within time O(t n) is decidable deterministically within time O((n + T n + 1) ^ d) for some d: the padded problem with padding t n is in NP, hence in P, and the padding is written within time O(n + T n).

theorem Cslib.Complexity.NTIME_two_pow_subset_iUnion_DTIME_of_NP_subset_P {α : Type} {enc : α ↪ List Bool} (hNP : NP Turing.MultiTapeTM.encBits ⊆ P Turing.MultiTapeTM.encBits) {f : ℕ → ℕ} (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hn : ∀ (n : ℕ), n ≤ f n) : (NTIME enc fun (n : ℕ) => 2 ^ f n) ⊆ ⋃ (d : ℕ), DTIME enc fun (n : ℕ) => 2 ^ (d * f n)

Padding exponential time. If NP ⊆ P for problems on bit words, and f is computable in unary in polynomial time with n ≤ f n, then every problem decidable by a nondeterministic machine within time O(2 ^ f n) is decidable deterministically within time O(2 ^ (d * f n)) for some d.

Exponential time

theorem Cslib.Complexity.NE_subset_E_of_NP_subset_P {α : Type} {enc : α ↪ List Bool} (hNP : NP Turing.MultiTapeTM.encBits ⊆ P Turing.MultiTapeTM.encBits) : NE enc ⊆ E enc

If NP ⊆ P, then NE ⊆ E, by padding Book.

theorem Cslib.Complexity.NEXP_subset_EXP_of_NP_subset_P {α : Type} {enc : α ↪ List Bool} (hNP : NP Turing.MultiTapeTM.encBits ⊆ P Turing.MultiTapeTM.encBits) : NEXP enc ⊆ EXP enc

If NP ⊆ P, then NEXP ⊆ EXP Arora and Barak, Section 2.6.

theorem Cslib.Complexity.E_eq_NE_of_P_eq_NP {α : Type} {enc : α ↪ List Bool} (h : P Turing.MultiTapeTM.encBits = NP Turing.MultiTapeTM.encBits) : E enc = NE enc

If P = NP, then E = NE, by padding Book.

theorem Cslib.Complexity.EXP_eq_NEXP_of_P_eq_NP {α : Type} {enc : α ↪ List Bool} (h : P Turing.MultiTapeTM.encBits = NP Turing.MultiTapeTM.encBits) : EXP enc = NEXP enc

If P = NP, then EXP = NEXP Arora and Barak, Section 2.6.

theorem Cslib.Complexity.P_ne_NP_of_EXP_ne_NEXP {α : Type} {enc : α ↪ List Bool} (h : EXP enc ≠ NEXP enc) : P Turing.MultiTapeTM.encBits ≠ NP Turing.MultiTapeTM.encBits

If EXP ≠ NEXP, then P ≠ NP.

Upward translation from NP to NTIME and NEXP

theorem Cslib.Complexity.preimage_mem_NTIME_of_mem_NP {α : Type} {enc : α ↪ List Bool} {B : Set (List Bool)} {g : α → List Bool} {T₀ : ℕ → ℕ} {S : α → ℕ} (hB : B ∈ NP Turing.MultiTapeTM.encBits) (hg : Turing.MultiTapeTM.ComputableTidilyInO g enc Turing.MultiTapeTM.encBits (fun (a : α) => T₀ (enc a).length) S) : ∃ (d : ℕ), g ⁻¹' B ∈ NTIME enc fun (n : ℕ) => (T₀ n + 1) ^ d

Pulling back a problem B ∈ NP encBits along a function g : α → List Bool computable tidily within time O(T₀ (enc a).length) places g ⁻¹' B in NTIME enc (fun n => (T₀ n + 1) ^ d) for some d: a deterministic machine writes g a to a buffer tape and hands off to the halting fair-coin certificate verifier for B.

theorem Cslib.Complexity.preimage_pad_mem_NEXP {α : Type} {enc : α ↪ List Bool} {B : Set (List Bool)} (hB : B ∈ NP Turing.MultiTapeTM.encBits) {f : ℕ → ℕ} (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hn : ∀ (n : ℕ), n ≤ f n) : (fun (a : α) => Turing.MultiTapeTM.frame (enc a) ++ List.replicate (2 ^ f (enc a).length) true) ⁻¹' B ∈ NEXP enc

Pulling back B ∈ NP encBits along the exponential-padding map a ↦ frame (enc a) ++ List.replicate (2 ^ f (enc a).length) true, where f is polynomial-time in unary with n ≤ f n, gives a problem in NEXP enc.