URM Core Definitions

This file contains the core definitions for Unlimited Register Machines (URMs): instructions, register state, programs, and machine configurations.

Main definitions

• URM.Instr: The four URM instructions (Z, S, T, J)
• URM.Regs: Register contents as a function ℕ → ℕ
• URM.Program: A finite sequence of instructions
• URM.State: Machine state (program counter + registers)

References

• [N.J. Cutland, Computability: An Introduction to Recursive Function Theory][Cutland1980]
• [J.C. Shepherdson and H.E. Sturgis, Computability of Recursive Functions][ShepherdsonSturgis1963]

Instructions

inductive Cslib.URM.Instr : Type

URM instructions.

• Z n: Set register n to zero
• S n: Increment register n by one
• T m n: Transfer (copy) the contents of register m to register n
• J m n q: If registers m and n have equal contents, jump to instruction q; otherwise proceed to the next instruction

• Z : ℕ → Instr
• S : ℕ → Instr
• T : ℕ → ℕ → Instr
• J : ℕ → ℕ → ℕ → Instr

@[implicit_reducible]

instance Cslib.URM.instDecidableEqInstr : DecidableEq Instr

Equations

• Cslib.URM.instDecidableEqInstr = Cslib.URM.instDecidableEqInstr.decEq

def Cslib.URM.instDecidableEqInstr.decEq (x✝ x✝¹ : Instr) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Cslib.URM.instDecidableEqInstr.decEq (Cslib.URM.Instr.Z a) (Cslib.URM.Instr.Z b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cslib.URM.instDecidableEqInstr.decEq (Cslib.URM.Instr.Z a) (Cslib.URM.Instr.S a_1) = isFalse ⋯
• Cslib.URM.instDecidableEqInstr.decEq (Cslib.URM.Instr.Z a) (Cslib.URM.Instr.T a_1 a_2) = isFalse ⋯
• Cslib.URM.instDecidableEqInstr.decEq (Cslib.URM.Instr.Z a) (Cslib.URM.Instr.J a_1 a_2 a_3) = isFalse ⋯
• Cslib.URM.instDecidableEqInstr.decEq (Cslib.URM.Instr.S a) (Cslib.URM.Instr.Z a_1) = isFalse ⋯
• Cslib.URM.instDecidableEqInstr.decEq (Cslib.URM.Instr.S a) (Cslib.URM.Instr.S b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cslib.URM.instDecidableEqInstr.decEq (Cslib.URM.Instr.S a) (Cslib.URM.Instr.T a_1 a_2) = isFalse ⋯
• Cslib.URM.instDecidableEqInstr.decEq (Cslib.URM.Instr.S a) (Cslib.URM.Instr.J a_1 a_2 a_3) = isFalse ⋯
• Cslib.URM.instDecidableEqInstr.decEq (Cslib.URM.Instr.T a a_1) (Cslib.URM.Instr.Z a_2) = isFalse ⋯
• Cslib.URM.instDecidableEqInstr.decEq (Cslib.URM.Instr.T a a_1) (Cslib.URM.Instr.S a_2) = isFalse ⋯
• Cslib.URM.instDecidableEqInstr.decEq (Cslib.URM.Instr.T a a_1) (Cslib.URM.Instr.T b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Cslib.URM.instDecidableEqInstr.decEq (Cslib.URM.Instr.T a a_1) (Cslib.URM.Instr.J a_2 a_3 a_4) = isFalse ⋯
• Cslib.URM.instDecidableEqInstr.decEq (Cslib.URM.Instr.J a a_1 a_2) (Cslib.URM.Instr.Z a_3) = isFalse ⋯
• Cslib.URM.instDecidableEqInstr.decEq (Cslib.URM.Instr.J a a_1 a_2) (Cslib.URM.Instr.S a_3) = isFalse ⋯
• Cslib.URM.instDecidableEqInstr.decEq (Cslib.URM.Instr.J a a_1 a_2) (Cslib.URM.Instr.T a_3 a_4) = isFalse ⋯

@[implicit_reducible]

instance Cslib.URM.instReprInstr : Repr Instr

Equations

• Cslib.URM.instReprInstr = { reprPrec := Cslib.URM.instReprInstr.repr }

def Cslib.URM.instReprInstr.repr : Instr → ℕ → Std.Format

Equations

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

def Cslib.URM.Instr.readsFrom : Instr → Finset ℕ

The registers read by an instruction.

Equations

• (Cslib.URM.Instr.Z a).readsFrom = ∅
• (Cslib.URM.Instr.S n).readsFrom = {n}
• (Cslib.URM.Instr.T m a).readsFrom = {m}
• (Cslib.URM.Instr.J m n a).readsFrom = {m, n}

def Cslib.URM.Instr.writesTo : Instr → Option ℕ

The register written to by an instruction, if any.

Equations

• (Cslib.URM.Instr.Z a).writesTo = some a
• (Cslib.URM.Instr.S n).writesTo = some n
• (Cslib.URM.Instr.T m a).writesTo = some a
• (Cslib.URM.Instr.J m n a).writesTo = none

def Cslib.URM.Instr.maxRegister : Instr → ℕ

The maximum register index referenced by an instruction.

Equations

• (Cslib.URM.Instr.Z a).maxRegister = a
• (Cslib.URM.Instr.S n).maxRegister = n
• (Cslib.URM.Instr.T m a).maxRegister = max m a
• (Cslib.URM.Instr.J m n a).maxRegister = max m n

def Cslib.URM.Instr.shiftJumps (offset : ℕ) : Instr → Instr

Shift all jump targets in an instruction by offset. Used when concatenating programs to maintain correct jump destinations.

Equations

• Cslib.URM.Instr.shiftJumps offset (Cslib.URM.Instr.Z a) = Cslib.URM.Instr.Z a
• Cslib.URM.Instr.shiftJumps offset (Cslib.URM.Instr.S n) = Cslib.URM.Instr.S n
• Cslib.URM.Instr.shiftJumps offset (Cslib.URM.Instr.T m a) = Cslib.URM.Instr.T m a
• Cslib.URM.Instr.shiftJumps offset (Cslib.URM.Instr.J m n a) = Cslib.URM.Instr.J m n (a + offset)

def Cslib.URM.Instr.shiftRegisters (offset : ℕ) : Instr → Instr

Shift all register references in an instruction by offset. Used to isolate register usage when composing programs.

Equations

• Cslib.URM.Instr.shiftRegisters offset (Cslib.URM.Instr.Z a) = Cslib.URM.Instr.Z (a + offset)
• Cslib.URM.Instr.shiftRegisters offset (Cslib.URM.Instr.S n) = Cslib.URM.Instr.S (n + offset)
• Cslib.URM.Instr.shiftRegisters offset (Cslib.URM.Instr.T m a) = Cslib.URM.Instr.T (m + offset) (a + offset)
• Cslib.URM.Instr.shiftRegisters offset (Cslib.URM.Instr.J m n a) = Cslib.URM.Instr.J (m + offset) (n + offset) a

Register Contents

@[reducible, inline]

abbrev Cslib.URM.Regs : Type

Register contents: maps register indices to natural number contents.

Uses the functional representation ℕ → ℕ for efficiency with rewrites, following the advice from the grind tactic documentation.

Equations

• Cslib.URM.Regs = (ℕ → ℕ)

def Cslib.URM.Regs.zero : Regs

The zero registers where all registers contain 0.

Equations

• Cslib.URM.Regs.zero x✝ = 0

def Cslib.URM.Regs.read (σ : Regs) (n : ℕ) : ℕ

Read the contents of register n.

Equations

• σ.read n = σ n

def Cslib.URM.Regs.write (σ : Regs) (n v : ℕ) : Regs

Write value v to register n.

Equations

• σ.write n v = Function.update σ n v

def Cslib.URM.Regs.ofInputs (inputs : List ℕ) : Regs

Initialize registers with input values in registers 0, 1, ..., k-1. Registers beyond the inputs are initialized to 0.

Equations

• Cslib.URM.Regs.ofInputs inputs n = inputs.getD n 0

def Cslib.URM.Regs.output (σ : Regs) : ℕ

Extract output from register 0.

Equations

• σ.output = σ 0

Programs

@[reducible, inline]

abbrev Cslib.URM.Program : Type

A URM program is a list of instructions.

Equations

• Cslib.URM.Program = List Cslib.URM.Instr

def Cslib.URM.Program.maxRegister (p : Program) : ℕ

The maximum register index referenced by any instruction in the program.

Equations

• p.maxRegister = List.foldl (fun (acc : ℕ) (instr : Cslib.URM.Instr) => max acc instr.maxRegister) 0 p

def Cslib.URM.Program.shiftJumps (p : Program) (offset : ℕ) : Program

Shift all jump targets in a program by offset. Used when concatenating programs: the second program's jumps must be adjusted by the length of the first program.

Equations

• p.shiftJumps offset = List.map (Cslib.URM.Instr.shiftJumps offset) p

def Cslib.URM.Program.shiftRegisters (p : Program) (offset : ℕ) : Program

Shift all register references in a program by offset. Used to isolate register usage when composing programs.

Equations

• p.shiftRegisters offset = List.map (Cslib.URM.Instr.shiftRegisters offset) p

Machine State

structure Cslib.URM.State : Type

Machine state: program counter (0-indexed) and register contents.

• pc : ℕ

  Program counter (0-indexed).

• regs : Regs

  Register contents.

def Cslib.URM.State.init (inputs : List ℕ) : State

Initial state for a program with given inputs. The program counter starts at 0, and inputs are loaded into registers 0, 1, ....

Equations

• Cslib.URM.State.init inputs = { pc := 0, regs := Cslib.URM.Regs.ofInputs inputs }

def Cslib.URM.State.isHalted (s : State) (p : Program) : Prop

A state is halted if the program counter is at or beyond the program length.

Equations

• s.isHalted p = (List.length p ≤ s.pc)

@[implicit_reducible]

instance Cslib.URM.State.instDecidableIsHalted (s : State) (p : Program) : Decidable (s.isHalted p)

Equations

• s.instDecidableIsHalted p = Cslib.URM.State.instDecidableIsHalted._aux_1 s p

@[implicit_reducible]

instance Cslib.URM.State.instInhabited : Inhabited State

Equations

• Cslib.URM.State.instInhabited = { default := Cslib.URM.State.init [] }

@[implicit_reducible]

instance Cslib.URM.State.instRepr : Repr State

Equations

• Cslib.URM.State.instRepr = { reprPrec := fun (s : Cslib.URM.State) (x : ℕ) => Std.Format.text (toString "State(pc=" ++ toString s.pc ++ toString ")") }