Polynomial lengths inside the algebra

A computation in Cobham's algebra measures sizes by string lengths, so a polynomial time or space bound has to be available as a string of that length. smash multiplies lengths and concatenation adds them, so Horner's scheme builds, for any polynomial with natural coefficients, a member of the algebra whose output has exactly the polynomial's value as its length.

Main definitions

• Cobham.hornerEval — Horner evaluation of a coefficient list
• Cobham.lenOfCoeffs — the string realizing that value as its length
• Cobham.polyLen — the same for a Polynomial ℕ

Main results

• Cobham.lenOfCoeffs_mem, Cobham.polyLen_mem — both are in the algebra
• Cobham.polyLen_length — polyLen q s has length exactly q.eval |s|

def Complexity.Cobham.hornerEval : List ℕ → ℕ → ℕ

Horner evaluation of a coefficient list, lowest coefficient first.

Equations

• Complexity.Cobham.hornerEval [] x✝ = 0
• Complexity.Cobham.hornerEval (a :: as) x✝ = a + x✝ * Complexity.Cobham.hornerEval as x✝

def Complexity.Cobham.lenOfCoeffs : List ℕ → List Bool → List Bool

The string whose length is the Horner value of the coefficient list at |s|: constants contribute blocks of that many bits, and each multiplication by |s| is one smash.

Equations

• Complexity.Cobham.lenOfCoeffs [] x✝ = []
• Complexity.Cobham.lenOfCoeffs (a :: as) x✝ = List.replicate a false ++ Complexity.smash x✝ (Complexity.Cobham.lenOfCoeffs as x✝)

@[simp]

theorem Complexity.Cobham.lenOfCoeffs_length (as : List ℕ) (s : List Bool) : (lenOfCoeffs as s).length = hornerEval as s.length

theorem Complexity.Cobham.lenOfCoeffs_mem {n : ℕ} (as : List ℕ) {g : (Fin n → List Bool) → List Bool} (hg : Cobham g) : Cobham fun (v : Fin n → List Bool) => lenOfCoeffs as (g v)

The Horner string is in the algebra.

theorem Complexity.Cobham.hornerEval_map_range (f : ℕ → ℕ) (d n : ℕ) : hornerEval (List.map f (List.range d)) n = ∑ i ∈ Finset.range d, f i * n ^ i

Horner evaluation of a truncated coefficient sequence is the truncated power sum.

noncomputable def Complexity.Cobham.polyLen (q : Polynomial ℕ) (s : List Bool) : List Bool

The string realizing a polynomial's value as its length.

Equations

• Complexity.Cobham.polyLen q s = Complexity.Cobham.lenOfCoeffs (List.map q.coeff (List.range (q.natDegree + 1))) s

@[simp]

theorem Complexity.Cobham.polyLen_length (q : Polynomial ℕ) (s : List Bool) : (polyLen q s).length = Polynomial.eval s.length q

The polynomial's value is the string's length.

theorem Complexity.Cobham.polyLen_mem {n : ℕ} (q : Polynomial ℕ) {g : (Fin n → List Bool) → List Bool} (hg : Cobham g) : Cobham fun (v : Fin n → List Bool) => polyLen q (g v)

The polynomial-length string is in the algebra.