A binary counter from a unary index

A polynomial-time loop receives its counter in unary, since that is the form a loop bound takes. This module turns such an index into fixed-width binary: the width-preserving counter of SavitchBits is incremented that many times, starting from all zeros.

Nothing here is arithmetic on the index. bumpBits is the width-preserving increment already proved polynomial-time for Savitch's theorem, and iterating a polynomial-time step a polynomial number of times is iterate_mem_FP.

Main definitions

• Complexity.coinStr — the counter after that many increments

Main results

• Complexity.coinStr_eq — below the wrap-around, it is bitsOfLenLE
• Complexity.coinStr_mem_FP — in polynomial time, for any index

theorem Complexity.zeroBlockFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => List.replicate (a z).length false) ∈ FP

A block of zeros as wide as a computed string.

theorem Complexity.bumpBits_mem_FP : bumpBits ∈ FP

theorem Complexity.length_bumpBits_iterate (n : ℕ) (w : List Bool) : (bumpBits^[n] w).length = w.length

def Complexity.coinStr (t c : ℕ) : List Bool

The width-t counter after c increments. Total: past 2 ^ t it wraps, which never happens where it is used but keeps the function unconditional.

Equations

• Complexity.coinStr t c = Complexity.bumpBits^[c] (List.replicate t false)

theorem Complexity.coinStr_eq {t c : ℕ} (h : c < 2 ^ t) : coinStr t c = bitsOfLenLE t c

theorem Complexity.coinStr_mem_FP {t c : List Bool → ℕ} (ht : (fun (z : List Bool) => List.replicate (t z) true) ∈ FP) (hc : (fun (z : List Bool) => List.replicate (c z) true) ∈ FP) : (fun (z : List Bool) => coinStr (t z) (c z)) ∈ FP

The counter value in polynomial time. With the width and the index both supplied in unary, the counter is polynomial-time computable — with no bound on the index, so that the function is total where a loop guard has not yet been applied.