Poly Mojo: Exact Polynomial Algebra, Gröbner Bases, and CAD in Pure Mojo

Community Showcase
1

Introducing Poly Mojo: Exact Polynomial Algebra, Gröbner Bases, and CAD in Pure Mojo

Hi everyone!

I’d like to introduce Poly Mojo, a pure Mojo library for exact and arbitrary-precision polynomial computation.

Poly Mojo provides dense and sparse polynomial arithmetic, GCDs, factorization, resultants, Gröbner bases, exact real and complex algebraic roots, cylindrical algebraic decomposition (CAD), and validated numerical root finding. Many operations also produce independently checkable certificates, allowing results to be verified without repeating the original computation.

Why polynomial algebra?

Polynomial algebra plays a fundamental role in computer algebra, symbolic computation, and formal mathematical reasoning.

Two particularly important algorithms are:

  • Gröbner bases, which provide systematic methods for simplifying systems of polynomial equations, eliminating variables, and establishing algebraic consequences through ideal membership. These methods are useful for reasoning over fields, including the complex numbers.
  • Cylindrical algebraic decomposition (CAD), which decomposes real space into regions where polynomial signs remain invariant, enabling exact reasoning about systems of polynomial equations and inequalities over the real numbers.

These techniques also form important building blocks for satisfiability modulo theories (SMT) solvers, particularly their nonlinear arithmetic engines, e.g Z3 incorporates Gröbner-basis simplification and CAD-based reasoning for polynomial constraints.

For example, consider deciding whether x^2+y^2\leq 1 and y\geq0.6 logically entail |x|\leq0.8. An SMT solver checks this by looking for a counterexample: it conjoins the premises with the negated goal and tests for satisfiability. Internally, this operation is usually enabled by a CAD system that systematically determines that no real solution exists, proving the implication. This capability to either prove non-linear statements or extract counterexamples is essential for formal verification, constraint solving, and program correctness.

The broader motivation is to make this kind of symbolic and validated computation available natively in Mojo, alongside numerical computing, without requiring a separate computer algebra system for every step.

A few examples

1. Basic exact polynomial arithmetic

Polynomial coefficients are supplied in ascending degree order. Here we expand (1 + x)^3 and evaluate the polynomial and its derivative at x = 3:

from poly import dense

def main() raises:
    var p = dense.power([1, 1], 3)
    print("p(3):", dense.evaluate(p, 3))
    print("p'(3):", dense.evaluate(dense.derivative(p), 3))

Output:

p(3): 64
p'(3): 48

These calculations use exact integer arithmetic.

2. Gröbner bases and verified ideal membership

Consider the polynomial system:

  • x - y = 0
  • x^2 - 1 = 0

We can use a Gröbner basis to verify that whenever these equations hold, y^2 - 1 =0 must hold as well (y^2 - 1 belongs to the ideal generated by these equations) :

from poly import sparse
from std.testing import assert_true

def main() raises:
    var f = [((1, 0), 1), ((0, 1), -1)]  # x - y
    var g = [((2, 0), 1), ((0, 0), -1)]  # x² - 1

    var basis = sparse.groebner([f.copy(), g.copy()], order="lex")
    assert_true(sparse.check_groebner(basis))

    var p = [((0, 2), 1), ((0, 0), -1)]  # y² - 1
    var witness = sparse.membership(p, basis)
    assert_true(Bool(witness))
    assert_true(sparse.check_membership(witness.value()))

    print("Ideal membership verified")

Importantly, sparse.membership returns an algebraic witness expressing the candidate polynomial as a combination of the original generators. The checker verifies that identity independently.

3. Verifying a nonlinear system with CAD

Consider the iterative update x_{n+1} = r x_n(1-x_n) and suppose 0 \le x_0 \le 1 and 0 \le r \le 4. Can we prove that every subsequent iteration remains within [0,1], regardless of the initial value or parameter?

CAD lets us establish this by searching for a counterexample, i.e. values of x and r satisfying the assumptions but producing rx(1-x)>1. Nonnegativity follows directly from the assumptions.

from poly import sparse, cad
from std.testing import assert_true

def main() raises:
    # Variables: x (axis 0), r (axis 1)
    var x = sparse.asarray([((1, 0), 1)])
    var one_minus_x = sparse.asarray([
        ((0, 0), 1), ((1, 0), -1)
    ])
    var r = sparse.asarray([((0, 1), 1)])
    var four_minus_r = sparse.asarray([
        ((0, 0), 4), ((0, 1), -1)
    ])

    # Counterexample: r*x*(1-x) > 1
    var overshoot = sparse.asarray([
        ((1, 1), 1), ((2, 1), -1), ((0, 0), -1)
    ])

    var result = cad.solve([
        cad.nonnegative(x),
        cad.nonnegative(one_minus_x),
        cad.nonnegative(r),
        cad.nonnegative(four_minus_r),
        cad.positive(overshoot),
    ])

    assert_true(cad.check(result))
    print("Counterexample exists:", result.satisfiable())
    # False — no counterexample exists

The constraints are UNSAT, meaning no counterexample exists. By induction, the interval [0,1] is invariant under arbitrarily many iterations. If we instead allow r=5, a counterexample exists: x=0.5 produces x_{n+1}=1.25.

This illustrates how CAD can be used to establish universal mathematical guarantees over continuous ranges of inputs, which is much more satisfying than testing individual cases.

Other capabilities

Beyond these examples, Poly Mojo supports:

  • Exact arithmetic over integers, rationals, finite fields, Gaussian rationals, and real and complex algebraic numbers.
  • Univariate and multivariate operations, including factorization, resultants, interpolation, rational functions, formal power series, and alternative polynomial bases.
  • Root finding, with exact algebraic root isolation and certified numerical enclosures for real and complex roots.
  • Independently checkable certificates for algebraic identities, roots, Gröbner bases, and CAD computations.
  • Streaming interfaces for processing large polynomial and certificate data incrementally, alongside configurable computational work limits.

Benchmarks

Poly Mojo has recently been integrated into polybench, an independent benchmark suite for multivariate polynomial arithmetic.

This allows its GCD and factorization implementations to be benchmarked alongside established systems such as FLINT, Singular, Mathematica, and Symbolica.

The integration includes both ordinary and certificate-producing modes, with separate measurements available for computation and certificate verification.

Going forward, I plan to add Poly Mojo to additional independent benchmark suites to provide broader, reproducible performance comparisons and identify opportunities for optimization.

Installation

Poly Mojo 1.0.2 targets Mojo 1.2.0 and supports Linux (x86-64 and ARM64) and macOS on Apple silicon.

With Pixi installed, you can set up a project:

pixi init poly-demo \
  --channel https://conda.modular.com/max \
  --channel https://repo.prefix.dev/modular-community \
  --channel conda-forge

cd poly-demo
pixi add "poly_mojo==1.0.2"

The package provides the poly and polynomials modules and includes the matching APN Mojo dependency. Alternatively, the library can be built from source.

Links & Feedback

3 Likes