Documentation

CslibFrontier.Computability.Complexity.Classes.Space.Closure

Characterizations and closure properties of PSPACE #

A problem is in PSPACE exactly when a Boolean function deciding it is computable within some time and space polynomial in the length of the encoded instance, in the quantitative calculus of Turing.MultiTapeTM.ComputableInO (Cslib.Complexity.mem_PSPACE_iff_computableInO). PSPACE is closed under complement, under polynomial-time reductions, and under polynomially bounded existential quantification Arora and Barak, Chapter 4. The existential quantifier over words w of length ℓ streams one candidate at a time and reuses the space of the decider for each (Turing.MultiTapeTM.ComputableInO.exists_bits).

Main results #

References #

source
theorem Cslib.Complexity.mem_PSPACE_iff_computableInO {α : Type} {enc : α ↪ List Bool} {A : Set α} :
A ∈ PSPACE enc ↔ ∃ (f : α → Bool) (T : α → ℕ) (S : α → ℕ), Turing.MultiTapeTM.ComputableInO f enc Turing.MultiTapeTM.encBool T S ∧ Turing.MultiTapeTM.PolyBounded (fun (a : α) => (enc a).length) S ∧ ∀ (a : α), a ∈ A ↔ f a = true

PSPACE in the quantitative calculus: a problem is in PSPACE exactly when a Boolean function deciding it is computable within some time and within space polynomial in the length of the encoded instance.

source
theorem Cslib.Complexity.compl_mem_PSPACE {α : Type} {enc : α ↪ List Bool} {A : Set α} (hA : A ∈ PSPACE enc) :
Aᶜ ∈ PSPACE enc

PSPACE is closed under complement: negate the answer.

source
theorem Cslib.Complexity.PSPACE_eq_preimage_compl_PSPACE {α : Type} (enc : α ↪ List Bool) :
PSPACE enc = compl ⁻¹' PSPACE enc

PSPACE equals its preimage under complement.

source
theorem Cslib.Complexity.inter_mem_PSPACE {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ PSPACE enc) (hB : B ∈ PSPACE enc) :
A ∩ B ∈ PSPACE enc

PSPACE is closed under intersection.

source
def Cslib.Complexity.PSPACE.booleanSubalgebra {α : Type} (enc : α ↪ List Bool) :
BooleanSubalgebra (Set α)

PSPACE as a Boolean subalgebra of Set α.

Instances For
    source
    @[simp]
    theorem Cslib.Complexity.PSPACE.coe_booleanSubalgebra {α : Type} {enc : α ↪ List Bool} :
    ↑(booleanSubalgebra enc) = PSPACE enc
    source
    @[simp]
    theorem Cslib.Complexity.PSPACE.mem_booleanSubalgebra {α : Type} {enc : α ↪ List Bool} {A : Set α} :
    A ∈ booleanSubalgebra enc ↔ A ∈ PSPACE enc
    source
    theorem Cslib.Complexity.union_mem_PSPACE {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ PSPACE enc) (hB : B ∈ PSPACE enc) :
    A ∪ B ∈ PSPACE enc

    PSPACE is closed under union.

    source
    theorem Cslib.Complexity.diff_mem_PSPACE {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ PSPACE enc) (hB : B ∈ PSPACE enc) :
    A \ B ∈ PSPACE enc

    PSPACE is closed under set difference.

    source
    theorem Cslib.Complexity.symmDiff_mem_PSPACE {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ PSPACE enc) (hB : B ∈ PSPACE enc) :
    symmDiff A B ∈ PSPACE enc

    PSPACE is closed under symmetric difference.

    source
    theorem Cslib.Complexity.PolyTimeReducible.mem_PSPACE {α : Type} {enc : α ↪ List Bool} {A : Set α} {β : Type} {encB : β ↪ List Bool} {B : Set β} (h : PolyTimeReducible enc encB A B) (hB : B ∈ PSPACE encB) :
    A ∈ PSPACE enc

    PSPACE is closed under polynomial-time reductions.

    source
    theorem Cslib.Complexity.setOf_exists_mem_PSPACE {β : Type} {encB : β ↪ List Bool} {B : Set (β × List Bool)} {ℓ : β → ℕ} (hB : B ∈ PSPACE (Turing.MultiTapeTM.encPair encB Turing.MultiTapeTM.encBits)) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encB Turing.MultiTapeTM.encUnary) :
    {x : β | ∃ (w : List Bool), w.length = ℓ x ∧ (x, w) ∈ B} ∈ PSPACE encB

    PSPACE is closed under polynomially bounded existential quantification. The candidates are streamed in place by ComputableInO.exists_bits, reusing the decider's workspace without a polynomial-time assumption on that decider.