nx_term_order.nx source

1// nx_term_order.nx -- Knuth-Bendix Order (KBO) over first-order Terms. 2// 3// Per Vampire-displacement roadmap Phase 1 step 1: KBO is the foundation 4// every saturation prover uses to orient rewrites, pick the smaller half 5// of a critical pair, and prune redundant clauses (forward subsumption, 6// demodulation, tautology deletion all depend on it). 7// 8// Knuth + Bendix 1970. Standard formulation: 9// Given: 10// - weight function w : Symbol -> nx_int 11// - precedence > on symbols (total order) 12// - constant w_0 >= 1 (minimum weight; weight of a variable) 13// 14// Admissibility (KBO is well-founded iff): 15// (A1) for every constant c, w(c) >= w_0 16// (A2) if f is a unary symbol with w(f) = 0, then f is maximal in > 17// 18// weight(x) = w_0 for variables x 19// weight(f(t1,..,tn)) = w(f) + sum_i weight(t_i) 20// 21// s >_KBO t iff (for every variable x, count(x, s) >= count(x, t)) 22// AND ONE OF: 23// (W1) weight(s) > weight(t) 24// (W2) weight(s) = weight(t) AND 25// (P1) head(s) > head(t) in precedence, 26// (P2) head(s) = head(t) AND args(s) >_lex args(t) 27// 28// Result is a sealed verdict {GT, EQ, LT, INCOMPARABLE}. 29// 30// Bits-up: pure nx_int arithmetic, no f64, no external library. 31// Result-typed for all fallible API. Scale-agnostic via nx_tier. 32 33// nx_safety_envelope: 34// intended_use: AUTO_APPLIED -- primitive-specific tuning queued 35// sil_target: SIL1 36// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail] 37// verdict: NOT_YET_EVALUATED 38 39import "nx_syscalls.nx" 40import "nx_runtime.nx" 41import "nx_tier.nx" 42import "nx_result.nx" 43import "nx_unify.nx" 44 45// ===== Sealed verdict =============================================== 46const NX_KBO_GT: nx_int = 1 47const NX_KBO_EQ: nx_int = 2 48const NX_KBO_LT: nx_int = 3 49const NX_KBO_INCOMP: nx_int = 4 50 51// ===== State ======================================================== 52// Flat tables indexed by sym_id. Variables are not symbols; they're 53// represented separately in the Term struct (NX_TERM_VAR). 54const NX_KBO_MAX_SYM: nx_int = 1024 55 56struct KboState { 57 weights: *nx_int, // [NX_KBO_MAX_SYM] -- w(f) 58 precedences: *nx_int, // [NX_KBO_MAX_SYM] -- prec(f) (higher = bigger) 59 arities: *nx_int, // [NX_KBO_MAX_SYM] -- declared arity (0 = const) 60 declared: *nx_int, // [NX_KBO_MAX_SYM] -- 1 if symbol has been registered 61 w0: nx_int, // variable weight, also min constant weight 62} 63 64const NX_KBO_STATE_BYTES: nx_int = 40 65 66func nx_kbo_new(w0: nx_int) -> *KboState { 67 let st: *KboState = (sys_mmap(NX_KBO_STATE_BYTES as i64)) as *KboState 68 st.w0 = w0 69 st.weights = (sys_mmap((NX_KBO_MAX_SYM * 8) as i64)) as *nx_int 70 st.precedences = (sys_mmap((NX_KBO_MAX_SYM * 8) as i64)) as *nx_int 71 st.arities = (sys_mmap((NX_KBO_MAX_SYM * 8) as i64)) as *nx_int 72 st.declared = (sys_mmap((NX_KBO_MAX_SYM * 8) as i64)) as *nx_int 73 return st 74} 75 76// Register a symbol. arity 0 means constant; >=1 means function. 77// Returns Result<nx_int, NX_ERR_OUT_OF_RANGE>. 78func nx_kbo_register(st: *KboState, sym_id: nx_int, weight: nx_int, 79 precedence: nx_int, arity: nx_int) -> *NxResult { 80 if sym_id < 0 { return nx_result_err(NX_ERR_OUT_OF_RANGE) } 81 if sym_id >= NX_KBO_MAX_SYM { return nx_result_err(NX_ERR_OUT_OF_RANGE) } 82 if weight < 0 { return nx_result_err(NX_ERR_INVALID_INPUT) } 83 if arity < 0 { return nx_result_err(NX_ERR_INVALID_INPUT) } 84 st.weights[sym_id] = weight 85 st.precedences[sym_id] = precedence 86 st.arities[sym_id] = arity 87 st.declared[sym_id] = 1 88 return nx_result_ok(sym_id) 89} 90 91// ===== Admissibility ================================================ 92// (A1) every constant c has w(c) >= w_0 93// (A2) if f is unary with w(f) = 0, f must be maximal in precedence 94// 95// Returns Result<nx_int, NX_ERR_INVALID_STATE> -- ok value is the 96// number of registered symbols. 97func nx_kbo_check_admissibility(st: *KboState) -> *NxResult { 98 var i: nx_int = 0 99 var max_prec: nx_int = -9223372036854775807 100 var max_prec_sym: nx_int = -1 101 var n_declared: nx_int = 0 102 103 // First pass: find the global precedence maximum. 104 while i < NX_KBO_MAX_SYM { 105 if st.declared[i] == 1 { 106 n_declared = n_declared + 1 107 if st.precedences[i] > max_prec { 108 max_prec = st.precedences[i] 109 max_prec_sym = i 110 } 111 } 112 i = i + 1 113 } 114 115 // Second pass: (A1) every constant >= w_0; (A2) unary weight-0 is max. 116 var j: nx_int = 0 117 while j < NX_KBO_MAX_SYM { 118 if st.declared[j] == 1 { 119 if st.arities[j] == 0 { 120 if st.weights[j] < st.w0 { return nx_result_err(NX_ERR_INVALID_STATE) } 121 } 122 if st.arities[j] == 1 { 123 if st.weights[j] == 0 { 124 if st.precedences[j] != max_prec { return nx_result_err(NX_ERR_INVALID_STATE) } 125 } 126 } 127 } 128 j = j + 1 129 } 130 return nx_result_ok(n_declared) 131} 132 133// ===== Term weight ================================================== 134// weight(x) = w_0 135// weight(f(t1,..,tn)) = w(f) + sum weight(t_i) 136func nx_kbo_weight(st: *KboState, t: *Term) -> nx_int { 137 if t.kind == NX_TERM_VAR { return st.w0 } 138 if t.kind == NX_TERM_CONST { 139 if st.declared[t.sym] == 1 { return st.weights[t.sym] } 140 return st.w0 141 } 142 // APP: w(head) + sum children 143 var total: nx_int = 0 144 if st.declared[t.sym] == 1 { total = st.weights[t.sym] } 145 var i: nx_int = 0 146 while i < t.n_args { 147 total = total + nx_kbo_weight(st, nx_term_arg(t, i)) 148 i = i + 1 149 } 150 return total 151} 152 153// ===== Variable count ============================================== 154// Count occurrences of a specific variable id in a term. 155func nx_kbo_var_count(t: *Term, var_id: nx_int) -> nx_int { 156 if t.kind == NX_TERM_VAR { 157 if t.sym == var_id { return 1 } 158 return 0 159 } 160 if t.kind == NX_TERM_CONST { return 0 } 161 var total: nx_int = 0 162 var i: nx_int = 0 163 while i < t.n_args { 164 total = total + nx_kbo_var_count(nx_term_arg(t, i), var_id) 165 i = i + 1 166 } 167 return total 168} 169 170// "s variable-dominates t" iff for every var_id in [0, max_var_id), 171// count(s, x) >= count(t, x). Caller declares the variable id space. 172// Returns 1 if s dominates t, else 0. 173func nx_kbo_var_dominates(s: *Term, t: *Term, max_var_id: nx_int) -> nx_int { 174 var x: nx_int = 0 175 while x < max_var_id { 176 let cs: nx_int = nx_kbo_var_count(s, x) 177 let ct: nx_int = nx_kbo_var_count(t, x) 178 if cs < ct { return 0 } 179 x = x + 1 180 } 181 return 1 182} 183 184// ===== Precedence comparison ======================================= 185// Returns +1 if a > b, 0 if equal, -1 if a < b. 186// Variables compared by their var_id (only equality matters for KBO). 187func nx_kbo_prec_cmp(st: *KboState, a_sym: nx_int, b_sym: nx_int) -> nx_int { 188 let pa: nx_int = st.precedences[a_sym] 189 let pb: nx_int = st.precedences[b_sym] 190 if pa > pb { return 1 } 191 if pa < pb { return -1 } 192 return 0 193} 194 195// ===== Main KBO comparison ========================================= 196// Returns one of NX_KBO_GT / NX_KBO_EQ / NX_KBO_LT / NX_KBO_INCOMP. 197// 198// max_var_id bounds the variable id space the caller is using. 199func nx_kbo_compare(st: *KboState, s: *Term, t: *Term, max_var_id: nx_int) -> nx_int { 200 // Trivial structural equality first. 201 if nx_term_eq(s, t) == 1 { return NX_KBO_EQ } 202 203 let s_dom_t: nx_int = nx_kbo_var_dominates(s, t, max_var_id) 204 let t_dom_s: nx_int = nx_kbo_var_dominates(t, s, max_var_id) 205 let ws: nx_int = nx_kbo_weight(st, s) 206 let wt: nx_int = nx_kbo_weight(st, t) 207 208 // (W1) strict weight inequality drives the direction 209 if ws > wt { 210 if s_dom_t == 1 { return NX_KBO_GT } 211 return NX_KBO_INCOMP 212 } 213 if wt > ws { 214 if t_dom_s == 1 { return NX_KBO_LT } 215 return NX_KBO_INCOMP 216 } 217 218 // weights equal -- need structural rules; both terms' var sets must 219 // agree (else INCOMP). 220 if s_dom_t == 0 { return NX_KBO_INCOMP } 221 if t_dom_s == 0 { return NX_KBO_INCOMP } 222 223 // If either side is a variable here, since they're equal-weight and 224 // mutually dominating but structurally distinct, they're incomparable. 225 if s.kind == NX_TERM_VAR { return NX_KBO_INCOMP } 226 if t.kind == NX_TERM_VAR { return NX_KBO_INCOMP } 227 228 // (P1) precedence on heads 229 let pc: nx_int = nx_kbo_prec_cmp(st, s.sym, t.sym) 230 if pc > 0 { return NX_KBO_GT } 231 if pc < 0 { return NX_KBO_LT } 232 233 // (P2) same head -- lex comparison on arguments. 234 if s.n_args != t.n_args { return NX_KBO_INCOMP } 235 var i: nx_int = 0 236 while i < s.n_args { 237 let sub: nx_int = nx_kbo_compare(st, nx_term_arg(s, i), nx_term_arg(t, i), max_var_id) 238 if sub == NX_KBO_GT { return NX_KBO_GT } 239 if sub == NX_KBO_LT { return NX_KBO_LT } 240 if sub == NX_KBO_INCOMP { return NX_KBO_INCOMP } 241 // sub == NX_KBO_EQ -- continue to next argument 242 i = i + 1 243 } 244 // All arguments structurally equal AND we got past nx_term_eq above 245 // (which means heads differ somehow). Defensive fallback. 246 return NX_KBO_INCOMP 247} 248 249// ===== Verdict name (for debug) ===================================== 250func nx_kbo_verdict_name(v: nx_int) -> *u8 { 251 if v == NX_KBO_GT { return "GT" as *u8 } 252 if v == NX_KBO_EQ { return "EQ" as *u8 } 253 if v == NX_KBO_LT { return "LT" as *u8 } 254 if v == NX_KBO_INCOMP { return "INCOMP" as *u8 } 255 return "?" as *u8 256}