8.2. Multiplication plans🔗
Every operation in this chapter takes a Hex.DensePoly.MulPlan: a
record of three multiplication functions together with proofs that they
compute the product of HexPoly.
🔗structure
A proof-carrying implementation of full, square, and clipped dense
polynomial multiplication. slice lo len a b stores coefficients beginning
at degree lo, shifted down to degree zero.
Fields
mul_eq : ∀ (a b : Hex.DensePoly R), self.mul a b = a * b
Full multiplication agrees with the reference product.
square_eq : ∀ (a : Hex.DensePoly R), self.square a = a * a
Squaring agrees with the reference product.
coeff_slice : ∀ (lo len : ℕ) (a b : Hex.DensePoly R) (i : ℕ),
(self.slice lo len a b).coeff i = if i < len then (a * b).coeff (lo + i) else 0
The slice contains exactly the selected product coefficients.
A plan is an ordinary value passed as an argument, not a typeclass instance.
The integer and prime-field polynomials ZPoly and FpPoly p of
HexPolyZ and HexPolyFp are
DensePoly Int and DensePoly (ZMod64 p), and those libraries provide their
own plans, Hex.ZPoly.fastPlan and Hex.FpPoly.fastPlan. For
full products these choose, by the sizes of the factors, between the
schoolbook method, Kronecker substitution, packed multiplication and
number-theoretic transforms; their squares and slices use Karatsuba's
method. A caller
chooses the plan at each call, and the * of DensePoly stays the schoolbook
product. HexPolyFast itself provides two plans that work over any
commutative ring: Hex.DensePoly.schoolbookPlan and
Hex.DensePoly.karatsubaPlan.
Karatsuba's method splits each factor at xᵏ, with k about half the length,
as a = a₀ + xᵏ a₁ and b = b₀ + xᵏ b₁, and computes three half-size
products a₀b₀, a₁b₁ and (a₀ + a₁)(b₀ + b₁). The middle coefficient
a₀b₁ + a₁b₀ is the third product minus the other two, so
ab = a₀b₀ + xᵏ ((a₀ + a₁)(b₀ + b₁) - a₀b₀ - a₁b₁) + x²ᵏ a₁b₁.
Applied recursively this takes O(n^log₂3) ≈ O(n^1.585) coefficient
operations for factors with n coefficients. The subtraction is why plans
need a commutative ring, while HexPoly's product needs only addition and
multiplication. karatsubaPlan cutoff uses the schoolbook method when a
factor has at most cutoff coefficients. When one factor is much longer than the other, it cuts
the longer one into blocks of the shorter one's length and adds up the block
products, so the cost is the number of blocks times the cost of one balanced
product. Squaring has its own recursion, which needs the three squares a₀²,
a₁² and (a₀ + a₁)².
The central trinomial coefficients count the ways to take n steps of -1,
0 or +1 and return to 0. The nth is the coefficient of xⁿ in
(1 + x + x²)ⁿ. Squaring six times computes the 64th:
def trinomial : DensePoly Int := #p[1, 1, 1]
def power64 : DensePoly Int :=
(List.range 6).foldl
(fun p _ => squareWith (karatsubaPlan 32) p)
trinomial
(129, 209099036316263774148543463251)#eval (power64.size, power64.coeff 64)
(129, 209099036316263774148543463251)
The theorems about planned products are the proof fields of the plan:
🔗theorem
Planned multiplication has the existing dense-polynomial semantics.
🔗theorem
Planned squaring has the existing dense-polynomial semantics.
8.2.1. Parts of a product🔗
Newton iteration and the half-gcd algorithm use only some coefficients of a
product. Hex.DensePoly.mulSlice returns len consecutive
coefficients of a * b, starting at xˡᵒ, as a polynomial whose constant
term is the coefficient of xˡᵒ, and Hex.DensePoly.mulLow returns the
first len. The Karatsuba plan skips every partial product that
cannot contribute to the requested coefficients. The middle product
Hex.DensePoly.mulMiddleChecked is the slice from xⁿ⁻¹ to xᵐ⁻¹ of
a product of factors with m ≥ n coefficients, taken in either order; it is
zero if either factor is.
🔗theorem
Coefficient law for an arbitrary planned slice.
The cyclic product Hex.DensePoly.mulCyclic? computes a * b modulo
xⁿ - 1, that is, the cyclic convolution of the coefficient sequences, and
Hex.DensePoly.mulNegacyclic? computes it modulo xⁿ + 1. Both fold a
planned product, and return none for n = 0:
some #p[31, 31, 28]#eval mulCyclic? (karatsubaPlan 32) 3
(#p[1, 2, 3] : DensePoly Int) #p[4, 5, 6]
some #p[31, 31, 28]
🔗theorem
Planned cyclic multiplication is polynomial remainder modulo x^n - 1.