Partial recursiveness of StateTransition, SingleTapeTM, TM0, and TM1

This file establishes Primcodable, Primrec, and Partrec instances and theorems for CSLib's and Mathlib's single-tape Turing machine stack.

Main definitions

• Cslib.Turing.BiTape.extractWord: extracts a word l : List Symbol when a BiTape Symbol is in standard output form BiTape.mk₁ l.
• Cslib.Turing.SingleTapeTM.stepOrStay: total one-step transition function fixing halted configurations (state = none).
• Cslib.Turing.SingleTapeTM.runFor: clocked execution returning some l' when tm reaches haltCfg l' in t steps.
• Cslib.Turing.SingleTapeTM.eval: partial evaluation function List Symbol →. List Symbol of a SingleTapeTM Symbol.

Main results

• Computable.stateTransition_eval: for any Primcodable state type σ and computable step function f : σ → Option σ, StateTransition.eval f : σ →. σ is Partrec (proved directly via Partrec.fix).
• Primrec.list_isEmpty: List.isEmpty is primitive recursive on any Primcodable element type.
• Primcodable and Primrec for StackTape Symbol, BiTape Symbol, _root_.Turing.ListBlank (Option Symbol), and _root_.Turing.Tape (Option Symbol).
• Cslib.Turing.SingleTapeTM.primrec_step, primrec_runFor, partrec_evalInit, partrec_eval, and partrec_eval_right₀: every SingleTapeTM Symbol has primitive recursive step and clocked-run functions and partial recursive evaluation functions.
• Cslib.Turing.SingleTapeTM.partrec_tm0_eval and partrec_tm1_eval: every finitely supported Mathlib TM0 or TM1 machine has a partial recursive evaluation function.

References

• M. Sipser, Introduction to the Theory of Computation

Partrec for StateTransition.eval

theorem Computable.stateTransition_eval {σ : Type u_1} [Primcodable σ] {f : σ → Option σ} (hf : Computable f) : Partrec (StateTransition.eval f)

If f : σ → Option σ is computable on a Primcodable state space σ, then StateTransition.eval f : σ →. σ is partial recursive.

Primcodable and Primrec for StackTape and ListBlank

theorem Primrec.list_isEmpty {α : Type u_1} [Primcodable α] : Primrec List.isEmpty

List.isEmpty is primitive recursive on any Primcodable element type.

def Cslib.Turing.StackTape.equivSubtype {Symbol : Type u_1} : StackTape Symbol ≃ { l : List (Option Symbol) // l.getLast? ≠ some none }

Equivalence between StackTape Symbol and its underlying subtype of List (Option Symbol).

theorem Cslib.Turing.StackTape.primrecPred_getLast?_ne_some_none {Symbol : Type u_1} [Primcodable Symbol] : PrimrecPred fun (l : List (Option Symbol)) => l.getLast? ≠ some none

@[instance_reducible]

instance Cslib.Turing.StackTape.instPrimcodable {Symbol : Type u_1} [Primcodable Symbol] : Primcodable (StackTape Symbol)

theorem Cslib.Turing.StackTape.primrec_toList_iff {Symbol : Type u_1} {α : Type u_2} [Primcodable α] [Primcodable Symbol] {f : α → StackTape Symbol} : (Primrec fun (a : α) => (f a).toList) ↔ Primrec f

theorem Cslib.Turing.StackTape.primrec_toList {Symbol : Type u_1} [Primcodable Symbol] : Primrec toList

theorem Cslib.Turing.StackTape.primrec_tail {Symbol : Type u_1} [Primcodable Symbol] : Primrec tail

theorem Cslib.Turing.StackTape.primrec_head {Symbol : Type u_1} [Primcodable Symbol] : Primrec head

theorem Cslib.Turing.StackTape.primrec_cons {Symbol : Type u_1} [Primcodable Symbol] : Primrec₂ cons

theorem Cslib.Turing.StackTape.primrec_ofList {Symbol : Type u_1} [Primcodable Symbol] : Primrec ofList

theorem Cslib.Turing.StackTape.primrec_mapSome {Symbol : Type u_1} [Primcodable Symbol] : Primrec mapSome

@[instance_reducible]

instance Cslib.Turing.StackTape.instPrimcodableListBlankOption {Symbol : Type u_1} [Primcodable Symbol] : Primcodable (Turing.ListBlank (Option Symbol))

theorem Cslib.Turing.StackTape.primrec_equivListBlank {Symbol : Type u_1} [Primcodable Symbol] : Primrec ⇑equivListBlank

theorem Cslib.Turing.StackTape.primrec_equivListBlank_symm {Symbol : Type u_1} [Primcodable Symbol] : Primrec ⇑equivListBlank.symm

Primcodable and Primrec for BiTape and Turing.Tape

def Cslib.Turing.BiTape.equivTuple {Symbol : Type u_1} : BiTape Symbol ≃ Option Symbol × StackTape Symbol × StackTape Symbol

Equivalence between BiTape Symbol and its triple of fields.

@[instance_reducible]

instance Cslib.Turing.BiTape.instPrimcodable {Symbol : Type u_1} [Primcodable Symbol] : Primcodable (BiTape Symbol)

theorem Cslib.Turing.BiTape.primrec_head {Symbol : Type u_1} [Primcodable Symbol] : Primrec head

theorem Cslib.Turing.BiTape.primrec_left {Symbol : Type u_1} [Primcodable Symbol] : Primrec left

theorem Cslib.Turing.BiTape.primrec_right {Symbol : Type u_1} [Primcodable Symbol] : Primrec right

theorem Cslib.Turing.BiTape.primrec_mk {Symbol : Type u_1} [Primcodable Symbol] {α : Type u_2} [Primcodable α] {h : α → Option Symbol} {l r : α → StackTape Symbol} (hh : Primrec h) (hl : Primrec l) (hr : Primrec r) : Primrec fun (a : α) => { head := h a, left := l a, right := r a }

theorem Cslib.Turing.BiTape.primrec_mk₁ {Symbol : Type u_1} [Primcodable Symbol] : Primrec mk₁

theorem Cslib.Turing.BiTape.primrec_write {Symbol : Type u_1} [Primcodable Symbol] : Primrec₂ write

theorem Cslib.Turing.BiTape.primrec_moveLeft {Symbol : Type u_1} [Primcodable Symbol] : Primrec moveLeft

theorem Cslib.Turing.BiTape.primrec_moveRight {Symbol : Type u_1} [Primcodable Symbol] : Primrec moveRight

def Cslib.Turing.BiTape.dirEquivBool : Turing.Dir ≃ Bool

Equivalence between _root_.Turing.Dir and Bool.

@[instance_reducible]

instance Cslib.Turing.BiTape.instPrimcodableDir : Primcodable Turing.Dir

theorem Cslib.Turing.BiTape.primrec_optionMove {Symbol : Type u_1} [Primcodable Symbol] : Primrec₂ optionMove

@[instance_reducible]

instance Cslib.Turing.BiTape.instPrimcodableTapeOption {Symbol : Type u_1} [Primcodable Symbol] : Primcodable (Turing.Tape (Option Symbol))

theorem Cslib.Turing.BiTape.primrec_equivTape {Symbol : Type u_1} [Primcodable Symbol] : Primrec ⇑equivTape

theorem Cslib.Turing.BiTape.primrec_equivTape_symm {Symbol : Type u_1} [Primcodable Symbol] : Primrec ⇑equivTape.symm

theorem Cslib.Turing.BiTape.primrec_right₀ {Symbol : Type u_1} [Primcodable Symbol] : Primrec fun (T : Turing.Tape (Option Symbol)) => T.right₀

def Cslib.Turing.BiTape.unmapSome {Symbol : Type u_1} : List (Option Symbol) → Option (List Symbol)

Invert List.map some: returns some l if every element is some, and none if any element is none.

@[simp]

theorem Cslib.Turing.BiTape.unmapSome_map_some {Symbol : Type u_1} (l : List Symbol) : unmapSome (List.map some l) = some l

theorem Cslib.Turing.BiTape.unmapSome_eq_some_iff {Symbol : Type u_1} {xs : List (Option Symbol)} {l : List Symbol} : unmapSome xs = some l ↔ xs = List.map some l

theorem Cslib.Turing.BiTape.primrec_unmapSome {Symbol : Type u_1} [Primcodable Symbol] : Primrec unmapSome

def Cslib.Turing.BiTape.extractWord {Symbol : Type u_1} (b : BiTape Symbol) : Option (List Symbol)

Extract the output word l' if b = BiTape.mk₁ l', and none otherwise.

@[simp]

theorem Cslib.Turing.BiTape.extractWord_mk₁ {Symbol : Type u_1} (l : List Symbol) : (mk₁ l).extractWord = some l

theorem Cslib.Turing.BiTape.extractWord_eq_some_iff {Symbol : Type u_1} {b : BiTape Symbol} {l : List Symbol} : b.extractWord = some l ↔ b = mk₁ l

theorem Cslib.Turing.BiTape.primrec_extractWord {Symbol : Type u_1} [Primcodable Symbol] : Primrec extractWord

Primrec and Partrec for SingleTapeTM, TM0, and TM1

def Cslib.Turing.SingleTapeTM.stmtEquiv (Symbol : Type) : Stmt Symbol ≃ Option Symbol × Option Turing.Dir

Equivalence between Stmt Symbol and Option Symbol × Option _root_.Turing.Dir.

@[instance_reducible]

instance Cslib.Turing.SingleTapeTM.instPrimcodableStmt {Symbol : Type} [Primcodable Symbol] : Primcodable (Stmt Symbol)

@[instance_reducible]

noncomputable instance Cslib.Turing.SingleTapeTM.instPrimcodableState {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) : Primcodable tm.State

def Cslib.Turing.SingleTapeTM.cfgEquiv {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) : tm.Cfg ≃ Option tm.State × BiTape Symbol

Equivalence between tm.Cfg and Option tm.State × BiTape Symbol.

@[instance_reducible]

noncomputable instance Cslib.Turing.SingleTapeTM.instPrimcodableCfg {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] [Primcodable Symbol] (tm : SingleTapeTM Symbol) : Primcodable tm.Cfg

theorem Cslib.Turing.SingleTapeTM.primrec_initCfg {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] [Primcodable Symbol] (tm : SingleTapeTM Symbol) : Primrec tm.initCfg

theorem Cslib.Turing.SingleTapeTM.primrec_step {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] [Primcodable Symbol] (tm : SingleTapeTM Symbol) : Primrec tm.step

The single-step transition function of any SingleTapeTM is primitive recursive.

theorem Cslib.Turing.SingleTapeTM.partrec_stateTransition_eval {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] [Primcodable Symbol] (tm : SingleTapeTM Symbol) : Partrec (StateTransition.eval tm.step)

StateTransition.eval tm.step is partial recursive for every SingleTapeTM Symbol.

theorem Cslib.Turing.SingleTapeTM.partrec_evalInit {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] [Primcodable Symbol] (tm : SingleTapeTM Symbol) : Partrec fun (l : List Symbol) => StateTransition.eval tm.step (tm.initCfg l)

Evaluating tm from tm.initCfg l to its final configuration is partial recursive.

def Cslib.Turing.SingleTapeTM.stepOrStay {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (c : tm.Cfg) : tm.Cfg

Self-looping step function on tm.Cfg: halted configurations remain fixed.

@[simp]

theorem Cslib.Turing.SingleTapeTM.stepOrStay_of_none {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (b : BiTape Symbol) : tm.stepOrStay { state := none, BiTape := b } = { state := none, BiTape := b }

theorem Cslib.Turing.SingleTapeTM.stepOrStay_of_transition {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) {c c' : tm.Cfg} (h : tm.TransitionRelation c c') : tm.stepOrStay c = c'

theorem Cslib.Turing.SingleTapeTM.stepOrStay_iterate_of_none {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (b : BiTape Symbol) (k : ℕ) : tm.stepOrStay^[k] { state := none, BiTape := b } = { state := none, BiTape := b }

theorem Cslib.Turing.SingleTapeTM.stepOrStay_iterate_of_relatesInSteps {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) {c₁ c₂ : tm.Cfg} {n : ℕ} (h : Relation.RelatesInSteps tm.TransitionRelation c₁ c₂ n) : tm.stepOrStay^[n] c₁ = c₂

theorem Cslib.Turing.SingleTapeTM.relatesWithinSteps_stepOrStay_iterate {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (c : tm.Cfg) (t : ℕ) : Relation.RelatesWithinSteps tm.TransitionRelation c (tm.stepOrStay^[t] c) t

theorem Cslib.Turing.SingleTapeTM.outputsWithinTime_iff_stepOrStay_iterate {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (l l' : List Symbol) (t : ℕ) : tm.OutputsWithinTime l l' t ↔ tm.stepOrStay^[t] (tm.initCfg l) = tm.haltCfg l'

tm.OutputsWithinTime l l' t holds if and only if t iterations of tm.stepOrStay from tm.initCfg l equal tm.haltCfg l'.

theorem Cslib.Turing.SingleTapeTM.primrec_stepOrStay {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] [Primcodable Symbol] (tm : SingleTapeTM Symbol) : Primrec tm.stepOrStay

def Cslib.Turing.SingleTapeTM.runFor {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (l : List Symbol) (t : ℕ) : Option (List Symbol)

Clocked run of tm: after t steps on input l, returns some l' if tm has halted in tm.haltCfg l', and none otherwise.

theorem Cslib.Turing.SingleTapeTM.mem_runFor_iff {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) {l l' : List Symbol} {t : ℕ} : l' ∈ tm.runFor l t ↔ tm.OutputsWithinTime l l' t

l' ∈ tm.runFor l t holds if and only if tm.OutputsWithinTime l l' t.

theorem Cslib.Turing.SingleTapeTM.runFor_mono {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (l : List Symbol) {t₁ t₂ : ℕ} (ht : t₁ ≤ t₂) {l' : List Symbol} (h : l' ∈ tm.runFor l t₁) : l' ∈ tm.runFor l t₂

theorem Cslib.Turing.SingleTapeTM.primrec_runFor {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] [Primcodable Symbol] (tm : SingleTapeTM Symbol) : Primrec₂ tm.runFor

def Cslib.Turing.SingleTapeTM.eval {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (l : List Symbol) : Part (List Symbol)

Partial evaluation of tm on input words: tm.eval l evaluates to l' iff tm.Outputs l l'.

@[simp]

theorem Cslib.Turing.SingleTapeTM.mem_eval_iff_outputs {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) {l l' : List Symbol} : l' ∈ tm.eval l ↔ tm.Outputs l l'

theorem Cslib.Turing.SingleTapeTM.partrec_eval {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] [Primcodable Symbol] (tm : SingleTapeTM Symbol) : Partrec tm.eval

The partial word evaluation tm.eval of any SingleTapeTM Symbol is partial recursive.

theorem Cslib.Turing.SingleTapeTM.partrec_eval_right₀ {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] [Primcodable Symbol] (tm : SingleTapeTM Symbol) : Partrec fun (l : List Symbol) => Part.map (fun (c : tm.Cfg) => (BiTape.equivTape c.BiTape).right₀) (StateTransition.eval tm.step (tm.initCfg l))

Evaluating tm from tm.initCfg l and reading the right half-tape right₀ of its final configuration is partial recursive.

theorem Cslib.Turing.SingleTapeTM.partrec_tm0_eval {Symbol : Type} [Inhabited Symbol] [Finite Symbol] [Primcodable Symbol] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option Symbol) Λ) (S : Finset Λ) (hs : Turing.TM0.Supports M ↑S) : Partrec fun (l : List Symbol) => Turing.TM0.eval M (List.map some l)

For any finitely supported Mathlib _root_.Turing.TM0.Machine, its partial evaluation fun l => _root_.Turing.TM0.eval M (l.map some) is Partrec.

theorem Cslib.Turing.SingleTapeTM.partrec_tm1_eval {Symbol : Type} [Inhabited Symbol] [Finite Symbol] [Primcodable Symbol] {Λ σ : Type} [Inhabited Λ] [Inhabited σ] [Finite σ] (M : Λ → Turing.TM1.Stmt (Option Symbol) Λ σ) (S : Finset Λ) (hs : Turing.TM1.Supports M S) : Partrec fun (l : List Symbol) => Turing.TM1.eval M (List.map some l)

For any finitely supported Mathlib _root_.Turing.TM1 statement family, its partial evaluation fun l => _root_.Turing.TM1.eval M (l.map some) is Partrec.