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 and, for indirect operands, the runtime addresses), plus a base cost of 1 so every step costs at least one time unit. 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 space
RAM.initCfg — input convention (length in R₀, bits in R₁ … Rₙ)
RAM.Program.DecidesInTime, RAM.Program.DecidesInSpace — deciding a Language with the verdict read from R₀, mirroring TM.DecidesInTime

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 measure well defined.
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.
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.