Background
The growth domain (src/growth.rs) computes a Big-O normal form as an antichain of monomials. Two operators that are mathematically identical — X * X (Expr::Mul) and X^2 (Expr::Pow) — produce different normal forms when X is a multi-term antichain:
$ pred-sym big-o "(n + m)^2"
O(m^2 + n^2)
$ pred-sym big-o "(n + m)*(n + m)"
O(m*n + m^2 + n^2)
$ pred-sym compare "(n+m)*(n+m)" "(n+m)^2"
Big-O equal: false
Root cause: Pow(X, 2) uses the raise-each-term rule (a deliberate widening introduced so sqrt((n-m)^2) ≍ n+m), which yields {n², m²}. Mul(X, X) uses the general antichain product, which yields all cross terms {n², n·m, m²}. The cross term n·m is asymptotically dominated by the sum n² + m² (AM–GM: n·m ≤ (n²+m²)/2), but the antichain order is per-term — no single term dominates n·m — so it is kept.
Why this is not a soundness bug (but worth fixing)
Both results are valid upper bounds — Mul merely over-approximates, Pow gives the tighter (and also valid) answer. Dominance decisions stay safe (an over-approximation never under-states growth), so find_dominated_rules and the measured search's pre-flight guard remain sound. The observable costs are:
pred-sym compare reports "not equal" for two expressions that are the same growth class, whenever one is written with * and the other with ^.- Composed overheads that happen to multiply an antichain by itself render a non-minimal Big-O (extra cross terms) in
pred path.
Objective
Make X * X and X^2 produce the same normal form — either by having Mul recognize a self-product, or (more generally) by teaching the antichain to drop a term that is dominated by the sum of other terms (AM–GM pruning), not just by a single term. Decide which; the second is more general but changes the antichain invariant, so it needs care.
Verification
pred-sym compare "(n+m)*(n+m)" "(n+m)^2" → equal, and pred-sym big-o "(n+m)*(n+m)" → O(m^2 + n^2) (no m*n term). Add a growth unit test pinning Mul(X,X) == Pow(X,2) for a multi-term X.
Negative control: the same test on today's code fails (the two forms differ) — proving the fix changed real behavior.
Related
Found during the old-vs-new correctness audit of PR #1083 (growth domain). Independent of the milestone's shipped correctness — this is a tightness/consistency refinement, not a soundness fix.
Background
The growth domain (
src/growth.rs) computes a Big-O normal form as an antichain of monomials. Two operators that are mathematically identical —X * X(Expr::Mul) andX^2(Expr::Pow) — produce different normal forms whenXis a multi-term antichain:Root cause:
Pow(X, 2)uses the raise-each-term rule (a deliberate widening introduced sosqrt((n-m)^2) ≍ n+m), which yields{n², m²}.Mul(X, X)uses the general antichain product, which yields all cross terms{n², n·m, m²}. The cross termn·mis asymptotically dominated by the sumn² + m²(AM–GM:n·m ≤ (n²+m²)/2), but the antichain order is per-term — no single term dominatesn·m— so it is kept.Why this is not a soundness bug (but worth fixing)
Both results are valid upper bounds —
Mulmerely over-approximates,Powgives the tighter (and also valid) answer. Dominance decisions stay safe (an over-approximation never under-states growth), sofind_dominated_rulesand the measured search's pre-flight guard remain sound. The observable costs are:pred-sym comparereports "not equal" for two expressions that are the same growth class, whenever one is written with*and the other with^.pred path.Objective
Make
X * XandX^2produce the same normal form — either by havingMulrecognize a self-product, or (more generally) by teaching the antichain to drop a term that is dominated by the sum of other terms (AM–GM pruning), not just by a single term. Decide which; the second is more general but changes the antichain invariant, so it needs care.Verification
pred-sym compare "(n+m)*(n+m)" "(n+m)^2"→ equal, andpred-sym big-o "(n+m)*(n+m)"→O(m^2 + n^2)(nom*nterm). Add a growth unit test pinningMul(X,X) == Pow(X,2)for a multi-termX.Negative control: the same test on today's code fails (the two forms differ) — proving the fix changed real behavior.
Related
Found during the old-vs-new correctness audit of PR #1083 (growth domain). Independent of the milestone's shipped correctness — this is a tightness/consistency refinement, not a soundness fix.