Why the RAM must use logarithmic cost: a formal soundness theorem

This module turns the model's central design decision into a theorem. A RAM stores unbounded natural numbers in each register. Under the unit-cost measure (one time unit per instruction, RAM.unitTimeUpto) a program can repeatedly square a register, reaching 2 ^ (2 ^ k) in k + 1 steps. That number has 2 ^ k + 1 binary digits, so any Turing machine needs at least 2 ^ k steps merely to write it: unit-cost RAM time is super-polynomially stronger than Turing time, and the two models are not polynomially equivalent.

RAM.logGap_squaring proves exactly this gap for the squaring program family RAM.sqProg: on the same run, the unit time is k + 1 while the logarithmic time (RAM.logTimeUpto, which charges each instruction the bit-length of the numbers it manipulates) is at least 2 ^ k. This is why the library adopts the logarithmic cost measure and never the unit-cost one — the difference is not a convention but the boundary between a sound Turing-equivalent model and a "reward-hacked" one that decides more than it should in polynomial time.

def Complexity.RAM.sqProg (k : ℕ) : Program

The k-fold squaring program: load 2 into register 1, then square register 1 a total of k times. After j + 1 steps register 1 holds 2 ^ (2 ^ j).

Equations

• Complexity.RAM.sqProg k = Complexity.RAM.Instr.imm 1 2 :: List.replicate k (Complexity.RAM.Instr.mul 1 1 1)

def Complexity.RAM.sqStart : Cfg

The start configuration for the squaring family: program counter 0, all registers 0.

Equations

• Complexity.RAM.sqStart = { pc := 0, regs := fun (x : ℕ) => 0 }

theorem Complexity.RAM.logGap_squaring {k : ℕ} (hk : 1 ≤ k) : ∃ (P : Program) (c : Cfg), Halted P (run P (k + 1) c) ∧ unitTimeUpto P (k + 1) c = k + 1 ∧ 2 ^ k ≤ logTimeUpto P (k + 1) c

The unit-vs-logarithmic gap for the squaring family. On the run of the k-fold squaring program sqProg k for k + 1 steps:

• the machine halts;
• the unit time is k + 1 (linear in k);
• the logarithmic time is at least 2 ^ k (exponential in k).

Hence any complexity measure based on unit cost differs super-polynomially from logarithmic cost, and only the logarithmic measure is polynomially related to Turing-machine time. This is the formal justification for the library's cost convention.