Numeric bounds for binary-polynomial computations

A polynomial in the binary length of a natural number is bounded by a constant times its value plus one. Thus every binary-polynomial computation on a natural number runs in time and space O(n + 1), independently of its output encoding. On a pair of binary naturals the corresponding bound is O(a + b + 1).

These bounds let constructible clocks and padding algorithms perform binary arithmetic while charging for the numeric quantities they already process.

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.nat_inO: a binary-polynomial computation on one natural number has numeric linear bounds.
• Turing.MultiTapeTM.ComputableInPolyTime.natPair_inO: the bound for two natural numbers is linear in their sum.

theorem Turing.MultiTapeTM.ComputableInPolyTime.nat_inO {β : Type} {encOut : β ↪ List Bool} {f : ℕ → β} (hf : ComputableInPolyTime f encNat encOut) : ComputableInO f encNat encOut (fun (n : ℕ) => n) fun (n : ℕ) => n

Every polynomial-time computation on a binary natural has time and space bounded by O(n + 1), where n is its numeric value.

theorem Turing.MultiTapeTM.ComputableInPolyTime.natPair_inO {β : Type} {encOut : β ↪ List Bool} {f : ℕ × ℕ → β} (hf : ComputableInPolyTime f (encPair encNat encNat) encOut) : ComputableInO f (encPair encNat encNat) encOut (fun (p : ℕ × ℕ) => p.1 + p.2) fun (p : ℕ × ℕ) => p.1 + p.2

Every polynomial-time computation on a pair of binary naturals has time and space bounded by O(a + b + 1), where a and b are their numeric values.