Random access machines: model and cost measures #

This file defines a Random Access Machine (RAM) — a register machine with indirect addressing — together with logarithmic-cost time and space measures. The design follows the standard successor/register RAM of Cook–Reckhow, Time bounded random access machines (JCSS 7 (1973), 354–375) and the textbook presentations of Papadimitriou (Computational Complexity, §2.6) and van Emde Boas (Machine models and simulations, Handbook of Theoretical Computer Science A, 1990). Conventions are adapted for a clean formalization where a text is silent or divergent, but the cost measure is kept faithful to the literature, because it is exactly the cost measure that determines whether the model is a sound stand-in for a Turing machine.

Why logarithmic cost (the soundness point) #

A RAM stores natural numbers of unbounded magnitude in each register. Under the naive unit-cost measure — one time unit per instruction regardless of operand size — a RAM can square a register repeatedly to build the number 2 ^ (2 ^ k) in O(k) steps. That number needs 2 ^ k bits to write down, so no Turing machine can even emit it in fewer than 2 ^ k steps: unit-cost RAM time is super-polynomially stronger than Turing time, and the two models are not polynomially equivalent. Adopting unit cost and then comparing to Turing machines would be a category error — the exact "reward hacking" this model is designed to avoid. RAM.logGap_squaring in the surface file turns this into a theorem about this very model.

The logarithmic-cost measure charges each instruction the total bit-length of the numbers it manipulates (operand contents, computed results, and, for indirect operands, the runtime addresses), plus a base cost of 1 so every step costs at least one time unit. The one exception is sub, which charges its operands but not its result; truncated subtraction never produces a number longer than its first operand, so the result is still paid for. Under this measure the RAM is polynomially equivalent to the multi-tape Turing machine of Complexitylib.Models.TuringMachine; the precise two-way simulation bounds are recorded in the surface module Complexitylib.Models.RandomAccessMachine.

Main definitions #

RAM.Instr — the instruction set (immediate, add/sub/mul, indirect load/store, conditional/unconditional jump, halt)
RAM.Cfg — a configuration: a program counter and a register file ℕ → ℕ
RAM.step, RAM.run — executable single step and fuel-bounded run
RAM.bitlen — the length function l(v) = Nat.size v (number of bits)
RAM.Instr.logCost — the logarithmic cost of one instruction in a state
RAM.logTimeUpto, RAM.unitTimeUpto — accumulated log-cost / step count
RAM.Cfg.space, RAM.spaceUpto — logarithmic-cost register footprint
RAM.initCfg — input convention (length in R₀, bits in R₁ … Rₙ)
RAM.Cfg.workSpace, RAM.workSpaceUpto — logarithmic-cost work space, which leaves registers still holding their input value free
RAM.Program.DecidesInTime, RAM.Program.DecidesInSpace — deciding a Language with the verdict read from R₀, mirroring TM.DecidesInTime and TM.DecidesInSpace

Design notes #

Register file ℕ → ℕ: total and computable, so programs are executable witnesses (#eval-able). Only finitely many registers are ever nonzero along a run; this finite-support invariant makes the space measures well defined.
Space excludes the unmodified input: RAM.Program.DecidesInSpace bounds RAM.workSpaceUpto, which charges a register its address bits plus content bits only while its content differs from its initial value. The input registers are therefore free until overwritten, as the read-only input tape is for TM.DecidesInSpace, and space bounds below the input length are meaningful. This follows the literature: Cook–Reckhow keep the input on a separate read-only device, and Slot–van Emde Boas (The problem of space invariance for sequential machines, Inform. and Comput. 77 (1988), 93–122) charge the address and content bits of the registers in use. The input-inclusive footprint RAM.spaceUpto remains the measure that the structured compiler preserves exactly and the TM-to-RAM simulation reports.
bitlen v = Nat.size v: the number of binary digits, with bitlen 0 = 0, bitlen 1 = 1, bitlen (2^k) = k + 1. Instruction costs add 1 so that each step costs ≥ 1 regardless of operand sizes.
Direct vs. indirect addressing: register literals named in an instruction (d, s, t, a) are program constants, bounded by the program size, so the cost does not separately charge for them; runtime addresses (R a in load/store) are charged via bitlen (c.regs a). This keeps the cost within a constant factor of the Cook–Reckhow measure while remaining sound: every value read, computed, or written is charged its bit-length, except the result of sub, which is bounded by the (charged) first operand.
Out-of-range pc halts: curInstr reads Instr.halt when pc is past the program, so a program need not end in halt and jumps may target the end.