Random-access machines

InductiveRAM addressing mode#✓fully proved

An addressing mode of a random-access machine specifies an operand by a natural number \(n\) in one of three ways: immediate (the operand is the value \(n\) itself), direct (the operand is the contents of register \(n\)), or indirect (the operand is the contents of the register whose index is the contents of register \(n\)).

inductive RAMAddr where
  | imm : ℕ → RAMAddr
  | dir : ℕ → RAMAddr
  | ind : ℕ → RAMAddr
Sources
  • Aho–Hopcroft–Ullman, The Design and Analysis of Computer Algorithms, 1974, §1.2.
Used by 4
Used byValue of a RAM operand · One step of a RAM machine · A RAM step is sticky at halting states · RAM instruction

InductiveRAM store destination#✓fully proved

A store destination of a random-access machine names, by a natural number \(n\), the register into which the accumulator is stored: either register \(n\) itself (direct) or the register whose index is the contents of register \(n\) (indirect).

An immediate operand is not a valid store destination.

inductive RAMDest where
  | dir : ℕ → RAMDest
  | ind : ℕ → RAMDest
Sources
  • Aho–Hopcroft–Ullman, The Design and Analysis of Computer Algorithms, 1974, §1.2.
Used by 4
Used byRegister written by a RAM store · One step of a RAM machine · A RAM step is sticky at halting states · RAM instruction

InductiveRAM instruction#✓fully proved

An instruction of a random-access machine is one of the following: load an operand into the accumulator; store the accumulator into a store destination; add an operand to the accumulator; subtract an operand from the accumulator, truncating at \(0\); jump to instruction \(q\); jump to instruction \(q\) if the accumulator is \(0\); halt. Here an operand is given by a RAM addressing mode, a store destination is a RAM store destination, and the jump target \(q\) is a natural number.

inductive RAMInstr where
  | load : RAMAddr → RAMInstr
  | store : RAMDest → RAMInstr
  | add : RAMAddr → RAMInstr
  | sub : RAMAddr → RAMInstr
  | jump : ℕ → RAMInstr
  | jz : ℕ → RAMInstr
  | halt : RAMInstr
Sources
  • Aho–Hopcroft–Ullman, The Design and Analysis of Computer Algorithms, 1974, §1.2.
Uses 2 · Used by 8
Statement usesRAM addressing mode · RAM store destination
Used byOutput membership for RAM machines · Output of a RAM machine · Bounded execution of a RAM machine · RAM execution stays at its halted state · RAM execution is stable once halted · One step of a RAM machine · A RAM step is sticky at halting states · RAM-decidable predicate

StructureRAM state#✓fully proved

A state of a random-access machine consists of a program counter in \(\mathbb{N}\), an accumulator value in \(\mathbb{N}\), and register contents, a function \(\mathbb{N} \to \mathbb{N}\) giving the contents of each register.

structure RAMState where
  /-- The program counter. -/
  pc : ℕ
  /-- The accumulator. -/
  acc : ℕ
  /-- The register contents. -/
  regs : ℕ → ℕ
Sources
  • Aho–Hopcroft–Ullman, The Design and Analysis of Computer Algorithms, 1974, §1.2.
Used by 10
Used byOutput membership for RAM machines · Register written by a RAM store · Output of a RAM machine · Bounded execution of a RAM machine · RAM execution stays at its halted state · RAM execution is stable once halted · Initial RAM state · Value of a RAM operand · One step of a RAM machine · A RAM step is sticky at halting states

DefinitionValue of a RAM operand#✓fully proved

In a RAM state with register contents \(r\), an operand resolves to a natural number: the immediate operand \(n\) resolves to \(n\) itself, the direct operand \(n\) to the contents \(r(n)\) of register \(n\), and the indirect operand \(n\) to \(r(r(n))\).

def ramResolve (s : RAMState) (a : RAMAddr) : ℕ :=
  match a with
  | .imm n => n
  | .dir r => s.regs r
  | .ind r => s.regs (s.regs r)
Sources
  • Aho–Hopcroft–Ullman, The Design and Analysis of Computer Algorithms, 1974, §1.2.
Uses 2 · Used by 2
Statement usesRAM addressing mode · RAM state
Used byOne step of a RAM machine · A RAM step is sticky at halting states

DefinitionRegister written by a RAM store#✓fully proved

In a RAM state with register contents \(r\), a store destination resolves to a register index: the direct destination \(n\) resolves to \(n\), and the indirect destination \(n\) resolves to the contents \(r(n)\) of register \(n\).

def ramDestIndex (s : RAMState) (d : RAMDest) : ℕ :=
  match d with
  | .dir r => r
  | .ind r => s.regs r
Sources
  • Aho–Hopcroft–Ullman, The Design and Analysis of Computer Algorithms, 1974, §1.2.
Uses 2 · Used by 2
Statement usesRAM store destination · RAM state
Used byOne step of a RAM machine · A RAM step is sticky at halting states

DefinitionOne step of a RAM machine#✓fully proved

Let \(P = (P_0, \dots, P_{\ell-1})\) be a program of length \(\ell\) and \(s\) a state with program counter \(p\), accumulator \(a\) and register contents \(r\). If \(p \ge \ell\), the step leaves \(s\) unchanged. Otherwise it executes \(P_p\), where \(v\) denotes the value of the instruction's operand in \(s\): a load sets the accumulator to \(v\), an add sets it to \(a + v\), a subtract sets it to \(\max(a - v, 0)\), and a store writes \(a\) into the register that its destination resolves to in \(s\); each of these also increases the program counter by \(1\). A jump to \(q\) sets the program counter to \(q\); a jump-if-zero to \(q\) sets it to \(q\) if \(a = 0\) and to \(p + 1\) otherwise; a halt sets it to \(\ell\). Nothing else changes.

In particular, once the program counter is at least \(\ell\) (for instance after a halt), every further step leaves the state unchanged.

def ramStep (prog : List RAMInstr) (s : RAMState) : RAMState :=
  match prog[s.pc]? with
  | none => s
  | some (.load a) => { s with pc := s.pc + 1, acc := ramResolve s a }
  | some (.store d) =>
      let regs' := Function.update s.regs (ramDestIndex s d) s.acc
      { s with pc := s.pc + 1, regs := regs' }
  | some (.add a) => { s with pc := s.pc + 1, acc := s.acc + ramResolve s a }
  | some (.sub a) => { s with pc := s.pc + 1, acc := s.acc - ramResolve s a }
  | some (.jump q) => { s with pc := q }
  | some (.jz q) => { s with pc := if s.acc = 0 then q else s.pc + 1 }
  | some .halt => { s with pc := prog.length }
Sources
  • Aho–Hopcroft–Ullman, The Design and Analysis of Computer Algorithms, 1974, §1.2.
Uses 6 · Used by 3
Statement usesRAM addressing mode · RAM store destination · RAM instruction · RAM state · Register written by a RAM store · Value of a RAM operand
Used byBounded execution of a RAM machine · RAM execution is stable once halted · A RAM step is sticky at halting states

DefinitionInitial RAM state#✓fully proved

The initial state on inputs \(x_0, \dots, x_{k-1}\) has program counter \(0\) and accumulator \(0\); register \(i\) holds \(x_i\) for \(i < k\), and every other register holds \(0\).

def ramInit (inputs : List ℕ) : RAMState :=
  { pc := 0, acc := 0, regs := fun i ↦ inputs.getD i 0 }
Sources
  • Aho–Hopcroft–Ullman, The Design and Analysis of Computer Algorithms, 1974, §1.2.
Uses 1 · Used by 2
Statement usesRAM state
Used byOutput membership for RAM machines · Output of a RAM machine

DefinitionBounded execution of a RAM machine#✓fully proved

For a program \(P\), a natural number \(t\) and a state \(s\), the state after \(t\) steps of \(P\) from \(s\) is obtained by applying one step of \(P\) to \(s\) exactly \(t\) times.

def ramExecN (prog : List RAMInstr) (t : ℕ) (s : RAMState) : RAMState :=
  (ramStep prog)^[t] s
Sources
  • Aho–Hopcroft–Ullman, The Design and Analysis of Computer Algorithms, 1974, §1.2.
Uses 3 · Used by 4
Statement usesRAM instruction · RAM state · One step of a RAM machine
Used byOutput membership for RAM machines · Output of a RAM machine · RAM execution stays at its halted state · RAM execution is stable once halted

DefinitionOutput of a RAM machine#✓fully proved

Let \(P\) be a program of length \(\ell\) and \(x_0, \dots, x_{k-1}\) inputs. Run \(P\) from the initial state on these inputs. If for some \(t\) the program counter after \(t\) steps is at least \(\ell\), the output of \(P\) on these inputs is the accumulator after the least such number of steps; otherwise the output is undefined.

def ramEval (prog : List RAMInstr) (inputs : List ℕ) : Part ℕ :=
  Nat.rfindOpt fun t ↦
    let s := ramExecN prog t (ramInit inputs)
    if prog.length ≤ s.pc then some s.acc else Option.none
Sources
  • Aho–Hopcroft–Ullman, The Design and Analysis of Computer Algorithms, 1974, §1.2.
Uses 4 · Used by 2
Statement usesRAM instruction · RAM state · Bounded execution of a RAM machine · Initial RAM state
Used byOutput membership for RAM machines · RAM-decidable predicate

TheoremA RAM step is sticky at halting states#✓fully proved

If the program counter of a state \(s\) is at least the length of a program \(P\), then one step of \(P\) leaves \(s\) unchanged.

A halt instruction sets the program counter to the length of the program, so once a halt has been executed the state no longer changes.

theorem ramStep_sticky {prog : List RAMInstr} {s : RAMState}
    (h : prog.length ≤ s.pc) : ramStep prog s = s
Sources
  • Aho–Hopcroft–Ullman, The Design and Analysis of Computer Algorithms, 1974, §1.2.
Uses 7 · Used by 1
Statement usesRAM instruction · RAM state · One step of a RAM machine
Proof usesRAM addressing mode · RAM store destination · Register written by a RAM store · Value of a RAM operand
Used byRAM execution is stable once halted

TheoremRAM execution is stable once halted#✓fully proved

Let \(P\) be a program of length \(\ell\), \(s\) a state and \(t\) a natural number. If the program counter after \(t\) steps of \(P\) from \(s\) is at least \(\ell\), then the state after \(t + 1\) steps of \(P\) from \(s\) equals the state after \(t\) steps.

theorem ramExecN_stable {prog : List RAMInstr} {t : ℕ} {s : RAMState}
    (h : prog.length ≤ (ramExecN prog t s).pc) :
    ramExecN prog (t + 1) s = ramExecN prog t s
Sources
  • Aho–Hopcroft–Ullman, The Design and Analysis of Computer Algorithms, 1974, §1.2.
Uses 5 · Used by 1
Statement usesRAM instruction · RAM state · Bounded execution of a RAM machine
Proof usesOne step of a RAM machine · A RAM step is sticky at halting states
Used byRAM execution stays at its halted state

TheoremRAM execution stays at its halted state#✓fully proved

Let \(P\) be a program of length \(\ell\), \(s\) a state and \(t_1 \le t_2\) natural numbers. If the program counter after \(t_1\) steps of \(P\) from \(s\) is at least \(\ell\), then the state after \(t_2\) steps of \(P\) from \(s\) equals the state after \(t_1\) steps.

theorem ramExecN_eq_of_halted {prog : List RAMInstr} {t₁ t₂ : ℕ} {s : RAMState}
    (h : prog.length ≤ (ramExecN prog t₁ s).pc) (hle : t₁ ≤ t₂) :
    ramExecN prog t₂ s = ramExecN prog t₁ s
Sources
  • Aho–Hopcroft–Ullman, The Design and Analysis of Computer Algorithms, 1974, §1.2.
Uses 4 · Used by 1
Statement usesRAM instruction · RAM state · Bounded execution of a RAM machine
Proof usesRAM execution is stable once halted
Used byOutput membership for RAM machines

TheoremOutput membership for RAM machines#✓fully proved

Let \(P\) be a program of length \(\ell\), let \(x_0, \dots, x_{k-1}\) be inputs and let \(t\) and \(y\) be natural numbers. If, after \(t\) steps of \(P\) from the initial state on these inputs, the program counter is at least \(\ell\) and the accumulator equals \(y\), then the output of \(P\) on these inputs is defined and equals \(y\).

theorem mem_ramEval_of_halted {prog : List RAMInstr} {inputs : List ℕ} {y : ℕ}
    {t : ℕ}
    (hhalt : prog.length ≤ (ramExecN prog t (ramInit inputs)).pc)
    (hout : (ramExecN prog t (ramInit inputs)).acc = y) :
    y ∈ ramEval prog inputs
Sources
  • Aho–Hopcroft–Ullman, The Design and Analysis of Computer Algorithms, 1974, §1.2.
Uses 6
Statement usesRAM instruction · RAM state · Output of a RAM machine · Bounded execution of a RAM machine · Initial RAM state
Proof usesRAM execution stays at its halted state

DefinitionRAM-decidable predicate#✓fully proved

A predicate \(P\) on the natural numbers is RAM decidable when there is a RAM program, a finite list of RAM instructions, such that for every natural number \(n\) the program, started with \(n\) in register \(0\) and with the accumulator, the program counter and every other register at \(0\), halts (its program counter reaches or passes the end of the program) with \(1\) in the accumulator if \(P(n)\) holds and with \(0\) in the accumulator otherwise; that is, its RAM evaluation on the single input \(n\) equals the characteristic function of \(P\) at \(n\).

def RAMDecidable (P : ℕ → Prop) : Prop :=
  ∃ prog : List RAMInstr, ∀ n, ramEval prog [n] = charFun P n
Sources
  • Aho–Hopcroft–Ullman, The Design and Analysis of Computer Algorithms, 1974, §1.2.
Uses 3
Statement usesRAM instruction · Characteristic function of a set of naturals · Output of a RAM machine
15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.