Repeated squaring separates unit and logarithmic cost

The unit cost measure charges a RAM one unit per instruction, however large the numbers involved. With multiplication it need not be polynomially comparable to logarithmic cost. The fixed program Cslib.RAM.repeatedSquaring reads k in register 0, puts 2 in register 1, then squares register 1 while counting register 0 down to zero, and copies the result to register 0: it computes k ↦ 2 ^ 2 ^ k within unit time 4 k + 5, taking exactly 4 k + 5 steps. The value 2 ^ 2 ^ k has 2 ^ k + 1 binary digits, and logarithmic time bounds the length of every number a RAM holds (Cslib.RAM.bitLength_read_run_le), so every program computing k ↦ 2 ^ 2 ^ k, this one included, takes logarithmic time more than 2 ^ k on input k. Hence no polynomial in the unit time 4 k + 5 bounds the logarithmic time of any program computing this function: unit time and logarithmic time are not polynomially related.

Hartmanis and Simon showed much more: under unit cost, RAMs with multiplication and bitwise Boolean operations decide in polynomial time exactly the languages that Turing machines decide in polynomial space Hartmanis and Simon. Without multiplication, an instruction other than loading a constant at most doubles the largest number held. To obtain a polynomial comparison from this observation, one must also control the initial bit lengths. Cook and Reckhow use charged input instructions on finite-alphabet strings and time bounds at least the input length Cook and Reckhow, Section 1 and Theorem 2. Here inputs are arbitrary natural numbers preloaded for free: a single addition has unit cost 1 but unbounded logarithmic cost across inputs. Thus no bound in unit time alone follows in this API. Neither the cited complexity-class result nor a RAM-to-Turing-machine simulation is formalized here. The parameter k in the proved separation is the input's numeric value, not its binary encoding length.

Main definitions

• Cslib.RAM.repeatedSquaring: the program computing k ↦ 2 ^ 2 ^ k by repeated squaring.

Main results

• Cslib.RAM.run_repeatedSquaring: the state in which the program halts on input k.
• Cslib.RAM.computesInTime_unitCost_repeatedSquaring, Cslib.RAM.time_unitCost_repeatedSquaring: the program computes k ↦ 2 ^ 2 ^ k within unit time 4 k + 5, and its run takes exactly that time.
• Cslib.RAM.two_pow_lt_of_computesInTime_logCost, Cslib.RAM.two_pow_lt_time_logCost_repeatedSquaring: every program computing k ↦ 2 ^ 2 ^ k within logarithmic time T has 2 ^ k < T k; in particular the run of repeatedSquaring on k takes logarithmic time more than 2 ^ k.
• Cslib.RAM.exists_mul_pow_lt_of_computesInTime_logCost: the logarithmic time of a program computing k ↦ 2 ^ 2 ^ k is bounded by no polynomial in the unit time 4 k + 5.

References

• S. A. Cook and R. A. Reckhow, Time bounded random access machines
• J. Hartmanis and J. Simon, On the power of multiplication in random access machines

def Cslib.RAM.repeatedSquaring : Program

The repeated-squaring program. With k in register 0, it puts 2 in register 1 and 1 in register 2 (instructions 0 and 1); while register 0 is positive, it squares register 1 and decrements register 0 (instructions 2 and 4 to 6); then it copies register 1 into register 0 (instructions 3 and 7). Register 2 holds the constant 1, which makes the jumps at instructions 3 and 6 unconditional.

@[simp]

theorem Cslib.RAM.length_repeatedSquaring : List.length repeatedSquaring = 8

theorem Cslib.RAM.run_two_repeatedSquaring (k : ℕ) : run repeatedSquaring 2 (State.init [k]) = { pc := 2, regs := URM.Regs.ofInputs [k, 2, 1] }

The first two steps load the constants.

theorem Cslib.RAM.run_four_repeatedSquaring (a b : ℕ) : run repeatedSquaring 4 { pc := 2, regs := URM.Regs.ofInputs [a + 1, b, 1] } = { pc := 2, regs := URM.Regs.ofInputs [a, b * b, 1] }

One round of the loop squares register 1 and decrements register 0.

theorem Cslib.RAM.run_four_mul_repeatedSquaring {j k : ℕ} (hj : j ≤ k) : run repeatedSquaring (4 * j) { pc := 2, regs := URM.Regs.ofInputs [k, 2, 1] } = { pc := 2, regs := URM.Regs.ofInputs [k - j, 2 ^ 2 ^ j, 1] }

After j ≤ k rounds of the loop, register 0 holds k - j and register 1 holds 2 ^ 2 ^ j.

theorem Cslib.RAM.run_four_mul_add_four_repeatedSquaring (k : ℕ) : run repeatedSquaring (4 * k + 4) (State.init [k]) = { pc := 7, regs := URM.Regs.ofInputs [0, 2 ^ 2 ^ k, 1] }

Once register 0 is zero, the loop exits at instruction 3.

theorem Cslib.RAM.run_repeatedSquaring (k : ℕ) : run repeatedSquaring (4 * k + 5) (State.init [k]) = { pc := 8, regs := URM.Regs.ofInputs [2 ^ 2 ^ k, 2 ^ 2 ^ k, 1] }

The run of the repeated-squaring program: on input k, it halts after 4 k + 5 steps with 2 ^ 2 ^ k in registers 0 and 1.

theorem Cslib.RAM.isHalted_run_repeatedSquaring (k : ℕ) : (run repeatedSquaring (4 * k + 5) (State.init [k])).isHalted repeatedSquaring

On input k, the program halts after 4 k + 5 steps.

theorem Cslib.RAM.output_run_repeatedSquaring (k : ℕ) : (run repeatedSquaring (4 * k + 5) (State.init [k])).regs.output = 2 ^ 2 ^ k

On input k, the program halts with 2 ^ 2 ^ k in the output register 0.

theorem Cslib.RAM.time_unitCost_repeatedSquaring (k : ℕ) : time unitCost repeatedSquaring (4 * k + 5) (State.init [k]) = 4 * k + 5

Under unit cost, the run on k takes time 4 k + 5: it halts after 4 k + 5 steps and not before.

theorem Cslib.RAM.computesInTime_unitCost_repeatedSquaring : ComputesInTime unitCost 1 repeatedSquaring (fun (x : Fin 1 → ℕ) => 2 ^ 2 ^ x 0) fun (x : Fin 1 → ℕ) => 4 * x 0 + 5

Repeated squaring computes k ↦ 2 ^ 2 ^ k within unit time 4 k + 5.

theorem Cslib.RAM.two_pow_lt_of_computesInTime_logCost {p : Program} {T : (Fin 1 → ℕ) → ℕ} (h : ComputesInTime logCost 1 p (fun (x : Fin 1 → ℕ) => 2 ^ 2 ^ x 0) T) (x : Fin 1 → ℕ) : 2 ^ x 0 < T x

Computing 2 ^ 2 ^ k takes logarithmic time more than 2 ^ k. Every program computing k ↦ 2 ^ 2 ^ k within logarithmic time T has 2 ^ k < T k: the output has 2 ^ k + 1 binary digits, and a run of logarithmic time T holds no number longer than T or than the input (Cslib.RAM.bitLength_read_run_le).

theorem Cslib.RAM.two_pow_lt_time_logCost_repeatedSquaring (k : ℕ) : 2 ^ k < time logCost repeatedSquaring (4 * k + 5) (State.init [k])

Under logarithmic cost, the run of the repeated-squaring program on k takes time more than 2 ^ k.

theorem Cslib.RAM.exists_mul_pow_lt_of_computesInTime_logCost {p : Program} {T : (Fin 1 → ℕ) → ℕ} (h : ComputesInTime logCost 1 p (fun (x : Fin 1 → ℕ) => 2 ^ 2 ^ x 0) T) (c d : ℕ) : ∃ (x : Fin 1 → ℕ), c * (4 * x 0 + 5) ^ d < T x

Unit cost is unsound. The repeated-squaring program computes k ↦ 2 ^ 2 ^ k within unit time 4 k + 5 (Cslib.RAM.computesInTime_unitCost_repeatedSquaring), but the logarithmic time T of any program computing it is bounded by no polynomial in 4 k + 5: for all c and d, some input k has c (4 k + 5) ^ d < T k.