Random-access machines

A random-access machine (RAM) is a register machine whose registers hold natural numbers of unbounded size, whose instructions do arithmetic on whole registers, and which can address a register through the contents of another (indirect addressing), so that a fixed program reaches unboundedly many registers Cook and Reckhow, Section 1. This file defines the machine, its single steps and its runs. How long a run takes depends on how instructions are charged, which is the subject of Cslib.RAM.time and its cost measures.

The model extends cslib's unlimited register machines (Cslib.URM): it uses the same register contents Cslib.URM.Regs and their read/write API, a program is again a list of instructions, a state is again a program counter with register contents, a run starts at instruction 0 with the inputs in registers 0, 1, … (Cslib.RAM.State.init), and a state is halted once its program counter is past the end of the program. The instruction set is that of Cook and Reckhow Cook and Reckhow, Table I with three changes: registers hold natural numbers rather than integers, so subtraction is truncated and the conditional jump tests for a nonzero register; there are no input and output instructions, since the inputs sit in registers as for URMs; and there is a multiplication instruction, which permits a separation between unit and logarithmic time (see Cslib.RAM.exists_mul_pow_lt_of_computesInTime_logCost). Halting and evaluation (Cslib.RAM.Halts, Cslib.RAM.HaltsWithResult, Cslib.RAM.eval) are as for URMs, with the output in register 0. Input initialization and output extraction incur no instruction cost. Consequently this is a natural-number function model, not Cook and Reckhow's charged finite-alphabet input/output convention. Complexity comparisons with string machines require explicit encoding and initial-bitlength assumptions; no such simulation is proved here.

Design notes

• Shared with Cslib.URM: the register contents Cslib.URM.Regs with read, write, ofInputs and output, hence the conventions for inputs (registers 0, 1, …) and output (register 0), and the notions of rewriting (Relation.Normal, Relation.Normalizable) through which halting is characterized.
• Not shared: the instructions, hence the step relation Cslib.RAM.Step, which mirrors Cslib.URM.Step; and the states. Cslib.RAM.State has the same two fields as Cslib.URM.State, but Cslib.URM.State.isHalted takes a URM program, so a shared structure would leave the halting predicate of RAM programs without the dot notation s.isHalted p. The halting and evaluation API repeats URM's statements and names for the RAM step relation, since cslib states it for URMs only rather than for a deterministic machine in general; eval is defined from the run (Nat.find) rather than by choice, and is computable.
• Besides the single-step relation Cslib.RAM.Step there is a total step function Cslib.RAM.step, which leaves a halted state fixed, and the run Cslib.RAM.run p n is its n-th iterate. Costs are sums over runs, and a run as a function of its length is what makes those sums definitions rather than relations; Cslib.RAM.steps_iff_exists_run connects the two views.

Main definitions

• Cslib.RAM.Instr: the instructions: constants, addition, truncated subtraction, multiplication, indirect load and store, and a conditional jump.
• Cslib.RAM.Program, Cslib.RAM.State: programs and machine states.
• Cslib.RAM.Instr.exec: the effect of one instruction on a state.
• Cslib.RAM.step, Cslib.RAM.run: the step function and the run for a given number of steps.
• Cslib.RAM.Step, Cslib.RAM.Steps: the single-step relation and its reflexive transitive closure.
• Cslib.RAM.Halts, Cslib.RAM.HaltsWithResult: halting, and halting with a given output.
• Cslib.RAM.eval: evaluation as a partial function.

Main results

• Cslib.RAM.Step.deterministic: a state has at most one successor.
• Cslib.RAM.isHalted_iff_normal: a state is halted iff it has no successor.
• Cslib.RAM.run_add, Cslib.RAM.run_eq_of_le: runs compose, and are stationary once halted.
• Cslib.RAM.steps_iff_exists_run: the states reachable from s are the states run p n s.
• Cslib.RAM.halts_iff_exists_run, Cslib.RAM.haltsWithResult_iff_exists_run: halting read on the run.
• Cslib.RAM.haltsWithResult_iff_eval: a program halts with result a iff it evaluates to a.

References

• S. A. Cook and R. A. Reckhow, Time bounded random access machines
• N. J. Cutland, Computability: An Introduction to Recursive Function Theory

Instructions, programs and states

inductive Cslib.RAM.Instr : Type

RAM instructions, written destination first as in Cook and Reckhow's X_i ← X_j + X_k Cook and Reckhow, Table I. The register named by a direct operand is part of the instruction; the register named by an indirect operand is the contents of another register.

• const (d v : ℕ) : Instr

  const d v sets register d to the constant v.

• add (d i j : ℕ) : Instr

  add d i j sets register d to the sum of registers i and j.

• sub (d i j : ℕ) : Instr

  sub d i j sets register d to the truncated difference of registers i and j.

• mul (d i j : ℕ) : Instr

  mul d i j sets register d to the product of registers i and j.

• load (d a : ℕ) : Instr

  load d a sets register d to the contents of the register whose index is in register a (an indirect read).

• store (a i : ℕ) : Instr

  store a i sets the register whose index is in register a to the contents of register i (an indirect write).

• jpos (i q : ℕ) : Instr

  jpos i q jumps to instruction q if register i is positive, and otherwise proceeds to the next instruction.

@[instance_reducible]

instance Cslib.RAM.instDecidableEqInstr : DecidableEq Instr

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

@[instance_reducible]

instance Cslib.RAM.instReprInstr : Repr Instr

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

@[reducible, inline]

abbrev Cslib.RAM.Program : Type

A RAM program is a list of instructions, indexed by the program counter.

structure Cslib.RAM.State : Type

A RAM state: a program counter (0-indexed) and register contents.

• pc : ℕ

  The program counter: the index of the next instruction.

• regs : URM.Regs

  The register contents.

theorem Cslib.RAM.State.ext {x y : State} (pc : x.pc = y.pc) (regs : x.regs = y.regs) : x = y

theorem Cslib.RAM.State.ext_iff {x y : State} : x = y ↔ x.pc = y.pc ∧ x.regs = y.regs

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

The initial state on the given inputs: the program counter is 0, and the inputs are in registers 0, 1, …, all other registers holding 0.

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

A state is halted for a program once its program counter is past the end of the program.

@[instance_reducible]

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

@[instance_reducible]

instance Cslib.RAM.State.instInhabited : Inhabited State

@[simp]

theorem Cslib.RAM.State.isHalted_iff {s : State} {p : Program} : s.isHalted p ↔ List.length p ≤ s.pc

@[simp]

theorem Cslib.RAM.State.init_pc (inputs : List ℕ) : (init inputs).pc = 0

@[simp]

theorem Cslib.RAM.State.read_init_nil (n : ℕ) : (init []).regs.read n = 0

Execution

def Cslib.RAM.Instr.exec : Instr → State → State

The state reached by executing an instruction.

def Cslib.RAM.step (p : Program) (s : State) : State

One step of p from s: execute the current instruction, or stay put if s is halted.

def Cslib.RAM.run (p : Program) (n : ℕ) : State → State

The state after running p from s for n steps, staying put once halted.

inductive Cslib.RAM.Step (p : Program) : State → State → Prop

The single-step relation of a program, as for URMs (Cslib.URM.Step): a state that is not halted steps to the result of executing its current instruction.

• exec {p : Program} {s : State} {i : Instr} (h : p[s.pc]? = some i) : Step p s (i.exec s)

@[reducible, inline]

abbrev Cslib.RAM.Steps (p : Program) : State → State → Prop

Multi-step execution: the reflexive transitive closure of Step.

Steps

theorem Cslib.RAM.step_of_getElem? {p : Program} {s : State} {i : Instr} (h : p[s.pc]? = some i) : step p s = i.exec s

theorem Cslib.RAM.step_of_isHalted {p : Program} {s : State} (h : s.isHalted p) : step p s = s

theorem Cslib.RAM.step_step {p : Program} {s : State} (h : ¬s.isHalted p) : Step p s (step p s)

A state that is not halted steps to step p s.

theorem Cslib.RAM.Step.step_eq {p : Program} {s t : State} (h : Step p s t) : step p s = t

theorem Cslib.RAM.Step.not_isHalted {p : Program} {s t : State} (h : Step p s t) : ¬s.isHalted p

theorem Cslib.RAM.Step.deterministic {p : Program} : Relator.RightUnique (Step p)

The step relation is deterministic: each state has at most one successor.

theorem Cslib.RAM.step_iff {p : Program} {s t : State} (h : ¬s.isHalted p) : Step p s t ↔ step p s = t

theorem Cslib.RAM.isHalted_iff_normal {p : Program} {s : State} : s.isHalted p ↔ Relation.Normal (Step p) s

A state is halted iff it is normal (has no successor) for the step relation.

Runs

@[simp]

theorem Cslib.RAM.run_zero {p : Program} {s : State} : run p 0 s = s

theorem Cslib.RAM.run_succ {p : Program} {s : State} {n : ℕ} : run p (n + 1) s = run p n (step p s)

theorem Cslib.RAM.run_succ' {p : Program} {s : State} {n : ℕ} : run p (n + 1) s = step p (run p n s)

theorem Cslib.RAM.run_add {p : Program} {s : State} {m n : ℕ} : run p (m + n) s = run p n (run p m s)

Runs compose: running for m + n steps is running for n steps after m.

theorem Cslib.RAM.run_of_isHalted {p : Program} {s : State} {n : ℕ} (h : s.isHalted p) : run p n s = s

A halted state stays put.

theorem Cslib.RAM.run_eq_of_le {p : Program} {s : State} {m n : ℕ} (hmn : m ≤ n) (h : (run p m s).isHalted p) : run p n s = run p m s

Once a run has halted, running longer changes nothing.

theorem Cslib.RAM.steps_run {p : Program} {s : State} {n : ℕ} : Steps p s (run p n s)

theorem Cslib.RAM.steps_iff_exists_run {p : Program} {s t : State} : Steps p s t ↔ ∃ (n : ℕ), run p n s = t

The states reachable from s are exactly the states of the run from s.

Halting and evaluation

The halting and evaluation API of Cslib.URM (URM/Execution.lean), for RAM programs.

theorem Cslib.RAM.Steps.eq_of_halts {p : Program} {s s₁ s₂ : State} (h₁ : Steps p s s₁) (hh₁ : s₁.isHalted p) (h₂ : Steps p s s₂) (hh₂ : s₂.isHalted p) : s₁ = s₂

Two halted states reachable from the same state are equal.

def Cslib.RAM.Halts (p : Program) (inputs : List ℕ) : Prop

A program halts on given inputs if its run from the initial state reaches a halted state.

def Cslib.RAM.Diverges (p : Program) (inputs : List ℕ) : Prop

A program diverges on given inputs if it does not halt.

def Cslib.RAM.HaltsWithResult (p : Program) (inputs : List ℕ) (result : ℕ) : Prop

A program halts on given inputs with result in the output register 0.

theorem Cslib.RAM.halts_iff_normalizable {p : Program} {inputs : List ℕ} : Halts p inputs ↔ Relation.Normalizable (Step p) (State.init inputs)

Halting is normalizability for the step relation.

theorem Cslib.RAM.halts_iff_exists_run {p : Program} {inputs : List ℕ} : Halts p inputs ↔ ∃ (n : ℕ), (run p n (State.init inputs)).isHalted p

A program halts exactly when its run is halted after some number of steps.

theorem Cslib.RAM.haltsWithResult_iff_exists_run {p : Program} {inputs : List ℕ} {result : ℕ} : HaltsWithResult p inputs result ↔ ∃ (n : ℕ), (run p n (State.init inputs)).isHalted p ∧ (run p n (State.init inputs)).regs.output = result

A program halts with result exactly when its run is halted after some number of steps with result in register 0.

theorem Cslib.RAM.HaltsWithResult.toHalts {p : Program} {inputs : List ℕ} {result : ℕ} (h : HaltsWithResult p inputs result) : Halts p inputs

A program that halts with a result halts.

def Cslib.RAM.evalState (p : Program) (inputs : List ℕ) : Part State

The halted state reached from the initial state, if any: the run after the least number of steps after which it is halted.

theorem Cslib.RAM.evalState_spec {p : Program} {inputs : List ℕ} (h : (evalState p inputs).Dom) : Steps p (State.init inputs) ((evalState p inputs).get h) ∧ ((evalState p inputs).get h).isHalted p

The state given by evalState is reachable and halted.

theorem Cslib.RAM.Halts.toHaltsWithResult {p : Program} {inputs : List ℕ} (h : Halts p inputs) : HaltsWithResult p inputs ((evalState p inputs).get h).regs.output

A program that halts halts with the output of the state given by evalState.

def Cslib.RAM.eval (p : Program) (inputs : List ℕ) : Part ℕ

Evaluation as a partial function: defined when the program halts, with the contents of the output register 0.

theorem Cslib.RAM.haltsWithResult_iff_eval {p : Program} {inputs : List ℕ} {result : ℕ} : HaltsWithResult p inputs result ↔ eval p inputs = Part.some result

A program halts with result iff it evaluates to result.