Building a Total Language for Experimental Mathematics in Rust

A termination-guaranteed programming language for experimental mathematics is achievable by combining System T-style higher-order primitive recursion with structural recursion on inductive types, implemented via the egg library for first-class e-graphs, and LALRPOP + logos for parsing in Rust. The key insight is that primitive recursion suffices for virtually all mathematical algorithms, while System T's higher-order recursors capture even Ackermann-class functions—meaning you lose almost nothing practical by abandoning Turing completeness. This report provides a complete blueprint: from termination-checking algorithms to Rust crate selection to notebook architecture.

The termination guarantee requires structural recursion plus sized types

The core challenge is ensuring all programs halt while retaining enough expressiveness for experimental mathematics. Three complementary mechanisms achieve this:

Structural recursion on inductive types forms the foundation. Every element of an inductively-defined type (natural numbers, lists, trees, polynomials) is built from constructors in finitely many steps. When recursive calls operate only on strict subterms obtained by pattern matching, termination is guaranteed—the call tree cannot descend infinitely. Agda, Coq, and Idris all use this as their primary termination criterion.

The Foetus algorithm, developed by Andreas Abel and now powering Agda's termination checker, extends structural recursion with call matrix analysis. For each function, it builds a call graph where edges are labeled with matrices showing how arguments change: < for strictly smaller, = for equal, ? for unknown. The algorithm searches for a lexicographic ordering of arguments where every recursive call cycle has at least one strictly decreasing component. This accepts Ackermann's function—which recurses on (m, A(m+1, n)) where either m decreases or it stays the same while the second argument (eventually) decreases.

Sized types offer a more modular alternative by tracking structural depth in the type system itself. A type like SNat i bounds the natural number's "size" by ordinal i, and the type system verifies that recursive calls receive arguments of strictly smaller size. This approach, developed by Hughes, Pareto, Sabry and extended by Abel and Barthe, handles non-structural recursion like division and GCD more naturally than syntactic checks.

For your language design, the recommended approach combines structural recursion as the default (covering 90%+ of use cases) with well-founded recursion for advanced algorithms. Provide escape hatches like assert_total clearly marked for experimental code where termination is believed but not proved.

Primitive recursion captures nearly all mathematical computation

Understanding what computational power you sacrifice for termination guarantees is crucial. The Meyer-Ritchie theorem provides the key insight: primitive recursive functions correspond exactly to LOOP programs—for-loops where iteration counts are fixed before execution begins. This includes:

All basic arithmetic (addition, multiplication, exponentiation, factorial, GCD), all number-theoretic functions (primality testing, nth prime, divisor functions), all standard combinatorics (binomial coefficients, Fibonacci, Catalan numbers), polynomial operations over integers and rationals, matrix arithmetic, and essentially every algorithm with a computable asymptotic runtime bound.

The Ackermann function marks the boundary—it grows faster than any primitive recursive function and cannot be expressed with simple bounded loops. However, Gödel's System T, which adds higher-order primitive recursion (recursors at all finite types), captures Ackermann and all functions provably total in Peano arithmetic. The key mechanism: partial application of iterators enables nested recursion patterns that transcend first-order primitive recursion.

What you genuinely lose by restricting to totality:

• Self-interpretation: A total language cannot interpret itself completely (this would allow constructing non-terminating programs)
• Unbounded search: Cannot express "find the smallest n such that P(n)" when P might never be true
• General program analysis: Cannot decide termination for arbitrary code

For experimental mathematics, these limitations rarely matter. The Grzegorczyk hierarchy shows that level E³ (elementary functions, closed under exponential towers) already captures all "practical" algorithms. Most mathematical computation lives at E² or below—polynomial time.

E-graphs and equality saturation belong in your core calculus

The egg library (POPL 2021 Distinguished Paper) provides production-ready e-graphs for Rust. An e-graph maintains equivalence classes of terms under a congruence relation, enabling equality saturation: applying rewrite rules non-destructively until reaching a fixed point, then extracting the optimal term.

The core architecture centers on three types: EGraph<L, N> holds the data structure, generic over your Language (AST node type) and Analysis (domain-specific data per e-class). Define your expression language using the define_language! macro:

define_language! {
    enum MathExpr {
        Num(i64),
        Rational(num_rational::Ratio<i64>),
        "+" = Add([Id; 2]),
        "*" = Mul([Id; 2]),
        "/" = Div([Id; 2]),
        "^" = Pow([Id; 2]),
        Symbol(Symbol),
    }
}

Rewrite rules use pattern variables: rewrite!("distrib"; "(* ?a (+ ?b ?c))" <=> "(+ (* ?a ?b) (* ?a ?c))"). The <=> creates bidirectional rules essential for algebraic reasoning where distribution and factoring are equally valid.

For a language with first-class e-graphs, expose saturation as an expression:

let simplified = saturate expr using [algebra_rules, trig_rules]
                 extracting by ast_size
                 with timeout 1000ms

The equality saturation algorithm iterates: (1) find all pattern matches, (2) apply rewrites adding new e-nodes, (3) call rebuild() to restore invariants, (4) repeat until saturated or timeout. Egg's key innovation is deferred rebuilding—invariant restoration happens in bulk, providing 30x speedups over traditional e-graph implementations.

Termination considerations: Equality saturation may not terminate if rewrite rules generate unbounded growth. For a total language, either (a) impose timeout/size limits as language-level constructs, (b) restrict to non-expanding rules where RHS is no larger than LHS, or (c) use guided equality saturation (POPL 2024) with user-provided sketches.

E-class analyses attach domain-specific data—constant folding, symbolic bounds, type information—that propagate through the e-graph and enable conditional rewrites. This mechanism naturally represents WZ certificates: the rational function certificate R(n,k) can be computed and verified during saturation.

Type system design balances expressiveness with decidable checking

The simply-typed lambda calculus and System F both guarantee termination through the strong normalization property—every well-typed term reduces to a unique normal form. The proof uses Tait's method of logical relations: define "reducibility predicates" for each type ensuring terms terminate, then show all well-typed terms satisfy their type's predicate.

For a practical total language, layer these mechanisms:

Base layer: System F with inductive types. Polymorphic types (∀α. τ) enable generic programming over rationals, polynomials, and algebraic structures without losing termination. Inductive types with strict positivity guarantee well-foundedness—the type being defined must appear only to the right of zero function arrows in constructor arguments. This prevents Curry's paradox: without strict positivity, you could encode data Bad = MkBad (Bad → ⊥) and derive a non-terminating term.

Structural recursion via eliminators. For each inductive type, automatically generate a recursor that enforces recursive calls only on subterms. The recursor for natural numbers has type rec : (P : Nat → Type) → P 0 → ((n : Nat) → P n → P (S n)) → (n : Nat) → P n—higher-order primitive recursion that captures System T.

Well-founded recursion for escape. When structural recursion fails (quicksort, GCD, division), require explicit termination proofs via accessibility predicates:

data Acc (x : A) : Type where
  acc : ((y : A) → y < x → Acc y) → Acc x

An element is "accessible" if all smaller elements are accessible. Recursion over Acc x is structural, but the user must prove their arguments decrease.

Sized types as optional upgrade. For mathematics-heavy code with complex recursion patterns, sized types eliminate much proof obligation. MiniAgda's approach annotates types with size bounds and tracks decrease through function composition—more modular than syntactic checking but adds type system complexity.

The Mathlib experience in Lean 4 offers guidance for algebraic hierarchies: use extension (CommRing extends Ring) rather than mixins to avoid term size blowup; only add type classes when there's "real mathematics" to be done; separate raw structures (operations only) from structures-with-laws (operations + proofs).

Rust tooling recommendations for language implementation

Parser stack: logos + LALRPOP. Logos generates the fastest Rust lexers (~1204 MB/s in benchmarks) via procedural macros that compile to deterministic state machines. LALRPOP, an LR(1) parser generator, directly produces typed Rust ASTs—no glue code. Together they handle mathematical syntax elegantly:

// logos lexer
#[derive(Logos)]
enum Token {
    #[token("+")] Plus,
    #[regex("[0-9]+", |lex| lex.slice().parse())] Number(i64),
    #[regex("[a-zA-Z_][a-zA-Z0-9_]*")] Ident,
}

// LALRPOP grammar
Expr: Expr = {
    <l:Expr> "+" <r:Term> => Expr::Add(Box::new(l), Box::new(r)),
    Term,
};

AST design: enum-based with spans. Use Box<T> for recursive types, keep enum variants small (Rust enum size equals largest variant), and attach source locations for error messages:

pub struct Spanned<T> { pub node: T, pub span: (usize, usize) }
pub type Expr = Spanned<ExprKind>;

pub enum ExprKind {
    Integer(i64),
    Rational(Ratio<BigInt>),
    Binary { op: BinOp, left: Box<Expr>, right: Box<Expr> },
    FnCall { name: String, args: Vec<Expr> },
}

Interpreter: start tree-walking. For a mathematical language with symbolic manipulation, tree-walking interpreters are simpler and often fast enough. Bytecode VMs offer 3-10x speedups but complicate symbolic operations. Start with tree-walking; profile later.

Rational arithmetic: num-rational for portability, malachite for performance. num-rational is pure Rust, works on WASM, and handles moderate-sized rationals well. malachite provides GMP-competitive performance without C dependencies, using algorithms derived from GMP/FLINT. Avoid rug unless you need absolute maximum performance and can accept LGPL licensing and C dependencies.

REPL: rustyline or reedline. Both provide readline-style editing with history, completion, and syntax highlighting. For notebook interfaces, implement a Jupyter kernel using the standard protocol—the two-process model (frontend ↔ ZeroMQ ↔ kernel) enables language-agnostic UIs.

WZ certificates and holonomic functions fit naturally in the type system

The Wilf-Zeilberger method reduces proving hypergeometric identities to finding rational function certificates. Given ∑_k F(n,k) = r(n), if there exists G(n,k) = R(n,k) · F(n,k) where R is rational and F(n+1,k) - F(n,k) = G(n,k+1) - G(n,k), summing over k telescopes the right side to zero, proving the sum is independent of n.

Representation: WZ certificates are elements of Q(n,k), the field of rational functions in two variables. Store as Rational(Polynomial, Polynomial) with GCD reduction for canonical form.

Type-theoretic view: A certificate is a witness proving the WZ equation holds—a dependent pair of the rational function and a proof that substituting it into the equation yields zero. In your language:

WZCertificate : (F : HypergeomTerm) → Type
WZCertificate F = Σ (R : Q(n,k)), proof (wz_equation_holds F R)

Gosper's algorithm computes certificates when they exist; Zeilberger's algorithm extends this to creative telescoping for holonomic sums.

Holonomic functions are finitely representable via annihilating differential/recurrence operators plus initial values. They're closed under addition, multiplication, and definite summation—perfect for a symbolic mathematics language. Model them as:

Holonomic A = { operator : DifferentialOperator, initials : List A }

The A=B book by Petkovšek, Wilf, and Zeilberger (freely available online) provides the complete algorithmic theory. Koutschan's HolonomicFunctions package for Mathematica demonstrates production implementation using Gröbner bases in Ore algebras.

Module systems and practical architecture complete the design

Follow the ML module system pattern: structures (value-level modules), signatures (type-level specifications), and functors (parameterized modules). For mathematical libraries, functors enable writing code generic over algebraic structures:

signature RING = sig
  type t
  val zero : t
  val one : t
  val add : t → t → t
  val mul : t → t → t
  val neg : t → t
end

functor PolynomialRing(R : RING) : RING where type t = Poly(R.t)

Applicative functors (OCaml-style) suit pure/total languages better than generative functors (SML-style)—same arguments yield type-compatible results without fresh abstract types.

For handling partiality gracefully, use Capretta's delay monad: data Delay a = Now a | Later (Delay a) (coinductive). Non-termination becomes an explicit effect. Provide run : Delay A → Nat → Maybe A for step-bounded evaluation and keep runForever at runtime only, outside proofs.

Error handling in total languages uses type holes for incremental development (?name marks incomplete code), rich unification error messages, and escape hatches (assert_total, assert_smaller) clearly documented as trusted-not-verified. Default to total; require explicit partial annotation.

Project structure recommendation:

src/
├── lexer/       (logos token definitions)
├── parser/      (LALRPOP grammar + AST types)
├── types/       (type checker, termination checker)
├── egraph/      (egg integration, rewrite rules)
├── interpreter/ (tree-walking evaluator)
├── rational/    (exact arithmetic)
└── repl/        (rustyline + notebook kernel)

Conclusion

A total language for experimental mathematics is not merely feasible—it's well-supported by existing theory and tooling. The Foetus algorithm and sized types provide practical termination checking. System T captures essentially all mathematical computation while guaranteeing halting. The egg library offers production-ready e-graphs for first-class term rewriting. LALRPOP + logos handle parsing elegantly in Rust.

The key architectural decisions: structural recursion as default with well-founded recursion escape; strict positivity for inductive types; ML-style modules with applicative functors; delay monad for partiality; e-graph saturation with explicit timeout/size bounds.

Start with a minimal core (System F + inductive types + structural recursion), add e-graphs for algebraic simplification, build rational polynomial infrastructure for WZ certificates, and wrap in a Jupyter kernel for the notebook interface. The result: a language where every program terminates, every simplification is guaranteed to complete, and mathematicians can experiment with identities knowing their computer won't spin forever.