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
• J.C. Shepherdson and H.E. Sturgis, Computability of Recursive Functions

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

@[instance_reducible]

instance Cslib.URM.instDecidableEqInstr : DecidableEq Instr

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

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

@[instance_reducible]

instance Cslib.URM.instReprInstr : Repr Instr

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

The registers read by an instruction.

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

The register written to by an instruction, if any.

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

The maximum register index referenced by an instruction.

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.

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.

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.

def Cslib.URM.Regs.zero : Regs

The zero registers where all registers contain 0.

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

Read the contents of register n.

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

Write value v to register n.

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.

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

Extract output from register 0.

Programs

@[reducible, inline]

abbrev Cslib.URM.Program : Type

A URM program is a list of instructions.

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

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

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.

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.

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, ....

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.

@[instance_reducible]

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

@[instance_reducible]

instance Cslib.URM.State.instInhabited : Inhabited State

@[instance_reducible]

instance Cslib.URM.State.instRepr : Repr State