Documentation

Complexitylib.Classes.Containments.Internal.BlockAccept

Scanning the visited string for an accepting record #

⚠️ Unreviewed by Bolton

The last step of the search is a scan of the visited string that ORs the accepting-record test of Complexitylib.Classes.Containments.Internal.CodeAccept over its records. It is the scan of Complexitylib.Classes.Containments.Internal.BlockMember with a different test, so its correctness comes straight from anyStepPair.

Two rulers travel in the state: the block ruler, which the test slices a record with, and the rewind ruler, which says how long to drive the output head left. The record width is 2(k+2)+1 block rulers, so it need not be carried.

Main definitions #

Main results #

The packed scan #

source
def Complexity.acceptPack (R ruler flag rest : List Bool) :
List Bool

The packed accept-scan state: the two rulers, then the flag and the rest.

Equations
Instances For
    source
    @[simp]
    theorem Complexity.acceptPack_length (R ruler flag rest : List Bool) :
    (acceptPack R ruler flag rest).length = 2 * (2 * R.length + ruler.length + 2) + 2 * flag.length + rest.length + 4
    source
    noncomputable def Complexity.acceptStep (k : ℕ) (qcode z : List Bool) :
    List Bool

    One step of the accept scan.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def Complexity.acceptPairStep (k : ℕ) (qcode R ruler : List Bool) :
      List Bool × List Bool → List Bool × List Bool

      The unpacked step the packed one performs.

      Equations
      Instances For
        source
        theorem Complexity.acceptStep_pack (k : ℕ) (qcode R ruler flag rest : List Bool) :
        acceptStep k qcode (acceptPack R ruler flag rest) = acceptPack R ruler (acceptPairStep k qcode R ruler (flag, rest)).1 (acceptPairStep k qcode R ruler (flag, rest)).2

        The packed step is the unpacked step.

        source
        theorem Complexity.acceptStep_iterate (k : ℕ) (qcode R ruler : List Bool) (s : List Bool × List Bool) (n : ℕ) :
        (acceptStep k qcode)^[n] (acceptPack R ruler s.1 s.2) = acceptPack R ruler ((acceptPairStep k qcode R ruler)^[n] s).1 ((acceptPairStep k qcode R ruler)^[n] s).2

        The packed iteration is the unpacked one.

        The verdict #

        source
        noncomputable def Complexity.acceptScan (k : ℕ) (qcode R ruler V : List Bool) :
        List Bool

        Does any record of V pass the accepting test?

        Equations
        Instances For
          source
          theorem Complexity.acceptScan_flag (k : ℕ) (qcode R ruler V : List Bool) :
          acceptScan k qcode R ruler V = [true] ∨ acceptScan k qcode R ruler V = [false]
          source
          theorem Complexity.acceptScan_eq_true_iff (k : ℕ) (qcode R ruler V : List Bool) (hR : 0 < R.length) :
          acceptScan k qcode R ruler V = [true] ↔ ∃ (i : ℕ), i * (wideRuler (codeBlocks k) R).length + (wideRuler (codeBlocks k) R).length ≤ V.length ∧ acceptFlag qcode R ruler (blockAt (wideRuler (codeBlocks k) R) V i) = [true]

          The scan finds an accepting record exactly when there is one.

          The scan is polynomial-time #

          source
          theorem Complexity.acceptStep_mem_FP (k : ℕ) (qcode : List Bool) :
          acceptStep k qcode ∈ FP
          source
          theorem Complexity.acceptStep_iterate_length_le (k : ℕ) (qcode R ruler : List Bool) (s : List Bool × List Bool) (hf : s.1 = [true] ∨ s.1 = [false]) (n : ℕ) :
          ((acceptStep k qcode)^[n] (acceptPack R ruler s.1 s.2)).length ≤ (acceptPack R ruler s.1 s.2).length

          The scan's state never grows.

          source
          theorem Complexity.acceptScanFn_mem_FP (k : ℕ) (qcode : List Bool) {Rf rulerf Vf : List Bool → List Bool} (hR : Rf ∈ FP) (hruler : rulerf ∈ FP) (hV : Vf ∈ FP) :
          (fun (w : List Bool) => acceptScan k qcode (Rf w) (rulerf w) (Vf w)) ∈ FP

          The accept scan is polynomial-time.