TM0 Blank-Free Map Machine

This file provides the TM0 machine that maps a function over a blank-free input block and rewinds to the left edge.

Main results

• TM0BB.mapM — the concrete map-and-rewind TM0 machine.
• TM0BB.tm0_map_blankfree — a TM0 that applies a function to each cell of a blank-free list, producing Tape.mk₁ (l.map f) as the output tape.

States for the map machine

inductive TM0BB.MState : Type

• start : MState
• readNext : MState
• advance : MState
• rewind : MState
• done : MState

instance TM0BB.instDecidableEqMState : DecidableEq MState

Equations

• TM0BB.instDecidableEqMState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def TM0BB.instReprMState.repr : MState → ℕ → Std.Format

Equations

• TM0BB.instReprMState.repr TM0BB.MState.start prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TM0BB.MState.start")).group prec✝
• TM0BB.instReprMState.repr TM0BB.MState.readNext prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TM0BB.MState.readNext")).group prec✝
• TM0BB.instReprMState.repr TM0BB.MState.advance prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TM0BB.MState.advance")).group prec✝
• TM0BB.instReprMState.repr TM0BB.MState.rewind prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TM0BB.MState.rewind")).group prec✝
• TM0BB.instReprMState.repr TM0BB.MState.done prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TM0BB.MState.done")).group prec✝

instance TM0BB.instReprMState : Repr MState

Equations

• TM0BB.instReprMState = { reprPrec := TM0BB.instReprMState.repr }

instance TM0BB.instInhabitedMState : Inhabited MState

Equations

• TM0BB.instInhabitedMState = { default := TM0BB.MState.start }

instance TM0BB.instFintypeMState : Fintype MState

Equations

• TM0BB.instFintypeMState = { elems := {TM0BB.MState.start, TM0BB.MState.readNext, TM0BB.MState.advance, TM0BB.MState.rewind, TM0BB.MState.done}, complete := TM0BB.instFintypeMState._proof_1 }

Machine Definition

noncomputable def TM0BB.mapM {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (f : Γ → Γ) : Turing.TM0.Machine Γ MState

Equations

• TM0BB.mapM f TM0BB.MState.start a = if a = default then none else some (TM0BB.MState.advance, Turing.TM0.Stmt.write (f a))
• TM0BB.mapM f TM0BB.MState.readNext a = if a = default then some (TM0BB.MState.rewind, Turing.TM0.Stmt.move Turing.Dir.left) else some (TM0BB.MState.advance, Turing.TM0.Stmt.write (f a))
• TM0BB.mapM f TM0BB.MState.advance a = some (TM0BB.MState.readNext, Turing.TM0.Stmt.move Turing.Dir.right)
• TM0BB.mapM f TM0BB.MState.rewind a = if a = default then some (TM0BB.MState.done, Turing.TM0.Stmt.move Turing.Dir.right) else some (TM0BB.MState.rewind, Turing.TM0.Stmt.move Turing.Dir.left)
• TM0BB.mapM f TM0BB.MState.done a = none

Step lemmas

@[simp]

theorem TM0BB.mapM_start_nondefault {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (f : Γ → Γ) (a : Γ) (ha : a ≠ default) : mapM f MState.start a = some (MState.advance, Turing.TM0.Stmt.write (f a))

@[simp]

theorem TM0BB.mapM_start_default {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (f : Γ → Γ) : mapM f MState.start default = none

@[simp]

theorem TM0BB.mapM_readNext_nondefault {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (f : Γ → Γ) (a : Γ) (ha : a ≠ default) : mapM f MState.readNext a = some (MState.advance, Turing.TM0.Stmt.write (f a))

@[simp]

theorem TM0BB.mapM_readNext_default {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (f : Γ → Γ) : mapM f MState.readNext default = some (MState.rewind, Turing.TM0.Stmt.move Turing.Dir.left)

@[simp]

theorem TM0BB.mapM_advance {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (f : Γ → Γ) (a : Γ) : mapM f MState.advance a = some (MState.readNext, Turing.TM0.Stmt.move Turing.Dir.right)

@[simp]

theorem TM0BB.mapM_rewind_nondefault {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (f : Γ → Γ) (a : Γ) (ha : a ≠ default) : mapM f MState.rewind a = some (MState.rewind, Turing.TM0.Stmt.move Turing.Dir.left)

@[simp]

theorem TM0BB.mapM_rewind_default {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (f : Γ → Γ) : mapM f MState.rewind default = some (MState.done, Turing.TM0.Stmt.move Turing.Dir.right)

@[simp]

theorem TM0BB.mapM_done {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (f : Γ → Γ) (a : Γ) : mapM f MState.done a = none

Forward phase helper

theorem TM0BB.readNext_process_one {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (f : Γ → Γ) (a : Γ) (ha : a ≠ default) (L R : Turing.ListBlank Γ) : Turing.Reaches (Turing.TM0.step (mapM f)) { q := MState.readNext, Tape := { head := a, left := L, right := R } } { q := MState.readNext, Tape := { head := R.head, left := Turing.ListBlank.cons (f a) L, right := R.tail } }

theorem TM0BB.forward_phase_cons {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (f : Γ → Γ) (a : Γ) (rest : List Γ) (ha : a ≠ default) (hrest : ∀ x ∈ rest, x ≠ default) : Turing.Reaches (Turing.TM0.step (mapM f)) (Turing.TM0.init (a :: rest)) { q := MState.readNext, Tape := Turing.Tape.mk' (Turing.ListBlank.mk (List.map f (a :: rest)).reverse) (Turing.ListBlank.mk []) }

ListBlank helpers

@[simp]

theorem TM0BB.listBlank_cons_default_nil {Γ : Type} [Inhabited Γ] : Turing.ListBlank.cons default (Turing.ListBlank.mk []) = Turing.ListBlank.mk []

theorem TM0BB.tape_mk'_eq_mk₁ {Γ : Type} [Inhabited Γ] (l : List Γ) : Turing.Tape.mk' (Turing.ListBlank.mk []) (Turing.ListBlank.mk l) = Turing.Tape.mk₁ l

Rewind phase

theorem TM0BB.rewind_loop {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (f : Γ → Γ) (L : List Γ) (hL : ∀ x ∈ L, x ≠ default) (acc : List Γ) : Turing.Reaches (Turing.TM0.step (mapM f)) { q := MState.rewind, Tape := { head := L.headI, left := Turing.ListBlank.mk L.tail, right := Turing.ListBlank.mk acc } } { q := MState.rewind, Tape := { head := default, left := Turing.ListBlank.mk [], right := Turing.ListBlank.mk (L.reverse ++ acc) } }

theorem TM0BB.rewind_phase {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (f : Γ → Γ) (rev_list : List Γ) (hm : ∀ x ∈ rev_list, x ≠ default) : Turing.Reaches (Turing.TM0.step (mapM f)) { q := MState.readNext, Tape := Turing.Tape.mk' (Turing.ListBlank.mk rev_list) (Turing.ListBlank.mk []) } { q := MState.done, Tape := Turing.Tape.mk₁ rev_list.reverse }

Main theorem

theorem TM0BB.tm0_map_blankfree {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (f : Γ → Γ) (_hf : f default = default) (hf_noblank : ∀ (a : Γ), a ≠ default → f a ≠ default) : ∃ (Λ : Type) (x : Inhabited Λ) (x_1 : Fintype Λ) (M : Turing.TM0.Machine Γ Λ), ∀ (l : List Γ), (∀ x ∈ l, x ≠ default) → (TM0Seq.evalCfg M l).Dom ∧ ∀ (h : (TM0Seq.evalCfg M l).Dom), ((TM0Seq.evalCfg M l).get h).Tape = Turing.Tape.mk₁ (List.map f l)