The largest of polynomially many values

An algorithm reading a formula has to know how many variables it mentions, which is the largest index any literal names. More generally: given a rule that computes a value for each index, take the largest over a bounded range.

Values are carried in unary, so "largest" is "longest", and the comparison is the length test already in the toolkit.

Main definitions

• Complexity.maxStep — one step of the running maximum
• Complexity.maxOver — the value it computes

Main results

• Complexity.maxStep_iterate — the loop takes the maximum
• Complexity.maxFn_mem_FP, Complexity.maxFn_eq — the packaged loop
• Complexity.le_maxOver, Complexity.maxOver_attained — it is the maximum

def Complexity.maxOver (f : List Bool → List Bool) (z : List Bool) : ℕ → ℕ

The largest of the first n values, as a length.

Equations

• Complexity.maxOver f z 0 = 0
• Complexity.maxOver f z n.succ = max (Complexity.maxOver f z n) (f (Complexity.pair z (List.replicate n true))).length

def Complexity.maxStep (f : List Bool → List Bool) (st : List Bool) : List Bool

One step of the running maximum. The state is pair (pair largest counter) input.

Equations

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

theorem Complexity.maxStep_mem_FP {f : List Bool → List Bool} (hf : f ∈ FP) : maxStep f ∈ FP

theorem Complexity.maxStep_iterate (f : List Bool → List Bool) (z : List Bool) (n : ℕ) : ∃ (M : List Bool), (maxStep f)^[n] (pair (pair [] []) z) = pair (pair M (List.replicate n true)) z ∧ M.length = maxOver f z n

The loop takes the maximum.

theorem Complexity.le_maxOver {f : List Bool → List Bool} {z : List Bool} (n i : ℕ) : i < n → (f (pair z (List.replicate i true))).length ≤ maxOver f z n

Every value is at most the maximum.

theorem Complexity.maxOver_attained {f : List Bool → List Bool} {z : List Bool} (n : ℕ) : 0 < n → ∃ i < n, (f (pair z (List.replicate i true))).length = maxOver f z n

The maximum is attained, when there is anything to maximise over.

theorem Complexity.maxOver_le {f : List Bool → List Bool} {z : List Bool} {B : ℕ} (n : ℕ) : (∀ i < n, (f (pair z (List.replicate i true))).length ≤ B) → maxOver f z n ≤ B

noncomputable def Complexity.maxFn (f : List Bool → List Bool) (w : List Bool) : List Bool

The packaged loop, on pair (unary count) input.

Equations

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

theorem Complexity.maxFn_mem_FP {f : List Bool → List Bool} (hf : f ∈ FP) : maxFn f ∈ FP

theorem Complexity.maxFn_eq (f : List Bool → List Bool) {n : ℕ} {z : List Bool} : (maxFn f (pair (List.replicate n true) z)).length = maxOver f z n