The interpreter machine: alphabet, tapes, instructions and programs

The interpreter U (planning/succinct-cook-levin.md, S2) is a multi-input Turing machine that runs the evaluation machine of the ambient model (MIPRE.Cost.Machine) on a configuration held on its work tapes. Its control is a small language of routine instructions — copy a subtree, copy to a marker, push and pop, locate an environment entry, charge the budget — each executed over a few phases, organized in short straight-line programs, one per case of the evaluation step. This file has the alphabet, the tape names, the instructions and the programs; Machine.lean interprets them.

Tapes

Seven input tapes: the program 𝒟 as the preorder bits of 𝒟.toData; the bits of encode n, encode x, encode y; the budget T in unary; the answers a', b' as raw bit strings. Six work tapes: C (the control), E (the environment), K (the stack), X (scratch), CNT (a unary depth counter), BUD (the unary budget).

Representation (Repr.lean)

Values v : Data as v.toBits, over the symbols 0, 1. The control on C: 0 · S(p.toData) for ev p, 1 · S(v) for ret v, from cell 0. The environment [v₁, …, vₙ] (v₁ the innermost) on E as S(vₙ) # … # S(v₁) #, head after the last #. The stack on K, frames bottom to top, each tag · payload · $, closures carrying their environment in the same form after a ¶.

inductive MIPRE.TM.Interp.Sym : Type

The work alphabet: the two bits, the environment separator #, the frame end $ and the environment mark ¶ of a closure frame.

• zero : Sym
• one : Sym
• sep : Sym
• fr : Sym
• en : Sym

@[instance_reducible]

instance MIPRE.TM.Interp.instDecidableEqSym : DecidableEq Sym

Equations

• MIPRE.TM.Interp.instDecidableEqSym x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MIPRE.TM.Interp.instReprSym.repr : Sym → ℕ → Std.Format

Equations

• MIPRE.TM.Interp.instReprSym.repr MIPRE.TM.Interp.Sym.zero prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MIPRE.TM.Interp.Sym.zero")).group prec✝
• MIPRE.TM.Interp.instReprSym.repr MIPRE.TM.Interp.Sym.one prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MIPRE.TM.Interp.Sym.one")).group prec✝
• MIPRE.TM.Interp.instReprSym.repr MIPRE.TM.Interp.Sym.sep prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MIPRE.TM.Interp.Sym.sep")).group prec✝
• MIPRE.TM.Interp.instReprSym.repr MIPRE.TM.Interp.Sym.fr prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MIPRE.TM.Interp.Sym.fr")).group prec✝
• MIPRE.TM.Interp.instReprSym.repr MIPRE.TM.Interp.Sym.en prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MIPRE.TM.Interp.Sym.en")).group prec✝

@[instance_reducible]

instance MIPRE.TM.Interp.instReprSym : Repr Sym

Equations

• MIPRE.TM.Interp.instReprSym = { reprPrec := MIPRE.TM.Interp.instReprSym.repr }

@[instance_reducible]

instance MIPRE.TM.Interp.instFintypeSym : Fintype Sym

Equations

• MIPRE.TM.Interp.instFintypeSym = Fintype.ofEquiv (Unit ⊕ Unit ⊕ Unit ⊕ Unit ⊕ Unit) MIPRE.TM.Interp.Sym.proxyTypeEquiv

@[reducible, inline]

abbrev MIPRE.TM.Interp.WT : Type

The work tapes.

Equations

• MIPRE.TM.Interp.WT = Fin 6

@[reducible, inline]

abbrev MIPRE.TM.Interp.IT : Type

The input tapes.

Equations

• MIPRE.TM.Interp.IT = Fin 7

@[reducible, inline]

abbrev MIPRE.TM.Interp.C : WT

The control tape.

Equations

• MIPRE.TM.Interp.C = 0

@[reducible, inline]

abbrev MIPRE.TM.Interp.E : WT

The environment tape.

Equations

• MIPRE.TM.Interp.E = 1

@[reducible, inline]

abbrev MIPRE.TM.Interp.K : WT

The stack tape.

Equations

• MIPRE.TM.Interp.K = 2

@[reducible, inline]

abbrev MIPRE.TM.Interp.X : WT

The scratch tape.

Equations

• MIPRE.TM.Interp.X = 3

@[reducible, inline]

abbrev MIPRE.TM.Interp.CNT : WT

The depth counter.

Equations

• MIPRE.TM.Interp.CNT = 4

@[reducible, inline]

abbrev MIPRE.TM.Interp.BUD : WT

The budget.

Equations

• MIPRE.TM.Interp.BUD = 5

@[reducible, inline]

abbrev MIPRE.TM.Interp.PROG : IT

The program 𝒟.

Equations

• MIPRE.TM.Interp.PROG = 0

@[reducible, inline]

abbrev MIPRE.TM.Interp.N : IT

encode n.

Equations

• MIPRE.TM.Interp.N = 1

@[reducible, inline]

abbrev MIPRE.TM.Interp.T : IT

T in unary.

Equations

• MIPRE.TM.Interp.T = 2

@[reducible, inline]

abbrev MIPRE.TM.Interp.XS : IT

encode x.

Equations

• MIPRE.TM.Interp.XS = 3

@[reducible, inline]

abbrev MIPRE.TM.Interp.YS : IT

encode y.

Equations

• MIPRE.TM.Interp.YS = 4

@[reducible, inline]

abbrev MIPRE.TM.Interp.A : IT

The answer a'.

Equations

• MIPRE.TM.Interp.A = 5

@[reducible, inline]

abbrev MIPRE.TM.Interp.B : IT

The answer b'.

Equations

• MIPRE.TM.Interp.B = 6

inductive MIPRE.TM.Interp.ProgId : Type

The programs: one per case of the evaluation step, the dispatcher, the initialization and the final check.

• init : ProgId
• dispatch : ProgId
• ret0x : ProgId
• evDispatch : ProgId
• evVar : ProgId
• evNil : ProgId
• evConst : ProgId
• evCons : ProgId
• evElim : ProgId
• evElimNil : ProgId
• evElimCons : ProgId
• evLet : ProgId
• evLoop : ProgId
• retCons1 : ProgId
• retCons2 : ProgId
• retLet1 : ProgId
• retLoop1 : ProgId
• retLoopNil : ProgId
• retLoopStop : ProgId
• retLoopCont : ProgId
• final : ProgId
• finalA : ProgId
• finalB : ProgId
• accept : ProgId

@[instance_reducible]

instance MIPRE.TM.Interp.instDecidableEqProgId : DecidableEq ProgId

Equations

• MIPRE.TM.Interp.instDecidableEqProgId x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MIPRE.TM.Interp.instReprProgId.repr : ProgId → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance MIPRE.TM.Interp.instReprProgId : Repr ProgId

Equations

• MIPRE.TM.Interp.instReprProgId = { reprPrec := MIPRE.TM.Interp.instReprProgId.repr }

@[instance_reducible]

instance MIPRE.TM.Interp.instFintypeProgId : Fintype ProgId

Equations

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

inductive MIPRE.TM.Interp.Instr : Type

The routine instructions. Every instruction leaves the heads it does not name where they are.

• copyTree (src : WT) (dst : Option WT) (charge : Bool) : Instr

  Copy the subtree (a preorder-serialized Data) under the head of src to dst (skip it if dst = none), advancing both heads past it; with charge, pop one budget cell per bit (halting if the budget is exhausted). Uses CNT, which must be empty with its head at 0, and leaves it so.

• copyUntil (m : Option Sym) (src dst : WT) : Instr

  Copy from src to dst up to the symbol m (none the blank), which is not copied; the src head ends on it.

• write (t : WT) (s : Sym) : Instr

  Write s and move right.

• move (t : WT) (dir : Bool) : Instr

  Move right (dir = true) or left.

• rewind (t : WT) : Instr

  One left, then left to the blank, then one right: to cell 0 when cells 0 … pos - 1 are not blank (the head may sit on the blank after the content).

• toEnd (t : WT) : Instr

  Move right to the first blank.

• eraseRight (t : WT) : Instr

  Erase rightwards to the first blank (the cells erased must not contain $, which marks the start meanwhile), ending where it started.

• leftToMarker (m : Sym) (t : WT) : Instr

  Move one left, then left to the marker m or a blank, then one right.

• popBack (m : Sym) (t : WT) : Instr

  From the end: erase the last cell and everything before it back to the marker m or a blank (exclusive), ending right after the marker; nothing on an empty tape.

• getEnv : Instr

  With the head of C on the unary index S(ofNat i) and the head of E at the end of the environment: write S(env.get i) on X from its head, leave C past the index and E at its end.

• charge (two : Bool) : Instr

  Pop one (or two) budget cells; halt if the budget is exhausted.

• branch (t : WT) (s : Option Sym) (target : ProgId) : Instr

  Jump to the start of target if the symbol under the head of t is s.

• jump (target : ProgId) : Instr

  Jump to the start of target.

• emit (s : Sym) : Instr

  Emit an output symbol.

• halt : Instr

  Halt.

• copyUnary (j : IT) (dst : WT) : Instr

  Write one 1 on dst per symbol of input j, up to the blank.

• copyInputBits (j : IT) (dst : WT) : Instr

  Copy the bits of input j to dst, up to the blank.

• buildAnswer (j : IT) (dst : WT) : Instr

  Write S(encode l) on dst for the bit string l on input j: 1 0 per 0, 1 1 0 0 per 1, then 0.

• checkLen (j ref : IT) : Instr

  Halt unless input j is at most as long as input ref; both heads advance.

• rewindInput (j : IT) : Instr

  Move the head of input j to the blank before the input.

• moveInput (j : IT) (dir : Bool) : Instr

  Move the head of input j right or left.

@[instance_reducible]

instance MIPRE.TM.Interp.instDecidableEqInstr : DecidableEq Instr

Equations

• MIPRE.TM.Interp.instDecidableEqInstr = MIPRE.TM.Interp.instDecidableEqInstr.decEq

def MIPRE.TM.Interp.instDecidableEqInstr.decEq (x✝ x✝¹ : Instr) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance MIPRE.TM.Interp.instReprInstr : Repr Instr

Equations

• MIPRE.TM.Interp.instReprInstr = { reprPrec := MIPRE.TM.Interp.instReprInstr.repr }

def MIPRE.TM.Interp.instReprInstr.repr : Instr → ℕ → Std.Format

Equations

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

inductive MIPRE.TM.Interp.Phase : Type

The phases of an instruction.

• p0 : Phase
• p1 : Phase
• p2 : Phase
• p3 : Phase
• p4 : Phase
• p5 : Phase
• p6 : Phase
• p7 : Phase
• p8 : Phase
• p9 : Phase

@[instance_reducible]

instance MIPRE.TM.Interp.instDecidableEqPhase : DecidableEq Phase

Equations

• MIPRE.TM.Interp.instDecidableEqPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MIPRE.TM.Interp.instReprPhase.repr : Phase → ℕ → Std.Format

Equations

• MIPRE.TM.Interp.instReprPhase.repr MIPRE.TM.Interp.Phase.p0 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MIPRE.TM.Interp.Phase.p0")).group prec✝
• MIPRE.TM.Interp.instReprPhase.repr MIPRE.TM.Interp.Phase.p1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MIPRE.TM.Interp.Phase.p1")).group prec✝
• MIPRE.TM.Interp.instReprPhase.repr MIPRE.TM.Interp.Phase.p2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MIPRE.TM.Interp.Phase.p2")).group prec✝
• MIPRE.TM.Interp.instReprPhase.repr MIPRE.TM.Interp.Phase.p3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MIPRE.TM.Interp.Phase.p3")).group prec✝
• MIPRE.TM.Interp.instReprPhase.repr MIPRE.TM.Interp.Phase.p4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MIPRE.TM.Interp.Phase.p4")).group prec✝
• MIPRE.TM.Interp.instReprPhase.repr MIPRE.TM.Interp.Phase.p5 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MIPRE.TM.Interp.Phase.p5")).group prec✝
• MIPRE.TM.Interp.instReprPhase.repr MIPRE.TM.Interp.Phase.p6 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MIPRE.TM.Interp.Phase.p6")).group prec✝
• MIPRE.TM.Interp.instReprPhase.repr MIPRE.TM.Interp.Phase.p7 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MIPRE.TM.Interp.Phase.p7")).group prec✝
• MIPRE.TM.Interp.instReprPhase.repr MIPRE.TM.Interp.Phase.p8 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MIPRE.TM.Interp.Phase.p8")).group prec✝
• MIPRE.TM.Interp.instReprPhase.repr MIPRE.TM.Interp.Phase.p9 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MIPRE.TM.Interp.Phase.p9")).group prec✝

@[instance_reducible]

instance MIPRE.TM.Interp.instReprPhase : Repr Phase

Equations

• MIPRE.TM.Interp.instReprPhase = { reprPrec := MIPRE.TM.Interp.instReprPhase.repr }

@[instance_reducible]

instance MIPRE.TM.Interp.instFintypePhase : Fintype Phase

Equations

• MIPRE.TM.Interp.instFintypePhase = Fintype.ofEquiv (Unit ⊕ Unit ⊕ Unit ⊕ Unit ⊕ Unit ⊕ Unit ⊕ Unit ⊕ Unit ⊕ Unit ⊕ Unit) MIPRE.TM.Interp.Phase.proxyTypeEquiv

def MIPRE.TM.Interp.initProg : List Instr

The initialization: the budget, the length checks of the answers, and the initial configuration ⟨ev 𝒟, [encode (n, x, y, a', b')], []⟩.

Equations

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

def MIPRE.TM.Interp.dispatchProg : List Instr

The dispatcher of a step: on ev, read the tag; on ret, the top frame's tag, or finish when the stack is empty.

Equations

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

def MIPRE.TM.Interp.ret0xProg : List Instr

Equations

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

def MIPRE.TM.Interp.evDispatchProg : List Instr

The tag of the program to evaluate: (10)^k 0 for k = 0 … 6; every case starts with the head of C on the final 0 of the tag.

Equations

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

def MIPRE.TM.Interp.evVarProg : List Instr

ev (var i): return env.get i, at cost its size plus one.

Equations

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

def MIPRE.TM.Interp.evNilProg : List Instr

ev nil: return nil, at cost one.

Equations

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

def MIPRE.TM.Interp.evConstProg : List Instr

ev (const d): return d, at cost its size.

Equations

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

def MIPRE.TM.Interp.evConsProg : List Instr

ev (cons h t): push the frame cons1 t env, evaluate h, at cost one.

Equations

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

def MIPRE.TM.Interp.evElimProg : List Instr

ev (elim i n c): fetch env.get i and dispatch on it.

Equations

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

def MIPRE.TM.Interp.evElimNilProg : List Instr

env.get i = nil: evaluate n, at cost one.

Equations

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

def MIPRE.TM.Interp.evElimConsProg : List Instr

env.get i = cons a b: push b then a, evaluate c, at cost one.

Equations

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

def MIPRE.TM.Interp.evLetProg : List Instr

ev (let_ e b): push the frame let1 b env, evaluate e, at cost one.

Equations

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

def MIPRE.TM.Interp.evLoopProg : List Instr

ev (loop b): push the frame loop1 b env, evaluate b, at no cost.

Equations

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

def MIPRE.TM.Interp.retCons1Prog : List Instr

ret v to cons1 t env': environment env', push cons2 v, evaluate t.

Equations

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

def MIPRE.TM.Interp.retCons2Prog : List Instr

ret v to cons2 a: return cons a v.

Equations

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

def MIPRE.TM.Interp.retLet1Prog : List Instr

ret v to let1 b env': environment v :: env', evaluate b.

Equations

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

def MIPRE.TM.Interp.retLoop1Prog : List Instr

ret v to loop1 b env': dispatch on the shape of v.

Equations

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

def MIPRE.TM.Interp.retLoopNilProg : List Instr

v = nil: return nil in env', at cost one.

Equations

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

def MIPRE.TM.Interp.retLoopStopProg : List Instr

v = cons nil r: return r in env', at cost one.

Equations

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

def MIPRE.TM.Interp.retLoopContProg : List Instr

v = cons (cons _ _) v': environment v' :: env'.tail, the frame updated, evaluate b, at cost one.

Equations

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

def MIPRE.TM.Interp.finalProg : List Instr

The final check: the result must be encode true = cons nil nil, bits 1 0 0.

Equations

• MIPRE.TM.Interp.finalProg = [MIPRE.TM.Interp.Instr.branch MIPRE.TM.Interp.C (some MIPRE.TM.Interp.Sym.one) MIPRE.TM.Interp.ProgId.finalA, MIPRE.TM.Interp.Instr.halt]

def MIPRE.TM.Interp.finalAProg : List Instr

Equations

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

def MIPRE.TM.Interp.finalBProg : List Instr

Equations

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

def MIPRE.TM.Interp.acceptProg : List Instr

Equations

• MIPRE.TM.Interp.acceptProg = [MIPRE.TM.Interp.Instr.emit MIPRE.TM.Interp.Sym.one, MIPRE.TM.Interp.Instr.halt]

def MIPRE.TM.Interp.prog : ProgId → List Instr

The programs.

Equations

• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.init = MIPRE.TM.Interp.initProg
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.dispatch = MIPRE.TM.Interp.dispatchProg
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.ret0x = MIPRE.TM.Interp.ret0xProg
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.evDispatch = MIPRE.TM.Interp.evDispatchProg
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.evVar = MIPRE.TM.Interp.evVarProg
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.evNil = MIPRE.TM.Interp.evNilProg
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.evConst = MIPRE.TM.Interp.evConstProg
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.evCons = MIPRE.TM.Interp.evConsProg
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.evElim = MIPRE.TM.Interp.evElimProg
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.evElimNil = MIPRE.TM.Interp.evElimNilProg
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.evElimCons = MIPRE.TM.Interp.evElimConsProg
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.evLet = MIPRE.TM.Interp.evLetProg
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.evLoop = MIPRE.TM.Interp.evLoopProg
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.retCons1 = MIPRE.TM.Interp.retCons1Prog
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.retCons2 = MIPRE.TM.Interp.retCons2Prog
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.retLet1 = MIPRE.TM.Interp.retLet1Prog
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.retLoop1 = MIPRE.TM.Interp.retLoop1Prog
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.retLoopNil = MIPRE.TM.Interp.retLoopNilProg
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.retLoopStop = MIPRE.TM.Interp.retLoopStopProg
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.retLoopCont = MIPRE.TM.Interp.retLoopContProg
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.final = MIPRE.TM.Interp.finalProg
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.finalA = MIPRE.TM.Interp.finalAProg
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.finalB = MIPRE.TM.Interp.finalBProg
• MIPRE.TM.Interp.prog MIPRE.TM.Interp.ProgId.accept = MIPRE.TM.Interp.acceptProg

def MIPRE.TM.Interp.maxPc : ℕ

The length bound on the programs.

Equations

• MIPRE.TM.Interp.maxPc = 32