Documentation

Complexity.Computability.Complexity.Classes.Oracle.TQBF

The words of TQBF #

TQBF is a problem on formulas. As an oracle language it is the set encQBF '' TQBF of words encoding true closed formulas, and a decider must handle every word. A word encodes a formula exactly when its framed tokens decode to the token list of a formula, which is encoded back to the word (Cslib.Complexity.TQBF.isCode_iff). Token lists are decoded by the total decoders of Turing.MultiTapeTM.Decoder, and the token lists of formulas, in prefix order, are recognized by counting the formulas still expected: a token is expected when the count is positive, consumes one expected formula and announces as many as it has operands (Cslib.Complexity.TQBF.foldl_wfStep_eq_iff). Both tests are polynomial-time (Cslib.Complexity.TQBF.isCode_pt), and a word that encodes a formula is evaluated by the polynomial-space evaluator of TQBF. Hence encQBF '' TQBF is in PSPACE (Cslib.Complexity.image_TQBF_mem_PSPACE), and, through encQBF, PSPACE-hard (Cslib.Complexity.image_TQBF_pspaceHard) Sipser, Theorem 8.9.

Main definitions #

Main results #

References #

Well-formed token lists #

source
def Cslib.Complexity.TQBF.arity :
Logic.PL.QBF.Kind → ℕ

The number of operands of a node of the kind.

Instances For
    source
    def Cslib.Complexity.TQBF.tokenOk (t : Logic.PL.QBF.Kind × ℕ) :
    Bool

    Whether the token can occur in a formula: only variables and quantifiers carry a variable.

    Instances For
      source
      def Cslib.Complexity.TQBF.wfStep (s : Bool × ℕ) (t : Logic.PL.QBF.Kind × ℕ) :
      Bool × ℕ

      A step of the well-formedness check: whether every token so far has been expected, and the number of formulas still expected.

      Instances For
        source
        theorem Cslib.Complexity.TQBF.foldl_wfStep_eq_iff (ts : List (Logic.PL.QBF.Kind × ℕ)) (n : ℕ) :
        List.foldl wfStep (true, n) ts = (true, 0) ↔ ∃ (φs : List (Logic.PL.QBF ℕ)), φs.length = n ∧ ts = (List.map Logic.PL.QBF.tokens φs).flatten

        The check accepts exactly the concatenated tokens of n formulas.

        Decoding words #

        source
        def Cslib.Complexity.TQBF.kindOfIndex :
        ℕ → Logic.PL.QBF.Kind

        The kind of a given index, all from 7 on.

        Instances For
          source
          def Cslib.Complexity.TQBF.kindDecoder :
          Turing.MultiTapeTM.Decoder encKind

          Kinds are decoded from the length of the word.

          Instances For
            source
            def Cslib.Complexity.TQBF.tokensDecoder :
            Turing.MultiTapeTM.Decoder (Turing.MultiTapeTM.encList encToken)

            Token lists are decoded element by element.

            Instances For
              source
              def Cslib.Complexity.TQBF.wellFormed (ts : List (Logic.PL.QBF.Kind × ℕ)) :
              Bool

              Whether a token list is the token list of a formula.

              Instances For
                source
                theorem Cslib.Complexity.TQBF.wellFormed_iff (ts : List (Logic.PL.QBF.Kind × ℕ)) :
                wellFormed ts = true ↔ ∃ (φ : Logic.PL.QBF ℕ), φ.tokens = ts

                wellFormed ts holds exactly when ts is the token list of a formula.

                source
                def Cslib.Complexity.TQBF.isCode (w : List Bool) :
                Bool

                Whether a word encodes a formula: it decodes to a well-formed token list that is encoded back to the word.

                Instances For
                  source
                  theorem Cslib.Complexity.TQBF.isCode_iff (w : List Bool) :
                  isCode w = true ↔ ∃ (φ : Logic.PL.QBF ℕ), encQBF φ = w

                  A word passes isCode exactly when it encodes a formula.

                  source
                  theorem Cslib.Complexity.TQBF.isCode_pt :
                  Turing.MultiTapeTM.ComputableTidilyInPolyTime isCode Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool

                  Whether a word encodes a formula is decidable in polynomial time.

                  source
                  noncomputable def Cslib.Complexity.TQBF.decodeQBF (w : List Bool) :
                  Logic.PL.QBF ℕ

                  The formula a word encodes, or bot if it encodes none.

                  Instances For
                    source
                    theorem Cslib.Complexity.TQBF.decodeQBF_pt :
                    Turing.MultiTapeTM.ComputableTidilyInPolyTime decodeQBF Turing.MultiTapeTM.encBits encQBF

                    decodeQBF is polynomial-time.

                    source
                    theorem Cslib.Complexity.mem_image_TQBF_iff (w : List Bool) :
                    w ∈ ⇑encQBF '' TQBF ↔ (TQBF.isCode w && TQBF.evaluate (TQBF.decodeQBF w)) = true

                    A word is in encQBF '' TQBF when it encodes a formula that the evaluator accepts.

                    source
                    theorem Cslib.Complexity.image_TQBF_mem_PSPACE :
                    ⇑encQBF '' TQBF ∈ PSPACE Turing.MultiTapeTM.encBits

                    The words encoding true closed formulas are decided within polynomial space: a word is tested for encoding a formula in polynomial time, and then evaluated.

                    source
                    theorem Cslib.Complexity.image_TQBF_pspaceHard :
                    PSPACEHard Turing.MultiTapeTM.encBits (⇑encQBF '' TQBF)

                    The words encoding true closed formulas are PSPACE-hard, through the encoding encQBF.

                    source
                    theorem Cslib.Complexity.image_TQBF_pspaceComplete :
                    PSPACEComplete Turing.MultiTapeTM.encBits (⇑encQBF '' TQBF)

                    The words encoding true closed formulas are PSPACE-complete.