Skip to content

Computation models for polynomials and finitely supported functions

Jump to bottom
Eric Wieser edited this page Sep 21, 2023 · 22 revisions

Today, MvPolynomial and Polynomial are both implemented in terms of Finsupp. As a result, all of:

  • Finsupp
  • Polynomial
  • MvPolynomial
  • Basis

are largely noncomputable.

Possible designs for a more computable Finsupp

Possible designs include:

  • De-classicalized Finsupp: promote any Classical.decEq terms to typeclass parameters. As a reminder, this stores the exact Finset of non-zero values.
  • DFinsupp: we already have a working model here. This stores a Multiset that is a superset of all the non-zero values.
  • DFinsupp': A version of DFinsupp that stores a Finset that is a superset.
  • Quotient of generators: an approach similar to FreeAlgebra. This could represent 1 + 3x^2 as add (monomial 0 1) (monomial 2 3) and quotient by algebraic rules.

The following table outlines the computational behavior that ι →₀ R could have under these strategies.

Operation De-classicalized Finsupp DFinsupp DFinsupp' Quotient of inductive type
f i (aka p.coeff i) ✓ ✓ ✓ DecidableEq ι
single i r (aka X) DecidableEq ι DecidableEq R DecidableEq ι DecidableEq ι ✓
support ✓ DecidableEq ι DecidableEq R DecidableEq R DecidableEq ι DecidableEq R
+ DecidableEq ι DecidableEq R ✓ DecidableEq ι ✓

Recall that Polynomials are ℕ →₀ R with ι = ℕ, so DecidableEq ι is not at all a burden here. MvPolynomials are (σ →₀ ℕ) →₀ R with ι = σ →₀ ℕ, so DecidableEq ι amounts to DecidableEq σ.

DFinsupp has the nice property of matching the computation model of Pi (via Pi.single, Function.support, and the usual arithmetic). Algorithmically though it is inefficient as the preSupport set grows with each operation.

Alternatives to computational models

TODO: describe norm_num-style computation.

List of prior Zulip discussions

List of relevant PRS

Clone this wiki locally