Skip to content

Computation models for polynomials and finitely supported functions

Jump to bottom
Eric Wieser edited this page Aug 3, 2023 · 22 revisions

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

  • Finsupp
  • Polynomial
  • MvPolynomial

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.
  • 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 outlines the computational behavior that ι →₀ R could have under these strategies

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

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.

List of prior Zulip discussions

List of relevant PRS

Clone this wiki locally