From Mathlib's partial recursive functions into the ambient model

Mathlib's Turing.ToPartrec.Code is a small first-order language on lists of naturals (zero', succ, tail, cons, comp, case, fix) in which every partial recursive function is computable (Turing.ToPartrec.Code.exists_code). It translates construct by construct into the ambient language (Prog.ofCode), with lists of naturals encoded as cons-chains of unary numerals (encL) and fix as a loop; ofCode_sound and ofCode_complete are the two directions of the correctness of the translation.

exists_compile is the resulting bridge for the halting problem: a map compile from Nat.Partrec.Code to programs, computable on descriptions, such that compile pc halts on the empty input iff pc does on 0: compile pc hardcodes the code number of pc into the translation of a ToPartrec.Code for the universal partial function n ↦ (ofNat n).eval 0.

def MIPRE.Cost.encL (v : List ℕ) : Data

Lists of naturals as data: a cons-chain of unary numerals.

Equations

• MIPRE.Cost.encL v = MIPRE.Cost.Data.list (List.map MIPRE.Cost.Data.ofNat v)

@[simp]

theorem MIPRE.Cost.encL_nil : encL [] = Data.nil

@[simp]

theorem MIPRE.Cost.encL_cons (n : ℕ) (v : List ℕ) : encL (n :: v) = (Data.ofNat n).cons (encL v)

theorem MIPRE.Cost.encL_injective : Function.Injective encL

def MIPRE.Cost.Prog.fixBody (pf : Prog) : Prog

The body of the translation of fix f: run f, then dispatch on the head of the result (stop with the tail if it is 0, continue with the tail otherwise).

Equations

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

def MIPRE.Cost.Prog.consTail : Prog

The headI :: tail assembly of the translation of cons f fs, in an environment [fs v, f v, v].

Equations

• MIPRE.Cost.Prog.consTail = (MIPRE.Cost.Prog.elim 1 MIPRE.Cost.Prog.nil (MIPRE.Cost.Prog.var 0)).cons (MIPRE.Cost.Prog.var 0)

def MIPRE.Cost.Prog.ofCode : Turing.ToPartrec.Code → Prog

Translation of ToPartrec.Code into the ambient language.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Cost.Prog.ofCode Turing.ToPartrec.Code.zero' = MIPRE.Cost.Prog.nil.cons (MIPRE.Cost.Prog.var 0)
• MIPRE.Cost.Prog.ofCode Turing.ToPartrec.Code.tail = MIPRE.Cost.Prog.elim 0 MIPRE.Cost.Prog.nil (MIPRE.Cost.Prog.var 1)
• MIPRE.Cost.Prog.ofCode (f.cons fs) = (MIPRE.Cost.Prog.ofCode f).let_ ((MIPRE.Cost.Prog.callVar 1 (MIPRE.Cost.Prog.ofCode fs)).let_ MIPRE.Cost.Prog.consTail)
• MIPRE.Cost.Prog.ofCode (f.comp g) = (MIPRE.Cost.Prog.ofCode g).let_ (MIPRE.Cost.Prog.ofCode f)
• MIPRE.Cost.Prog.ofCode f.fix = (MIPRE.Cost.Prog.ofCode f).fixBody.loop

theorem MIPRE.Cost.Prog.consTail_wellScoped : WellScoped 3 consTail

theorem MIPRE.Cost.Prog.fixBody_wellScoped {pf : Prog} (h : WellScoped 1 pf) : WellScoped 1 pf.fixBody

theorem MIPRE.Cost.Prog.ofCode_wellScoped (c : Turing.ToPartrec.Code) : WellScoped 1 (ofCode c)

Forward runs of the pieces

def MIPRE.Cost.Prog.fixFlag : List ℕ → Data

The result of the dispatch of fixBody on the value fv of f.

Equations

• MIPRE.Cost.Prog.fixFlag [] = MIPRE.Cost.Data.nil.cons MIPRE.Cost.Data.nil
• MIPRE.Cost.Prog.fixFlag (0 :: t) = MIPRE.Cost.Data.nil.cons (MIPRE.Cost.encL t)
• MIPRE.Cost.Prog.fixFlag (n.succ :: t) = (MIPRE.Cost.Data.nil.cons MIPRE.Cost.Data.nil).cons (MIPRE.Cost.encL t)

theorem MIPRE.Cost.Prog.fixBody_runs {pf : Prog} (hpf : WellScoped 1 pf) (v fv : List ℕ) {t : ℕ} (h : pf.Runs (encL v) (encL fv) t) : ∃ (s : ℕ), Eval [encL v] pf.fixBody (fixFlag fv) s

theorem MIPRE.Cost.Prog.consTail_runs (fv fsv v : List ℕ) : ∃ (s : ℕ), Eval [encL fsv, encL fv, encL v] consTail (encL (fv.headI :: fsv)) s

theorem MIPRE.Cost.Prog.casePair_runs (y : ℕ) (v' : List ℕ) : Eval [Data.nil, Data.ofNat y, Data.ofNat (y + 1), encL v', encL ((y + 1) :: v')] ((var 1).cons (var 3)) (encL (y :: v')) ((Data.ofNat y).size + 1 + ((encL v').size + 1) + 1)

The pairing step of the case translation, in an environment [nil, ofNat y, ofNat (y + 1), encL v', encL (y + 1 :: v')].

Soundness

theorem MIPRE.Cost.Prog.ofCode_sound (c : Turing.ToPartrec.Code) (v w : List ℕ) : w ∈ c.eval v → ∃ (t : ℕ), (ofCode c).Runs (encL v) (encL w) t

Completeness

theorem MIPRE.Cost.Prog.ofCode_complete (c : Turing.ToPartrec.Code) (v : List ℕ) (r : Data) (t : ℕ) : (ofCode c).Runs (encL v) r t → ∃ (w : List ℕ), r = encL w ∧ w ∈ c.eval v

theorem MIPRE.Cost.Prog.ofCode_halts_iff (c : Turing.ToPartrec.Code) (v : List ℕ) : Halts (ofCode c) (encL v) ↔ (c.eval v).Dom

Halting of the translation of c on encL v is halting of c on v.

The halting-problem bridge

noncomputable def MIPRE.Cost.univPart (n : ℕ) : Part ℕ

The universal partial function on code numbers: n ↦ (decode n).eval 0.

Equations

• MIPRE.Cost.univPart n = (↑(Encodable.decode n)).bind fun (c : Nat.Partrec.Code) => c.eval 0

theorem MIPRE.Cost.partrec_univPart : Partrec univPart

theorem MIPRE.Cost.univPart_encode (pc : Nat.Partrec.Code) : univPart (Encodable.encode pc) = pc.eval 0

theorem MIPRE.Cost.exists_compile : ∃ (compile : Nat.Partrec.Code → Prog), (Computable fun (pc : Nat.Partrec.Code) => encode (compile pc)) ∧ ∀ (pc : Nat.Partrec.Code), Halts (compile pc) Data.nil ↔ (pc.eval 0).Dom

The halting problem transfers from Nat.Partrec.Code to the ambient model along a map compile, computable on descriptions (encode (compile pc) : Data).