Polynomial space

Cslib.Complexity.PSPACE enc consists of the problems decided by a Boolean function computable within polynomial space (Turing.MultiTapeTM.ComputableInPolySpace), as Cslib.Complexity.P and Cslib.Complexity.L use polynomial time and logarithmic space: one deterministic machine with a binary alphabet and finitely many states halts on every encoded instance enc a with output [true] or [false], visiting at most s (enc a).length work-tape cells for a polynomially bounded s (upstream Turing.MultiTapeTM.ComputableInTimeAndSpace, with no tidiness requirement). No bound on the time is imposed beyond halting. Equivalently (Cslib.Complexity.mem_PSPACE_iff), the problem is decidable within some time bound and a space bound polynomially bounded in the length of enc a, in the sense of upstream Turing.MultiTapeTM.DecidableInTimeAndSpace. The proposed upstream complexity classes (cslib pull request #767, open) build DSPACE on the same notion of decidability and define PSPACE as the union of the classes of space O(n ^ k); their bounds are functions of the input length. For the local encoded-instance classes, Cslib.Complexity.mem_PSPACE_iff_exists_mem_DSPACE proves this union characterization without changing the instance-dependent space-bound definition below. A bridge to the upstream language-indexed classes is not formalized here.

Cslib.Complexity.NPSPACE enc consists of the problems decided by one nondeterministic machine with a binary alphabet and finitely many states within space s (Turing.MultiTapeNTM.DecidesInSpace), for an s polynomially bounded in the length of enc a: every computation path on enc a visits at most s a work-tape cells (upstream Turing.MultiTapeNTM.RunsInSpace, over every prefix of every path), every branch halts, and a ∈ A exactly when some computation path halts with output exactly [true] (Turing.MultiTapeNTM.Accepts) Sipser, Definition 8.1. No time bound is imposed beyond halting; a path may end stuck, and then does not accept. Recognizers, whose branches may run forever (Turing.MultiTapeNTM.RecognizesInSpace), are no stronger: Savitch's theorem places a problem recognized within polynomial space in PSPACE (Cslib.Complexity.mem_PSPACE_of_recognizesInSpace).

A problem is PSPACE-hard when every problem in PSPACE, with any encoding of its instances, reduces to it in polynomial time (Cslib.Complexity.PolyTimeReducible), and PSPACE-complete when it is moreover in PSPACE Arora and Barak, Section 4.2 Sipser, Section 8.3. The true quantified Boolean formulas are PSPACE-complete; see CslibFrontier.Computability.Complexity.Classes.Space.TQBF.

Space counts visited work-tape cells, as upstream does: the input tape is read-only and the output tape write-only Sipser, Section 8.4 and Definition 8.21.

Main definitions

• Cslib.Complexity.PSPACE: deterministic polynomial space.
• Cslib.Complexity.NPSPACE: nondeterministic polynomial space.
• Cslib.Complexity.PSPACEHard, Cslib.Complexity.PSPACEComplete: hardness and completeness under polynomial-time reductions, the instances of Cslib.Complexity.PolyTimeHard and Cslib.Complexity.PolyTimeComplete for PSPACE.

Main results

• Cslib.Complexity.mem_PSPACE: a Boolean decider computable within polynomial space.
• Cslib.Complexity.mem_PSPACE_of_computableInTimeAndSpace: a decider within a polynomially bounded space bound.
• Cslib.Complexity.mem_PSPACE_iff: PSPACE in terms of upstream DecidableInTimeAndSpace.
• Cslib.Complexity.mem_PSPACE_iff_exists_mem_DSPACE: the union of DSPACE (n ^ k).
• Cslib.Complexity.DSPACE_subset_PSPACE: polynomially bounded space is within PSPACE.
• Cslib.Complexity.P_subset_PSPACE: polynomial time is within polynomial space.
• Cslib.Complexity.PSPACE_subset_NPSPACE: a deterministic machine is a nondeterministic machine with one computation path.
• Cslib.Complexity.PSPACEHard.trans: hardness transfers along polynomial-time reductions.

References

• M. Sipser, Introduction to the Theory of Computation
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

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

The problems decided by one deterministic machine within polynomial space, with respect to the encoding enc: a Boolean function deciding membership is computable within some time and within space polynomial in the length of the encoded instance (Turing.MultiTapeTM.ComputableInPolySpace) Sipser, Section 8.2.

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

theorem Cslib.Complexity.mem_PSPACE_of_computableInTimeAndSpace {α : Type} {enc : α ↪ List Bool} {A : Set α} {f : α → Bool} {t s : α → ℕ} (hs : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (enc a).length) s) (hf : Turing.MultiTapeTM.ComputableInTimeAndSpace f enc Turing.MultiTapeTM.encBool t s) (hA : ∀ (a : α), a ∈ A ↔ f a = true) : A ∈ PSPACE enc

A Boolean decider computable within some time and within a space bound polynomially bounded in the length of the encoded instance decides a problem in PSPACE.

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

Membership in PSPACE is upstream decidability within some time and polynomial space.

theorem Cslib.Complexity.DSPACE_subset_PSPACE {α : Type} {enc : α ↪ List Bool} {s : ℕ → ℕ} (hs : PolynomiallyBounded s) : DSPACE enc s ⊆ PSPACE enc

A space class of a polynomially bounded bound is within PSPACE.

theorem Cslib.Complexity.mem_PSPACE_iff_exists_mem_DSPACE {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ PSPACE enc ↔ ∃ (k : ℕ), A ∈ DSPACE enc fun (x : ℕ) => x ^ k

PSPACE is the union of the classes DSPACE (n ^ k), the definition of PSPACE in cslib pull request #767.

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

The problems decided by one nondeterministic machine within polynomial space, with respect to the encoding enc (Turing.MultiTapeNTM.DecidesInSpace): every computation path on enc a visits at most s a work-tape cells, for a polynomially bounded s, every branch halts, and a ∈ A exactly when some computation path halts with output [true] Sipser, Section 8.2.

theorem Cslib.Complexity.P_subset_PSPACE {α : Type} {enc : α ↪ List Bool} : P enc ⊆ PSPACE enc

Polynomial time is within polynomial space.

theorem Cslib.Complexity.PSPACE_subset_NPSPACE {α : Type} {enc : α ↪ List Bool} : PSPACE enc ⊆ NPSPACE enc

A deterministic polynomial-space machine is a nondeterministic one, with one computation path (Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_decidesInSpace).

Hardness and completeness

@[reducible, inline]

abbrev Cslib.Complexity.PSPACEHard {β : Type u_1} (encB : β ↪ List Bool) (B : Set β) : Prop

Every problem in PSPACE, with any encoding of its instances, reduces to B in polynomial time.

@[reducible, inline]

abbrev Cslib.Complexity.PSPACEComplete {β : Type} (encB : β ↪ List Bool) (B : Set β) : Prop

B is in PSPACE and every problem in PSPACE reduces to it.

theorem Cslib.Complexity.polyTimeHard_PSPACE_iff {β : Type u_1} {encB : β ↪ List Bool} {B : Set β} : PolyTimeHard (@PSPACE) encB B ↔ PSPACEHard encB B

Hardness for the class PSPACE is PSPACEHard.

theorem Cslib.Complexity.polyTimeComplete_PSPACE_iff {β : Type} {encB : β ↪ List Bool} {B : Set β} : PolyTimeComplete (@PSPACE) encB B ↔ PSPACEComplete encB B

Completeness for the class PSPACE is PSPACEComplete.

theorem Cslib.Complexity.PSPACEHard.trans {β : Type u_1} {γ : Type u_2} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {B : Set β} {C : Set γ} (hB : PSPACEHard encB B) (hBC : PolyTimeReducible encB encC B C) : PSPACEHard encC C

PSPACE-hardness transfers along a polynomial-time reduction.