The interpreter machine

U is the multi-input Turing machine interpreting the programs of Instr.lean: a state is a program, a position in it and the phase of the instruction there (Ctl), and one step executes one phase of the current instruction (execInstr), producing head moves, writes, an optional output symbol and the next control: the same instruction in another phase, the next instruction, a jump to the start of another program, or a halt.

The instructions' semantics, phase by phase, is documented on execInstr; their specifications as reachability triples are in Routines.lean.

structure MIPRE.TM.Interp.Ctl : Type

The control of the machine: a program, a position, a phase.

• k : ProgId
• pc : Fin maxPc
• ph : Phase

@[instance_reducible]

instance MIPRE.TM.Interp.instDecidableEqCtl : DecidableEq Ctl

Equations

• MIPRE.TM.Interp.instDecidableEqCtl = MIPRE.TM.Interp.instDecidableEqCtl.decEq

def MIPRE.TM.Interp.instDecidableEqCtl.decEq (x✝ x✝¹ : Ctl) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance MIPRE.TM.Interp.instFintypeCtl : Fintype Ctl

Equations

• MIPRE.TM.Interp.instFintypeCtl = Fintype.ofEquiv ((_ : MIPRE.TM.Interp.ProgId) × (_ : Fin MIPRE.TM.Interp.maxPc) × MIPRE.TM.Interp.Phase) MIPRE.TM.Interp.Ctl.proxyTypeEquiv

inductive MIPRE.TM.Interp.Next : Type

What an instruction phase does to the control.

• stay (ph : Phase) : Next
• adv : Next
• jmp (k : ProgId) : Next
• halt : Next

structure MIPRE.TM.Interp.Act : Type

The actions of one step: input head moves, work-tape writes and moves, the output, and the next control.

• inMoves : IT → SignType
• works : WT → Option (Option Sym) × SignType
• out : Option Sym
• next : Next

def MIPRE.TM.Interp.Act.base (n : Next) : Act

No moves, no writes, no output.

Equations

• MIPRE.TM.Interp.Act.base n = { next := n }

def MIPRE.TM.Interp.Act.mw (a : Act) (t : WT) (m : SignType) : Act

Move the head of work tape t.

Equations

• a.mw t m = { inMoves := a.inMoves, works := Function.update a.works t ((a.works t).1, m), out := a.out, next := a.next }

def MIPRE.TM.Interp.Act.ww (a : Act) (t : WT) (s : Option Sym) : Act

Write s (none the blank) on work tape t.

Equations

• a.ww t s = { inMoves := a.inMoves, works := Function.update a.works t (some s, (a.works t).2), out := a.out, next := a.next }

def MIPRE.TM.Interp.Act.mi (a : Act) (j : IT) (m : SignType) : Act

Move the head of input tape j.

Equations

• a.mi j m = { inMoves := Function.update a.inMoves j m, works := a.works, out := a.out, next := a.next }

def MIPRE.TM.Interp.Act.emit (a : Act) (s : Sym) : Act

Emit s.

Equations

• a.emit s = { inMoves := a.inMoves, works := a.works, out := some s, next := a.next }

def MIPRE.TM.Interp.execInstr (ins : Instr) (ph : Phase) (as : IT → Option Sym) (bs : WT → Option Sym) : Act

The semantics of an instruction phase, given the symbols under the input heads as and the work heads bs.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.TM.Interp.execInstr (MIPRE.TM.Interp.Instr.copyTree src dst ch) ph as bs = MIPRE.TM.Interp.Act.base MIPRE.TM.Interp.Next.halt
• MIPRE.TM.Interp.execInstr (MIPRE.TM.Interp.Instr.write t s) ph as bs = ((MIPRE.TM.Interp.Act.base MIPRE.TM.Interp.Next.adv).ww t (some s)).mw t 1
• MIPRE.TM.Interp.execInstr (MIPRE.TM.Interp.Instr.move t dir) ph as bs = (MIPRE.TM.Interp.Act.base MIPRE.TM.Interp.Next.adv).mw t (if dir = true then 1 else -1)
• MIPRE.TM.Interp.execInstr (MIPRE.TM.Interp.Instr.rewind t) MIPRE.TM.Interp.Phase.p0 as bs = (MIPRE.TM.Interp.Act.base (MIPRE.TM.Interp.Next.stay MIPRE.TM.Interp.Phase.p1)).mw t (-1)
• MIPRE.TM.Interp.execInstr (MIPRE.TM.Interp.Instr.leftToMarker m t) MIPRE.TM.Interp.Phase.p0 as bs = (MIPRE.TM.Interp.Act.base (MIPRE.TM.Interp.Next.stay MIPRE.TM.Interp.Phase.p1)).mw t (-1)
• MIPRE.TM.Interp.execInstr (MIPRE.TM.Interp.Instr.popBack m t) MIPRE.TM.Interp.Phase.p0 as bs = (MIPRE.TM.Interp.Act.base (MIPRE.TM.Interp.Next.stay MIPRE.TM.Interp.Phase.p1)).mw t (-1)
• MIPRE.TM.Interp.execInstr MIPRE.TM.Interp.Instr.getEnv MIPRE.TM.Interp.Phase.p0 as bs = (MIPRE.TM.Interp.Act.base (MIPRE.TM.Interp.Next.stay MIPRE.TM.Interp.Phase.p1)).mw MIPRE.TM.Interp.E (-1)
• MIPRE.TM.Interp.execInstr MIPRE.TM.Interp.Instr.getEnv MIPRE.TM.Interp.Phase.p2 as bs = (MIPRE.TM.Interp.Act.base (MIPRE.TM.Interp.Next.stay MIPRE.TM.Interp.Phase.p3)).mw MIPRE.TM.Interp.C 1
• MIPRE.TM.Interp.execInstr MIPRE.TM.Interp.Instr.getEnv MIPRE.TM.Interp.Phase.p7 as bs = (MIPRE.TM.Interp.Act.base (MIPRE.TM.Interp.Next.stay MIPRE.TM.Interp.Phase.p6)).mw MIPRE.TM.Interp.C 1
• MIPRE.TM.Interp.execInstr (MIPRE.TM.Interp.Instr.jump target) ph as bs = MIPRE.TM.Interp.Act.base (MIPRE.TM.Interp.Next.jmp target)
• MIPRE.TM.Interp.execInstr (MIPRE.TM.Interp.Instr.emit s) ph as bs = (MIPRE.TM.Interp.Act.base MIPRE.TM.Interp.Next.adv).emit s
• MIPRE.TM.Interp.execInstr MIPRE.TM.Interp.Instr.halt ph as bs = MIPRE.TM.Interp.Act.base MIPRE.TM.Interp.Next.halt
• MIPRE.TM.Interp.execInstr (MIPRE.TM.Interp.Instr.rewindInput j) MIPRE.TM.Interp.Phase.p0 as bs = (MIPRE.TM.Interp.Act.base (MIPRE.TM.Interp.Next.stay MIPRE.TM.Interp.Phase.p1)).mi j (-1)
• MIPRE.TM.Interp.execInstr (MIPRE.TM.Interp.Instr.moveInput j dir) ph as bs = (MIPRE.TM.Interp.Act.base MIPRE.TM.Interp.Next.adv).mi j (if dir = true then 1 else -1)

def MIPRE.TM.Interp.instrAt (k : ProgId) (pc : Fin maxPc) : Instr

The instruction at a position of a program (halt past the end).

Equations

• MIPRE.TM.Interp.instrAt k pc = (MIPRE.TM.Interp.prog k).getD (↑pc) MIPRE.TM.Interp.Instr.halt

def MIPRE.TM.Interp.resolve (k : ProgId) (pc : Fin maxPc) : Next → Option Ctl

The control after a step.

Equations

• MIPRE.TM.Interp.resolve k pc (MIPRE.TM.Interp.Next.stay ph) = some { k := k, pc := pc, ph := ph }
• MIPRE.TM.Interp.resolve k pc MIPRE.TM.Interp.Next.adv = if h : ↑pc + 1 < MIPRE.TM.Interp.maxPc then some { k := k, pc := ⟨↑pc + 1, h⟩, ph := MIPRE.TM.Interp.Phase.p0 } else none
• MIPRE.TM.Interp.resolve k pc (MIPRE.TM.Interp.Next.jmp k') = some { k := k', pc := ⟨0, MIPRE.TM.Interp.resolve._proof_3⟩, ph := MIPRE.TM.Interp.Phase.p0 }
• MIPRE.TM.Interp.resolve k pc MIPRE.TM.Interp.Next.halt = none

def MIPRE.TM.Interp.U : Turing.MultiInputTM 7 6 Sym Ctl

The interpreter machine.

Equations

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