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.

from alkahest import simplify

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)

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.

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

# 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)

Customizing the rule set

from alkahest import simplify_with, make_rule

# Add a custom rule: sin²(x) → 1 - cos²(x)
my_rule = make_rule("sin_sq_to_cos", lhs=sin(x)**2, rhs=pool.integer(1) - cos(x)**2)
r = simplify_with(expr, rules=[my_rule])

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 all of them decline:

import alkahest as ak

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

ak.simplify(undefined).value          # (0 * 0^-1) — left alone
ak.simplify_egraph(undefined).value   # (0 * 0^-1) — same
ak.simplify(pool.integer(5) * Z ** pool.integer(-1) * Z).value   # (0 * 0^-1 * 5)

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) no longer reports 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

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 simplify; only the schedule differs. 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

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.