Simplification

Alkahest provides two complementary simplification engines that operate on the same expression pool.

#Rule-based simplification

simplify applies a fixed set of algebraic rewrite rules until no more apply (fixpoint). It is fast, predictable, and always terminates.

import alkahest as ak
from alkahest import simplify, sin, cos, asin, exp, sqrt, is_zero, equals, to_real_form

pool = ak.ExprPool()
x, y, a, w, t = (pool.symbol(n) for n in ("x", "y", "a", "w", "t"))
I = ak.I

r = simplify(x + pool.integer(0))   # → x
r = simplify(x * pool.integer(1))   # → x
r = simplify(pool.integer(2) * pool.integer(3))  # → 6  (constant folding)

The default rule set covers:

• Identity and absorbing elements (x + 0 → x, x * 1 → x, x * 0 → 0)
• Constant folding (integer and rational arithmetic)
• Basic polynomial simplification (x + x → 2*x, x² * x → x³)
• Commutativity and associativity (normalized at construction)

#Domain passes: the simplest form

After the rule engine, Python simplify (and simplify_auto) try the domain passes the core rule set leaves out, each only when its trigger occurs in the expression, and keep a candidate only if it is strictly smaller (node count, then radical nesting) — so simplify never returns something larger than the rule engine gave:

Side conditions appear on the step in .steps. The rewrites without a Lean tactic withhold .certificate rather than emit one that does not check. The Rust alkahest_cas::simplify that subsystems call on intermediate results is the rule engine alone; simplify_full is the Rust spelling of the above.

A denominator that simplifies to 0 is an error, not a value: simplify(1/(x + 2*x - 3*x)) raises DivisionByZeroError (E-DOMAIN-001), which is both a DomainError and a ZeroDivisionError, as x / 0 does.

#Special values and zero recognition

Every entry point also folds exact special values (cos(pi) → -1, sin(pi/6) → 1/2, gamma(1/2) → sqrt(pi), dilog(1) → pi²/6, asin(1) → pi/2, sin(n·pi) → 0 for an integer-domain n), radical powers (sqrt(2)² → 2, sqrt(8) → 2·sqrt(2); sqrt(x)² → x only for a provably non-negative x), i² = −1 inside products, cancelling exponentials (exp(−x)·exp(x) → 1), and replaces a sum that is identically zero by 0.

is_zero(expr) / equals(a, b) answer the question directly. True is only ever a proof (simplification to 0, or a zero numerator in the rational normal form over atoms, where trig/hyperbolic functions go through exp and radicals and i are reduced by their defining relations); False is a proof too (an exact non-zero normal form, or a rigorous Arb ball excluding zero at a sample point inside the symbols' domains and the assumptions); None is undetermined. equals reports the provenance, including the numeric-only probably_zero status, which never counts as True.

is_zero(sin(x)**2 + cos(x)**2 - 1)            # True
equals(asin(sin(x)), x).status                # 'proved_nonzero'

#Real form

to_real_form(expr, assumptions=None) rewrites an expression written through complex quantities into an equal real one: exp(±i·θ) pairs become cos/sin, √X with X ≤ 0 proved becomes i·√(−X), cosh(i·x) becomes cos x, and perfect squares leave square roots (√(4a²) → 2|a|, → 2a once a ≥ 0 is known; √(9m²k² − 4k²m²) → √5·k·m for positive k, m). The real part is returned only when the imaginary part is proved identically zero; otherwise the input comes back unchanged. Signs come from symbol domains, the assumptions, and a polynomial certificate (AM–GM absorption, then factorisation), which is what proves the two-compartment discriminant (k₁₀+k₁₂+k₂₁)² − 4k₁₀k₂₁ positive. matrix_exp, dsolve and the inverse Laplace transform (hence TransferFunction.step_response) apply it to their results, so an oscillatory expm comes back as cos(w·t) and a two-compartment inverse as a biexponential — both evaluable by eval_expr, the JIT and emit_c_expr. experimental.dsolve_system, Matrix.eigenvals() and solve apply it too (all three take real_form=False to return the raw closed form); a value is rewritten only where its imaginary part is proved zero.

to_real_form(sqrt(4*a**2))                           # 2*abs(a)
to_real_form((exp(sqrt(-4*w**2*t**2)/2) + exp(-sqrt(-4*w**2*t**2)/2))/2)   # cos(w*t)
to_real_form(exp(I*x))                               # unchanged: genuinely complex

#Domain-specific rule sets

from alkahest import simplify_trig, simplify_log_exp, simplify_expanded, log

# Pythagorean identity and double-angle formulas
r = simplify_trig(sin(x)**2 + cos(x)**2)  # → 1

# Conservatively leaves branch-sensitive identities unchanged
r = simplify_log_exp(exp(log(x)))

# Expand products and collect like terms
r = simplify_expanded((x + pool.integer(1))**3)

simplify_expanded expands every power of a sum whose expansion has at most 4096 monomials ((x+1)**13, (x+y+z)**8). A larger one is left as written, with an expand_pow_limit_reached step naming it and a UserWarning; expand such polynomials with UniPoly / MultiPoly.

#Customizing the rule set

from alkahest import simplify_with, make_rule

# Add a custom rule: sin²(u) → 1 - cos²(u). Lower-case symbols in the
# left-hand side (here `a`) are wildcards that bind to any sub-expression.
my_rule = make_rule(sin(a)**2, pool.integer(1) - cos(a)**2)
r = simplify_with(sin(x)**2 + y, [my_rule])   # → y + 1 - cos(x)²

simplify_with applies only the rules it is given; add alkahest.default_rules() to the list to keep the default arithmetic rules.

#Conditional simplification (colored e-graphs)

Branch-sensitive rewrites are opt-in. In Python, create an explicit experimental context tied to one expression pool; x > 0 then enables sqrt(x²) → x:

from alkahest.experimental import Assumptions

assumptions = Assumptions(pool)
assumptions.refine(pool.gt(x, pool.integer(0)))
r = assumptions.simplify(sqrt(x**2))  # → x

The current fact language recognizes conjunctions of positive and non-zero predicates. Unsupported predicates are retained for contradiction detection but do not authorize a rewrite; a definitive contradiction raises AssumptionError with code E-SIMPLIFY-001. Contexts never modify the thread-local context() helper or global simplifier state.

Without a proven fact, branch-cut identities such as sqrt(x²) → x, exp(log(x)) → x, and log(a*b) → log(a) + log(b) remain unchanged. Algebraic cancelations such as x/x → 1 and x^0 → 1 still fire in the default simplifier and record NonZero side conditions in the derivation log. The colored pass runs after ordinary rule simplification and preserves repeated terms and factors.

#The literal-zero carve-out

b · b⁻¹ → 1 is a documented convention for a symbolic base, but it is not a convention anybody holds when the base is the literal integer 0: 0⁻¹ is division by zero, so 0 · 0⁻¹ is the indeterminate form 0 · ∞ and has no value. Through 3.7 simplify returned 1 for it, simplify_egraph returned 0, and simplify(5 · 0⁻¹ · 0) returned 0 — three answers that were their own proof that at least two were wrong. As of 3.8 none of them returns a value: simplify raises DivisionByZeroError (E-DOMAIN-001) and simplify_egraph leaves the product alone:

Z = pool.integer(0)
undefined = Z * Z ** pool.integer(-1)

ak.simplify_egraph(undefined).value   # (0 * 0^-1) — left alone
for e in (undefined, pool.integer(5) * Z ** pool.integer(-1) * Z):
    try:
        ak.simplify(e)
    except ak.DivisionByZeroError as err:
        print(err.code)               # E-DOMAIN-001

The guard tests for a literal zero base. Because the rule engine normalises strictly bottom-up, that also covers every base the simplifier can itself reduce to zero — x - x included, so diff(2/(x - x), x) now raises DivisionByZeroError instead of reporting 1 for a function whose domain is empty. A base that is zero but not provably so keeps the b · b⁻¹ → 1 convention: deciding it would need a three-valued zero test on the Mul rewrite path, which costs several 128-bit ball evaluations per node.

Unaffected controls, so you can see the boundary: x · x⁻¹ → 1, 0 · x → 0, and 2x − 2x → 0 all still fire.

#Parallel simplification

from alkahest import simplify_auto, simplify_par, simplify_redex, simplify_strategy

expr = (x + pool.integer(0)) * pool.integer(1) + x * y + x * y + (x + 1)**2

simplify_par(expr)      # fork-join: best on wide expressions
simplify_redex(expr)    # level-scheduled: best on deep ones, deterministic log
simplify_auto(expr)     # picks one of the two from the expression's shape
simplify_strategy(expr) # "fork_join" | "level_scheduled" | "sequential"

Each takes a single expression and returns the same result as the rule engine; only the schedule differs (simplify_par and simplify_redex run the rule engine alone, while simplify_auto also tries the domain passes above, as simplify does). Published wheels are built with --features parallel, so all three schedulers are real there. parallel is not a Cargo default, though: a source build that omits it falls back to the sequential path, so all four remain callable and simplify_strategy then reports "sequential" — which is the way to tell the two situations apart.

Neither parallel scheduler dominates:

Measured on 32 cores, best time over 1–32 threads:

Fork-join keeps each chain on one worker and wins on wide expressions through cache locality. Level scheduling wins on deep ones, where fork-join finds no wide node to fork on and runs essentially sequentially. At one thread the level scheduler is faster on every shape measured. Reproduce with cargo run --release --features parallel --example simplify_three_way.

Both are experimental: alkahest_cas::experimental::{simplify_par, simplify_redex}.

#E-graph simplification

simplify_egraph uses equality saturation via egglog to explore many equivalent forms simultaneously before committing to the best one via a cost function.

from alkahest import simplify_egraph

# The e-graph can discover non-obvious equivalences
r = simplify_egraph(x * x - pool.integer(1))  # may factor or simplify; here → -1 + x²

E-graph saturation is more powerful than rule-based simplification for some inputs but slower and has non-deterministic performance for complex expressions. See E-graph saturation for configuration options (EgraphConfig, including disjoint_schedule for match-disjoint rule groups).

User-defined PatternRule sets can use discrimination-net indexing on the Rust side (PatternRuleSet, simplify_with_pattern_rules); the built-in RewriteRule engine still scans rules linearly.

#Choosing between the two

For most workflows: use simplify (or a domain-specific variant) first. Reach for simplify_egraph when you need the system to discover a non-obvious equivalence.

#Collect and normalize

Two utility passes that sit between the two engines:

from alkahest import collect_like_terms, poly_normal

# 2*x + 3*x → 5*x
r = collect_like_terms(pool.integer(2) * x + pool.integer(3) * x)

# Normalize to canonical polynomial form over given variables
r = poly_normal(x**2 + pool.integer(2) * x * y + y**2, [x, y])

#Complex constructors (experimental)

alkahest.experimental exposes symbolic conjugate, re, im, and principal arg. These are symbolic-only: they are not registered for f64, ball, or JIT evaluation.

Safe simplifications include involution of conjugate, real/integer literals for re/im, arg of a strictly positive literal or Domain.Positive symbol, and exact arg(I) / arg(-I). Branch-sensitive cases such as conjugate(log(z)), arg(0), negative reals, and generic complex inputs stay unevaluated. Principal Arg uses the conventional range (−π, π] with a cut on the negative real axis; do not rewrite through atan2, log, or sqrt yet.