Documentation

Complexity.Computability.Machines.Turing.TM2.Reverse.Representation

Stack representation for the reverse TM2 compiler #

Each native transition compiles to one fixed Mathlib stack-machine statement. The finite control holds the current work cells; raw stacks retain blank cells and preserve the two-sided geometry.

Main definitions #

source
def Turing.MultiTapeTM.ToTM2.control {k : ℕ} {State : Type} (d : Data k State) (symbol : Option Bool := none) (busy : Bool := false) :
Control k State

Finite control corresponding to raw simulation data, with arbitrary scratch registers.

Instances For
    source
    def Turing.MultiTapeTM.ToTM2.store {k : ℕ} {State : Type} (d : Data k State) (s : Stack k) :
    List (Alphabet s)

    The stack representation keeps output in reverse order until cleanup.

    Instances For
      source
      def Turing.MultiTapeTM.ToTM2.encode {k : ℕ} {State : Type} (d : Data k State) :
      TM2.Cfg Alphabet Label (Control k State)

      The TM2 configuration at a source-step boundary.

      Instances For