Ambient evaluation is partial recursive

The step of the evaluation machine on data is primitive recursive (primrec_stepData), so evaluation — its PFun.fix from the initial configuration — is partial recursive (partrec_evalData), and agrees with Eval (mem_evalData_iff). Consequently a polynomial-time function of the ambient model is Mathlib-computable, as soon as its input is produced by a computable encoding (PolyTimeFun.computable_comp). This is the bridge from the ambient model to Mathlib's computability used by the halting-problem form of the compression lemma; the other bridge (from Nat.Partrec.Code into the model) is Cost/FromPartrec.lean.

The step is primitive recursive

theorem MIPRE.Cost.Machine.primrec_evD : Primrec evD

theorem MIPRE.Cost.Machine.primrec_retD : Primrec retD

theorem MIPRE.Cost.Machine.primrec_tag : Primrec fun (d : Data) => d.left.unaryToNat

p ↦ unaryToNat p.left, the tag of an encoded program or frame.

theorem MIPRE.Cost.Machine.primrec_stepEv : Primrec fun (q : Data × Data × Data) => stepEv q.1 q.2.1 q.2.2

theorem MIPRE.Cost.Machine.primrec_stepRet : Primrec fun (q : Data × Data × Data) => stepRet q.1 q.2.1 q.2.2

theorem MIPRE.Cost.Machine.primrec_stepData : Primrec stepData

theorem MIPRE.Cost.Machine.primrec_isFinalD : PrimrecPred IsFinalD

theorem MIPRE.Cost.Machine.primrec_resultD : Primrec resultD

theorem MIPRE.Cost.Machine.primrec_initData : Primrec₂ initData

Evaluation as a fixed point

def MIPRE.Cost.Machine.evalStep (d : Data) : Data ⊕ Data

One iteration of the evaluation loop: stop with the value on a final configuration, otherwise step.

Equations

• MIPRE.Cost.Machine.evalStep d = if MIPRE.Cost.Machine.IsFinalD d then Sum.inl (MIPRE.Cost.Machine.resultD d) else Sum.inr (MIPRE.Cost.Machine.stepData d)

theorem MIPRE.Cost.Machine.computable_evalStep : Computable evalStep

def MIPRE.Cost.Machine.evalData (p x : Data) : Part Data

Evaluation of the program p (as data) on x, as a partial function: the fixed point of the evaluation loop from the initial configuration.

Equations

• MIPRE.Cost.Machine.evalData p x = PFun.fix (fun (d : MIPRE.Cost.Data) => Part.some (MIPRE.Cost.Machine.evalStep d)) (MIPRE.Cost.Machine.initData p x)

theorem MIPRE.Cost.Machine.partrec_evalData : Partrec₂ evalData

theorem MIPRE.Cost.Machine.mem_fix_of_iterate (d : Data) (N : ℕ) (hfin : IsFinalD (stepData^[N] d)) (hstep : ∀ n < N, ¬IsFinalD (stepData^[n] d)) : resultD (stepData^[N] d) ∈ PFun.fix (fun (d : Data) => Part.some (evalStep d)) d

theorem MIPRE.Cost.Machine.exists_iterate_of_mem_fix {d r : Data} (h : r ∈ PFun.fix (fun (d : Data) => Part.some (evalStep d)) d) : ∃ (N : ℕ), IsFinalD (stepData^[N] d) ∧ resultD (stepData^[N] d) = r

theorem MIPRE.Cost.Machine.mem_fix_of_steps (N : ℕ) (c : Cfg) (r : Data) (e : Env) : step^[N] c = { ctrl := Ctrl.ret r, env := e, kont := [] } → r ∈ PFun.fix (fun (d : Data) => Part.some (evalStep d)) c.toData

theorem MIPRE.Cost.Machine.mem_evalData_iff (c : Prog) (x r : Data) : r ∈ evalData c.toData x ↔ ∃ (t : ℕ), c.Runs x r t

Evaluation on data agrees with Eval.

Polynomial-time functions are computable

theorem MIPRE.Cost.evalData_encode {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (F : PolyTimeFun α β) (a : α) : Machine.evalData (encode F.code) (encode a) = Part.some (encode (F.toFun a))

theorem MIPRE.Cost.PolyTimeFun.computable_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SizedEncoding α] [SizedEncoding β] [Primcodable γ] [Primcodable β] [Inhabited β] (F : PolyTimeFun α β) (h : γ → α) (hh : Computable fun (c : γ) => encode (h c)) (hβ : Computable fun (d : Data) => decode d) : Computable fun (c : γ) => F.toFun (h c)

A polynomial-time function of the ambient model, precomposed with a computable encoding of its input and followed by a computable decoding of its output, is Mathlib-computable.