Documentation

Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.InductiveCounting.Encoding

Binary storage for the inductive-counting controller #

The controller stores ten binary natural registers, a finite instruction label and two bits. The choice history used in its semantic proofs is absent from the encoding.

Main definitions #

References #

source
def Turing.InductiveCounting.phaseCode :
Cslib.InductiveCounting.Phase → ℕ

Fixed labels for the controller's finite phases.

Instances For
    source
    theorem Turing.InductiveCounting.phaseCode_injective :
    Function.Injective phaseCode
    source
    def Turing.InductiveCounting.registers (s : Cslib.InductiveCounting.State) :
    List ℕ

    Only ten binary registers are stored; there is no stored walk or round list.

    Instances For
      source
      def Turing.InductiveCounting.stateData (s : Cslib.InductiveCounting.State) :
      ℕ × List ℕ × Bool × Bool

      The fixed data represented by a controller state.

      Instances For
        source
        theorem Turing.InductiveCounting.stateData_injective :
        Function.Injective stateData
        source
        def Turing.InductiveCounting.encState :
        Cslib.InductiveCounting.State ↪ List Bool

        The encoded finite phase, binary registers and flags.

        Instances For
          source
          @[simp]
          theorem Turing.InductiveCounting.length_registers (s : Cslib.InductiveCounting.State) :
          (registers s).length = 10
          source
          theorem Turing.InductiveCounting.mem_registers_lt {N width : ℕ} {s : Cslib.InductiveCounting.State} (h : Cslib.InductiveCounting.Bounded N width s) (r : ℕ) :
          r ∈ registers s → r < Cslib.InductiveCounting.registerBound N width
          source
          theorem Turing.InductiveCounting.length_encState_le {s : Cslib.InductiveCounting.State} {L : ℕ} (h : ∀ r ∈ registers s, (MultiTapeTM.encNat r).length ≤ L) :
          (encState s).length ≤ 40 * (L + 1)

          A uniform bit bound on each of the ten registers bounds the complete stored state.

          source
          theorem Turing.InductiveCounting.length_encState_le_log {N width : ℕ} {s : Cslib.InductiveCounting.State} (h : Cslib.InductiveCounting.Bounded N width s) :
          (encState s).length ≤ 40 * ((Cslib.InductiveCounting.registerBound N width).log2 + 2)

          Every bounded controller state has logarithmic size in its register bound.

          source
          theorem Turing.InductiveCounting.length_encState_le_of_registerBound_le {N width n A D : ℕ} {s : Cslib.InductiveCounting.State} (h : Cslib.InductiveCounting.Bounded N width s) (hbound : Cslib.InductiveCounting.registerBound N width ≤ A * (n + 1) ^ D) :
          (encState s).length ≤ 40 * (A.size + 2 * D + 2) * (n.log2 + 1)

          Polynomial register bounds give native logarithmic-space storage, including on rejecting branches. This estimate concerns the state alone, not a supplied choice history.