qualia_core_db/specialized_libs/
symbolic_assumptions.rs

1//! **Simplification under assumptions** (Gap analysis §3.3) — CAS simplifications that are
2//! only *valid* when the simplifier knows a variable's sign / nonzero-ness.
3//!
4//! Plain [`simplify`](super::symbolic_algebra::simplify) must stay sound for *all* real
5//! inputs, so it cannot turn `√(x²)` into `x` (that is `|x|`), or `ln(a·b)` into
6//! `ln a + ln b` (the log laws need positivity). This module takes an explicit
7//! [`Assumptions`] set (`x > 0`, `n ≠ 0`, …) and applies exactly those rewrites the
8//! assumptions license — and **no others**. Every rewrite is gated on a *proof* of the
9//! needed sign from the assumptions (see [`Assumptions::is_positive`] etc.); when the sign
10//! cannot be established the node is left untouched (fail-closed: never an unsound rewrite).
11
12use super::symbolic_algebra::{add, c, ln, mul, neg, pow, simplify, sqrt, Expr};
13use std::collections::HashMap;
14
15/// A sign / domain assumption about a single variable.
16#[derive(Debug, Clone, Copy, PartialEq, Eq)]
17pub enum Sign {
18    /// `x > 0`.
19    Positive,
20    /// `x ≥ 0`.
21    NonNegative,
22    /// `x < 0`.
23    Negative,
24    /// `x ≤ 0`.
25    NonPositive,
26    /// `x ≠ 0` (sign unknown).
27    Nonzero,
28}
29
30/// A set of per-variable sign assumptions used to license otherwise-unsound rewrites.
31#[derive(Debug, Clone, Default)]
32pub struct Assumptions {
33    signs: HashMap<String, Sign>,
34}
35
36impl Assumptions {
37    pub fn new() -> Self {
38        Self {
39            signs: HashMap::new(),
40        }
41    }
42
43    /// Assert a sign for `var`. Builder-style (chainable).
44    pub fn assume(mut self, var: &str, sign: Sign) -> Self {
45        self.signs.insert(var.to_string(), sign);
46        self
47    }
48
49    fn var_sign(&self, name: &str) -> Option<Sign> {
50        self.signs.get(name).copied()
51    }
52
53    /// Provable `expr ≥ 0` under these assumptions (a *sufficient* test — `None`-of-proof
54    /// means "unknown", never "negative").
55    pub fn is_nonnegative(&self, e: &Expr) -> bool {
56        match e {
57            Expr::Const(k) => *k >= 0.0,
58            Expr::Var(name) => matches!(
59                self.var_sign(name),
60                Some(Sign::Positive) | Some(Sign::NonNegative)
61            ),
62            // Even integer powers are ≥ 0 for any real base; odd powers inherit the base.
63            Expr::Pow(a, n) => *n % 2 == 0 || self.is_nonnegative(a),
64            Expr::Sqrt(_) | Expr::Exp(_) => true, // real sqrt ≥ 0, exp > 0
65            Expr::Mul(a, b) => {
66                (self.is_nonnegative(a) && self.is_nonnegative(b))
67                    || (self.is_nonpositive(a) && self.is_nonpositive(b))
68            }
69            Expr::Add(a, b) => self.is_nonnegative(a) && self.is_nonnegative(b),
70            Expr::Neg(a) => self.is_nonpositive(a),
71            _ => false,
72        }
73    }
74
75    /// Provable `expr > 0` under these assumptions.
76    pub fn is_positive(&self, e: &Expr) -> bool {
77        match e {
78            Expr::Const(k) => *k > 0.0,
79            Expr::Var(name) => matches!(self.var_sign(name), Some(Sign::Positive)),
80            Expr::Exp(_) => true,
81            Expr::Sqrt(a) => self.is_positive(a),
82            Expr::Pow(a, n) => *n % 2 == 0 && self.is_nonzero(a) || self.is_positive(a),
83            Expr::Mul(a, b) => {
84                (self.is_positive(a) && self.is_positive(b))
85                    || (self.is_negative(a) && self.is_negative(b))
86            }
87            Expr::Add(a, b) => {
88                self.is_positive(a) && self.is_nonnegative(b)
89                    || self.is_nonnegative(a) && self.is_positive(b)
90            }
91            Expr::Neg(a) => self.is_negative(a),
92            _ => false,
93        }
94    }
95
96    /// Provable `expr ≤ 0`.
97    pub fn is_nonpositive(&self, e: &Expr) -> bool {
98        match e {
99            Expr::Const(k) => *k <= 0.0,
100            Expr::Var(name) => matches!(
101                self.var_sign(name),
102                Some(Sign::Negative) | Some(Sign::NonPositive)
103            ),
104            Expr::Neg(a) => self.is_nonnegative(a),
105            _ => false,
106        }
107    }
108
109    /// Provable `expr < 0`.
110    pub fn is_negative(&self, e: &Expr) -> bool {
111        match e {
112            Expr::Const(k) => *k < 0.0,
113            Expr::Var(name) => matches!(self.var_sign(name), Some(Sign::Negative)),
114            Expr::Neg(a) => self.is_positive(a),
115            _ => false,
116        }
117    }
118
119    /// Provable `expr ≠ 0`.
120    pub fn is_nonzero(&self, e: &Expr) -> bool {
121        match e {
122            Expr::Const(k) => *k != 0.0,
123            Expr::Var(name) => matches!(
124                self.var_sign(name),
125                Some(Sign::Positive) | Some(Sign::Negative) | Some(Sign::Nonzero)
126            ),
127            Expr::Exp(_) => true,
128            Expr::Pow(a, _) => self.is_nonzero(a),
129            Expr::Sqrt(a) => self.is_positive(a),
130            Expr::Mul(a, b) => self.is_nonzero(a) && self.is_nonzero(b),
131            Expr::Neg(a) => self.is_nonzero(a),
132            _ => false,
133        }
134    }
135}
136
137/// Simplify `expr` using assumption-gated rewrites on top of the plain (always-sound)
138/// [`simplify`]. Applied to a bounded fixpoint. Rewrites performed (each only when the
139/// assumptions *prove* the side condition):
140///
141/// - `√(x²) → x`           when `x ≥ 0`  (and `→ −x` when `x ≤ 0`)
142/// - `(√x)² → x`           when `x ≥ 0`
143/// - `ln(a·b) → ln a + ln b`   when `a, b > 0`
144/// - `ln(aⁿ) → n·ln a`         when `a > 0`
145pub fn simplify_with_assumptions(expr: &Expr, asm: &Assumptions) -> Expr {
146    let mut cur = simplify(expr);
147    for _ in 0..16 {
148        let next = simplify(&rewrite(&cur, asm));
149        if next == cur {
150            break;
151        }
152        cur = next;
153    }
154    cur
155}
156
157fn rewrite(e: &Expr, asm: &Assumptions) -> Expr {
158    // Rewrite children first (bottom-up).
159    let e = match e {
160        Expr::Add(a, b) => add(rewrite(a, asm), rewrite(b, asm)),
161        Expr::Sub(a, b) => Expr::Sub(Box::new(rewrite(a, asm)), Box::new(rewrite(b, asm))),
162        Expr::Mul(a, b) => mul(rewrite(a, asm), rewrite(b, asm)),
163        Expr::Div(a, b) => Expr::Div(Box::new(rewrite(a, asm)), Box::new(rewrite(b, asm))),
164        Expr::Pow(a, n) => pow(rewrite(a, asm), *n),
165        Expr::Neg(a) => neg(rewrite(a, asm)),
166        Expr::Sqrt(a) => sqrt(rewrite(a, asm)),
167        Expr::Exp(a) => Expr::Exp(Box::new(rewrite(a, asm))),
168        Expr::Ln(a) => ln(rewrite(a, asm)),
169        Expr::Sin(a) => Expr::Sin(Box::new(rewrite(a, asm))),
170        Expr::Cos(a) => Expr::Cos(Box::new(rewrite(a, asm))),
171        Expr::Tan(a) => Expr::Tan(Box::new(rewrite(a, asm))),
172        Expr::Const(_) | Expr::Var(_) => e.clone(),
173    };
174
175    match &e {
176        // √(x²) → x (x≥0) / −x (x≤0).
177        Expr::Sqrt(inner) => {
178            if let Expr::Pow(base, 2) = &**inner {
179                if asm.is_nonnegative(base) {
180                    return (**base).clone();
181                }
182                if asm.is_nonpositive(base) {
183                    return neg((**base).clone());
184                }
185            }
186            e
187        }
188        // (√x)² → x  when x ≥ 0.
189        Expr::Pow(base, 2) => {
190            if let Expr::Sqrt(under) = &**base {
191                if asm.is_nonnegative(under) {
192                    return (**under).clone();
193                }
194            }
195            e
196        }
197        // ln laws under positivity.
198        Expr::Ln(arg) => match &**arg {
199            Expr::Mul(a, b) if asm.is_positive(a) && asm.is_positive(b) => {
200                add(ln((**a).clone()), ln((**b).clone()))
201            }
202            Expr::Pow(a, n) if asm.is_positive(a) => mul(c(*n as f64), ln((**a).clone())),
203            _ => e,
204        },
205        _ => e,
206    }
207}
208
209#[cfg(test)]
210mod tests {
211    use super::super::symbolic_algebra::{c, exp, mul, pow, sqrt, var};
212    use super::*;
213
214    #[test]
215    fn sqrt_of_square_uses_sign() {
216        // √(x²) → x when x ≥ 0.
217        let pos = Assumptions::new().assume("x", Sign::Positive);
218        assert_eq!(
219            simplify_with_assumptions(&sqrt(pow(var("x"), 2)), &pos),
220            var("x")
221        );
222        // → −x when x ≤ 0.
223        let neg_x = Assumptions::new().assume("x", Sign::Negative);
224        assert_eq!(
225            simplify_with_assumptions(&sqrt(pow(var("x"), 2)), &neg_x),
226            neg(var("x"))
227        );
228        // Unknown sign → left as √(x²) (no unsound rewrite).
229        let unknown = Assumptions::new();
230        let s = simplify_with_assumptions(&sqrt(pow(var("x"), 2)), &unknown);
231        assert_eq!(s, sqrt(pow(var("x"), 2)));
232    }
233
234    #[test]
235    fn sqrt_square_inverse() {
236        // (√x)² → x when x ≥ 0.
237        let asm = Assumptions::new().assume("x", Sign::NonNegative);
238        assert_eq!(
239            simplify_with_assumptions(&pow(sqrt(var("x")), 2), &asm),
240            var("x")
241        );
242    }
243
244    #[test]
245    fn log_laws_need_positivity() {
246        let asm = Assumptions::new()
247            .assume("a", Sign::Positive)
248            .assume("b", Sign::Positive);
249        // ln(a·b) → ln a + ln b ; numerically equal at a sample point.
250        let got = simplify_with_assumptions(&ln(mul(var("a"), var("b"))), &asm);
251        let mut env = HashMap::new();
252        env.insert("a".to_string(), 3.0);
253        env.insert("b".to_string(), 5.0);
254        assert!((got.eval(&env).unwrap() - (15.0_f64).ln()).abs() < 1e-9);
255        assert_eq!(got, add(ln(var("a")), ln(var("b"))));
256        // ln(a³) → 3·ln a.
257        let got2 = simplify_with_assumptions(&ln(pow(var("a"), 3)), &asm);
258        assert_eq!(got2, mul(c(3.0), ln(var("a"))));
259        // Without the positivity assumption, no rewrite.
260        let none = Assumptions::new();
261        assert_eq!(
262            simplify_with_assumptions(&ln(mul(var("a"), var("b"))), &none),
263            ln(mul(var("a"), var("b")))
264        );
265    }
266
267    #[test]
268    fn sign_inference_basics() {
269        let asm = Assumptions::new().assume("x", Sign::Positive);
270        assert!(asm.is_positive(&exp(var("x"))));
271        assert!(asm.is_nonnegative(&pow(var("y"), 2))); // even power, any base
272        assert!(asm.is_nonzero(&var("x")));
273        assert!(!asm.is_positive(&var("y"))); // unknown
274    }
275}
qualia_core_db/specialized_libs/symbolic_assumptions.rs

qualia_core_db/specialized_libs/
symbolic_assumptions.rs
