The class P

A decision problem is a set A : Set α of instances, together with an encoding enc : α ↪ List Bool of instances as binary words, in the style of Turing.MultiTapeTM.DecidableInTimeAndSpace. It is in P when a Boolean function deciding membership is computable in polynomial time (Turing.MultiTapeTM.ComputableInPolyTime) with respect to enc and the encoding Turing.MultiTapeTM.encBool of answers Arora and Barak, Definition 1.13. Equivalently, A ∈ P enc when upstream Turing.MultiTapeTM.DecidableInTimeAndSpace holds within time and space bounded by polynomially bounded functions of the length of the encoded instance (Cslib.Complexity.mem_P_iff_exists_decidableInTimeAndSpace), and, as in the textbook definition, a polynomial time bound alone suffices (Cslib.Complexity.mem_P_of_decidableInTimeAndSpace).

Mathlib's Turing.TM2ComputableInPolyTime is stated for Mathlib's stack machines; this file uses cslib's multi-tape machines, which carry the time and space measures the rest of the development is built on. For machines with finite stack alphabets, Turing.TM2ComputableInPolyTime.computableInPolyTime in CslibFrontier.Computability.Machines.Turing.TM2.Recoding transfers Mathlib certificates over binary encodings to this notion.

Main definitions

• Cslib.Complexity.P: problems decidable in polynomial time.

Main results

• Cslib.Complexity.mem_P_iff_exists_decidableInTimeAndSpace: P in terms of upstream Turing.MultiTapeTM.DecidableInTimeAndSpace with polynomially bounded time and space.
• Cslib.Complexity.mem_P_of_decidableInTimeAndSpace: a polynomial time bound alone suffices.
• Cslib.Complexity.empty_mem_P, Cslib.Complexity.univ_mem_P: the empty and universal problems are in P.
• Cslib.Complexity.compl_mem_P, Cslib.Complexity.P_eq_preimage_compl_P: P is closed under complement.

References

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

def Cslib.Complexity.P {α : Type u_1} (enc : α ↪ List Bool) : Set (Set α)

The problems decidable in polynomial time with respect to the encoding enc: A ∈ P enc when a Boolean function deciding membership in A is computable in polynomial time Arora and Barak, Definition 1.13.

theorem Cslib.Complexity.mem_P {α : Type u_1} {enc : α ↪ List Bool} {A : Set α} : A ∈ P enc ↔ ∃ (f : α → Bool), Turing.MultiTapeTM.ComputableInPolyTime f enc Turing.MultiTapeTM.encBool ∧ ∀ (a : α), a ∈ A ↔ f a = true

theorem Cslib.Complexity.mem_P_iff_exists_decidableInTimeAndSpace {α : Type u_1} {enc : α ↪ List Bool} {A : Set α} : A ∈ P enc ↔ ∃ (t : ℕ → ℕ) (s : ℕ → ℕ), PolynomiallyBounded t ∧ PolynomiallyBounded s ∧ Turing.MultiTapeTM.DecidableInTimeAndSpace A enc (fun (a : α) => t (enc a).length) fun (a : α) => s (enc a).length

P in upstream terms: A ∈ P enc exactly when some machine with a binary alphabet and finitely many states decides A within time and space bounded by polynomially bounded functions of the length of the encoded instance.

theorem Cslib.Complexity.mem_P_of_decidableInTimeAndSpace {α : Type u_1} {enc : α ↪ List Bool} {A : Set α} {t : ℕ → ℕ} {s : α → ℕ} (ht : PolynomiallyBounded t) (h : Turing.MultiTapeTM.DecidableInTimeAndSpace A enc (fun (a : α) => t (enc a).length) s) : A ∈ P enc

A problem that some machine decides within a time bound polynomial in the length of the encoded instance, with any space bound, is in P, as in the textbook definition.

theorem Cslib.Complexity.empty_mem_P {α : Type u_1} {enc : α ↪ List Bool} : ∅ ∈ P enc

The empty problem is in P.

theorem Cslib.Complexity.univ_mem_P {α : Type u_1} {enc : α ↪ List Bool} : Set.univ ∈ P enc

The universal problem is in P.

theorem Cslib.Complexity.compl_mem_P {α : Type u_1} {enc : α ↪ List Bool} {A : Set α} (hA : A ∈ P enc) : Aᶜ ∈ P enc

P is closed under complement: negate the answer of the decider.

theorem Cslib.Complexity.P_eq_preimage_compl_P {α : Type u_1} (enc : α ↪ List Bool) : P enc = compl ⁻¹' P enc

P equals its preimage under complement.