Cost measures for random-access machines

A cost measure charges each instruction, executed on given register contents, an amount of time, and the time of a run is the total charge of the instructions it executes. Two measures are standard Cook and Reckhow, Section 1:

• the unit cost measure charges every instruction 1, so that time counts steps;
• the logarithmic cost measure charges every instruction the lengths of the numbers it reads, so that time accounts for the size of the numbers in the registers.

Within logarithmic time T a RAM never holds a number longer than T or than the longest number it starts with (Cslib.RAM.bitLength_read_run_le), whereas within unit time 4 k + 5 a fixed program builds from k a number with 2 ^ k + 1 binary digits (Cslib.RAM.computesInTime_unitCost_repeatedSquaring), so that logarithmic time is not bounded by any polynomial in unit time (Cslib.RAM.exists_mul_pow_lt_of_computesInTime_logCost).

A program computes a function within time T (Cslib.RAM.ComputesInTime) when on every input it halts with the value of the function in the output register 0 (Cslib.RAM.HaltsWithResult) after a run of time at most T. The time bound is a function of the input tuple, with no chosen string encoding or input-length measure. Input loading and output extraction are free. For example, the empty program returns its first preloaded input in time 0 under either measure. The bit-length bound above therefore retains the initial-size term: it cannot in general be replaced by a bound in execution time alone. These costs adapt Cook and Reckhow's conventions; no Turing-machine simulation or equality of polynomial-time language classes is proved here.

The length of a number is Cslib.RAM.bitLength n = ⌊log₂ n⌋ + 1, its number of binary digits with 0 written as one digit: it is max n.size 1, Mathlib's Nat.size n except at 0 (Cslib.RAM.bitLength_eq_max_size). It is defined through Nat.log, which the kernel evaluates, so that decide computes costs, and it is the ⌊log₂ n⌋ + 1 of the bounds of Cslib.polynomiallyBounded_two_pow_mul_log. Cook and Reckhow's logarithmic function l(n) is ⌈log₂ n⌉ for n ≥ 2 and 1 below, so that l(n) ≤ bitLength n ≤ 2 * l(n).

Main definitions

• Cslib.RAM.bitLength: the length of a natural number.
• Cslib.RAM.unitCost, Cslib.RAM.logCost: the unit and the logarithmic cost measures.
• Cslib.RAM.stepCost: the cost of the next step of a program.
• Cslib.RAM.time: the time of a run of a given number of steps.
• Cslib.RAM.HaltsWithResultInTime, Cslib.RAM.ComputesInTime: halting with a given output, and computing a function, within a time bound.

Main results

• Cslib.RAM.time_add: time is additive along a run.
• Cslib.RAM.bitLength_eq_max_size: the length of a number is max n.size 1.
• Cslib.RAM.time_le_time_of_le, Cslib.RAM.time_mono_cost, Cslib.RAM.time_eq_of_le: time is monotone in the number of steps and in the cost measure, and stationary once halted.
• Cslib.RAM.time_unitCost: unit time counts the steps taken.
• Cslib.RAM.time_unitCost_le_time_logCost: unit time is at most logarithmic time.
• Cslib.RAM.bitLength_read_run_le: the numbers held after a run of logarithmic time T are no longer than T or the longest number held at the start.

References

• S. A. Cook and R. A. Reckhow, Time bounded random access machines

The length of a number

def Cslib.RAM.bitLength (n : ℕ) : ℕ

The length ⌊log₂ n⌋ + 1 of a natural number n: its number of binary digits, where 0 is written with one digit. This is the logarithmic cost of storing n Cook and Reckhow, Section 1. It is max n.size 1 (Cslib.RAM.bitLength_eq_max_size), and is defined through Nat.log so that the kernel evaluates it.

theorem Cslib.RAM.bitLength_eq_max_size (n : ℕ) : bitLength n = max n.size 1

The length of a number is Mathlib's Nat.size, except that 0 has length 1.

theorem Cslib.RAM.bitLength_eq_size {n : ℕ} (hn : n ≠ 0) : bitLength n = n.size

@[simp]

theorem Cslib.RAM.bitLength_zero : bitLength 0 = 1

theorem Cslib.RAM.one_le_bitLength (n : ℕ) : 1 ≤ bitLength n

theorem Cslib.RAM.bitLength_mono : Monotone bitLength

@[simp]

theorem Cslib.RAM.bitLength_two_pow (k : ℕ) : bitLength (2 ^ k) = k + 1

theorem Cslib.RAM.length_digits_two {n : ℕ} (hn : n ≠ 0) : (Nat.digits 2 n).length = bitLength n

A nonzero number has as many binary digits as its length.

theorem Cslib.RAM.lt_two_pow_bitLength (n : ℕ) : n < 2 ^ bitLength n

theorem Cslib.RAM.bitLength_le_iff {n k : ℕ} (hk : k ≠ 0) : bitLength n ≤ k ↔ n < 2 ^ k

theorem Cslib.RAM.bitLength_add_le (m n : ℕ) : bitLength (m + n) ≤ bitLength m + bitLength n

theorem Cslib.RAM.bitLength_mul_le (m n : ℕ) : bitLength (m * n) ≤ bitLength m + bitLength n

Cost measures and time

def Cslib.RAM.unitCost : Instr → URM.Regs → ℕ

The unit cost measure charges every instruction one unit of time, whatever the size of the numbers it manipulates.

def Cslib.RAM.logCost : Instr → URM.Regs → ℕ

The logarithmic cost measure charges every instruction the lengths of the numbers it reads: its constant, the contents of its operand registers, and, for an indirect operand, both the address and the contents of the register at that address. This is Cook and Reckhow's measure Cook and Reckhow, Table I with bitLength for their l, multiplication charged like addition, and a constant charged its length rather than 1, so that the bound Cslib.RAM.bitLength_read_run_le does not depend on the program. Register indices written in the instruction are not charged, since they are bounded by the program. Neither is the number written: it is never longer than the charge (Cslib.RAM.bitLength_read_exec_le).

def Cslib.RAM.stepCost (cost : Instr → URM.Regs → ℕ) (p : Program) (s : State) : ℕ

The cost of the next step of p from s under cost: the cost of the current instruction, or 0 if s is halted.

def Cslib.RAM.time (cost : Instr → URM.Regs → ℕ) (p : Program) (n : ℕ) (s : State) : ℕ

The time of the run of p from s for n steps under cost: the total cost of the instructions it executes. Steps taken after the run halts cost nothing.

theorem Cslib.RAM.stepCost_of_getElem? {cost : Instr → URM.Regs → ℕ} {p : Program} {s : State} {i : Instr} (h : p[s.pc]? = some i) : stepCost cost p s = cost i s.regs

theorem Cslib.RAM.stepCost_of_isHalted {cost : Instr → URM.Regs → ℕ} {p : Program} {s : State} (h : s.isHalted p) : stepCost cost p s = 0

theorem Cslib.RAM.stepCost_mono {cost cost' : Instr → URM.Regs → ℕ} {p : Program} {s : State} (h : cost ≤ cost') : stepCost cost p s ≤ stepCost cost' p s

@[simp]

theorem Cslib.RAM.time_zero {cost : Instr → URM.Regs → ℕ} {p : Program} {s : State} : time cost p 0 s = 0

theorem Cslib.RAM.time_succ {cost : Instr → URM.Regs → ℕ} {p : Program} {s : State} {n : ℕ} : time cost p (n + 1) s = stepCost cost p s + time cost p n (step p s)

theorem Cslib.RAM.time_succ' {cost : Instr → URM.Regs → ℕ} {p : Program} {s : State} {n : ℕ} : time cost p (n + 1) s = time cost p n s + stepCost cost p (run p n s)

theorem Cslib.RAM.time_add {cost : Instr → URM.Regs → ℕ} {p : Program} {s : State} {m n : ℕ} : time cost p (m + n) s = time cost p m s + time cost p n (run p m s)

Time is additive along a run.

theorem Cslib.RAM.time_of_isHalted {cost : Instr → URM.Regs → ℕ} {p : Program} {s : State} {n : ℕ} (h : s.isHalted p) : time cost p n s = 0

A halted state takes no time.

theorem Cslib.RAM.time_eq_of_le {cost : Instr → URM.Regs → ℕ} {p : Program} {s : State} {m n : ℕ} (hmn : m ≤ n) (h : (run p m s).isHalted p) : time cost p n s = time cost p m s

Once a run has halted, running longer takes no more time.

theorem Cslib.RAM.time_le_time_of_le {cost : Instr → URM.Regs → ℕ} {p : Program} {s : State} {m n : ℕ} (hmn : m ≤ n) : time cost p m s ≤ time cost p n s

Time is monotone in the number of steps.

theorem Cslib.RAM.time_mono_cost {cost cost' : Instr → URM.Regs → ℕ} {p : Program} {s : State} {n : ℕ} (h : cost ≤ cost') : time cost p n s ≤ time cost' p n s

Time is monotone in the cost measure.

Unit cost

theorem Cslib.RAM.stepCost_unitCost_le {p : Program} {s : State} : stepCost unitCost p s ≤ 1

theorem Cslib.RAM.stepCost_unitCost {p : Program} {s : State} (h : ¬s.isHalted p) : stepCost unitCost p s = 1

theorem Cslib.RAM.time_unitCost_le {p : Program} {s : State} {n : ℕ} : time unitCost p n s ≤ n

Unit time is at most the number of steps.

theorem Cslib.RAM.time_unitCost {p : Program} {s : State} {n : ℕ} (h : ∀ j < n, ¬(run p j s).isHalted p) : time unitCost p n s = n

Unit time counts the steps taken: a run that has not halted before its last step takes unit time equal to its number of steps.

Logarithmic cost

theorem Cslib.RAM.one_le_logCost (i : Instr) (r : URM.Regs) : 1 ≤ logCost i r

theorem Cslib.RAM.unitCost_le_logCost : unitCost ≤ logCost

theorem Cslib.RAM.time_unitCost_le_time_logCost {p : Program} {s : State} {n : ℕ} : time unitCost p n s ≤ time logCost p n s

Unit time is at most logarithmic time.

theorem Cslib.RAM.bitLength_read_exec_le {s : State} {b : ℕ} (i : Instr) (hs : ∀ (r : ℕ), bitLength (s.regs.read r) ≤ b) (r : ℕ) : bitLength ((i.exec s).regs.read r) ≤ max b (logCost i s.regs)

An instruction writes no number longer than its logarithmic cost: if the registers of s hold numbers of length at most b, then after executing i they hold numbers of length at most the larger of b and the logarithmic cost of i.

theorem Cslib.RAM.bitLength_read_step_le {p : Program} {s : State} {b : ℕ} (hs : ∀ (r : ℕ), bitLength (s.regs.read r) ≤ b) (r : ℕ) : bitLength ((step p s).regs.read r) ≤ max b (stepCost logCost p s)

theorem Cslib.RAM.bitLength_read_run_le {p : Program} {s : State} {b : ℕ} (hs : ∀ (r : ℕ), bitLength (s.regs.read r) ≤ b) (n r : ℕ) : bitLength ((run p n s).regs.read r) ≤ max b (time logCost p n s)

Logarithmic cost bounds the numbers a RAM holds. If the registers of s hold numbers of length at most b, then after a run of logarithmic time T they hold numbers of length at most the larger of b and T. This is the fact on which Cook and Reckhow's simulation of RAMs by Turing machines rests Cook and Reckhow, Section 4, Lemma.

Computing within a time bound

def Cslib.RAM.HaltsWithResultInTime (cost : Instr → URM.Regs → ℕ) (p : Program) (inputs : List ℕ) (result T : ℕ) : Prop

p halts on inputs with result in the output register 0 within time T under cost: its run from the initial state is halted after some number of steps, with result in register 0, and takes time at most T until then.

def Cslib.RAM.ComputesInTime (cost : Instr → URM.Regs → ℕ) (k : ℕ) (p : Program) (f T : (Fin k → ℕ) → ℕ) : Prop

p computes the function f of k arguments within time T under cost: on every input x it halts with f x in the output register 0 within time T x. As for URMs (Cslib.URM.Computes), the arguments are the inputs in registers 0, …, k - 1. Initialization and output extraction are uncharged; T is indexed by the input tuple, not by a specified string-encoding length.

theorem Cslib.RAM.HaltsWithResultInTime.haltsWithResult {cost : Instr → URM.Regs → ℕ} {p : Program} {inputs : List ℕ} {result T : ℕ} (h : HaltsWithResultInTime cost p inputs result T) : HaltsWithResult p inputs result

A program halting with a result within a time bound halts with that result.

theorem Cslib.RAM.HaltsWithResultInTime.mono {cost : Instr → URM.Regs → ℕ} {p : Program} {inputs : List ℕ} {result T T' : ℕ} (h : HaltsWithResultInTime cost p inputs result T) (hT : T ≤ T') : HaltsWithResultInTime cost p inputs result T'

A time bound can be increased.

theorem Cslib.RAM.HaltsWithResultInTime.mono_cost {cost cost' : Instr → URM.Regs → ℕ} {p : Program} {inputs : List ℕ} {result T : ℕ} (h : HaltsWithResultInTime cost' p inputs result T) (hc : cost ≤ cost') : HaltsWithResultInTime cost p inputs result T

A cost measure can be decreased.

theorem Cslib.RAM.ComputesInTime.eval_eq {cost : Instr → URM.Regs → ℕ} {p : Program} {k : ℕ} {f T : (Fin k → ℕ) → ℕ} (h : ComputesInTime cost k p f T) (x : Fin k → ℕ) : eval p (List.ofFn x) = Part.some (f x)

A program computing f evaluates to f.

theorem Cslib.RAM.ComputesInTime.mono {cost : Instr → URM.Regs → ℕ} {p : Program} {k : ℕ} {f T T' : (Fin k → ℕ) → ℕ} (h : ComputesInTime cost k p f T) (hT : T ≤ T') : ComputesInTime cost k p f T'

A time bound can be increased.

theorem Cslib.RAM.ComputesInTime.mono_cost {cost cost' : Instr → URM.Regs → ℕ} {p : Program} {k : ℕ} {f T : (Fin k → ℕ) → ℕ} (h : ComputesInTime cost' k p f T) (hc : cost ≤ cost') : ComputesInTime cost k p f T

A cost measure can be decreased.