From 2fdb8df15879f6ec9f04d26e9f060466c6b8821c Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Tue, 27 Oct 2026 06:27:46 -0700 Subject: [PATCH 1/2] Report whether a growth bound is exact, and make factorial exact by Stirling Growth::relation() returns ParameterRelation::Exact when the Big-O form is also a lower bound (Theta) and UpperBound when any step widened it. factorial(x) of an exact single monomial now uses x^(x+1/2) e^(-x). A lower-bound property harness with a seeded negative control checks every exact claim numerically; four Stirling cases join the SymPy oracle. Co-Authored-By: Claude Opus 5.5 --- .../tests/fixtures/sympy_oracle.json | 28 +++ scripts/generate_symbolic_expr_fixture.py | 4 + src/growth.rs | 190 ++++++++++---- src/unit_tests/growth.rs | 236 +++++++++++++++--- 4 files changed, 372 insertions(+), 86 deletions(-) diff --git a/problemreductions-expr/tests/fixtures/sympy_oracle.json b/problemreductions-expr/tests/fixtures/sympy_oracle.json index 3daf2f1ca..27feff24d 100644 --- a/problemreductions-expr/tests/fixtures/sympy_oracle.json +++ b/problemreductions-expr/tests/fixtures/sympy_oracle.json @@ -926,6 +926,34 @@ "right": "n^n", "ratio_limit": "0", "relation": "right_dominates" + }, + { + "name": "stirling_factorial", + "left": "factorial(n)", + "right": "n^n * sqrt(n) * exp(-n)", + "ratio_limit": "sqrt(2)*sqrt(pi)", + "relation": "equivalent" + }, + { + "name": "factorial_below_self_power", + "left": "n^n", + "right": "factorial(n)", + "ratio_limit": "oo", + "relation": "left_dominates" + }, + { + "name": "factorial_above_base_e_power", + "left": "factorial(n)", + "right": "(n / 3)^n", + "ratio_limit": "oo", + "relation": "left_dominates" + }, + { + "name": "scaled_factorial", + "left": "factorial(2 * n)", + "right": "(2 * n)^(2 * n) * sqrt(n) * exp(-2 * n)", + "ratio_limit": "2*sqrt(pi)", + "relation": "equivalent" } ], "factorial_domain_cases": [ diff --git a/scripts/generate_symbolic_expr_fixture.py b/scripts/generate_symbolic_expr_fixture.py index c9ba5e32e..52bf21f45 100644 --- a/scripts/generate_symbolic_expr_fixture.py +++ b/scripts/generate_symbolic_expr_fixture.py @@ -159,6 +159,10 @@ ("exponent_cancellation", "2^((n + 1)^2 - n^2)", "2^(2 * n)"), ("decaying_factor", "2^n * 0.5^n", "1"), ("reverse_variable_base", "2^n", "n^n"), + ("stirling_factorial", "factorial(n)", "n^n * sqrt(n) * exp(-n)"), + ("factorial_below_self_power", "n^n", "factorial(n)"), + ("factorial_above_base_e_power", "factorial(n)", "(n / 3)^n"), + ("scaled_factorial", "factorial(2 * n)", "(2 * n)^(2 * n) * sqrt(n) * exp(-2 * n)"), ] diff --git a/src/growth.rs b/src/growth.rs index 6aade0cae..121d1748b 100644 --- a/src/growth.rs +++ b/src/growth.rs @@ -30,8 +30,17 @@ //! **weakly monotone** (nondecreasing in each variable) on `vars ≥ 2`, and //! asymptotic statements quantify over all variables growing together //! (`∃N: ∀ vars ≥ N`). Under these axioms `f + g ≍ max(f, g)` up to a constant -//! factor, which licenses `add = antichain union + prune`. All bounds produced -//! are **upper** bounds. +//! factor, which licenses `add = antichain union + prune`. Every known growth is +//! an **upper** bound; [`Growth::relation`] reports +//! [`ParameterRelation::Exact`] when it is also a lower bound (`f = Θ(growth)`) +//! and [`ParameterRelation::UpperBound`] when any step below widened it. +//! +//! Exactness is preserved by sums and products of exact operands, constant +//! powers, exactly expanded exponents with exactly bounded bases, logarithms +//! whose argument grows without bound, and sums whose widened summands are +//! strictly dominated by an exact summand (so `n − 1` and `n² − n` stay exact). +//! `factorial(x)` is exact by Stirling, `x! ≍ x^(x+1/2)·e^(−x)`, when `x` +//! expands exactly to one monomial. //! //! Widening (always toward a valid upper bound): //! - Subtraction is normalized to addition of a negative term, and @@ -46,7 +55,7 @@ //! floating-point logarithm and never reconstructed by rounding. //! - A variable base `B` with exact expansion `Σ c_i μ_i` is bounded by //! `C · M`, where `C = Σ c_i` and `M` takes the largest power of every -//! variable, so `B^E ≤ C^E · M^E`. `factorial(x)` widens to `x^x`. +//! variable, so `B^E ≤ C^E · M^E`. Any other `factorial(x)` widens to `x^x`. //! - `ln ln v` inside an exponent widens to `ln v`. //! - The explicit approximation boundary treats [`Expr::log`] as the natural //! logarithm, but all fixed @@ -72,6 +81,7 @@ //! `sqrt((n − m)^2) ≍ n + m` hold exactly. use crate::expr::{AlgebraicAnalysis, BigInt, Expr, ExprNode, ExprNodeId}; +use crate::parameters::ParameterRelation; use num_rational::BigRational; use num_traits::{One, Signed, ToPrimitive, Zero}; use std::cmp::Ordering; @@ -296,7 +306,11 @@ pub struct Growth(GrowthState); #[derive(Clone, Debug, PartialEq, Eq)] enum GrowthState { - Known(Vec), + /// A pruned antichain and whether it is also a lower bound. + Known { + terms: Vec, + relation: ParameterRelation, + }, /// Content outside the represented growth domain, with every reason that /// contributed to the result. Unknown(Vec), @@ -440,11 +454,20 @@ impl Growth { pub fn failures(&self) -> Option<&[GrowthFailure]> { match &self.0 { - GrowthState::Known(_) => None, + GrowthState::Known { .. } => None, GrowthState::Unknown(failures) => Some(failures), } } + /// Whether a known growth is tight (`Exact`, a Θ bound) or only an + /// `UpperBound`; `None` for unknown growth. + pub fn relation(&self) -> Option { + match &self.0 { + GrowthState::Known { relation, .. } => Some(*relation), + GrowthState::Unknown(_) => None, + } + } + /// Compute the growth class of an expression in a single bottom-up pass. pub fn from_expr(expr: &Expr) -> Growth { let analysis = AlgebraicAnalysis::new(&[expr]); @@ -462,7 +485,7 @@ impl Growth { /// some term of `self` — the standard antichain (Pareto) comparison. pub fn dominates(&self, other: &Growth) -> bool { match (&self.0, &other.0) { - (GrowthState::Known(a), GrowthState::Known(b)) => { + (GrowthState::Known { terms: a, .. }, GrowthState::Known { terms: b, .. }) => { b.iter().all(|tb| a.iter().any(|ta| ta.dominates_or_eq(tb))) } _ => false, @@ -478,7 +501,7 @@ impl Growth { pub fn to_expr(&self) -> Option { match &self.0 { GrowthState::Unknown(_) => None, - GrowthState::Known(terms) => Some( + GrowthState::Known { terms, .. } => Some( terms .iter() .map(term_to_expr) @@ -513,7 +536,10 @@ fn growth_from_analysis( let facts = analysis.facts(expression); if facts.is_constant { let growth = if facts.constant_domain == Some(true) { - constant_growth() + known( + vec![GrowthTerm::one()], + exact_if(facts.sign == Some(Ordering::Greater)), + ) } else { unknown(GrowthFailure::InvalidConstantDomain { expression: expression.to_string(), @@ -525,10 +551,13 @@ fn growth_from_analysis( let growth = match expression.node() { ExprNode::Const(_) => unreachable!("constants are handled before node projection"), - ExprNode::Var(variable) => exact_growth(vec![GrowthTerm::from_atoms([( - ln_atom(variable.as_str()), - natural(BigRational::one()), - )])]), + ExprNode::Var(variable) => known( + vec![GrowthTerm::from_atoms([( + ln_atom(variable.as_str()), + natural(BigRational::one()), + )])], + ParameterRelation::Exact, + ), ExprNode::Add(values) => values .iter() .map(|value| growth_from_analysis(value, analysis, memo)) @@ -569,18 +598,42 @@ fn growth_from_analysis( Err(failure) => unknown(failure), }, ExprNode::Log(value) => log_growth(growth_from_analysis(value, analysis, memo)), - // x! ≤ x^x for x ≥ 1. - ExprNode::Factorial(value) => match power_growth(value, value, analysis) { - growth if growth.failures().is_some() => { - unknown(GrowthFailure::UnsupportedFactorial(expression.to_string())) - } - growth => growth, - }, + ExprNode::Factorial(value) => factorial_growth(expression, value, analysis, memo), }; memo.insert(expression.node_identity(), growth.clone()); growth } +/// `x!` is `x^(x+1/2)·e^(−x)` up to a constant (Stirling) when `x^x` is exact, +/// which holds when `x` expands exactly to one monomial; otherwise `x! ≤ x^x`. +fn factorial_growth( + expression: &Expr, + value: &Expr, + analysis: &AlgebraicAnalysis, + memo: &mut HashMap, +) -> Growth { + let self_power = power_growth(value, value, analysis); + match self_power.relation() { + None => unknown(GrowthFailure::UnsupportedFactorial(expression.to_string())), + Some(ParameterRelation::UpperBound) => self_power, + Some(ParameterRelation::Exact) => { + let root = pow_const( + growth_from_analysis(value, analysis, memo), + &BigRational::new(BigInt::from(1), BigInt::from(2)), + ); + let decay = match exponent_poly(value, analysis) { + Ok(poly) => exponential( + LogBound::constant(natural(-BigRational::one())), + &poly, + value, + ), + Err(failure) => unknown(failure), + }; + mul(mul(self_power, root), decay) + } + } +} + /// `base^exponent` for a nonconstant exponent. fn power_growth(base: &Expr, exponent: &Expr, analysis: &AlgebraicAnalysis) -> Growth { match (log_bound(base, analysis), exponent_poly(exponent, analysis)) { @@ -661,7 +714,8 @@ impl LogBound { struct MonomialBound { scale: BigRational, largest: Monomial, - /// The polynomial is exactly one unit monomial without log powers. + /// The polynomial is exactly one monomial without log powers, so + /// `B = scale · largest`. exact: bool, } @@ -689,7 +743,7 @@ fn exponential(bound: LogBound, exponent: &ExponentPoly, source: &Expr) -> Growt ); } } - exact_growth(vec![term]) + known(vec![term], exact_if(bound.exact && exponent.exact)) } /// An exponent expanded as `Σ coefficient · monomial`. @@ -838,7 +892,6 @@ impl ExponentPoly { } let exact = self.exact && self.terms.len() == 1 - && scale.is_one() && largest.values().all(|(_, log_power)| log_power.is_zero()); Some(MonomialBound { scale, @@ -862,7 +915,8 @@ impl ExponentPoly { ) }); let constant = (Monomial::new(), ln_upper_bound(&bound.scale)); - Ok(Self::from_terms(logs.chain([constant]), bound.exact)) + let exact = bound.exact && bound.scale.is_one(); + Ok(Self::from_terms(logs.chain([constant]), exact)) } } @@ -956,8 +1010,12 @@ fn exponent_poly( } } -fn constant_growth() -> Growth { - exact_growth(vec![GrowthTerm::one()]) +fn exact_if(exact: bool) -> ParameterRelation { + if exact { + ParameterRelation::Exact + } else { + ParameterRelation::UpperBound + } } fn unknown(failure: GrowthFailure) -> Growth { @@ -1064,7 +1122,13 @@ fn prune(mut terms: Vec) -> Vec { result } -fn exact_growth(terms: Vec) -> Growth { +fn both_exact(a: &Growth, b: &Growth) -> bool { + [a, b] + .iter() + .all(|growth| growth.relation() == Some(ParameterRelation::Exact)) +} + +fn known(terms: Vec, relation: ParameterRelation) -> Growth { let terms = prune(terms); if terms.len() > ANTICHAIN_CAP { return unknown(GrowthFailure::AntichainLimitExceeded { @@ -1072,17 +1136,28 @@ fn exact_growth(terms: Vec) -> Growth { terms: terms.len(), }); } - Growth(GrowthState::Known(terms)) + Growth(GrowthState::Known { terms, relation }) } -/// Antichain union (asymptotic `+ ≍ max`). +/// Antichain union (asymptotic `+ ≍ max`). The sum stays exact when every +/// widened summand is strictly dominated by an exact one: a widened summand, +/// even a subtracted one, is then `o` of the exact part. fn add(a: Growth, b: Growth) -> Growth { if a.failures().is_some() || b.failures().is_some() { return merge_unknown(a, b); } - let mut terms = into_terms(a); - terms.extend(into_terms(b)); - exact_growth(terms) + let covers = |high: &Growth, low: &Growth| { + high.relation() == Some(ParameterRelation::Exact) + && terms(low).iter().all(|l| { + terms(high) + .iter() + .any(|h| h.cmp(l) == Some(Ordering::Greater)) + }) + }; + let relation = exact_if(both_exact(&a, &b) || covers(&a, &b) || covers(&b, &a)); + let mut sum = into_terms(a); + sum.extend(into_terms(b)); + known(sum, relation) } /// Pairwise product of two antichains. @@ -1090,52 +1165,73 @@ fn mul(a: Growth, b: Growth) -> Growth { if a.failures().is_some() || b.failures().is_some() { return merge_unknown(a, b); } - let x = into_terms(a); - let y = into_terms(b); - let mut product = Vec::with_capacity(x.len() * y.len()); - for tx in &x { - for ty in &y { + let relation = exact_if(both_exact(&a, &b)); + let mut product = Vec::with_capacity(terms(&a).len() * terms(&b).len()); + for tx in terms(&a) { + for ty in terms(&b) { product.push(tx.mul(ty)); } } - exact_growth(product) + known(product, relation) } /// Raise a whole antichain to a nonnegative real power `k` (raise each term). fn pow_const(g: Growth, k: &BigRational) -> Growth { match g.0 { GrowthState::Unknown(failures) => Growth(GrowthState::Unknown(failures)), - GrowthState::Known(terms) => exact_growth(terms.iter().map(|term| term.pow(k)).collect()), + GrowthState::Known { terms, relation } => { + known(terms.iter().map(|term| term.pow(k)).collect(), relation) + } + } +} + +fn terms(growth: &Growth) -> &[GrowthTerm] { + match &growth.0 { + GrowthState::Known { terms, .. } => terms, + GrowthState::Unknown(_) => unreachable!("unknown growth is handled before term access"), } } fn into_terms(growth: Growth) -> Vec { match growth.0 { - GrowthState::Known(terms) => terms, + GrowthState::Known { terms, .. } => terms, GrowthState::Unknown(_) => unreachable!("unknown growth is handled before term access"), } } /// Transfer function for `Log(a)`: `log` of an antichain is `log` of its /// dominant term(s), unioned. Uses `log(n^a · m^b) ≍ log n + log m` and -/// `log(2^(r·n)) ≍ n`. +/// `log(2^(r·n)) ≍ n`. Since `ln max = max ln`, the result is exact when the +/// argument is exact and every term's logarithm is exact. fn log_growth(g: Growth) -> Growth { match g.0 { GrowthState::Unknown(failures) => Growth(GrowthState::Unknown(failures)), - GrowthState::Known(terms) => { - let mut out = Vec::new(); - for t in &terms { - out.extend(log_term(t)); - } - exact_growth(out) + GrowthState::Known { terms, relation } => { + let exact = relation == ParameterRelation::Exact && terms.iter().all(log_is_exact); + known(terms.iter().flat_map(log_term).collect(), exact_if(exact)) } } } +/// `ln t = Σ w · atom` is `Θ` of its positive atoms when one of them strictly +/// dominates every atom not proved positive (so `ln t` is unbounded), and no +/// positive `ln ln v` atom was widened to `ln v`. +fn log_is_exact(t: &GrowthTerm) -> bool { + let signs: Vec<(&Atom, Sign)> = t + .atoms + .iter() + .map(|(atom, weight)| (atom, weight_sign(weight))) + .collect(); + grows_unboundedly(&signs, Sign::Positive) + && !signs + .iter() + .any(|(atom, sign)| matches!(atom, Atom::LogLog(_)) && *sign == Sign::Positive) +} + /// `log` of a single term, returned as its own (small) antichain of summands: /// `ln exp(Σ w · atom) = Σ w · atom`, so every atom with a possibly positive /// weight contributes the growth of the atom itself. None may be dropped (e.g. -/// `log(2^n·m)` is `n + log m`, not `n`); `finish_growth`/`prune` then collapse +/// `log(2^n·m)` is `n + log m`, not `n`); `prune` then collapses /// any dominated summands (so `log(2^n·n^2)` reduces back to `n`). `ln ln ln v` /// widens to `ln ln v`. fn log_term(t: &GrowthTerm) -> Vec { diff --git a/src/unit_tests/growth.rs b/src/unit_tests/growth.rs index e399975ee..af15bfc7b 100644 --- a/src/unit_tests/growth.rs +++ b/src/unit_tests/growth.rs @@ -1,12 +1,13 @@ //! Unit tests for the symbolic growth domain (`src/growth.rs`). use super::{ - add, exact_growth, ln_atom, mul, natural, single_variable, Atom, ExpBase, Growth, - GrowthFailure, GrowthState, GrowthTerm, ANTICHAIN_CAP, + add, known, ln_atom, mul, natural, single_variable, Atom, ExpBase, Growth, GrowthFailure, + GrowthState, GrowthTerm, ANTICHAIN_CAP, }; use crate::expr::{ evaluate_approximate, expression_from_approximation, AlgebraicAnalysis, Expr, ExprNode, }; +use crate::parameters::ParameterRelation; use crate::registry::variant_entries; use num_rational::BigRational; use num_traits::{FromPrimitive, One, Signed, Zero}; @@ -44,11 +45,15 @@ fn term(exp: &[(&str, f64)], poly: &[(&str, f64)], logs: &[(&str, u32)]) -> Grow fn terms_of(g: &Growth) -> &[GrowthTerm] { match &g.0 { - GrowthState::Known(terms) => terms, + GrowthState::Known { terms, .. } => terms, GrowthState::Unknown(failures) => panic!("expected known growth, got {failures:?}"), } } +fn exact(terms: Vec) -> Growth { + known(terms, ParameterRelation::Exact) +} + fn g(s: &str) -> Growth { Growth::from_expr(&Expr::parse(s)) } @@ -81,7 +86,7 @@ fn test_growth_relations_against_sympy_limits() { "../../problemreductions-expr/tests/fixtures/sympy_oracle.json" )) .unwrap(); - assert_eq!(fixture.growth_cases.len(), 25); + assert_eq!(fixture.growth_cases.len(), 29); for case in fixture.growth_cases { let left = g(&case.left); @@ -203,8 +208,8 @@ fn test_every_registered_complexity_uses_the_shared_analysis() { let growth = Growth::from_expr(&expression); if let Some(rendered) = growth.to_expr() { assert_eq!( - Growth::from_expr(&rendered), - growth, + terms_of(&Growth::from_expr(&rendered)), + terms_of(&growth), "{}: {}", entry.name, entry.complexity @@ -292,8 +297,79 @@ fn test_proven_equal_exponential_spelling_is_deterministic() { /// absolute-value idiom. #[test] fn test_growth_widening() { - assert_eq!(g("n - m"), g("n + m")); - assert_eq!(g("sqrt((n - m)^2)"), g("n + m")); + assert_eq!(terms_of(&g("n - m")), terms_of(&g("n + m"))); + assert_eq!(terms_of(&g("sqrt((n - m)^2)")), terms_of(&g("n + m"))); + assert_eq!(g("n - m").relation(), Some(ParameterRelation::UpperBound)); +} + +/// Exactness: a known growth is tight unless a step widened it. +#[test] +fn test_growth_relation() { + for source in [ + "n", + "3", + "n^2 + m", + "n - 1", + "n^2 - n*log(n)", + "2^n * n^3 - n^5", + "sqrt(n*m)", + "log(n)", + "log(n + 1)", + "log(2^n * m)", + "2^(n - log(n))", + "(2*n)^n", + "n^(n*m)", + "factorial(n)", + "factorial(n^2/2)", + ] { + assert_eq!( + g(source).relation(), + Some(ParameterRelation::Exact), + "{source}" + ); + } + for source in [ + "n - m", + "-n + 2", + "n*m - n^2", + "(n + 1)^n", + "2^log(n + m)", + "2^((n + m)^(1/2))", + "log(log(log(n)))", + "log(2^n * log(m))", + "log(1)", + "log(1 + 2^(-n))", + "factorial(n + m)", + "factorial(n * log(n))", + ] { + assert_eq!( + g(source).relation(), + Some(ParameterRelation::UpperBound), + "{source}" + ); + } + assert_eq!(g("2^(2^n)").relation(), None); +} + +/// Stirling: `n! ≍ n^(n+1/2)·e^(−n)`, strictly between `(n/e)^n` and `n^n`. +#[test] +fn test_growth_factorial_stirling() { + assert_eq!(g("factorial(n)"), g("n^n * sqrt(n) * exp(-n)")); + assert_eq!(g("factorial(2*n)"), g("(2*n)^(2*n) * sqrt(n) * exp(-2*n)")); + for (lower, upper) in [ + ("(n/3)^n", "factorial(n)"), + ("factorial(n)", "n^n"), + ("factorial(n)", "factorial(n + 1)"), + ("2^(n*log(n))", "factorial(2*n)"), + ] { + assert!(g(upper).dominates(&g(lower)), "{upper} ≻ {lower}"); + assert!(!g(lower).dominates(&g(upper)), "{lower} ⊁ {upper}"); + } + // Without an exact single-monomial argument, x! ≤ x^x is kept. + assert_eq!( + terms_of(&g("factorial(n + m)")), + terms_of(&g("(n + m)^(n + m)")) + ); } /// 6. Determinism: the antichain is canonically sorted, so structurally @@ -376,7 +452,7 @@ fn test_growth_reports_nested_and_numeric_failures() { )); assert_eq!(Growth::from_expr(&Expr::variable("n")).failures(), None); - assert_eq!(exact_growth(Vec::new()).to_expr(), Some(Expr::integer(1))); + assert_eq!(exact(Vec::new()).to_expr(), Some(Expr::integer(1))); } // --- Additional coverage --- @@ -517,7 +593,6 @@ fn test_growth_superexponential_shapes() { g("num_groups^(2*num_groups)").to_big_o(), "O(num_groups^(2 * num_groups))" ); - assert_eq!(g("factorial(n)"), g("n^n")); // (k + 1)^n ≤ (2k)^n keeps the base-2 factor, which is not O(k^n). assert_eq!(g("(k + 1)^n").to_big_o(), "O(2^n * k^n)"); assert!(g("(k + 1)^n").dominates(&g("k^n"))); @@ -545,7 +620,7 @@ fn test_growth_log_levels() { assert_eq!(g("log(3^n)"), g("n")); assert_eq!(g("log(exp(n))"), g("n")); // log(n) is a single log term. - assert_eq!(g("log(n)"), exact_growth(vec![term(&[], &[], &[("n", 1)])])); + assert_eq!(g("log(n)"), exact(vec![term(&[], &[], &[("n", 1)])])); // log(n*m) ≍ log n + log m (two summands, not a product). assert_eq!(terms_of(&g("log(n*m)")).len(), 2); // log of a constant is O(1). @@ -554,7 +629,7 @@ fn test_growth_log_levels() { // A mixed monomial's log keeps *every* factor class: log(2^n * m) ≍ n + log m. // The exponential factor must not swallow the polynomial one. let mixed = g("log(2^n * m)"); - let expected = exact_growth(vec![ + let expected = exact(vec![ term(&[], &[("n", 1.0)], &[]), term(&[], &[], &[("m", 1)]), ]); @@ -590,17 +665,17 @@ fn test_growth_antichain_cap_reports_overflow() { .map(|variable| term(&[], &[(variable, 1.0)], &[])) .collect(); - let at_cap = exact_growth(terms[..ANTICHAIN_CAP].to_vec()); + let at_cap = exact(terms[..ANTICHAIN_CAP].to_vec()); assert_eq!(terms_of(&at_cap).len(), ANTICHAIN_CAP); - let overflow = exact_growth(terms.clone()); + let overflow = exact(terms.clone()); assert!(matches!( overflow.failures(), Some([GrowthFailure::AntichainLimitExceeded { limit, terms }]) if *limit == ANTICHAIN_CAP && *terms == ANTICHAIN_CAP + 1 )); - let reversed = exact_growth( + let reversed = exact( vars.iter() .rev() .map(|variable| term(&[], &[(variable, 1.0)], &[])) @@ -622,7 +697,7 @@ fn test_growth_rejects_large_exponential_antichain() { }) .collect::>(); - let growth = exact_growth(terms); + let growth = exact(terms); assert!(matches!( growth.failures(), Some([GrowthFailure::AntichainLimitExceeded { limit, terms }]) @@ -761,26 +836,46 @@ fn gen_exponential_base(rng: &mut SplitMix64, bases: &[f64]) -> Expr { expression_from_approximation(bases[rng.below(bases.len() as u64) as usize]) } -fn gen_expr(rng: &mut SplitMix64, depth: u32, exponential_bases: &[f64]) -> Expr { +/// Generator knobs: the exponential bases and the leaf generator. +#[derive(Clone, Copy)] +struct GenConfig { + exponential_bases: &'static [f64], + leaf: fn(&mut SplitMix64) -> Expr, +} + +const STABLE: GenConfig = GenConfig { + exponential_bases: STABLE_EXPONENTIAL_BASES, + leaf: gen_leaf, +}; + +/// Constant leaves can hold off an exact term past the finite observation +/// window (`(192 + sqrt(m))^3` looks like `m^0` until `m ≈ 2^15`), which +/// breaks the numeric lower-bound check but not the upper-bound one. +const STABLE_VARIABLE_LEAVES: GenConfig = GenConfig { + exponential_bases: STABLE_EXPONENTIAL_BASES, + leaf: gen_var, +}; + +const ADVERSARIAL: GenConfig = GenConfig { + exponential_bases: ADVERSARIAL_EXPONENTIAL_BASES, + leaf: gen_leaf, +}; + +fn gen_expr(rng: &mut SplitMix64, depth: u32, config: GenConfig) -> Expr { + let exponential_bases = config.exponential_bases; if depth == 0 { - return gen_leaf(rng); + return (config.leaf)(rng); } match rng.below(100) { - 0..=19 => gen_leaf(rng), - 20..=39 => { - gen_expr(rng, depth - 1, exponential_bases) - + gen_expr(rng, depth - 1, exponential_bases) - } - 40..=54 => { - gen_expr(rng, depth - 1, exponential_bases) - * gen_expr(rng, depth - 1, exponential_bases) - } + 0..=19 => (config.leaf)(rng), + 20..=39 => gen_expr(rng, depth - 1, config) + gen_expr(rng, depth - 1, config), + 40..=54 => gen_expr(rng, depth - 1, config) * gen_expr(rng, depth - 1, config), 55..=69 => Expr::pow( - gen_expr(rng, depth - 1, exponential_bases), + gen_expr(rng, depth - 1, config), Expr::integer(1 + rng.below(3)), ), - 70..=79 => Expr::sqrt(gen_expr(rng, depth - 1, exponential_bases)), - 80..=89 => Expr::log(gen_expr(rng, depth - 1, exponential_bases)), + 70..=79 => Expr::sqrt(gen_expr(rng, depth - 1, config)), + 80..=89 => Expr::log(gen_expr(rng, depth - 1, config)), 90..=95 => Expr::pow( gen_exponential_base(rng, exponential_bases), gen_linear(rng), @@ -854,6 +949,13 @@ struct UbResult { /// `broken_from_expr`. Parameterizing here is what gives the harness teeth: the /// exact same code must accept the sound transfer and reject the broken one. fn run_upper_bound(transfer: fn(&Expr) -> Growth, seed: u64, iters: usize) -> UbResult { + run_bound(transfer, seed, iters, false) +} + +/// With `lower`, check only growths reported [`ParameterRelation::Exact`], and +/// check them in the other direction: `growth ≤ C · e` (non-exact results are +/// counted as `unknown`). +fn run_bound(transfer: fn(&Expr) -> Growth, seed: u64, iters: usize, lower: bool) -> UbResult { // Anchor 2^6; check at 2^8, 2^10, 2^12 — all *larger* than the anchor. let anchor = 64_u64; let large = [256_u64, 1024, 4096]; @@ -863,11 +965,16 @@ fn run_upper_bound(transfer: fn(&Expr) -> Growth, seed: u64, iters: usize) -> Ub let mut r = UbResult::default(); for _ in 0..iters { - let e = gen_expr(&mut rng, MAX_DEPTH, STABLE_EXPONENTIAL_BASES); + let config = if lower { + STABLE_VARIABLE_LEAVES + } else { + STABLE + }; + let e = gen_expr(&mut rng, MAX_DEPTH, config); let g = transfer(&e); let gexpr = match g.to_expr() { - Some(x) => x, - None => { + Some(x) if !lower || g.relation() == Some(ParameterRelation::Exact) => x, + _ => { r.unknown += 1; continue; } @@ -890,7 +997,8 @@ fn run_upper_bound(transfer: fn(&Expr) -> Growth, seed: u64, iters: usize) -> Ub r.skipped += 1; continue; } - let c = (ve0 / vg0) * slack; + let (bounded0, bound0) = if lower { (vg0, ve0) } else { (ve0, vg0) }; + let c = (bounded0 / bound0) * slack; let mut conclusive = false; for &s in &large { @@ -907,12 +1015,12 @@ fn run_upper_bound(transfer: fn(&Expr) -> Growth, seed: u64, iters: usize) -> Ub } // Both finite and positive: a real, decidable comparison. conclusive = true; - let bound = c * vg; - if ve > bound { + let (bounded, bound) = if lower { (vg, c * ve) } else { (ve, c * vg) }; + if bounded > bound { r.violations += 1; if r.first_violation.is_none() { r.first_violation = Some(format!( - "e = {e} | g = {gexpr} | s = {s}: eval(e) = {ve} > {c} * {vg} = {bound}" + "e = {e} | g = {gexpr} | s = {s}: {bounded} > {bound} (eval(e) = {ve}, eval(g) = {vg}, C = {c})" )); } } @@ -997,6 +1105,56 @@ fn test_growth_property_upper_bound_negative_control() { ); } +/// Every growth reported exact is also a lower bound: `growth ≤ C · e`. +#[test] +fn test_growth_property_exact_lower_bound_sound() { + let r = run_bound(Growth::from_expr, MASTER_SEED ^ 0x04, UB_ITERS, true); + assert_eq!( + r.violations, + 0, + "lower-bound violation ({} total); first: {}", + r.violations, + r.first_violation.as_deref().unwrap_or("") + ); + assert!( + r.meaningful >= 3000, + "need >= 3000 meaningful exact checks, got {} (non-exact {}, skipped {})", + r.meaningful, + r.unknown, + r.skipped + ); +} + +/// A deliberately broken transfer function: a top-level `Add` returns the +/// *product* of its summands' growths and claims it exact. This is still an +/// upper bound, but not a lower one, so the lower-bound harness must fail. +fn overgrown_from_expr(expression: &Expr) -> Growth { + match expression.node() { + ExprNode::Add(values) => { + let product = values + .iter() + .map(Growth::from_expr) + .reduce(mul) + .expect("normalized sum has at least two terms"); + match product.failures() { + Some(_) => product, + None => exact(terms_of(&product).to_vec()), + } + } + _ => Growth::from_expr(expression), + } +} + +#[test] +fn test_growth_property_exact_lower_bound_negative_control() { + let r = run_bound(overgrown_from_expr, MASTER_SEED ^ 0x04, UB_ITERS, true); + assert!( + r.violations > 0, + "harness failed to catch the seeded Add bug (meaningful {})", + r.meaningful + ); +} + // --- Contract 2: idempotence --- fn term_approx_eq(x: &GrowthTerm, y: &GrowthTerm) -> bool { @@ -1006,7 +1164,7 @@ fn term_approx_eq(x: &GrowthTerm, y: &GrowthTerm) -> bool { fn growth_approx_eq(a: &Growth, b: &Growth) -> bool { match (&a.0, &b.0) { (GrowthState::Unknown(_), GrowthState::Unknown(_)) => true, - (GrowthState::Known(ta), GrowthState::Known(tb)) => { + (GrowthState::Known { terms: ta, .. }, GrowthState::Known { terms: tb, .. }) => { ta.len() == tb.len() && ta.iter().all(|t| tb.iter().any(|u| term_approx_eq(t, u))) && tb.iter().all(|u| ta.iter().any(|t| term_approx_eq(t, u))) @@ -1024,7 +1182,7 @@ fn test_growth_property_idempotence() { for _ in 0..UB_ITERS { // Idempotence is purely symbolic, so it can safely exercise bases near // one whose numeric crossover lies far beyond the f64 test window. - let e = gen_expr(&mut rng, MAX_DEPTH, ADVERSARIAL_EXPONENTIAL_BASES); + let e = gen_expr(&mut rng, MAX_DEPTH, ADVERSARIAL); let g = Growth::from_expr(&e); let rendered = match g.to_expr() { Some(x) => x, From 0b41f6beba60c06db704ecf4200017f789ab8b1f Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Tue, 27 Oct 2026 06:57:18 -0700 Subject: [PATCH 2/2] Bound the magnitude of logarithms of decaying terms log_term dropped negative-weight atoms, so log(exp(-n)) = -n got growth O(1): a signed bound, not a magnitude bound. That made the dominance rule in add report n + log(exp(-n)) + 1 as exact O(n), and log(exp(-n))^2 as O(1). Every atom now contributes regardless of sign. Also adds signed shapes to the property generator and checks that exact registered complexities stay exact on round trip. Co-Authored-By: Claude Opus 5.5 --- src/growth.rs | 19 ++++++++------- src/unit_tests/growth.rs | 51 ++++++++++++++++++++++++++++++++++++++-- 2 files changed, 59 insertions(+), 11 deletions(-) diff --git a/src/growth.rs b/src/growth.rs index 121d1748b..0e05679fb 100644 --- a/src/growth.rs +++ b/src/growth.rs @@ -31,7 +31,9 @@ //! asymptotic statements quantify over all variables growing together //! (`∃N: ∀ vars ≥ N`). Under these axioms `f + g ≍ max(f, g)` up to a constant //! factor, which licenses `add = antichain union + prune`. Every known growth is -//! an **upper** bound; [`Growth::relation`] reports +//! an **upper** bound on the expression's magnitude, including subexpressions +//! that are negative (a subtracted summand, `log` of a decaying term); +//! [`Growth::relation`] reports //! [`ParameterRelation::Exact`] when it is also a lower bound (`f = Θ(growth)`) //! and [`ParameterRelation::UpperBound`] when any step below widened it. //! @@ -1140,8 +1142,8 @@ fn known(terms: Vec, relation: ParameterRelation) -> Growth { } /// Antichain union (asymptotic `+ ≍ max`). The sum stays exact when every -/// widened summand is strictly dominated by an exact one: a widened summand, -/// even a subtracted one, is then `o` of the exact part. +/// widened summand is strictly dominated by an exact one: growths bound +/// magnitudes, so a widened summand, even a negative one, is `o` of the exact part. fn add(a: Growth, b: Growth) -> Growth { if a.failures().is_some() || b.failures().is_some() { return merge_unknown(a, b); @@ -1229,18 +1231,17 @@ fn log_is_exact(t: &GrowthTerm) -> bool { } /// `log` of a single term, returned as its own (small) antichain of summands: -/// `ln exp(Σ w · atom) = Σ w · atom`, so every atom with a possibly positive -/// weight contributes the growth of the atom itself. None may be dropped (e.g. +/// `|ln exp(Σ w · atom)| ≤ Σ |w| · atom`, so every atom contributes the growth +/// of the atom itself, whatever its sign: a decaying term has a large negative +/// logarithm (`log(exp(-n)) = -n`), and growths bound magnitudes so that sums +/// and powers stay sound. Dominated summands are pruned. None may be dropped (e.g. /// `log(2^n·m)` is `n + log m`, not `n`); `prune` then collapses /// any dominated summands (so `log(2^n·n^2)` reduces back to `n`). `ln ln ln v` /// widens to `ln ln v`. fn log_term(t: &GrowthTerm) -> Vec { let one = BigRational::one(); let mut out = Vec::new(); - for (atom, weight) in &t.atoms { - if matches!(weight_sign(weight), Sign::Negative | Sign::Zero) { - continue; - } + for atom in t.atoms.keys() { out.push(match atom { Atom::Mono(monomial) => GrowthTerm::from_atoms(monomial.iter().flat_map( |(variable, (power, log_power))| { diff --git a/src/unit_tests/growth.rs b/src/unit_tests/growth.rs index af15bfc7b..7cf5a6fa0 100644 --- a/src/unit_tests/growth.rs +++ b/src/unit_tests/growth.rs @@ -207,8 +207,19 @@ fn test_every_registered_complexity_uses_the_shared_analysis() { let expression = Expr::parse(entry.complexity); let growth = Growth::from_expr(&expression); if let Some(rendered) = growth.to_expr() { + let reparsed = Growth::from_expr(&rendered); + // A rendered upper bound may legitimately re-parse as exact, but an + // exact normal form must stay exact. + if growth.relation() == Some(ParameterRelation::Exact) { + assert_eq!( + reparsed.relation(), + growth.relation(), + "{}", + entry.complexity + ); + } assert_eq!( - terms_of(&Growth::from_expr(&rendered)), + terms_of(&reparsed), terms_of(&growth), "{}: {}", entry.name, @@ -351,6 +362,33 @@ fn test_growth_relation() { assert_eq!(g("2^(2^n)").relation(), None); } +/// `log` of a decaying term is large and negative; its growth must bound the +/// magnitude, so it can neither be dropped from a sum nor vanish under a power. +#[test] +fn test_growth_log_of_decaying_term_bounds_magnitude() { + assert_eq!(terms_of(&g("log(exp(-n))")), terms_of(&g("n"))); + assert_eq!(terms_of(&g("log(exp(-n))^2")), terms_of(&g("n^2"))); + assert_eq!(terms_of(&g("log(2^n * 3^(-m))")), terms_of(&g("n + m"))); + for source in [ + "n + log(exp(-n)) + 1", + "n^2 + n*log(exp(-n))", + "log(n) + log(exp(-log(n)))", + "n^(1/2) + log(exp(-(n^(1/2))))", + "n + log(exp(-n))^2", + ] { + assert_eq!( + g(source).relation(), + Some(ParameterRelation::UpperBound), + "{source}" + ); + } + // A dominated decaying logarithm still leaves the sum exact. + assert_eq!( + g("n^2 + log(exp(-n))").relation(), + Some(ParameterRelation::Exact) + ); +} + /// Stirling: `n! ≍ n^(n+1/2)·e^(−n)`, strictly between `(n/e)^n` and `n^n`. #[test] fn test_growth_factorial_stirling() { @@ -880,7 +918,16 @@ fn gen_expr(rng: &mut SplitMix64, depth: u32, config: GenConfig) -> Expr { gen_exponential_base(rng, exponential_bases), gen_linear(rng), ), - 96..=97 => Expr::exp(gen_var(rng)), + 96 => Expr::exp(gen_var(rng)), + // Signed shapes: a subtracted lower-order term (exact through the + // dominance rule) and the negative logarithm of a decaying term. The + // numeric harness cannot witness an undominated decaying logarithm — + // `exp(-x)` underflows f64 past `x ≈ 745` — so that case is pinned by + // `test_growth_log_of_decaying_term_bounds_magnitude`. + 97 => match rng.below(2) { + 0 => gen_var(rng) * gen_var(rng) - gen_var(rng), + _ => Expr::log(Expr::exp(Expr::integer(0) - gen_linear(rng))), + }, 98 => match rng.below(3) { 0 => Expr::pow( gen_exponential_base(rng, exponential_bases),