NP is nondeterministic polynomial time

The verifier class Cslib.Complexity.NP consists exactly of the problems decided in polynomial time by nondeterministic machines with a binary alphabet and finitely many states Arora and Barak, Theorem 2.6. Guessing a certificate and verifying it gives one inclusion (Cslib.Complexity.decidableInPolyTime_of_mem_NP). This file proves the converse by checking an encoded accepting computation.

A computation path is encoded by its choices, as coins of the fixed finite choice table Turing.MultiTapeNTM.choiceTable: a step taking the permitted action of zero-based index j costs j + 1 coins, at most M = Nat.card of the action type. If every computation path on enc a with at least c * ((enc a).length + 1) ^ d steps has halted (stuck paths may be shorter), accepting computations are encoded within M * c * ((enc a).length + 1) ^ d coins, and padded to exactly this polynomial length, which a halted table ignores. The verifier Turing.MultiTapeNTM.checkChoices replays the certificate with the choice table and accepts when the table emits [true]: then the coins encode a computation path that halts with output [true]. Every coin list selects permitted actions, except at a stuck configuration, which has none; there the table rejects. Testing the output of a fixed finite fair-coin table replayed from encoded coins and input is polynomial-time (Turing.MultiTapePTM.computableInPolyTime_decide_runClosedCoins), so the verifier needs no machine built by hand.

Main definitions

• Turing.MultiTapeNTM.checkChoices: the verifier of encoded accepting computations.

Main results

• Turing.MultiTapeNTM.computableInPolyTime_checkChoices: the verifier is polynomial-time.
• Turing.MultiTapeNTM.DecidesInTime.mem_iff_exists_checkChoices: accepting computations have certificates of every length at least the action count times the time bound.
• Turing.MultiTapeNTM.DecidesInTime.isVerifier: a machine deciding a problem within c * ((enc a).length + 1) ^ d steps yields a verifier with certificates of length M * c * ((enc a).length + 1) ^ d.
• Cslib.Complexity.mem_NP_of_decidableInPolyTime: the converse inclusion.
• Cslib.Complexity.mem_NP_iff_decidableInPolyTime: NP is nondeterministic polynomial time.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

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

The verifier of encoded accepting computations. It accepts when the certificate, read as coins of the choice table, replays a computation path on the encoded instance that halts with output [true].

theorem Turing.MultiTapeNTM.computableInPolyTime_checkChoices {k : ℕ} {State : Type} [Finite State] {α : Type} {enc : α ↪ List Bool} (ntm : MultiTapeNTM k Bool State) : MultiTapeTM.ComputableInPolyTime (ntm.checkChoices enc) (MultiTapeTM.encPair enc MultiTapeTM.encBits) MultiTapeTM.encBool

Checking an encoded computation is polynomial-time: it replays a fixed finite fair-coin table.

theorem Turing.MultiTapeNTM.DecidesInTime.mem_iff_exists_checkChoices {k : ℕ} {State : Type} [Finite State] {α : Type} {enc : α ↪ List Bool} {ntm : MultiTapeNTM k Bool State} {A : Set α} {t : α → ℕ} (h : ntm.DecidesInTime enc A t) {a : α} {L : ℕ} (hL : Nat.card (Action k Bool State) * t a ≤ L) : a ∈ A ↔ ∃ (w : List Bool), w.length = L ∧ ntm.checkChoices enc (a, w) = true

Accepting computations as certificates of any sufficient length. If ntm decides A within t, then a ∈ A exactly when some certificate of length L encodes an accepting computation on enc a, for every L of at least M * t a, for the number M of actions.

theorem Turing.MultiTapeNTM.DecidesInTime.isVerifier {k : ℕ} {State : Type} [Finite State] {α : Type} {enc : α ↪ List Bool} {ntm : MultiTapeNTM k Bool State} {A : Set α} {c d : ℕ} (h : ntm.DecidesInTime enc A fun (a : α) => c * ((enc a).length + 1) ^ d) : Cslib.Complexity.IsVerifier enc (Polynomial.C (Nat.card (Action k Bool State) * c) * (Polynomial.X + 1) ^ d) (ntm.checkChoices enc) A

Accepting computations as certificates. A machine deciding A within c * ((enc a).length + 1) ^ d steps (every computation path with at least that many steps has halted) yields a verifier whose certificates have length exactly M * c * ((enc a).length + 1) ^ d, for the number M of actions.

theorem Cslib.Complexity.mem_NP_of_decidableInPolyTime {α : Type} {enc : α ↪ List Bool} {A : Set α} (h : Turing.MultiTapeNTM.DecidableInPolyTime A enc) : A ∈ NP enc

Checking accepting computations, the inclusion of nondeterministic polynomial time in NP Arora and Barak, Theorem 2.6.

theorem Cslib.Complexity.mem_NP_iff_decidableInPolyTime {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ NP enc ↔ Turing.MultiTapeNTM.DecidableInPolyTime A enc

NP is nondeterministic polynomial time Arora and Barak, Theorem 2.6: a problem has a polynomial-time verifier with certificates of polynomial length exactly when a nondeterministic machine with a binary alphabet and finitely many states decides it in polynomial time, relative to the same encoding of instances.