Polynomial-time numbers and tests — loops

The facts behind the loop rules of Complexitylib.Classes.P.Unary: a loop on a number, run as a loop on strings that carry the input alongside the number; the maximum of Complexitylib.Classes.P.Range as a Finset.sup; and the first index at which a test passes as a count.

Contents

• unaryLoopStep, unaryLoopStep_iterate — one round of a loop on a number, and what the rounds compute
• unaryFn_iterate_internal — the loop is polynomial-time while its values stay below a polynomial-time bound
• maxOver_eq_sup — the maximum over a range is a Finset.sup
• findIdx_range_eq_card — the first index at which a test passes counts the indices before which it never passes

A loop on a number

def Complexity.unaryLoopStep (s : List Bool → ℕ → ℕ) (st : List Bool) : List Bool

One round of the loop that updates a number x by x ↦ s z x, on pair (1^x) z. The input z rides along, so that the update can read it.

Equations

• Complexity.unaryLoopStep s st = Complexity.pair (List.replicate (s (Complexity.pairSnd st) (Complexity.pairFst st).length) true) (Complexity.pairSnd st)

theorem Complexity.unaryLoopStep_iterate (s : List Bool → ℕ → ℕ) (z : List Bool) (x j : ℕ) : (unaryLoopStep s)^[j] (pair (List.replicate x true) z) = pair (List.replicate ((s z)^[j] x) true) z

j rounds of the loop apply the update j times.

theorem Complexity.unaryFn_iterate_internal {s : List Bool → ℕ → ℕ} {a k B : List Bool → ℕ} (hs : UnaryFn fun (w : List Bool) => s (pairFst w) (pairSnd w).length) (ha : UnaryFn a) (hk : UnaryFn k) (hB : UnaryFn B) (hbound : ∀ (z : List Bool), ∀ j ≤ k z, (s z)^[j] (a z) ≤ B z) : UnaryFn fun (z : List Bool) => (s z)^[k z] (a z)

A loop on a number is polynomial-time while its values stay below a polynomial-time bound. The update reads pair z (1^x).

The maximum

theorem Complexity.maxOver_eq_sup (f : List Bool → List Bool) (z : List Bool) (n : ℕ) : maxOver f z n = (Finset.range n).sup fun (i : ℕ) => (f (pair z (List.replicate i true))).length

The maximum over a range, as a Finset.sup.

The first index

theorem Complexity.findIdx_range_eq_card (q : ℕ → Prop) [DecidablePred q] (n : ℕ) : List.findIdx (fun (i : ℕ) => decide (q i)) (List.range n) = {j ∈ Finset.range n | (Finset.filter q (Finset.range (j + 1))).card = 0}.card

The first index at which a test passes is a count: the number of indices j such that the test fails at every index up to j.