TM0 Reverse Block Machine

The machine is parameterized by a separator sep that marks the right end of the block. It works on any separator as long as block elements are distinct from both default (the tape blank) and sep.

Key results

• RevBlock.MSep: the separator-parametric reverse-block TM0 machine.
• RevBlock.full_reaches: the machine reaches a reversed block plus suffix.
• RevBlock.full_reaches_default: blank-delimited specialization.

State type

inductive RevBlock.CarryPhase : Type

• carryRight : CarryPhase
• shifting : CarryPhase
• returning : CarryPhase

instance RevBlock.instDecidableEqCarryPhase : DecidableEq CarryPhase

Equations

• RevBlock.instDecidableEqCarryPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive RevBlock.NoCarryPhase : Type

• grab : NoCarryPhase
• advance : NoCarryPhase
• rewind : NoCarryPhase
• rewindDone : NoCarryPhase

instance RevBlock.instDecidableEqNoCarryPhase : DecidableEq NoCarryPhase

Equations

• RevBlock.instDecidableEqNoCarryPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance RevBlock.instFintypeCarryPhase : Fintype CarryPhase

Equations

• RevBlock.instFintypeCarryPhase = { elems := {RevBlock.CarryPhase.carryRight, RevBlock.CarryPhase.shifting, RevBlock.CarryPhase.returning}, complete := ⋯ }

instance RevBlock.instFintypeNoCarryPhase : Fintype NoCarryPhase

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev RevBlock.RSt (Γ : Type) : Type

Equations

• RevBlock.RSt Γ = (Γ × RevBlock.CarryPhase ⊕ RevBlock.NoCarryPhase)

instance RevBlock.instInhabitedRSt {Γ : Type} [Inhabited Γ] : Inhabited (RSt Γ)

Equations

• RevBlock.instInhabitedRSt = { default := Sum.inr RevBlock.NoCarryPhase.grab }

Machine definition

noncomputable def RevBlock.MSep (Γ : Type) [Inhabited Γ] [DecidableEq Γ] (sep : Γ) : Turing.TM0.Machine Γ (RSt Γ)

Reverse-block machine parameterized by separator sep.

• grab / shifting / returning use sep to detect the right block boundary and as the temporary "erased" marker when a cell is grabbed.
• rewind uses default to find the left edge of the tape.

Equations

• One or more equations did not get rendered due to their size.
• RevBlock.MSep Γ sep (Sum.inl (g, RevBlock.CarryPhase.carryRight)) a = some (Sum.inl (g, RevBlock.CarryPhase.shifting), Turing.TM0.Stmt.move Turing.Dir.right)
• RevBlock.MSep Γ sep (Sum.inr RevBlock.NoCarryPhase.advance) a = some (Sum.inr RevBlock.NoCarryPhase.grab, Turing.TM0.Stmt.move Turing.Dir.right)
• RevBlock.MSep Γ sep (Sum.inr RevBlock.NoCarryPhase.rewindDone) a = none

noncomputable def RevBlock.M (Γ : Type) [Inhabited Γ] [DecidableEq Γ] : Turing.TM0.Machine Γ (RSt Γ)

The original machine with default as separator.

Equations

• RevBlock.M Γ = RevBlock.MSep Γ default

Tape.mk₂ helpers

theorem RevBlock.mk₂_move_right {Γ : Type} [Inhabited Γ] (L : List Γ) (x : Γ) (R : List Γ) : Turing.Tape.move Turing.Dir.right (Turing.Tape.mk₂ L (x :: R)) = Turing.Tape.mk₂ (x :: L) R

theorem RevBlock.mk₂_move_left {Γ : Type} [Inhabited Γ] (x : Γ) (L R : List Γ) : Turing.Tape.move Turing.Dir.left (Turing.Tape.mk₂ (x :: L) R) = Turing.Tape.mk₂ L (x :: R)

theorem RevBlock.mk₂_write {Γ : Type} [Inhabited Γ] (a : Γ) (L : List Γ) (x : Γ) (R : List Γ) : Turing.Tape.write a (Turing.Tape.mk₂ L (x :: R)) = Turing.Tape.mk₂ L (a :: R)

theorem RevBlock.mk₂_head {Γ : Type} [Inhabited Γ] (L : List Γ) (x : Γ) (R : List Γ) : (Turing.Tape.mk₂ L (x :: R)).head = x

theorem RevBlock.mk₂_nil_eq_mk₁ {Γ : Type} [Inhabited Γ] (R : List Γ) : Turing.Tape.mk₂ [] R = Turing.Tape.mk₁ R

Return loop

theorem RevBlock.return_loop {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep carry h : Γ) (elems L_orig R : List Γ) (hh : h ≠ sep) (helems : ∀ y ∈ elems, y ≠ sep) : Turing.Reaches (Turing.TM0.step (MSep Γ sep)) { q := Sum.inl (carry, CarryPhase.returning), Tape := Turing.Tape.mk₂ (elems ++ sep :: L_orig) (h :: R) } { q := Sum.inl (carry, CarryPhase.returning), Tape := Turing.Tape.mk₂ L_orig (sep :: elems.reverse ++ h :: R) }

Return loop: from returning(carry), move left through non-sep head elements. Each step pops from the left and pushes the old head onto the right.

Shift-to-grab

theorem RevBlock.shift_to_grab {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep carry : Γ) (rest shifted L_orig suffix : List Γ) (hcarry : carry ≠ sep) (hrest : ∀ y ∈ rest, y ≠ sep) (hshifted : ∀ y ∈ shifted, y ≠ sep) : Turing.Reaches (Turing.TM0.step (MSep Γ sep)) { q := Sum.inl (carry, CarryPhase.shifting), Tape := Turing.Tape.mk₂ (shifted ++ sep :: L_orig) (rest ++ sep :: suffix) } { q := Sum.inr NoCarryPhase.grab, Tape := Turing.Tape.mk₂ ((carry :: rest).getLast ⋯ :: L_orig) (shifted.reverse ++ (carry :: rest).dropLast ++ sep :: suffix) }

One iteration

theorem RevBlock.one_iteration {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep x : Γ) (rest L_orig suffix : List Γ) (hx : x ≠ sep) (hrest : ∀ y ∈ rest, y ≠ sep) : Turing.Reaches (Turing.TM0.step (MSep Γ sep)) { q := Sum.inr NoCarryPhase.grab, Tape := Turing.Tape.mk₂ L_orig (x :: rest ++ sep :: suffix) } { q := Sum.inr NoCarryPhase.grab, Tape := Turing.Tape.mk₂ ((x :: rest).getLast ⋯ :: L_orig) ((x :: rest).dropLast ++ sep :: suffix) }

Iteration loop

theorem RevBlock.iteration_loop {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep : Γ) (block suffix : List Γ) (hblock : ∀ y ∈ block, y ≠ sep) : Turing.Reaches (Turing.TM0.step (MSep Γ sep)) { q := Sum.inr NoCarryPhase.grab, Tape := Turing.Tape.mk₂ [] (block ++ sep :: suffix) } { q := Sum.inr NoCarryPhase.grab, Tape := Turing.Tape.mk₂ block (sep :: suffix) }

Rewind loop

theorem RevBlock.rewind_loop {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep s : Γ) (rest R_rest : List Γ) (hs : s ≠ default) (hrest : ∀ y ∈ rest, y ≠ default) : Turing.Reaches (Turing.TM0.step (MSep Γ sep)) { q := Sum.inr NoCarryPhase.rewind, Tape := Turing.Tape.mk₂ rest (s :: R_rest) } { q := Sum.inr NoCarryPhase.rewind, Tape := Turing.Tape.mk₂ [] (default :: rest.reverse ++ s :: R_rest) }

Rewind uses default (not sep) to find the left tape edge.

Rewind phase

theorem RevBlock.rewind_phase {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep : Γ) (block suffix : List Γ) (hblock_nd : ∀ y ∈ block, y ≠ default) (hblock_nsep : ∀ y ∈ block, y ≠ sep) : Turing.Reaches (Turing.TM0.step (MSep Γ sep)) { q := Sum.inr NoCarryPhase.grab, Tape := Turing.Tape.mk₂ block (sep :: suffix) } { q := Sum.inr NoCarryPhase.rewindDone, Tape := Turing.Tape.mk₂ [] (block.reverse ++ sep :: suffix) }

Full computation

theorem RevBlock.full_reaches {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep : Γ) (block suffix : List Γ) (hblock_nd : ∀ y ∈ block, y ≠ default) (hblock_nsep : ∀ y ∈ block, y ≠ sep) : Turing.Reaches (Turing.TM0.step (MSep Γ sep)) (Turing.TM0.init (block ++ sep :: suffix)) { q := Sum.inr NoCarryPhase.rewindDone, Tape := Turing.Tape.mk₁ (block.reverse ++ sep :: suffix) }

theorem RevBlock.step_rewindDone {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep : Γ) (T : Turing.Tape Γ) : Turing.TM0.step (MSep Γ sep) { q := Sum.inr NoCarryPhase.rewindDone, Tape := T } = none

Backward compatibility wrappers

theorem RevBlock.full_reaches_default {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (block suffix : List Γ) (hblock : ∀ y ∈ block, y ≠ default) (_hsuf : ∀ y ∈ suffix, y ≠ default) : Turing.Reaches (Turing.TM0.step (M Γ)) (Turing.TM0.init (block ++ default :: suffix)) { q := Sum.inr NoCarryPhase.rewindDone, Tape := Turing.Tape.mk₁ (block.reverse ++ default :: suffix) }

theorem RevBlock.step_rewindDone_default {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (T : Turing.Tape Γ) : Turing.TM0.step (M Γ) { q := Sum.inr NoCarryPhase.rewindDone, Tape := T } = none