phop_core/analyze.rs
1//! Layer D⁺ — post-discovery analysis of a recovered law via the `oxieml` computer-algebra system.
2//!
3//! A discovered expression is a live [`oxieml::EmlTree`], not a string, so the whole CAS applies
4//! to it directly: symbolic **differentiation**, **antidifferentiation**, **series** expansion,
5//! **limits**, and **certified** root finding (interval Newton/Krawczyk) — all in-ecosystem, with
6//! no round-trip through an external tool. This realizes phop's "discover → analyze → verify"
7//! pipeline, which string-emitting symbolic-regression tools cannot offer without external glue.
8//!
9//! Operations lower the tree to `oxieml`'s `LoweredOp` IR (`EmlTree::lower`) and delegate; the
10//! results are simplified and rendered to LaTeX. Certified roots come back as an
11//! [`oxieml::RootCertificate`] that proves unique existence / no root / indeterminacy in an
12//! interval enclosure.
13
14use crate::error::{PhopError, Result};
15use oxieml::numeric_verified::{find_root_verified, RootOpts};
16use oxieml::{
17 EmlTree, EvalCtx, IntegrateResult, IntervalLO, LimitPoint, LimitResult, RootCertificate,
18};
19
20/// Rendered symbolic analysis of a discovered law (each form simplified, as LaTeX).
21#[derive(Debug, Clone)]
22pub struct Analysis {
23 /// The canonical law itself.
24 pub latex: String,
25 /// `d/d x_wrt` of the law.
26 pub derivative: String,
27 /// An antiderivative `∫ · d x_wrt`, or `None` if the CAS finds no closed form.
28 pub antiderivative: Option<String>,
29 /// Maclaurin series in `x_wrt` to the requested order, or `None` if it could not be formed.
30 pub maclaurin: Option<String>,
31 /// `lim x_wrt → +∞` of the law, if it is finite.
32 pub limit_pos_inf: Option<f64>,
33}
34
35/// Differentiate, integrate, expand, and take the `+∞` limit of `tree` with respect to variable
36/// `wrt`, rendering each canonical form to LaTeX. `series_order` is the Maclaurin truncation order.
37#[must_use]
38pub fn analyze(tree: &EmlTree, wrt: usize, series_order: usize) -> Analysis {
39 let f = tree.lower().simplify();
40 let derivative = f.grad(wrt).simplify().to_latex();
41 let antiderivative = match f.integrate(wrt) {
42 IntegrateResult::Closed(g) => Some(g.simplify().to_latex()),
43 IntegrateResult::Unsupported => None,
44 };
45 let maclaurin = f
46 .maclaurin(wrt, series_order)
47 .ok()
48 .map(|s| s.simplify().to_latex());
49 let limit_pos_inf = match f.limit(wrt, LimitPoint::PosInf) {
50 LimitResult::Finite(v) => Some(v),
51 _ => None,
52 };
53 Analysis {
54 latex: f.to_latex(),
55 derivative,
56 antiderivative,
57 maclaurin,
58 limit_pos_inf,
59 }
60}
61
62/// Find a **certified** root of `tree` in `[lo, hi]` along variable `wrt`, with the other variables
63/// fixed to `others` (the `wrt` slot is overwritten by the search; pass `&[]` for a single-variable
64/// law). Uses `oxieml`'s interval Newton/Krawczyk verifier; the returned [`RootCertificate`] proves
65/// unique existence, absence, or indeterminacy within the interval enclosure.
66///
67/// # Errors
68/// Returns [`PhopError::Symbolic`] if the verifier errors.
69pub fn certified_root(
70 tree: &EmlTree,
71 wrt: usize,
72 others: &[f64],
73 lo: f64,
74 hi: f64,
75) -> Result<RootCertificate> {
76 let expr = tree.lower();
77 let ctx = EvalCtx::new(others);
78 find_root_verified(&expr, wrt, &ctx, lo, hi, &RootOpts::default())
79 .map_err(|e| PhopError::Symbolic(format!("certified root finding failed: {e:?}")))
80}
81
82/// A **guaranteed** enclosure of the law's range over an axis-aligned box, via interval arithmetic.
83///
84/// `domain` gives `[lo, hi]` for each variable; the returned `(lo, hi)` is a sound enclosure: every
85/// value the law takes on the box lies within it (`f(x) ∈ [lo, hi]` for all `x` in the box). This is
86/// the second half of "certified discovery" — alongside [`certified_root`] — and lets a recovered
87/// law come with proven bounds (sign, monotone bracketing, safety envelopes), which no
88/// string-emitting symbolic-regression tool offers.
89#[must_use]
90pub fn certified_range(tree: &EmlTree, domain: &[(f64, f64)]) -> (f64, f64) {
91 let ivs: Vec<IntervalLO> = domain
92 .iter()
93 .map(|&(lo, hi)| IntervalLO::new(lo, hi))
94 .collect();
95 let r = tree.lower().eval_interval(&ivs);
96 (r.lo, r.hi)
97}
98
99#[cfg(test)]
100mod tests {
101 use super::*;
102 use oxieml::RootStatus;
103
104 #[test]
105 fn analyze_exp_derivative_and_integral() {
106 // eml(x0, 1) = exp(x0). d/dx exp = exp ; ∫ exp dx = exp.
107 let tree = EmlTree::eml(&EmlTree::var(0), &EmlTree::one());
108 let f = tree.lower();
109
110 // Symbolic derivative evaluated numerically: (exp)'(0.7) = exp(0.7).
111 let d = f.grad(0);
112 assert!(
113 (d.eval(&[0.7]) - 0.7_f64.exp()).abs() < 1e-6,
114 "d/dx mismatch: {}",
115 d.eval(&[0.7])
116 );
117
118 // Antiderivative F with F'(x) ≈ exp(x).
119 let integ_ok = match f.integrate(0) {
120 IntegrateResult::Closed(g) => (g.grad(0).eval(&[0.4]) - 0.4_f64.exp()).abs() < 1e-5,
121 IntegrateResult::Unsupported => false,
122 };
123 assert!(integ_ok, "expected a closed antiderivative for exp");
124
125 // Rendered analysis is populated.
126 let a = analyze(&tree, 0, 4);
127 assert!(!a.latex.is_empty() && !a.derivative.is_empty());
128 }
129
130 #[test]
131 fn certified_range_encloses_exp() {
132 // exp(x0) over x0 ∈ [0, 1] has true range [1, e]; the interval enclosure must contain it.
133 let tree = EmlTree::eml(&EmlTree::var(0), &EmlTree::one());
134 let (lo, hi) = certified_range(&tree, &[(0.0, 1.0)]);
135 assert!(lo <= 1.0 + 1e-9, "lower bound {lo} should be ≤ 1");
136 assert!(
137 hi >= std::f64::consts::E - 1e-9,
138 "upper bound {hi} should be ≥ e"
139 );
140 }
141
142 #[test]
143 fn certified_root_brackets_known_zero() {
144 // eml(x0, e) = exp(x0) - ln(e) = exp(x0) - 1, whose unique root is x0 = 0.
145 let tree = EmlTree::eml(&EmlTree::var(0), &EmlTree::const_val(std::f64::consts::E));
146 let cert = certified_root(&tree, 0, &[], -1.0, 1.0).expect("verifier ran");
147 assert!(
148 matches!(cert.status, RootStatus::UniqueExists),
149 "expected a certified unique root, got {:?}",
150 cert.status
151 );
152 assert!(
153 cert.enclosure.contains(0.0),
154 "enclosure must bracket the root x0 = 0"
155 );
156 }
157}