Skip to content

Add growth domain (src/growth.rs): growth terms, antichain, symbolic dominance #1075

Description

@isPANN

Background

This library represents each problem reduction's size overhead as a symbolic expression (Expr in src/expr.rs) over size variables such as num_vertices. Today, asymptotic (Big-O) questions are answered by fully expanding expressions to monomial normal form (src/canonical.rs), which is exponential in nesting depth and was the root cause of issue #1069. The growth domain is a dedicated asymptotic normal form that computes Big-O bottom-up without ever expanding.

Full design (shared overview for this batch): docs/design/symbolic-growth-domain.md — read the Semantic foundation and M1 sections before starting.

Objective

Implement the growth domain as a new module src/growth.rs: growth terms, antichain-based growth classes, a purely symbolic dominance order, pruning, caps, and serde support. This issue creates the module and its unit tests only — it changes no existing behavior (no existing file is rewired yet).

Interface (Input → Output)

In: &Expr (the existing AST; no changes to Expr).
Out:

pub struct GrowthTerm {
    exp:  BTreeMap<&'static str, f64>, // variable → rate, base normalized to 2; linear forms only
    poly: BTreeMap<&'static str, f64>, // variable → degree (0.5 covers sqrt)
    logs: BTreeMap<&'static str, u32>, // variable → log power
}
pub enum Growth {
    Terms(Vec<GrowthTerm>), // antichain of pairwise-incomparable dominant terms, deterministically sorted
    Unknown,                // absorbing sentinel
}
impl Growth {
    pub fn from_expr(expr: &Expr) -> Growth;
    pub fn dominates(&self, other: &Growth) -> bool; // partial order; see design for semantics
}

Both types derive Clone, Debug, PartialEq, Serialize, Deserialize.

Technical recommendations (non-binding)

  • Transfer functions: Var → {poly:{v:1}}; Const → empty term (O(1)); Add → antichain union + prune; Mul → pairwise map-merge + prune; Pow(base, const k ≥ 0) → antichain of pairwise products; c^x/c^(r·x)/exp(x) with linear exponent → exp entries (base normalized to 2, e.g. 3^n → {n: log2(3)}); Log → log(n^a·m^b) ≍ log n + log m; Sqrt = Pow 0.5.
  • Widening (always toward a valid upper bound): subtraction a − b ⇝ a + b; constants dropped; nonlinear exponents (2^(n*k), 2^sqrt(n)), factorial, negative exponents → Unknown. Unknown absorbs through every operation.
  • Dominance: per variable, lexicographic on (exp rate, poly degree, log power); a term is dominated iff ≤ on every variable and < on at least one. Growth-level: every term of the smaller is dominated-or-equal, standard antichain comparison.
  • Antichain cap 32: on overflow, widen upward to the single componentwise-max term (a valid upper bound) — never truncate by iteration order.
  • Sort terms by a deterministic total order (e.g. lexicographic on the serialized key) so PartialEq and serialization are platform-stable.
  • Axioms (document in module docs, debug_assert! where cheap): all size variables ≥ 2; nonnegative coefficients; weak monotonicity. See the design doc's Semantic foundation.

Verification

cargo test growth passes, including these named cases (add them verbatim as unit tests in src/unit_tests/growth.rs):

  1. No-expansion regression: Growth::from_expr on the parse of "(12*(n + 3*m) + 5)^2 * (12*(n + 3*m) + 5)^2" returns Terms containing the terms n^4 and m^4, with ≤ 6 terms total, in < 10 ms — which proves nested sums-of-squares are handled without expansion (the shape that OOM'd in pred path --all OOMs/hangs: big_o_normal_form exponentially expands composed overhead expressions #1069).
  2. Dominance beats the old sampling heuristic: the growth of 1.001^n dominates the growth of n^100 (and not conversely) — the current numerical_dominance_check in src/big_o.rs decides this pair wrongly; this test documents the correction.
  3. Incomparability is honest: neither n^2 nor n*m dominates the other; from_expr("n^2 + n*m") keeps both terms.
  4. Exponent rates are exact: growth of 2^(2*n) dominates growth of 2^n, not conversely; 2^n and 3^n compare via base-2 rates (3^n dominates).
  5. Widening: from_expr("n - m") equals from_expr("n + m"); from_expr("sqrt((n - m)^2)") equals from_expr("n + m").
  6. Determinism: from_expr("n*m + m*n") == from_expr("m*n + n*m") (structural equality after canonical sorting).

Negative control: from_expr("2^(n*k)") and from_expr("factorial(n)") both return Growth::Unknown, and Unknown absorbs: combining Unknown with the growth of n^2 under add/mul yields Unknown — which proves unsupported content cannot silently produce a fake bound.

Dependencies

None (first issue of the batch). Milestone: Symbolic Growth Domain & Pareto Search.

Out of scope

Rewiring big_o.rs, analysis.rs, search, or any CLI — later issues in this milestone.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    Status
    No status

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions