Documentation

CslibFrontier.Computability.Complexity.Classes.Space.TQBF.Membership

TQBF is in polynomial space #

The evaluator of Cslib.Computability.Complexity.Classes.Space.TQBF.Evaluation runs its stack machine for 2 ^ L steps on a formula whose encoding has length L. This file bounds its time and space in the quantitative calculus of plain computability (Turing.MultiTapeTM.ComputableInO), charging every stored frame, the input, the counter of the rounds and every copy.

The states of the machine are encoded by framed tuples (Cslib.Complexity.TQBF.encState). A step is polynomial-time in the encoded state (Cslib.Complexity.TQBF.computableInPolyTime_step): it branches on whether a value is being returned, on the kind of the next token or of the top frame, and looks variables up in the stack. Along a run on a formula with encoding of length L, the stack holds at most L frames, each storing a token and a suffix of the tokens of the formula, so every state has an encoding of length O((L + 1) ^ 2) (Cslib.Complexity.TQBF.length_encState_le). The rounds are counted by a binary counter of L + 1 digits, from 2 ^ L written in linear time (Turing.MultiTapeTM.ComputableInDegree.two_pow_length), so the evaluator runs in space polynomial in L and in time 2 ^ L times a polynomial in L (Cslib.Complexity.TQBF.exists_computableInO_evaluate). Hence TQBF ∈ PSPACE Sipser, Theorem 8.9 Arora and Barak, Theorem 4.13.

Main definitions #

Main results #

References #

Encodings #

source
def Cslib.Complexity.TQBF.Frame.fields (f : Frame) :
(Logic.PL.QBF.Kind × ℕ) × Option Bool × List (Logic.PL.QBF.Kind × ℕ)

The fields of a frame.

Instances For
    source
    @[reducible, inline]
    abbrev Cslib.Complexity.TQBF.encFrameFields :
    (Logic.PL.QBF.Kind × ℕ) × Option Bool × List (Logic.PL.QBF.Kind × ℕ) ↪ List Bool

    The encoding of the fields of a frame.

    Instances For
      source
      def Cslib.Complexity.TQBF.encFrame :
      Frame ↪ List Bool

      Frames encoded by their fields.

      Instances For
        source
        def Cslib.Complexity.TQBF.State.fields (s : State) :
        List (Logic.PL.QBF.Kind × ℕ) × List Frame × Option Bool × Bool

        The fields of a state.

        Instances For
          source
          @[reducible, inline]
          abbrev Cslib.Complexity.TQBF.encStateFields :
          List (Logic.PL.QBF.Kind × ℕ) × List Frame × Option Bool × Bool ↪ List Bool

          The encoding of the fields of a state.

          Instances For
            source
            def Cslib.Complexity.TQBF.encState :
            State ↪ List Bool

            States encoded by their fields.

            Instances For

              The step in polynomial time #

              source
              theorem Cslib.Complexity.TQBF.computableInPolyTime_step :
              Turing.MultiTapeTM.ComputableInPolyTime step encState encState

              A step of the evaluator is polynomial-time in the encoded state.

              The size of the states of a run #

              source
              theorem Cslib.Complexity.TQBF.length_encState_le {φ : Logic.PL.QBF ℕ} {s : State} (h : Good φ s) :
              (encState s).length ≤ 16 * ((encQBF φ).length + 1) ^ 2

              The states of a run are of quadratic size: a state satisfying the invariant on φ has an encoding of length at most 16 * ((encQBF φ).length + 1) ^ 2.

              The evaluator in polynomial space #

              source
              theorem Cslib.Complexity.TQBF.exists_computableInO_evaluate :
              ∃ (e : ℕ), Turing.MultiTapeTM.ComputableInO evaluate encQBF Turing.MultiTapeTM.encBool (fun (φ : Logic.PL.QBF ℕ) => 2 ^ (encQBF φ).length * ((encQBF φ).length + 1) ^ e) fun (φ : Logic.PL.QBF ℕ) => ((encQBF φ).length + 1) ^ e

              The evaluator in polynomial space. On a formula whose encoding has length L, the evaluator is computable within time O(2 ^ L * (L + 1) ^ e) and space O((L + 1) ^ e), for some fixed e. The space charges the input, the stack of at most L frames, each storing a token and a suffix of the tokens, the value, the flag, the counter of the 2 ^ L rounds in binary, and the polynomial space of a step; the time charges every round Sipser, Theorem 8.9 Arora and Barak, Theorem 4.13.

              source
              theorem Cslib.Complexity.TQBF_mem_PSPACE :
              TQBF ∈ PSPACE encQBF

              TQBF is in polynomial space Sipser, Theorem 8.9 Arora and Barak, Theorem 4.13: the explicit-stack evaluator decides it within space polynomial in the length of the encoded formula.