Compiled input movement and output emission

Main definitions

• Turing.MultiTapeTM.ToTM2.inputSymbol: the scratch symbol after compiled input movement.

Main results

• Turing.MultiTapeTM.ToTM2.stepAux_moveInput: compiled movement agrees with the raw input zipper, without a validity assumption.
• Turing.MultiTapeTM.ToTM2.stepAux_finish: emit an optional bit and restore boundary control.

def Turing.MultiTapeTM.ToTM2.inputSymbol {k : ℕ} {State : Type} (d : Data k State) (direction : SignType) (scratch : Option Bool) : Option Bool

Input movement retains scratch at the left boundary and otherwise remembers the popped bit.

theorem Turing.MultiTapeTM.ToTM2.stepAux_moveInput {k : ℕ} {State : Type} (d : Data k State) (direction : SignType) (next : Statement k State) (scratch : Option Bool) (busy : Bool) : TM2.stepAux (moveInput direction next) (control d scratch busy) (store d) = TM2.stepAux next (control { state := d.state, input := d.input.move direction, work := d.work, output := d.output } (inputSymbol d direction scratch) busy) (store { state := d.state, input := d.input.move direction, work := d.work, output := d.output })

The compiled input movement agrees with the zipper on every raw configuration.

theorem Turing.MultiTapeTM.ToTM2.stepAux_finish {k : ℕ} {State : Type} (d : Data k State) (state : Option State) (output scratch : Option Bool) (busy : Bool) : TM2.stepAux (output.elim id (fun (b : Bool) => TM2.Stmt.push Stack.reversed fun (x : Control k State) => b) (TM2.Stmt.load (fun (v : Control k State) => { state := state, atLeft := v.atLeft, head := v.head, symbol := none, busy := false }) (TM2.Stmt.goto fun (x : Control k State) => Label.run))) (control d scratch busy) (store d) = encode { state := state, input := d.input, work := d.work, output := d.output ++ output.toList }

Emitting an optional bit and loading the next source state restores a step boundary.