A bounded input zipper for the TM2 compiler

The left stack is reversed and the right stack includes the symbol under the head. A separate flag distinguishes the left boundary from the first input symbol. An empty right stack with the flag unset represents the right boundary, including the initial position on empty input.

Main definitions

• Turing.MultiTapeTM.ToTM2.Input: the two stacks and the left-boundary flag.
• Turing.MultiTapeTM.ToTM2.Input.Represents: agreement with a native input and head position.

Main results

• Turing.MultiTapeTM.ToTM2.Input.represents_init: initialization represents native position one.
• Turing.MultiTapeTM.ToTM2.Input.Represents.read_eq_inputSymbol: reads agree with native reads.
• Turing.MultiTapeTM.ToTM2.Input.Represents.move: moves agree, including boundary clamping.

structure Turing.MultiTapeTM.ToTM2.Input (Symbol : Type) : Type

A read-only input tape represented by two stacks and a left-boundary flag.

• left : List Symbol

  Input symbols strictly to the left of the head, in reverse order.

• right : List Symbol

  Input symbols from the head onward, in input order.

• atLeft : Bool

  Whether the head is at the blank before the input.

theorem Turing.MultiTapeTM.ToTM2.Input.ext {Symbol : Type} {x y : Input Symbol} (left : x.left = y.left) (right : x.right = y.right) (atLeft : x.atLeft = y.atLeft) : x = y

theorem Turing.MultiTapeTM.ToTM2.Input.ext_iff {Symbol : Type} {x y : Input Symbol} : x = y ↔ x.left = y.left ∧ x.right = y.right ∧ x.atLeft = y.atLeft

@[instance_reducible]

instance Turing.MultiTapeTM.ToTM2.instInhabitedInput {a✝ : Type} : Inhabited (Input a✝)

def Turing.MultiTapeTM.ToTM2.Input.init {Symbol : Type} (input : List Symbol) : Input Symbol

Start at native position one, also when the input is empty.

def Turing.MultiTapeTM.ToTM2.Input.read {Symbol : Type} (z : Input Symbol) : Option Symbol

Read the current input symbol, or a blank at either boundary.

def Turing.MultiTapeTM.ToTM2.Input.moveLeft {Symbol : Type} (z : Input Symbol) : Input Symbol

Move left, stopping at the blank before the input.

def Turing.MultiTapeTM.ToTM2.Input.moveRight {Symbol : Type} (z : Input Symbol) : Input Symbol

Move right, stopping at the blank after the input.

def Turing.MultiTapeTM.ToTM2.Input.move {Symbol : Type} (z : Input Symbol) : SignType → Input Symbol

Move the input head in the indicated direction.

structure Turing.MultiTapeTM.ToTM2.Input.Represents {Symbol : Type} (z : Input Symbol) (input : List Symbol) (pos : Fin (input.length + 2)) : Prop

The stacks reconstruct the input and locate the head at the native bounded position.

• contents : z.left.reverse ++ z.right = input

  The two stacks hold exactly the original input.

• left_nil : z.atLeft = true → z.left = []

  No symbols precede the left boundary.

• pos_eq : ↑pos = if z.atLeft = true then 0 else z.left.length + 1

  Native positions count the left boundary as zero.

theorem Turing.MultiTapeTM.ToTM2.Input.represents_init {Symbol : Type} (input : List Symbol) : (init input).Represents input ⟨1, ⋯⟩

Initialization agrees with the native initial head position, including on empty input.

theorem Turing.MultiTapeTM.ToTM2.Input.Represents.length_eq {Symbol : Type} {z : Input Symbol} {input : List Symbol} {pos : Fin (input.length + 2)} (h : z.Represents input pos) : z.left.length + z.right.length = input.length

The stacks retain exactly the number of input symbols.

theorem Turing.MultiTapeTM.ToTM2.Input.Represents.read_eq_getElem? {Symbol : Type} {z : Input Symbol} {input : List Symbol} {pos : Fin (input.length + 2)} (h : z.Represents input pos) : z.read = if ↑pos = 0 then none else input[↑pos - 1]?

A zipper read agrees with indexing the original input at the native head position.

theorem Turing.MultiTapeTM.ToTM2.Input.Represents.read_eq_inputSymbol {Symbol : Type} {z : Input Symbol} {input : List Symbol} {k : ℕ} {State : Type u_1} {cfg : Cfg k Symbol State input} (h : z.Represents input cfg.inputPos) : z.read = cfg.inputSymbol

A zipper read agrees with the input symbol of any represented native configuration.

theorem Turing.MultiTapeTM.ToTM2.Input.Represents.moveLeft {Symbol : Type} {z : Input Symbol} {input : List Symbol} {pos : Fin (input.length + 2)} (h : z.Represents input pos) : z.moveLeft.Represents input (moveInputPos pos SignType.neg)

Moving left preserves the representation, with clamping at the left boundary.

theorem Turing.MultiTapeTM.ToTM2.Input.Represents.moveRight {Symbol : Type} {z : Input Symbol} {input : List Symbol} {pos : Fin (input.length + 2)} (h : z.Represents input pos) : z.moveRight.Represents input (moveInputPos pos SignType.pos)

Moving right preserves the representation, with clamping at the right boundary.

theorem Turing.MultiTapeTM.ToTM2.Input.Represents.move {Symbol : Type} {z : Input Symbol} {input : List Symbol} {pos : Fin (input.length + 2)} (h : z.Represents input pos) (d : SignType) : (z.move d).Represents input (moveInputPos pos d)

Each zipper move simulates the corresponding native bounded head move.