Partial recursiveness of MultiTapeTM and bridges to Mathlib computability

This file proves that the universal multi-tape simulator Turing.MultiTapeTM.Universal.simulate is primitive recursive (Primrec) and bridges multi-tape Turing machine computability, decidability, and mapping reductions with Mathlib's Partrec, Computable, ComputablePred, and ManyOneReducible.

Main definitions

• Turing.MultiTapeTM.Universal.Desc.runFor and Desc.eval: clocked and unbounded evaluation of a universal machine description Desc.
• Turing.MultiTapeTM.runFor and MultiTapeTM.eval: clocked and unbounded partial evaluation of a multi-tape Turing machine MultiTapeTM k Symbol State.

Main results

• Turing.MultiTapeTM.Universal.primrec_simulate and Desc.partrec_eval: simulate is Primrec and Desc.eval is Partrec, characterizing Desc.Computes and Desc.Halts.
• Turing.MultiTapeTM.primrec_runFor and MultiTapeTM.partrec_eval: for every finite-state binary multi-tape Turing machine tm : MultiTapeTM k Bool State, tm.runFor is Primrec₂ and tm.eval is Partrec.
• Turing.MultiTapeTM.IsComputable.computable, IsComputable.computable_bits, IsComputable.computable_bool, IsComputable.computable_option, IsComputable.computable_option_bits, and ComputableInPolyTime.isComputable: every function satisfying IsComputable f encIn encOut (with computable encIn and left-invertible encOut) is Computable in Mathlib's sense, and polynomial-time functions are IsComputable.
• Turing.MultiTapeTM.computable_frame, Turing.MultiTapeTM.primrec_encUnary, Turing.MultiTapeTM.computable_encUnary, and Turing.MultiTapeTM.computable_encPair: Mathlib Primrec/Computable certificates for frame, encUnary, and encPair.
• Turing.MultiTapeTM.IsDecidable.computablePred and IsDecidable.computablePred_bits: every set satisfying MultiTapeTM.IsDecidable L enc (with computable enc) satisfies Mathlib's ComputablePred (· ∈ L).
• Turing.MultiTapeTM.MappingReducible.manyOneReducible and MappingReducible.manyOneReducible_bits: every MultiTapeTM.MappingReducible reduction induces a Mathlib ManyOneReducible (≤₀) reduction.

References

• M. Sipser, Introduction to the Theory of Computation

Primcodable instances for Universal types

def Turing.MultiTapeTM.Universal.signTypeEquivFin3 : SignType ≃ Fin 3

Equivalence between SignType and Fin 3.

@[instance_reducible]

instance Turing.MultiTapeTM.Universal.instPrimcodableSignType : Primcodable SignType

def Turing.MultiTapeTM.Universal.intEquivNatSumNat : ℤ ≃ ℕ ⊕ ℕ

Equivalence between ℤ and ℕ ⊕ ℕ.

def Turing.MultiTapeTM.Universal.Key.equivTuple : Key ≃ ℕ × Option ℕ × List (Option ℕ)

Equivalence between Key and its tuple of fields.

@[instance_reducible]

instance Turing.MultiTapeTM.Universal.instPrimcodableKey : Primcodable Key

def Turing.MultiTapeTM.Universal.Act.equivTuple : Act ≃ SignType × List (Option (Option ℕ) × SignType) × Option ℕ × Option ℕ

Equivalence between Act and its tuple of fields.

@[instance_reducible]

instance Turing.MultiTapeTM.Universal.instPrimcodableAct : Primcodable Act

def Turing.MultiTapeTM.Universal.Desc.equivTuple : Desc ≃ ℕ × ℕ × List (Key × Act)

Equivalence between Desc and its tuple of fields.

@[instance_reducible]

instance Turing.MultiTapeTM.Universal.instPrimcodableDesc : Primcodable Desc

def Turing.MultiTapeTM.Universal.Tape.equivTuple : Tape ≃ (ℕ ⊕ ℕ) × List (Option ℕ) × List (Option ℕ)

Equivalence between Universal.Tape and its tuple of fields (with ℤ encoded as ℕ ⊕ ℕ).

@[instance_reducible]

instance Turing.MultiTapeTM.Universal.instPrimcodableTape : Primcodable Tape

def Turing.MultiTapeTM.Universal.SCfg.equivTuple : SCfg ≃ Option ℕ × ℕ × List Tape

Equivalence between SCfg and its tuple of fields.

@[instance_reducible]

instance Turing.MultiTapeTM.Universal.instPrimcodableSCfg : Primcodable SCfg

Primrec for Universal.simulate

theorem Turing.MultiTapeTM.Universal.primrec_intAddOne : Primrec fun (s : ℕ ⊕ ℕ) => intEquivNatSumNat (intEquivNatSumNat.symm s + 1)

theorem Turing.MultiTapeTM.Universal.primrec_intSubOne : Primrec fun (s : ℕ ⊕ ℕ) => intEquivNatSumNat (intEquivNatSumNat.symm s - 1)

theorem Turing.MultiTapeTM.Universal.primrec_tape_head : Primrec fun (t : Tape) => intEquivNatSumNat t.head

theorem Turing.MultiTapeTM.Universal.primrec_tape_left : Primrec Tape.left

theorem Turing.MultiTapeTM.Universal.primrec_tape_right : Primrec Tape.right

theorem Turing.MultiTapeTM.Universal.primrec_tape_mk {α : Type u_1} [Primcodable α] {h : α → ℕ ⊕ ℕ} {l r : α → List (Option ℕ)} (hh : Primrec h) (hl : Primrec l) (hr : Primrec r) : Primrec fun (a : α) => { head := intEquivNatSumNat.symm (h a), left := l a, right := r a }

theorem Turing.MultiTapeTM.Universal.primrec_list_headD_none : Primrec fun (l : List (Option ℕ)) => l.headD none

theorem Turing.MultiTapeTM.Universal.primrec_tape_read : Primrec Tape.read

theorem Turing.MultiTapeTM.Universal.primrec_tape_write : Primrec₂ Tape.write

theorem Turing.MultiTapeTM.Universal.primrec_tape_move : Primrec₂ Tape.move

theorem Turing.MultiTapeTM.Universal.primrec_tape_apply : Primrec₂ Tape.apply

theorem Turing.MultiTapeTM.Universal.primrec_inputSymbol : Primrec₂ inputSymbol

theorem Turing.MultiTapeTM.Universal.primrec_moveInput : Primrec fun (p : ℕ × Option ℕ × SignType) => moveInput p.1 p.2.1 p.2.2

theorem Turing.MultiTapeTM.Universal.applyTapes_eq_map_range (ts : List Tape) (as : List (Option (Option ℕ) × SignType)) : applyTapes ts as = List.map (fun (i : ℕ) => match ts[i]?, as[i]? with | some t, some a => t.apply a | some t, none => t | none, x => default) (List.range ts.length)

theorem Turing.MultiTapeTM.Universal.primrec_applyTapes : Primrec₂ applyTapes

theorem Turing.MultiTapeTM.Universal.primrec_scfg_state : Primrec SCfg.state

theorem Turing.MultiTapeTM.Universal.primrec_scfg_inputPos : Primrec SCfg.inputPos

theorem Turing.MultiTapeTM.Universal.primrec_scfg_workTapes : Primrec SCfg.workTapes

theorem Turing.MultiTapeTM.Universal.primrec_scfg_mk {α : Type u_1} [Primcodable α] {s : α → Option ℕ} {i : α → ℕ} {w : α → List Tape} (hs : Primrec s) (hi : Primrec i) (hw : Primrec w) : Primrec fun (a : α) => { state := s a, inputPos := i a, workTapes := w a }

theorem Turing.MultiTapeTM.Universal.primrec_act_inputTape : Primrec Act.inputTape

theorem Turing.MultiTapeTM.Universal.primrec_act_workTapes : Primrec Act.workTapes

theorem Turing.MultiTapeTM.Universal.primrec_act_output : Primrec Act.output

theorem Turing.MultiTapeTM.Universal.primrec_act_state : Primrec Act.state

theorem Turing.MultiTapeTM.Universal.primrec_act_apply : Primrec fun (p : Act × List ℕ × SCfg) => p.1.apply p.2.1 p.2.2

theorem Turing.MultiTapeTM.Universal.primrec_scfg_key : Primrec fun (p : SCfg × List ℕ × ℕ) => p.1.key p.2.1 p.2.2

theorem Turing.MultiTapeTM.Universal.primrec_find_table : Primrec₂ fun (table : List (Key × Act)) (k : Key) => List.find? (fun (x : Key × Act) => decide (x.1 = k)) table

theorem Turing.MultiTapeTM.Universal.primrec_desc_tapes : Primrec Desc.tapes

theorem Turing.MultiTapeTM.Universal.primrec_desc_q₀ : Primrec Desc.q₀

theorem Turing.MultiTapeTM.Universal.primrec_desc_table : Primrec Desc.table

theorem Turing.MultiTapeTM.Universal.primrec_step : Primrec fun (p : Desc × List ℕ × SCfg) => step p.1 p.2.1 p.2.2

theorem Turing.MultiTapeTM.Universal.primrec_stepOut : Primrec fun (p : (Desc × List ℕ) × SCfg × List ℕ) => stepOut p.1.1 p.1.2 p.2

theorem Turing.MultiTapeTM.Universal.primrec_init : Primrec init

theorem Turing.MultiTapeTM.Universal.primrec_simulate : Primrec fun (p : Desc × List ℕ × ℕ) => simulate p.1 p.2.1 p.2.2

The universal simulator Universal.simulate is primitive recursive.

Partial recursive evaluation of Desc

theorem Turing.MultiTapeTM.Universal.stepOut_of_state_none (d : Desc) (x : List ℕ) (c : SCfg) (out : List ℕ) (h : c.state = none) : stepOut d x (c, out) = (c, out)

theorem Turing.MultiTapeTM.Universal.stepOut_iterate_of_state_none (d : Desc) (x : List ℕ) (c : SCfg) (out : List ℕ) (h : c.state = none) (k : ℕ) : (stepOut d x)^[k] (c, out) = (c, out)

theorem Turing.MultiTapeTM.Universal.simulate_eq_of_halted {d : Desc} {x out : List ℕ} {t₁ t₂ : ℕ} (ht : t₁ ≤ t₂) (h : simulate d x t₁ = (out, true)) : simulate d x t₂ = (out, true)

def Turing.MultiTapeTM.Universal.Desc.runFor (d : Desc) (x : List ℕ) (t : ℕ) : Option (List ℕ)

Clocked evaluation of a machine description d on input x after t steps.

theorem Turing.MultiTapeTM.Universal.Desc.mem_runFor_iff {d : Desc} {x out : List ℕ} {t : ℕ} : out ∈ d.runFor x t ↔ simulate d x t = (out, true)

theorem Turing.MultiTapeTM.Universal.Desc.runFor_mono (d : Desc) (x : List ℕ) {t₁ t₂ : ℕ} (ht : t₁ ≤ t₂) {out : List ℕ} (h : out ∈ d.runFor x t₁) : out ∈ d.runFor x t₂

theorem Turing.MultiTapeTM.Universal.Desc.primrec_runFor : Primrec₂ fun (dx : Desc × List ℕ) (t : ℕ) => dx.1.runFor dx.2 t

def Turing.MultiTapeTM.Universal.Desc.eval (d : Desc) (x : List ℕ) : Part (List ℕ)

Partial evaluation of a machine description d on input x.

@[simp]

theorem Turing.MultiTapeTM.Universal.Desc.mem_eval_iff_computes {d : Desc} {x out : List ℕ} : out ∈ d.eval x ↔ d.Computes x out

@[simp]

theorem Turing.MultiTapeTM.Universal.Desc.dom_eval_iff_halts {d : Desc} {x : List ℕ} : (d.eval x).Dom ↔ d.Halts x

theorem Turing.MultiTapeTM.Universal.Desc.partrec_eval : Partrec fun (p : Desc × List ℕ) => p.1.eval p.2

Evaluating a machine description (d, x) ↦ d.eval x is partial recursive.

Partial recursiveness of MultiTapeTM and bridges to Computable

noncomputable def Turing.MultiTapeTM.runFor {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (x : List Symbol) (t : ℕ) : Option (List Symbol)

Clocked run of a MultiTapeTM: returns some output if tm has halted after t steps on x, and none otherwise.

theorem Turing.MultiTapeTM.mem_runFor_iff {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) {x y : List Symbol} {t : ℕ} : y ∈ tm.runFor x t ↔ (runFrom (tm.initCfg x) t).Halted ∧ (runFrom (tm.initCfg x) t).output = y

theorem Turing.MultiTapeTM.runFor_mono {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (x : List Symbol) {t₁ t₂ : ℕ} (ht : t₁ ≤ t₂) {y : List Symbol} (h : y ∈ tm.runFor x t₁) : y ∈ tm.runFor x t₂

noncomputable def Turing.MultiTapeTM.eval {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (x : List Symbol) : Part (List Symbol)

Partial evaluation of a MultiTapeTM: tm.eval x evaluates to y iff tm.Computes x y.

@[simp]

theorem Turing.MultiTapeTM.mem_eval_iff_computes {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) {x y : List Symbol} : y ∈ tm.eval x ↔ tm.Computes x y

@[simp]

theorem Turing.MultiTapeTM.dom_eval_iff_halts {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) {x : List Symbol} : (tm.eval x).Dom ↔ tm.Halts x

theorem Turing.MultiTapeTM.runFor_eq_simulate {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) [Fintype State] (eS : State ↪ ℕ) (x : List Bool) (t : ℕ) : tm.runFor x t = have r := Universal.simulate (Universal.desc eS Universal.eBit tm) (List.map (⇑Universal.eBit) x) t; if r.2 = true then some (List.map (fun (x : ℕ) => x != 0) r.1) else none

theorem Turing.MultiTapeTM.primrec_runFor {k : ℕ} {State : Type} [Finite State] (tm : MultiTapeTM k Bool State) : Primrec₂ tm.runFor

For every finite-state binary MultiTapeTM, its clocked run tm.runFor is primitive recursive.

theorem Turing.MultiTapeTM.partrec_eval {k : ℕ} {State : Type} [Finite State] (tm : MultiTapeTM k Bool State) : Partrec tm.eval

For every finite-state binary MultiTapeTM, its partial evaluation tm.eval is partial recursive.

Bridges from IsComputable, IsDecidable, and MappingReducible to Mathlib

theorem Turing.MultiTapeTM.IsComputable.computable_enc {α : Type u_1} {β : Type u_2} [Primcodable α] {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} (hf : IsComputable f encIn encOut) (hIn : Computable ⇑encIn) : Computable fun (a : α) => encOut (f a)

If IsComputable f encIn encOut and encIn is Computable, then fun a => encOut (f a) is Computable in Mathlib's sense.

theorem Turing.MultiTapeTM.IsComputable.computable {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {decOut : List Bool → β} (hf : IsComputable f encIn encOut) (hIn : Computable ⇑encIn) (hOut : Computable decOut) (hdec : ∀ (b : β), decOut (encOut b) = b) : Computable f

If IsComputable f encIn encOut, encIn is Computable, and decOut is a computable left inverse of encOut, then f is Computable in Mathlib's sense.

theorem Turing.MultiTapeTM.IsComputable.computable_bits {f : List Bool → List Bool} (hf : IsComputable f encBits encBits) : Computable f

Any function f : List Bool → List Bool that is MultiTapeTM.IsComputable under the identity encoding encBits is Computable in Mathlib's sense.

theorem Turing.MultiTapeTM.IsComputable.computable_bool {α : Type u_1} [Primcodable α] {f : α → Bool} {encIn : α ↪ List Bool} (hf : IsComputable f encIn encBool) (hIn : Computable ⇑encIn) : Computable f

Any Boolean-valued function f : α → Bool that is MultiTapeTM.IsComputable with respect to a computable input encoding encIn and encBool is Computable in Mathlib's sense.

theorem Turing.MultiTapeTM.ComputableInPolyTime.isComputable {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} (h : ComputableInPolyTime f encIn encMid) : IsComputable f encIn encMid

Functions computable in polynomial time are computable (IsComputable).

theorem Turing.MultiTapeTM.computable_frame : Computable frame

Bit-word framing (frame) is Computable in Mathlib's sense.

theorem Turing.MultiTapeTM.primrec_encUnary : Primrec ⇑encUnary

Unary natural-number encoding (encUnary) is primitive recursive (Primrec).

theorem Turing.MultiTapeTM.computable_encUnary : Computable ⇑encUnary

Unary natural-number encoding (encUnary) is Computable in Mathlib's sense.

theorem Turing.MultiTapeTM.computable_encPair {α β : Type} [Primcodable α] [Primcodable β] {encA : α ↪ List Bool} {encB : β ↪ List Bool} (hA : Computable ⇑encA) (hB : Computable ⇑encB) : Computable ⇑(encPair encA encB)

If encA and encB are Computable in Mathlib's sense, then encPair encA encB is Computable.

theorem Turing.MultiTapeTM.IsComputable.computable_option {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α → Option β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {decOut : List Bool → β} (hf : IsComputable f encIn (encOption encOut)) (hIn : Computable ⇑encIn) (hOut : Computable decOut) (hdec : ∀ (b : β), decOut (encOut b) = b) : Computable f

If IsComputable f encIn (encOption encOut), encIn is Computable, and decOut is a computable left inverse of encOut, then f is Computable in Mathlib's sense.

theorem Turing.MultiTapeTM.IsComputable.computable_option_bits {α : Type u_1} [Primcodable α] {f : α → Option (List Bool)} {encIn : α ↪ List Bool} (hf : IsComputable f encIn (encOption encBits)) (hIn : Computable ⇑encIn) : Computable f

Any Option (List Bool)-valued function f : α → Option (List Bool) that is MultiTapeTM.IsComputable with respect to a computable input encoding encIn and encOption encBits is Computable in Mathlib's sense.

theorem Turing.MultiTapeTM.IsDecidable.computablePred {α : Type u_1} [Primcodable α] {L : Set α} {enc : α ↪ List Bool} (hL : IsDecidable L enc) (henc : Computable ⇑enc) : ComputablePred fun (x : α) => x ∈ L

Any set L : Set α that is MultiTapeTM.IsDecidable with respect to a computable encoding enc satisfies Mathlib's ComputablePred (· ∈ L).

theorem Turing.MultiTapeTM.IsDecidable.computablePred_bits {L : Set (List Bool)} (hL : IsDecidable L encBits) : ComputablePred fun (x : List Bool) => x ∈ L

Any language L : Set (List Bool) that is MultiTapeTM.IsDecidable under encBits satisfies Mathlib's ComputablePred (· ∈ L).

theorem Turing.MultiTapeTM.MappingReducible.manyOneReducible {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {encA : α ↪ List Bool} {encB : β ↪ List Bool} {decB : List Bool → β} {A : Set α} {B : Set β} (h : MappingReducible encA encB A B) (hA : Computable ⇑encA) (hB : Computable decB) (hdec : ∀ (b : β), decB (encB b) = b) : (fun (x : α) => x ∈ A) ≤₀ fun (x : β) => x ∈ B

Any MultiTapeTM.MappingReducible reduction between Primcodable types with computable encoding encA and left-invertible encB yields a Mathlib ManyOneReducible (≤₀) reduction.

theorem Turing.MultiTapeTM.MappingReducible.manyOneReducible_bits {A B : Set (List Bool)} (h : MappingReducible encBits encBits A B) : (fun (x : List Bool) => x ∈ A) ≤₀ fun (x : List Bool) => x ∈ B

Any MultiTapeTM.MappingReducible reduction on bit strings under encBits yields a Mathlib ManyOneReducible (≤₀) reduction.