Documentation

Complexitylib.Models.RandomAccessMachine.Simulation.RegisterStore.Machine.Program.DenseDefs

Dense-overlay RAM program controller -- definitions #

source
def Complexity.RAM.RegisterStore.Machine.denseProgramOutputTM {n : ℕ} (tapes : ControlInstructionTapes n) :
TM (n + 1)

Recover dense register R₀ through the overlay-aware lookup and emit its Boolean verdict on the real output tape.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Complexity.RAM.RegisterStore.Machine.denseProgramOutputTime {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) (overlay : Store) :
    ℕ

    Exact dense final-verdict extraction bound.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.RAM.RegisterStore.Machine.denseProgramLoopTM {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) :
      TM (n + 1)

      Fixed halt-aware loop for one concrete RAM program using dense overlay steps and the representation-independent halt test.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def Complexity.RAM.RegisterStore.Machine.denseProgramLoopIterationTime {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (input : List Bool) (snapshot : DenseOverlay.Snapshot) :
        ℕ

        Bound for one dense loop body, halt test, their seams, and the three-step rewind/check tail.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def Complexity.RAM.RegisterStore.Machine.denseProgramLoopTime {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (input : List Bool) :
          ℕ → DenseOverlay.Snapshot → ℕ

          Sum of the first fuel dense loop-iteration bounds.

          Equations
          Instances For