Lengths, comparisons and unary conversion within given bounds

Routines that compute resource bounds from an input, with computability up to constants (Turing.MultiTapeTM.ComputableInO): the length of a bit word in binary, the comparison of two unary numbers, and conversions between unary and binary. They are the building blocks of constructible resource bounds, of padding arguments and of the diagonal machines of the hierarchy theorems.

The conversions are linear. From unary to binary, a counter is halved once per round and the parity of each nonzero value is emitted; the rounds cost n + n / 2 + ⋯ = O(n). From binary to unary, the digits are read least significant first while a unary place value doubles, and the place value is emitted at each digit one; round i costs O(2 ^ i). The number of binary digits of m is logarithmic in m, so every power of it is O(m + 1); this absorbs binary counters into bounds linear in the counted value.

Main results

• Turing.MultiTapeTM.two_pow_length_encNat_le: the binary digits of m are logarithmic.
• Turing.MultiTapeTM.exists_pow_length_encNat_le: every power of the number of binary digits of m is O(m + 1).
• Turing.MultiTapeTM.ComputableInO.unary_halvings: halving a unary number once per round and emitting a function of each value, within time and space linear in the number and the rounds.
• Turing.MultiTapeTM.ComputableInO.unaryToNat: from unary to binary, within linear time and space.
• Turing.MultiTapeTM.ComputableInO.lengthNat: the length of a bit word in binary, within linear time and space.
• Turing.MultiTapeTM.ComputableInO.unaryLe: the comparison of unary numbers, within quadratic time and linear space.
• Turing.MultiTapeTM.ComputableInO.natToUnary: from binary to unary, within time and space linear in the number converted, not in the length of its binary encoding.

theorem Turing.MultiTapeTM.two_pow_length_encNat_le (m : ℕ) : 2 ^ (encNat m).length ≤ 2 * (m + 1)

The binary digits of m are logarithmic: 2 ^ (encNat m).length ≤ 2 * (m + 1).

theorem Turing.MultiTapeTM.exists_pow_length_encNat_le (d : ℕ) : ∃ (C : ℕ), ∀ (m : ℕ), ((encNat m).length + 1) ^ d ≤ C * (m + 1)

Every power of the number of binary digits of m is O(m + 1).

Conversions between unary and binary, in linear time

theorem Turing.MultiTapeTM.ComputableInO.unary_halvings {emit finish : ℕ → List Bool} (hemit : ComputableInO emit encUnary encBits (fun (v : ℕ) => v) fun (v : ℕ) => v) (hfinish : ComputableInO finish encUnary encBits (fun (v : ℕ) => v) fun (v : ℕ) => v) : ComputableInO (fun (x : ℕ × ℕ) => (List.map (fun (i : ℕ) => emit (x.1 / 2 ^ i)) (List.range x.2)).flatten ++ finish (x.1 / 2 ^ x.2)) (encPair encUnary encUnary) encBits (fun (x : ℕ × ℕ) => x.1 + x.2) fun (x : ℕ × ℕ) => x.1 + x.2

Repeated halving with emission. From (n, m) in unary, round i < m emits emit (n / 2 ^ i) and the last value n / 2 ^ m is finished by finish, within time and space O(n + m) when emit and finish are linear in the value: the rounds cost n + n / 2 + ⋯ ≤ 2 n (Nat.sum_div_two_pow_le).

theorem Turing.MultiTapeTM.ComputableInO.unaryToNat : ComputableInO (fun (n : ℕ) => n) encUnary encNat (fun (n : ℕ) => n) fun (n : ℕ) => n

From unary to binary, by repeated halving, within linear time and space. Round i halves the counter n / 2 ^ i and emits its parity while it is positive (Nat.flatten_map_range_halfBit), so the rounds cost O(n) in total.

theorem Turing.MultiTapeTM.ComputableInO.lengthNat : ComputableInO (fun (l : List Bool) => l.length) encBits encNat (fun (l : List Bool) => l.length) fun (l : List Bool) => l.length

The length of a bit word in binary, within linear time and space: the word is measured in unary and converted by Turing.MultiTapeTM.ComputableInO.unaryToNat.

theorem Turing.MultiTapeTM.ComputableInO.unaryLe : ComputableInO (fun (p : ℕ × ℕ) => decide (p.1 ≤ p.2)) (encPair encUnary encUnary) encBool (fun (p : ℕ × ℕ) => (((encPair encUnary encUnary) p).length + 1) ^ 2) fun (p : ℕ × ℕ) => ((encPair encUnary encUnary) p).length + 1

The comparison of unary numbers, by counting down, within quadratic time and linear space.

theorem Turing.MultiTapeTM.ComputableInO.natToUnary : ComputableInO (fun (n : ℕ) => n) encNat encUnary (fun (n : ℕ) => n) fun (n : ℕ) => n

From binary to unary, within linear time and space. The digits are read least significant first while a unary place value 2 ^ i doubles, and the place value is emitted at every digit one. Round i costs O(2 ^ i), so the rounds cost O(n + 1) in total.