polynomial.cppm File Reference

The monoid algebra R[M]: polynomials as finitely supported nets over the monomials, and the normal form of a rig's, ring's or field's terms. More...

#include <algorithm>
#include <array>
#include <bit>
#include <compare>
#include <concepts>
#include <cstddef>
#include <functional>
#include <limits>
#include <optional>
#include <stdexcept>
#include <string>
#include <type_traits>
#include <utility>
#include <vector>
import dedekind.algebra:free;
import dedekind.sequences;
import dedekind.order;
import dedekind.sets;
import dedekind.category;

Include dependency graph for polynomial.cppm:

Classes
struct	dedekind::algebra::Monomial< N >
	A monomial in N variables: its exponents, one per slot (π is the slot 0; π_1, π_2, π_3 the slots 1, 2, 3). The free commutative monoid on N generators, written multiplicatively (the exponents add, as natural numbers: leaving the word raises), and a chain under the graded lexicographic order: by total degree, then by exponents. More...
struct	dedekind::algebra::detail_polynomial::ByMonomial
	The support's order: by monomial. More...
class	dedekind::algebra::Polynomial< R, M >
	The monoid algebra R[M]: a finitely supported function from the monomials to the coefficients, stored as its support sorted along the monomials' chain, no coefficient zero. A net (Domain the monomials, Codomain the coefficients, p(m) the coefficient of m), a commutative rig over a commutative rig, a ring over a ring (- where R has additive inverses). More...
struct	dedekind::algebra::Poly< C, N >
	The polynomial reading of a term on the carrier C, an algebra for cata: a projection is its variable, a constant a coefficient, + - * the polynomial's where the carrier admits them, a division by a nonzero constant on a field the multiplication by its inverse. Any other node (//, %, a division by a term, an applied arrow, a conditional) has no free algebra catalogued here and is refused. Expanding into polynomials uses commutativity of * and its distributivity over +, so the carrier must be a certified commutative rig. More...
struct	dedekind::algebra::detail_canonical::AtomAt< P, K, Lift >
	The dispatch of an atom's normal form to its sort: a comparison of two constants decided in it, any other atom in the polynomials over a carrier of the points where + and · are total on it, and on a carrier without them (𝔹, K₃) kept as written: equal forms still cut out equal sets, and different ones decide nothing. More...
struct	dedekind::category::SpeciesTraits< dedekind::algebra::Monomial< N > >
struct	dedekind::category::unit_trait< dedekind::algebra::Monomial< N >, std::multiplies< dedekind::algebra::Monomial< N > > >
struct	dedekind::category::is_exact_total< dedekind::algebra::Monomial< N >, std::multiplies< dedekind::algebra::Monomial< N > > >
struct	dedekind::category::free_algebra_base< dedekind::algebra::Polynomial< R, M > >
struct	dedekind::category::unit_trait< dedekind::algebra::Polynomial< R, M >, std::plus< dedekind::algebra::Polynomial< R, M > > >
struct	dedekind::category::unit_trait< dedekind::algebra::Polynomial< R, M >, std::multiplies< dedekind::algebra::Polynomial< R, M > > >
struct	dedekind::category::is_periodic< dedekind::algebra::Polynomial< R, M >, std::plus< dedekind::algebra::Polynomial< R, M > > >
struct	dedekind::category::is_periodic< dedekind::algebra::Polynomial< R, M >, std::multiplies< dedekind::algebra::Polynomial< R, M > > >

Namespaces
namespace	dedekind::category

Typedefs
using	dedekind::algebra::M4 = Monomial<4>
using	dedekind::algebra::PolyWord = Polynomial<unsigned int, M4>

Functions
template<typename C, typename T>
constexpr auto	dedekind::algebra::canonical (const T &t)
	The normal form of the term t in the polynomials over C: the fold of Poly<C>. Two terms are equal in the free algebra iff their normal forms are.
template<typename K, typename C, std::size_t N, typename Lift>
dedekind::sets::Term< K >	dedekind::algebra::as_term (const Polynomial< C, Monomial< N > > &p, const Lift &lift)
	A polynomial written back as a term of the grammar: its terms from the leading monomial down, each the coefficient times the product of its variables (a coefficient 1 omitted), summed; the zero polynomial is the constant 0.
template<typename C>
constexpr C	dedekind::algebra::unit_normaliser (const C &)
	A unit u of the carrier with u·c the chosen representative of c's associates (the elements c times a unit): the hook the normal form of an equation divides by. 1 by default, nothing divided out; a carrier with more units states its own overload, found by ADL.
template<std::unsigned_integral W> requires (!std::same_as<W, bool>) && (sizeof(W) >= sizeof(unsigned))
constexpr W	dedekind::algebra::unit_normaliser (const W &c)
	On a word, ℤ/2ⁿ: c = 2ᵏ·o with o odd, and the odd elements are the units, so o⁻¹ (Newton's iteration, 2-adic: each step doubles the correct low bits) makes u·c = 2ᵏ. 0 has no unit part.
template<typename C, std::size_t N, typename K, typename Lift>
dedekind::sets::Pred< K >	dedekind::algebra::canonical_atom_in (const dedekind::sets::Pred< K > &p, const Lift &lift)
	The normal form of a comparison atom read in the sort C: an equation or its negation a ⋈ b on a ring moves to a - b ⋈ 0 with the difference a polynomial, the unit part of its leading coefficient divided out (monic on a field; unit_normaliser elsewhere), so an equation and its multiple by any unit meet; any other atom has its sides normalised and its comparison kept.
template<typename C, typename K, typename Lift>
dedekind::sets::Pred< K >	dedekind::algebra::canonical_atom (const dedekind::sets::Pred< K > &p, const Lift &lift)
	An atom's normal form with as many variables as it reads: the monomials' width chosen by the atom's highest slot (π and up to π_7, or up to π_31, the width of the slot mask). A slot past the mask is refused; a sparse monomial would lift the bound (#1023).
template<typename P, typename K, typename Lift>
dedekind::sets::Pred< K >	dedekind::algebra::detail_canonical::canonical_lifted (const dedekind::sets::Pred< K > &p, const Lift &lift, const P &rep)
	The normal form of a predicate without conditionals: atom by atom, the bounds ⊤ / ⊥ folded into the connectives (the lattice's units and absorbers), the operands of each connective sorted and kept once.
template<typename P, typename K, typename Lift>
void	dedekind::algebra::detail_canonical::operands_of (const dedekind::sets::Pred< K > &p, typename dedekind::sets::Pred< K >::Kind k, const Lift &lift, const P &rep, std::vector< dedekind::sets::Pred< K > > &out)
	The operands of a chain of the connective k, each in normal form; a normal form that is itself a chain of k contributes its operands (associativity).
template<typename P, typename K, typename Lift>
dedekind::sets::Pred< K >	dedekind::algebra::canonical (const dedekind::sets::Pred< K > &p, const Lift &lift, const P &rep=P{})
	The normal form of a predicate at points of P: its conditionals lifted out of the atoms (lift_conditionals, so an applied set ap(S, t) reads as S's predicate at t), then atom by atom, each atom in its operands' sort (a point of one carrier has one; a pair of two carriers two, each axis its own), a decided atom ⊤ or ⊥ and folded into its connective. Equal normal forms cut out equal sets; different ones need not (πᵖ = π everywhere on 𝔽ₚ). An atom outside the catalogue is refused (not_admitted).

Variables
template<std::size_t N>
constexpr bool	dedekind::category::is_reflexive_v< dedekind::algebra::Monomial< N >, std::less_equal<> > = true
template<std::size_t N>
constexpr bool	dedekind::category::is_transitive_v< dedekind::algebra::Monomial< N >, std::less_equal<> > = true
template<std::size_t N>
constexpr bool	dedekind::category::is_antisymmetric_v< dedekind::algebra::Monomial< N >, std::less_equal<> >
template<std::size_t N>
constexpr bool	dedekind::category::is_connex_v< dedekind::algebra::Monomial< N >, std::less_equal<> > = true
template<std::size_t N>
constexpr bool	dedekind::category::is_associative_v< dedekind::algebra::Monomial< N >, std::multiplies< dedekind::algebra::Monomial< N > > > = true
template<std::size_t N>
constexpr bool	dedekind::category::is_commutative_v< dedekind::algebra::Monomial< N >, std::multiplies< dedekind::algebra::Monomial< N > > > = true
constexpr Projection< 0 >	dedekind::algebra::π
	The unary projection, the identity: the variable of a comprehension over one carrier.
constexpr Projection< 1 >	dedekind::algebra::π_1
	The projections of a pair (and the first three of a tuple).
constexpr Projection< 2 >	dedekind::algebra::π_2

Detailed Description

The monoid algebra R[M]: polynomials as finitely supported nets over the monomials, and the normal form of a rig's, ring's or field's terms.

@partition :polynomial

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

polynomial__The_Monoid_Algebra

A polynomial over a commutative rig R in the variables π, π_1, π_2, π_3 is a finitely supported function from the monomials (the free commutative monoid on the variables, Monomial<N>) to R: the monoid algebra R[M] (Lang, Algebra, §II.3). Addition is pointwise; multiplication is the convolution Σ_{m·m' = n} a_m b_{m'}, the Cauchy product in one variable. A formal power series R[[M]] is any function M → R; a polynomial is one with finite support, and it is the support that is stored.

In the DSL's grammar a polynomial is a net (sequences::IsNet), an arrow from a directed set: the monomials ordered by total degree and then lexicographically (the graded lexicographic order; Cox, Little, O'Shea, §2.2), a chain compatible with multiplication, along which the support is stored sorted. The arrow's graph restricted to the support is a finite functional graph: the finite function the normal form is compared and printed by.

polynomial__The_Normal_Form_Of_Terms

The reading Poly<C> is an algebra for cata over the term grammar (sets:terms, terms__Signature_And_Free_Algebra): a projection is its variable, a constant a coefficient, + - * the polynomial's, and a division by a nonzero constant on a field a multiplication by its inverse. Every operator must be admitted on the carrier (admits: the laws decide the syntax), and //, % and a division by a term have no free algebra here: they are refused, never rewritten. canonical<C>(t) is the fold; two terms are equal in the free algebra iff their normal forms are equal, which is equality of two finite functions, monomial to coefficient.

A set expression is normalised through its predicate, atom by atom (canonical(pred, lift)): an equation a = b on a ring becomes a - b = 0 with the difference a polynomial, the unit part of its leading coefficient divided out (monic on a field), written back as a term (as_term). Equal normal forms cut out equal sets; the converse fails (the next paragraph), so a comparison of sets by normal form may answer only "equal" or "not decided".

Over a finite carrier that is not equality of the polynomial functions: on 𝔽ₚ, πᵖ and π agree at every point, and on ℤ/2⁶⁴ so do 2⁶³·π·(π+1) and 0. That quotient (by the vanishing ideal) is a further reading, not this one.

The exponents are natural numbers, held in machine words: a product whose exponent would leave the word raises std::overflow_error rather than wrap. A wrapping coefficient is the carrier's own arithmetic; a wrapping exponent would change the term (π^(2³²−1)·π is not the constant 1), so the monoid is ℕᴺ, certified total on the exact path with the overflow a tripwire, the posture of Rational's out-of-memory sentinel.

Wikipedia: Monoid ring, Polynomial ring, Monomial order

Note

"Die ganzen Zahlen hat der liebe Gott gemacht, alles andere ist Menschenwerk." [Trans: "God made the integers; all else is the work of man."] Leopold Kronecker, as reported by Heinrich Weber, "Leopold Kronecker", Jahresbericht der DMV 2 (1893), p. 19.

Typedef Documentation

M4

using dedekind::algebra::M4 = Monomial<4>

polynomial__Formal_Verification

Function Documentation

as_term()

template<typename K, typename C, std::size_t N, typename Lift>

dedekind::sets::Term< K > dedekind::algebra::as_term ( const Polynomial< C, Monomial< N > > & p, const Lift & lift )

export

A polynomial written back as a term of the grammar: its terms from the leading monomial down, each the coefficient times the product of its variables (a coefficient 1 omitted), summed; the zero polynomial is the constant 0.

Template Parameters

K	the constants' type.

Parameters

p	the polynomial.
lift	a coefficient into a constant.

canonical() [1/2]

template<typename P, typename K, typename Lift>

dedekind::sets::Pred< K > dedekind::algebra::canonical ( const dedekind::sets::Pred< K > & p, const Lift & lift, const P & rep = P{} )

export

The normal form of a predicate at points of P: its conditionals lifted out of the atoms (lift_conditionals, so an applied set ap(S, t) reads as S's predicate at t), then atom by atom, each atom in its operands' sort (a point of one carrier has one; a pair of two carriers two, each axis its own), a decided atom ⊤ or ⊥ and folded into its connective. Equal normal forms cut out equal sets; different ones need not (πᵖ = π everywhere on 𝔽ₚ). An atom outside the catalogue is refused (not_admitted).

Template Parameters

P	the point type.

Parameters

p	the predicate.
lift	a coefficient into a constant of the predicate's type.
rep	a point of P (a row is its own schema).

canonical() [2/2]

template<typename C, typename T>

auto dedekind::algebra::canonical ( const T & t )

constexprexport

The normal form of the term t in the polynomials over C: the fold of Poly<C>. Two terms are equal in the free algebra iff their normal forms are.

Template Parameters

C	the carrier.

Parameters

t	a typed term, or one built at run time.

canonical_atom()

template<typename C, typename K, typename Lift>

dedekind::sets::Pred< K > dedekind::algebra::canonical_atom	(	const dedekind::sets::Pred< K > &	p,
		const Lift &	lift )

An atom's normal form with as many variables as it reads: the monomials' width chosen by the atom's highest slot (π and up to π_7, or up to π_31, the width of the slot mask). A slot past the mask is refused; a sparse monomial would lift the bound (#1023).

Template Parameters

C

the sort.

canonical_atom_in()

template<typename C, std::size_t N, typename K, typename Lift>

dedekind::sets::Pred< K > dedekind::algebra::canonical_atom_in	(	const dedekind::sets::Pred< K > &	p,
		const Lift &	lift )

The normal form of a comparison atom read in the sort C: an equation or its negation a ⋈ b on a ring moves to a - b ⋈ 0 with the difference a polynomial, the unit part of its leading coefficient divided out (monic on a field; unit_normaliser elsewhere), so an equation and its multiple by any unit meet; any other atom has its sides normalised and its comparison kept.

Template Parameters

C

the sort.

operands_of()

template<typename P, typename K, typename Lift>

void dedekind::algebra::detail_canonical::operands_of	(	const dedekind::sets::Pred< K > &	p,
		typename dedekind::sets::Pred< K >::Kind	k,
		const Lift &	lift,
		const P &	rep,
		std::vector< dedekind::sets::Pred< K > > &	out )

The operands of a chain of the connective k, each in normal form; a normal form that is itself a chain of k contributes its operands (associativity).

Parameters

out	the operands, appended.

unit_normaliser() [1/2]

template<typename C>

C dedekind::algebra::unit_normaliser ( const C & )

constexprexport

A unit u of the carrier with u·c the chosen representative of c's associates (the elements c times a unit): the hook the normal form of an equation divides by. 1 by default, nothing divided out; a carrier with more units states its own overload, found by ADL.

Parameters

c	the leading coefficient.

unit_normaliser() [2/2]

template<std::unsigned_integral W>
requires (!std::same_as<W, bool>) && (sizeof(W) >= sizeof(unsigned))

W dedekind::algebra::unit_normaliser ( const W & c )

constexprexport

On a word, ℤ/2ⁿ: c = 2ᵏ·o with o odd, and the odd elements are the units, so o⁻¹ (Newton's iteration, 2-adic: each step doubles the correct low bits) makes u·c = 2ᵏ. 0 has no unit part.

Parameters

c	the leading coefficient.