Polynomial-time loops — proof internals

The helper facts behind Complexitylib.Classes.P.Iterate. The two machines are Cobham's: Cobham.iterate_mem_FP runs a step under a width clamp, and Cobham.recFoldClamp_mem_FP runs a fold with every intermediate value truncated. What is proved here is that the clamps never fire under the hypotheses the surface statements ask for, and how to feed a fold with an arbitrary workspace and an arbitrary string to fold over.

Contents

• iterate_length_le_of_step_le — per-step growth adds up along an orbit
• recFoldClamp_eq_of_eqns — a clamped fold computes any function obeying the fold's equations, as long as that function's values on the suffixes fit
• foldUnpack — the step argument the fold hands over, with a workspace that also carries the input, rewritten to the workspace the caller asked for
• recFold_mem_FP_of_bound_internal — the fold with a polynomially short state

Iterating a step that grows by a bounded amount

theorem Complexity.iterate_length_le_of_step_le {F : List Bool → List Bool} {x : List Bool} {N c : ℕ} (hstep : ∀ n < N, (F^[n + 1] x).length ≤ (F^[n] x).length + c) (m : ℕ) : m ≤ N → (F^[m] x).length ≤ x.length + c * m

If each of the first N steps adds at most c bits, then after m ≤ N steps the state is at most c * m bits longer than the start.

Folds whose values stay short

theorem Complexity.recFoldClamp_eq_of_eqns {A B : List Bool → List Bool} {bound : ℕ} {e W : List Bool} {f : List Bool → List Bool} (s : List Bool) (hnil : f [] = e) (hfalse : ∀ (t : List Bool), f (false :: t) = A (pair (pair W (f t)) t)) (htrue : ∀ (t : List Bool), f (true :: t) = B (pair (pair W (f t)) t)) (hle : ∀ (t : List Bool), t <:+ s → (f t).length ≤ bound) : Cobham.recFoldClamp A B bound e W s = f s

A clamped fold computes its specification. If f obeys the equations of the fold of A (on a false bit) and B (on a true bit) from e with workspace W, and f is at most bound bits long on every suffix of s, then the fold clamped to bound bits computes f s: the truncation never fires.

def Complexity.foldUnpack (y : List Bool) : List Bool

The fold of recFold_mem_FP_of_bound_internal runs with the workspace pair W z, so that the start can read the input z. Each step first rewrites its argument pair (pair (pair W z) acc) t to pair (pair W acc) t, the argument the caller's step expects.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.foldUnpack_pair (W z acc t : List Bool) : foldUnpack (pair (pair (pair W z) acc) t) = pair (pair W acc) t

theorem Complexity.foldUnpack_mem_FP : foldUnpack ∈ FP

theorem Complexity.recFold_mem_FP_of_bound_internal {A B E w s : List Bool → List Bool} {g : List Bool → List Bool → List Bool} (hA : A ∈ FP) (hB : B ∈ FP) (hE : E ∈ FP) (hw : w ∈ FP) (hs : s ∈ FP) (hnil : ∀ (z : List Bool), g z [] = E z) (hfalse : ∀ (z t : List Bool), g z (false :: t) = A (pair (pair (w z) (g z t)) t)) (htrue : ∀ (z t : List Bool), g z (true :: t) = B (pair (pair (w z) (g z t)) t)) {bound : ℕ → ℕ} (hbound : PolyBound bound) (hle : ∀ (z t : List Bool), t <:+ s z → (g z t).length ≤ bound z.length) : (fun (z : List Bool) => g z (s z)) ∈ FP

A fold with a polynomially short state is polynomial-time. The value is Cobham's clamped fold, run on pair (pair (w z) z) (s z) with the steps precomposed with foldUnpack and a clamp polynomial in the length of that argument. The clamp never fires (recFoldClamp_eq_of_eqns), because the length of the argument is at least |z|.