Skip to main content

Module growth

Module growth 

Source
Expand description

Symbolic growth domain: a dedicated asymptotic normal form for reduction parameter expressions.

Where full monomial canonicalization answers Big-O questions by expanding an Expr to monomial normal form, with exponential cost in nesting depth, the growth domain computes a Big-O normal form bottom-up without rewriting the source AST into a fully distributed polynomial. Work is output-sensitive: antichains are retained up to 32 terms; larger fronts are reported as unsupported instead of silently approximated.

§Representation

One internal growth term is a monomial

∏_v ∏_f base[f]^(coefficient[f] · v)
    · ∏_v v^(poly[v]) · ∏_v (log v)^(logs[v])

and a Growth is either a known antichain of pairwise-incomparable dominant terms (each summand of an asymptotic sum), or an unknown result with explicit reasons for content we cannot represent symbolically.

§Semantic foundation (the trust contract)

Every expression admitted to the domain is assumed nonnegative and weakly monotone (nondecreasing in each variable) on vars ≥ 2. Under these axioms Howell’s multivariate-O inconsistencies vanish and f + g ≍ max(f, g) up to a constant factor, which licenses add = antichain union + prune. All bounds produced are upper bounds.

Widening (always toward a valid upper bound):

  • Subtraction is normalized to addition of a negative term, and Growth::from_expr widens it to the union of both operands. This also covers the sqrt((a − b)^2) absolute-value idiom (|a − b| ≤ a + b).
  • Constants and constant multipliers/divisors are dropped on entry.
  • Exponentials with a linear exponent (c^x, c^(r·x), exp(x)) are first-class via symbolic base/coefficient factors. The original base is authoritative: it is never normalized through a floating-point logarithm and never reconstructed by rounding. Nonlinear exponents (2^(n·k), 2^sqrt(n)), factorial(·), and negative polynomial exponents widen to an unknown result, which preserves its reasons through every operation.
  • The explicit approximation boundary treats Expr::log as the natural logarithm, but all fixed logarithm bases greater than one have the same asymptotic class and are intentionally represented by the single log(v) factor.

§Pow note

Pow(base, k) for a nonnegative constant k raises each antichain term of base to the power k (scaling its exponents). This is the tight asymptotic answer — (n + m)^2 ≍ max(n, m)^2 = max(n^2, m^2) by AM-GM, so no binomial cross term is introduced — and it is what makes the widening chain sqrt((n − m)^2) ≍ n + m hold exactly.

Structs§

Growth
The asymptotic growth class of an Expr.

Enums§

GrowthFailure
A precise reason why an expression has no represented Growth value.