The evaluation machine on data

Configurations of the evaluation machine (Cost/Machine.lean) encoded as Data (Machine.Cfg.toData), and the step function transported to Data (Machine.stepData), defined by the first-order operations left, right, cons, unaryToNat, getList only — so that it is primitive recursive (Cost/Partrec.lean) and implementable by a program of the ambient model (the self-interpreter). The correspondence is stepData_toData : stepData c.toData = (step c).toData.

Encoding: a control is cons nil (toData p) ("evaluate p") or cons (cons nil nil) v ("return v"); a configuration is cons ctrl (cons env kont) with the environment and the stack as cons-chains; a frame is cons (ofNat tag) payload with tags 0–3 for cons1 t env (payload cons t env), cons2 a (payload a), let1 b env, loop1 b env.

Encoding

def MIPRE.Cost.Machine.evD (p : Data) : Data

The control "evaluate the program p" (as data).

Equations

• MIPRE.Cost.Machine.evD p = MIPRE.Cost.Data.nil.cons p

def MIPRE.Cost.Machine.retD (v : Data) : Data

The control "return the value v".

Equations

• MIPRE.Cost.Machine.retD v = (MIPRE.Cost.Data.nil.cons MIPRE.Cost.Data.nil).cons v

def MIPRE.Cost.Machine.Ctrl.toData : Ctrl → Data

Controls as data.

Equations

• (MIPRE.Cost.Machine.Ctrl.ev p).toData = MIPRE.Cost.Machine.evD p.toData
• (MIPRE.Cost.Machine.Ctrl.ret v).toData = MIPRE.Cost.Machine.retD v

def MIPRE.Cost.Machine.Frame.toData : Frame → Data

Frames as data.

Equations

• (MIPRE.Cost.Machine.Frame.cons1 t env).toData = (MIPRE.Cost.Data.ofNat 0).cons (t.toData.cons (MIPRE.Cost.Data.list env))
• (MIPRE.Cost.Machine.Frame.cons2 a).toData = (MIPRE.Cost.Data.ofNat 1).cons a
• (MIPRE.Cost.Machine.Frame.let1 b env).toData = (MIPRE.Cost.Data.ofNat 2).cons (b.toData.cons (MIPRE.Cost.Data.list env))
• (MIPRE.Cost.Machine.Frame.loop1 b env).toData = (MIPRE.Cost.Data.ofNat 3).cons (b.toData.cons (MIPRE.Cost.Data.list env))

def MIPRE.Cost.Machine.Cfg.toData (c : Cfg) : Data

Configurations as data.

Equations

• c.toData = c.ctrl.toData.cons ((MIPRE.Cost.Data.list c.env).cons (MIPRE.Cost.Data.list (List.map MIPRE.Cost.Machine.Frame.toData c.kont)))

def MIPRE.Cost.Machine.initData (p x : Data) : Data

The initial configuration for the program p (as data) on the input x.

Equations

• MIPRE.Cost.Machine.initData p x = (MIPRE.Cost.Machine.evD p).cons ((x.cons MIPRE.Cost.Data.nil).cons MIPRE.Cost.Data.nil)

theorem MIPRE.Cost.Machine.initData_eq (p : Prog) (x : Data) : initData p.toData x = { ctrl := Ctrl.ev p, env := [x], kont := [] }.toData

def MIPRE.Cost.Machine.IsFinalD (d : Data) : Prop

Final configurations, as data: a returned value with an empty stack.

Equations

• MIPRE.Cost.Machine.IsFinalD d = (d.left.left ≠ MIPRE.Cost.Data.nil ∧ d.right.right = MIPRE.Cost.Data.nil)

@[instance_reducible]

instance MIPRE.Cost.Machine.instDecidablePredDataIsFinalD : DecidablePred IsFinalD

Equations

• MIPRE.Cost.Machine.instDecidablePredDataIsFinalD d = id inferInstance

def MIPRE.Cost.Machine.resultD (d : Data) : Data

The value of a final configuration.

Equations

• MIPRE.Cost.Machine.resultD d = d.left.right

theorem MIPRE.Cost.Machine.isFinalD_toData (c : Cfg) : IsFinalD c.toData ↔ ∃ (r : Data) (e : Env), c = { ctrl := Ctrl.ret r, env := e, kont := [] }

theorem MIPRE.Cost.Machine.resultD_toData (r : Data) (e : Env) : resultD { ctrl := Ctrl.ret r, env := e, kont := [] }.toData = r

The step function on data

def MIPRE.Cost.Machine.stepEv (p env kont : Data) : Data

The step on "evaluate p" with environment env and stack kont.

Equations

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

def MIPRE.Cost.Machine.stepRet (v env kont : Data) : Data

The step on "return v" with environment env and stack kont.

Equations

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

def MIPRE.Cost.Machine.stepData (d : Data) : Data

The step function on data.

Equations

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

theorem MIPRE.Cost.Machine.right_list (l : List Data) : (Data.list l).right = Data.list l.tail

theorem MIPRE.Cost.Machine.stepData_toData (c : Cfg) : stepData c.toData = (step c).toData

The step on data agrees with the machine.

theorem MIPRE.Cost.Machine.iterate_stepData_toData (c : Cfg) (N : ℕ) : stepData^[N] c.toData = (step^[N] c).toData