Canonical binary evaluation of a fixed natural polynomial — definitions

A fixed polynomial is compiled into finitely many Horner layers. Each layer multiplies the current accumulator by the preserved input, adds one hardwired coefficient, clears the old accumulator, and swaps the two accumulator roles. The initial orientation is chosen from coefficient-list parity so the designated result tape holds the final value and the other accumulator is zero.

structure Complexity.TM.BinaryPolynomialDistinct {n : ℕ} (inputIdx resultIdx scratchIdx mulCounterIdx addCounterIdx : Fin n) : Prop

The five tape roles used by binary polynomial evaluation are pairwise distinct.

• input_ne_result : inputIdx ≠ resultIdx
• input_ne_scratch : inputIdx ≠ scratchIdx
• input_ne_mulCounter : inputIdx ≠ mulCounterIdx
• input_ne_addCounter : inputIdx ≠ addCounterIdx
• result_ne_scratch : resultIdx ≠ scratchIdx
• result_ne_mulCounter : resultIdx ≠ mulCounterIdx
• result_ne_addCounter : resultIdx ≠ addCounterIdx
• scratch_ne_mulCounter : scratchIdx ≠ mulCounterIdx
• scratch_ne_addCounter : scratchIdx ≠ addCounterIdx
• mulCounter_ne_addCounter : mulCounterIdx ≠ addCounterIdx

def Complexity.TM.binaryPolynomialCoeffs (p : Polynomial ℕ) : List ℕ

Coefficients of p, highest degree first.

Equations

• Complexity.TM.binaryPolynomialCoeffs p = (List.map p.coeff (List.range (p.natDegree + 1))).reverse

def Complexity.TM.binaryHornerFold (x : ℕ) : List ℕ → ℕ → ℕ

Horner evaluation of a highest-degree-first coefficient list.

Equations

• Complexity.TM.binaryHornerFold x [] x✝ = x✝
• Complexity.TM.binaryHornerFold x (coeff :: coeffs) x✝ = Complexity.TM.binaryHornerFold x coeffs (x✝ * x + coeff)

def Complexity.TM.binaryHornerLayerTM {n : ℕ} (inputIdx sourceIdx targetIdx mulCounterIdx addCounterIdx : Fin n) (coeff : ℕ) : TM n

One Horner layer: target := source * input + coeff, followed by clearing source to canonical zero.

Equations

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

def Complexity.TM.binaryHornerLayersTM {n : ℕ} (inputIdx sourceIdx targetIdx mulCounterIdx addCounterIdx : Fin n) : List ℕ → TM n

Compile a coefficient list into finitely many alternating Horner layers.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.TM.binaryHornerLayersTM inputIdx sourceIdx targetIdx mulCounterIdx addCounterIdx [] = Complexity.TM.binaryAddConstTM sourceIdx 0

def Complexity.TM.binaryPolynomialEvalTM {n : ℕ} (inputIdx resultIdx scratchIdx mulCounterIdx addCounterIdx : Fin n) (p : Polynomial ℕ) : TM n

Evaluate a fixed natural polynomial. Parity chooses which zero accumulator is the initial source so the designated result is final.

Equations

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

def Complexity.TM.binaryHornerLayerTime (inputValue accValue coeff : ℕ) : ℕ

Runtime of one Horner layer.

Equations

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

def Complexity.TM.binaryHornerLayersTime (inputValue : ℕ) : List ℕ → ℕ → ℕ

Runtime of a finite Horner layer list.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.TM.binaryHornerLayersTime inputValue [] x✝ = 1

def Complexity.TM.binaryPolynomialTime (p : Polynomial ℕ) (inputValue : ℕ) : ℕ

Runtime of fixed-polynomial evaluation.

Equations

• Complexity.TM.binaryPolynomialTime p inputValue = Complexity.TM.binaryHornerLayersTime inputValue (Complexity.TM.binaryPolynomialCoeffs p) 0

def Complexity.TM.binaryHornerLayerSpace (initialSpace inputValue accValue coeff : ℕ) : ℕ

Local all-prefix space bound for one Horner layer.

Equations

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

def Complexity.TM.binaryPolynomialValueCap (p : Polynomial ℕ) (inputValue : ℕ) : ℕ

Polynomial cap dominating every Horner prefix value.

Equations

• Complexity.TM.binaryPolynomialValueCap p inputValue = ((Complexity.TM.binaryPolynomialCoeffs p).sum + 1) * (inputValue + 1) ^ (Complexity.TM.binaryPolynomialCoeffs p).length

noncomputable def Complexity.TM.binaryPolynomialSpaceWidthPolynomial (p : Polynomial ℕ) : Polynomial ℕ

A natural polynomial whose value is exactly twice the Horner-prefix cap used by binaryPolynomialSpace.

Equations

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

def Complexity.TM.binaryPolynomialSpace (initialSpace : ℕ) (p : Polynomial ℕ) (inputValue : ℕ) : ℕ

Public width-based all-prefix space bound for polynomial evaluation.

Equations

• Complexity.TM.binaryPolynomialSpace initialSpace p inputValue = initialSpace + 10 * (2 * Complexity.TM.binaryPolynomialValueCap p inputValue).size + 17