nx_calc_integrate.nx source
↩ module page · 171 lines · 5829 B
1// nx_calc_integrate.nx -- symbolic integration engine.
2//
3// Per the comparison commit's named LOSE_BIG improvement vs
4// Mathematica: "ship symbolic Integrate + Series + Solve".
5// This commit ships Integrate. Series and Solve are queued.
6//
7// Pattern-matched antiderivative rules (the standard textbook table).
8// Returns a *Term that downstream proofs can verify by differentiating
9// and checking the result equals the integrand (the Fundamental
10// Theorem of Calculus check, doable via nx_calc_deriv + EQ check).
11
12// nx_safety_envelope:
13// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
14// sil_target: SIL1
15// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
16// verdict: NOT_YET_EVALUATED
17
18import "nx_calc.nx"
19
20// Sentinel symbol for "unintegrable in this engine" results.
21// Caller checks: if result.sym == NX_INTEG_UNKNOWN, expand the table.
22const NX_INTEG_UNKNOWN: nx_int = 414099
23
24func nx_calc_unknown() -> *Term {
25 return nx_term_const(NX_INTEG_UNKNOWN)
26}
27
28// Build (-cos x).
29func nx_calc_neg_cos(t: *Term) -> *Term {
30 return nx_calc_un(NX_CALC_SYM_NEG, nx_calc_cos(t))
31}
32
33// Integrate(f, x):
34// integrate(c) = c * x
35// integrate(x) = x^2 / 2
36// integrate(x^n) = x^(n+1) / (n+1) (n is a CONST != -1)
37// integrate(1/x) = ln(x)
38// integrate(sin(x)) = -cos(x)
39// integrate(cos(x)) = sin(x)
40// integrate(exp(x)) = exp(x)
41// integrate(a + b) = integrate(a) + integrate(b)
42// integrate(c * f(x)) = c * integrate(f(x)) (c is constant)
43//
44// For inputs that don't match: return NX_INTEG_UNKNOWN sentinel so
45// callers can either fall back to numeric or extend the table.
46func nx_calc_integrate(t: *Term, var_id: nx_int) -> *Term {
47 let x: *Term = nx_term_var(var_id)
48
49 // VAR matching the integration variable -> x^2 / 2
50 if t.kind == NX_TERM_VAR {
51 if t.sym == var_id {
52 let two: *Term = nx_calc_const_int(2)
53 let xsq: *Term = nx_calc_pow(x, two)
54 return nx_calc_bin(NX_CALC_SYM_DIV, xsq, two)
55 }
56 // Different variable -- treat as constant.
57 return nx_calc_mul(t, x)
58 }
59
60 // CONST -> c * x
61 if t.kind == NX_TERM_CONST {
62 return nx_calc_mul(t, x)
63 }
64
65 // CONST wrapper c (from nx_calc_const_int)
66 if t.sym == NX_CALC_SYM_CONST {
67 return nx_calc_mul(t, x)
68 }
69
70 // Sum -> distributed
71 if t.sym == NX_CALC_SYM_ADD {
72 let a: *Term = nx_term_arg(t, 0)
73 let b: *Term = nx_term_arg(t, 1)
74 return nx_calc_add(nx_calc_integrate(a, var_id),
75 nx_calc_integrate(b, var_id))
76 }
77
78 // Difference -> distributed
79 if t.sym == NX_CALC_SYM_SUB {
80 let a: *Term = nx_term_arg(t, 0)
81 let b: *Term = nx_term_arg(t, 1)
82 return nx_calc_sub(nx_calc_integrate(a, var_id),
83 nx_calc_integrate(b, var_id))
84 }
85
86 // Constant times function -- factor out.
87 if t.sym == NX_CALC_SYM_MUL {
88 let a: *Term = nx_term_arg(t, 0)
89 let b: *Term = nx_term_arg(t, 1)
90 // a is a constant? Two cases: literal CONST, or wrapped const.
91 if a.kind == NX_TERM_CONST {
92 return nx_calc_mul(a, nx_calc_integrate(b, var_id))
93 }
94 if a.sym == NX_CALC_SYM_CONST {
95 return nx_calc_mul(a, nx_calc_integrate(b, var_id))
96 }
97 if b.kind == NX_TERM_CONST {
98 return nx_calc_mul(b, nx_calc_integrate(a, var_id))
99 }
100 if b.sym == NX_CALC_SYM_CONST {
101 return nx_calc_mul(b, nx_calc_integrate(a, var_id))
102 }
103 // Product of two non-constant Terms -- requires integration by
104 // parts. Named follow-up: implement IBP heuristic.
105 return nx_calc_unknown()
106 }
107
108 // Power: integrate(x^n) = x^(n+1) / (n+1) when n != -1.
109 if t.sym == NX_CALC_SYM_POW {
110 let base: *Term = nx_term_arg(t, 0)
111 let exp_t: *Term = nx_term_arg(t, 1)
112 // base must be the integration variable.
113 if base.kind == NX_TERM_VAR {
114 if base.sym == var_id {
115 let one: *Term = nx_calc_const_int(1)
116 let new_exp: *Term = nx_calc_add(exp_t, one)
117 let new_pow: *Term = nx_calc_pow(base, new_exp)
118 return nx_calc_bin(NX_CALC_SYM_DIV, new_pow, new_exp)
119 }
120 }
121 return nx_calc_unknown()
122 }
123
124 // Trig and transcendentals.
125 if t.sym == NX_CALC_SYM_SIN {
126 let inner: *Term = nx_term_arg(t, 0)
127 if inner.kind == NX_TERM_VAR {
128 if inner.sym == var_id {
129 return nx_calc_neg_cos(inner)
130 }
131 }
132 return nx_calc_unknown()
133 }
134 if t.sym == NX_CALC_SYM_COS {
135 let inner: *Term = nx_term_arg(t, 0)
136 if inner.kind == NX_TERM_VAR {
137 if inner.sym == var_id {
138 return nx_calc_sin(inner)
139 }
140 }
141 return nx_calc_unknown()
142 }
143 if t.sym == NX_CALC_SYM_EXP {
144 let inner: *Term = nx_term_arg(t, 0)
145 if inner.kind == NX_TERM_VAR {
146 if inner.sym == var_id {
147 return nx_calc_exp(inner)
148 }
149 }
150 return nx_calc_unknown()
151 }
152
153 // 1/x -> ln(x). Encoded as DIV(1, x).
154 if t.sym == NX_CALC_SYM_DIV {
155 let num: *Term = nx_term_arg(t, 0)
156 let den: *Term = nx_term_arg(t, 1)
157 if den.kind == NX_TERM_VAR {
158 if den.sym == var_id {
159 if num.sym == NX_CALC_SYM_CONST {
160 let inner_num: *Term = nx_term_arg(num, 0)
161 if inner_num.sym == 1 {
162 return nx_calc_ln(den)
163 }
164 }
165 }
166 }
167 return nx_calc_unknown()
168 }
169
170 return nx_calc_unknown()
171}