nx_calc.nx source

1// nx_calc.nx -- symbolic calculus engine. 2// 3// Native NishiLang symbolic differentiation by structural recursion 4// over Term values. No third-party CAS; output is itself a *Term that 5// downstream proofs can manipulate via SUBST/EQ_TRANS in the v2 kernel. 6// 7// Patent-clean implementation: standard derivative rules from any 8// calculus textbook. 9 10// nx_safety_envelope: 11// intended_use: AUTO_APPLIED -- primitive-specific tuning queued 12// sil_target: SIL1 13// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail] 14// verdict: NOT_YET_EVALUATED 15 16import "nx_kernel_v2.nx" 17 18// ===== Sym IDs (calc family 414xxx) ================================= 19const NX_CALC_SYM_X: nx_int = 414001 // distinguished variable 20const NX_CALC_SYM_ADD: nx_int = 414002 21const NX_CALC_SYM_SUB: nx_int = 414003 22const NX_CALC_SYM_MUL: nx_int = 414004 23const NX_CALC_SYM_DIV: nx_int = 414005 24const NX_CALC_SYM_POW: nx_int = 414006 25const NX_CALC_SYM_NEG: nx_int = 414007 26const NX_CALC_SYM_SIN: nx_int = 414008 27const NX_CALC_SYM_COS: nx_int = 414009 28const NX_CALC_SYM_EXP: nx_int = 414010 29const NX_CALC_SYM_LN: nx_int = 414011 30const NX_CALC_SYM_CONST: nx_int = 414012 // wraps an integer literal 31 32// ===== Term constructors ============================================ 33func nx_calc_var(var_id: nx_int) -> *Term { 34 return nx_term_var(var_id) 35} 36 37func nx_calc_const_int(n: nx_int) -> *Term { 38 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term 39 arg.kind = NX_TERM_CONST; arg.sym = n; arg.n_args = 0; arg.args = 0 as *Term 40 return nx_term_app(NX_CALC_SYM_CONST, 1, arg) 41} 42 43func nx_calc_x() -> *Term { return nx_term_var(NX_CALC_SYM_X) } 44 45func nx_calc_bin(sym: nx_int, a: *Term, b: *Term) -> *Term { 46 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term 47 let a0: *Term = args 48 a0.kind = a.kind; a0.sym = a.sym; a0.n_args = a.n_args; a0.args = a.args 49 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term 50 a1.kind = b.kind; a1.sym = b.sym; a1.n_args = b.n_args; a1.args = b.args 51 return nx_term_app(sym, 2, args) 52} 53 54func nx_calc_un(sym: nx_int, a: *Term) -> *Term { 55 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term 56 arg.kind = a.kind; arg.sym = a.sym; arg.n_args = a.n_args; arg.args = a.args 57 return nx_term_app(sym, 1, arg) 58} 59 60func nx_calc_add(a: *Term, b: *Term) -> *Term { return nx_calc_bin(NX_CALC_SYM_ADD, a, b) } 61func nx_calc_sub(a: *Term, b: *Term) -> *Term { return nx_calc_bin(NX_CALC_SYM_SUB, a, b) } 62func nx_calc_mul(a: *Term, b: *Term) -> *Term { return nx_calc_bin(NX_CALC_SYM_MUL, a, b) } 63func nx_calc_pow(a: *Term, b: *Term) -> *Term { return nx_calc_bin(NX_CALC_SYM_POW, a, b) } 64func nx_calc_sin(a: *Term) -> *Term { return nx_calc_un(NX_CALC_SYM_SIN, a) } 65func nx_calc_cos(a: *Term) -> *Term { return nx_calc_un(NX_CALC_SYM_COS, a) } 66func nx_calc_exp(a: *Term) -> *Term { return nx_calc_un(NX_CALC_SYM_EXP, a) } 67func nx_calc_ln(a: *Term) -> *Term { return nx_calc_un(NX_CALC_SYM_LN, a) } 68 69// ===== Symbolic differentiation ===================================== 70// 71// nx_calc_deriv(t, var_id) returns the derivative of t wrt the 72// variable-id var_id, as a *Term. Standard rules: 73// d/dx[c] = 0 74// d/dx[x] = 1 75// d/dx[y] = 0 (y != x) 76// d/dx[a + b] = d/dx[a] + d/dx[b] 77// d/dx[a - b] = d/dx[a] - d/dx[b] 78// d/dx[a * b] = (d/dx[a])*b + a*(d/dx[b]) -- product rule 79// d/dx[a^n] = n * a^(n-1) * d/dx[a] -- power-chain rule 80// d/dx[sin a] = cos(a) * d/dx[a] -- chain rule 81// d/dx[cos a] = -sin(a) * d/dx[a] 82// d/dx[exp a] = exp(a) * d/dx[a] 83// d/dx[ln a] = (1/a) * d/dx[a] 84// 85// Output is NOT simplified -- a separate normaliser (nx_rewrite + 86// algebraic identity rules) handles canonicalisation if desired. 87// HOL Light / Mathematica do the same: differentiate first, simplify 88// later. 89 90func nx_calc_deriv(t: *Term, var_id: nx_int) -> *Term { 91 if t.kind == NX_TERM_VAR { 92 if t.sym == var_id { return nx_calc_const_int(1) } 93 return nx_calc_const_int(0) 94 } 95 if t.kind == NX_TERM_CONST { return nx_calc_const_int(0) } 96 97 if t.sym == NX_CALC_SYM_CONST { return nx_calc_const_int(0) } 98 99 if t.sym == NX_CALC_SYM_ADD { 100 return nx_calc_add(nx_calc_deriv(nx_term_arg(t, 0), var_id), 101 nx_calc_deriv(nx_term_arg(t, 1), var_id)) 102 } 103 if t.sym == NX_CALC_SYM_SUB { 104 return nx_calc_sub(nx_calc_deriv(nx_term_arg(t, 0), var_id), 105 nx_calc_deriv(nx_term_arg(t, 1), var_id)) 106 } 107 if t.sym == NX_CALC_SYM_MUL { 108 let a: *Term = nx_term_arg(t, 0) 109 let b: *Term = nx_term_arg(t, 1) 110 let da: *Term = nx_calc_deriv(a, var_id) 111 let db: *Term = nx_calc_deriv(b, var_id) 112 return nx_calc_add(nx_calc_mul(da, b), nx_calc_mul(a, db)) 113 } 114 if t.sym == NX_CALC_SYM_POW { 115 // Assumes exponent is a constant int (most common case); 116 // general case x^x needs exp(x ln x) expansion -- named follow-up. 117 let base: *Term = nx_term_arg(t, 0) 118 let exp_t: *Term = nx_term_arg(t, 1) 119 let new_exp: *Term = nx_calc_sub(exp_t, nx_calc_const_int(1)) 120 let dbase: *Term = nx_calc_deriv(base, var_id) 121 return nx_calc_mul(nx_calc_mul(exp_t, nx_calc_pow(base, new_exp)), dbase) 122 } 123 if t.sym == NX_CALC_SYM_SIN { 124 let inner: *Term = nx_term_arg(t, 0) 125 let dinner: *Term = nx_calc_deriv(inner, var_id) 126 return nx_calc_mul(nx_calc_cos(inner), dinner) 127 } 128 if t.sym == NX_CALC_SYM_COS { 129 let inner: *Term = nx_term_arg(t, 0) 130 let dinner: *Term = nx_calc_deriv(inner, var_id) 131 // -sin(inner) * dinner 132 return nx_calc_mul(nx_calc_un(NX_CALC_SYM_NEG, nx_calc_sin(inner)), dinner) 133 } 134 if t.sym == NX_CALC_SYM_EXP { 135 let inner: *Term = nx_term_arg(t, 0) 136 let dinner: *Term = nx_calc_deriv(inner, var_id) 137 return nx_calc_mul(nx_calc_exp(inner), dinner) 138 } 139 if t.sym == NX_CALC_SYM_LN { 140 let inner: *Term = nx_term_arg(t, 0) 141 let dinner: *Term = nx_calc_deriv(inner, var_id) 142 // (1 / inner) * dinner 143 return nx_calc_mul(nx_calc_bin(NX_CALC_SYM_DIV, nx_calc_const_int(1), inner), dinner) 144 } 145 // Unknown function: return zero (caller can extend by adding cases). 146 return nx_calc_const_int(0) 147}