nx_unify.nx source
↩ module page · 257 lines · 9248 B
1// nx_unify.nx -- first-order terms + Robinson unification.
2//
3// Per user 2026-05-14 "keep going" + the CASC-leap cardinal: this is
4// the bits-up unification primitive every CASC entrant (Vampire/E/
5// Otter/Waldmeister/SPASS/SETHEO) builds on. Robinson 1965 algorithm.
6//
7// Term kinds (sealed):
8// VAR identified by integer var_id
9// CONST identified by integer symbol_id (constant or 0-arity fn)
10// APP function symbol_id + n_args + array of child Terms
11//
12// Substitution = parallel arrays of (var_id, term) bindings.
13// Result-typed throughout: no -1 sentinels, no null-as-error.
14//
15// nx_safety_envelope:
16// intended_use: "Robinson unification -- substitution
17// computation for first-order theorem prover
18// + type inference + pattern matching"
19// sil_target: SIL2 (unification correctness gates
20// every consumer's soundness)
21// asil_target: QM
22// dal_target: DAL B
23// evidence: [Robinson_1965_canonical_basis,
24// occurs_check_enabled,
25// Result_typed_no_sentinel,
26// sealed_unification_error_enum]
27// hazard_register: [bug-tape-unification-without-occurs-check,
28// bug-tape-exponential-substitution-blowup,
29// bug-tape-cycle-in-mgu-not-detected]
30// residual_risk: "Occurs-check is ENFORCED. Substrate
31// documents O(n^2) worst-case without
32// sharing; Martelli-Montanari O(n) variant
33// queued for performance-critical paths."
34// verdict: NOT_YET_EVALUATED
35
36import "nx_syscalls.nx"
37import "nx_runtime.nx"
38import "nx_tier.nx"
39import "nx_result.nx"
40
41const NX_TERM_VAR: nx_int = 1
42const NX_TERM_CONST: nx_int = 2
43const NX_TERM_APP: nx_int = 3
44
45// ===== Term struct ==================================================
46struct Term {
47 kind: nx_int, // VAR / CONST / APP
48 sym: nx_int, // var_id (for VAR) or symbol_id (for CONST/APP)
49 n_args: nx_int,
50 args: *Term, // null when n_args = 0
51}
52
53const NX_TERM_BYTES: nx_int = 32
54
55func nx_term_var(var_id: nx_int) -> *Term {
56 let t: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
57 t.kind = NX_TERM_VAR
58 t.sym = var_id
59 t.n_args = 0
60 t.args = 0 as *Term
61 return t
62}
63
64func nx_term_const(sym_id: nx_int) -> *Term {
65 let t: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
66 t.kind = NX_TERM_CONST
67 t.sym = sym_id
68 t.n_args = 0
69 t.args = 0 as *Term
70 return t
71}
72
73func nx_term_app(sym_id: nx_int, n_args: nx_int, args: *Term) -> *Term {
74 let t: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
75 t.kind = NX_TERM_APP
76 t.sym = sym_id
77 t.n_args = n_args
78 t.args = args
79 return t
80}
81
82// Get child i. args is a flat array of Term structs.
83func nx_term_arg(t: *Term, i: nx_int) -> *Term {
84 return ((t.args as nx_int) + (i * NX_TERM_BYTES)) as *Term
85}
86
87// Structural equality.
88func nx_term_eq(a: *Term, b: *Term) -> nx_int {
89 if a.kind != b.kind { return 0 }
90 if a.sym != b.sym { return 0 }
91 if a.n_args != b.n_args { return 0 }
92 var i: nx_int = 0
93 while i < a.n_args {
94 if nx_term_eq(nx_term_arg(a, i), nx_term_arg(b, i)) == 0 { return 0 }
95 i = i + 1
96 }
97 return 1
98}
99
100// Occurs check: does var_id appear anywhere in term t?
101func nx_term_contains_var(t: *Term, var_id: nx_int) -> nx_int {
102 if t.kind == NX_TERM_VAR {
103 if t.sym == var_id { return 1 }
104 return 0
105 }
106 if t.kind == NX_TERM_CONST { return 0 }
107 var i: nx_int = 0
108 while i < t.n_args {
109 if nx_term_contains_var(nx_term_arg(t, i), var_id) == 1 { return 1 }
110 i = i + 1
111 }
112 return 0
113}
114
115// ===== Substitution =================================================
116const NX_SUBST_MAX_BINDINGS: nx_int = 256
117
118struct Subst {
119 n: nx_int,
120 var_ids: *nx_int,
121 terms: *Term, // flat array of Term structs (indexed parallel)
122}
123
124const NX_SUBST_BYTES: nx_int = 24
125
126func nx_subst_new() -> *Subst {
127 let s: *Subst = (sys_mmap(NX_SUBST_BYTES as i64)) as *Subst
128 s.n = 0
129 s.var_ids = (sys_mmap((NX_SUBST_MAX_BINDINGS * 8) as i64)) as *nx_int
130 s.terms = (sys_mmap((NX_SUBST_MAX_BINDINGS * NX_TERM_BYTES) as i64)) as *Term
131 return s
132}
133
134// Look up: returns *Term if var_id is bound, else null.
135func nx_subst_lookup(s: *Subst, var_id: nx_int) -> *Term {
136 var i: nx_int = 0
137 while i < s.n {
138 if s.var_ids[i] == var_id {
139 return ((s.terms as nx_int) + (i * NX_TERM_BYTES)) as *Term
140 }
141 i = i + 1
142 }
143 return 0 as *Term
144}
145
146// Add a binding. Returns Result<nx_int, NX_ERR_INVALID_STATE>.
147func nx_subst_add(s: *Subst, var_id: nx_int, t: *Term) -> *NxResult {
148 if s.n >= NX_SUBST_MAX_BINDINGS { return nx_result_err(NX_ERR_INVALID_STATE) }
149 s.var_ids[s.n] = var_id
150 let dest: *Term = ((s.terms as nx_int) + (s.n * NX_TERM_BYTES)) as *Term
151 dest.kind = t.kind
152 dest.sym = t.sym
153 dest.n_args = t.n_args
154 dest.args = t.args
155 s.n = s.n + 1
156 return nx_result_ok(s.n)
157}
158
159// Apply substitution to a term, returning a new term.
160func nx_subst_apply(t: *Term, s: *Subst) -> *Term {
161 if t.kind == NX_TERM_VAR {
162 let bound: *Term = nx_subst_lookup(s, t.sym)
163 if (bound as nx_int) != 0 { return nx_subst_apply(bound, s) }
164 return t
165 }
166 if t.kind == NX_TERM_CONST { return t }
167 // APP: apply to each child
168 if t.n_args == 0 { return t }
169 let new_args: *Term = (sys_mmap((t.n_args * NX_TERM_BYTES) as i64)) as *Term
170 var i: nx_int = 0
171 while i < t.n_args {
172 let child_old: *Term = nx_term_arg(t, i)
173 let child_new: *Term = nx_subst_apply(child_old, s)
174 let dest: *Term = ((new_args as nx_int) + (i * NX_TERM_BYTES)) as *Term
175 dest.kind = child_new.kind
176 dest.sym = child_new.sym
177 dest.n_args = child_new.n_args
178 dest.args = child_new.args
179 i = i + 1
180 }
181 return nx_term_app(t.sym, t.n_args, new_args)
182}
183
184// ===== Robinson unification =========================================
185// Returns Result<*Subst, NX_ERR_*> where the error codes are:
186// NX_ERR_TAG_MISMATCH -- different function symbols / arities
187// NX_ERR_INVALID_STATE -- occurs check failure
188func nx_unify(t1: *Term, t2: *Term, s: *Subst) -> *NxResult {
189 // First, walk through substitutions
190 let a: *Term = nx_subst_apply(t1, s)
191 let b: *Term = nx_subst_apply(t2, s)
192
193 // Equal? done.
194 if nx_term_eq(a, b) == 1 { return nx_result_ok(s.n) }
195
196 // VAR on either side
197 if a.kind == NX_TERM_VAR {
198 if nx_term_contains_var(b, a.sym) == 1 { return nx_result_err(NX_ERR_INVALID_STATE) }
199 return nx_subst_add(s, a.sym, b)
200 }
201 if b.kind == NX_TERM_VAR {
202 if nx_term_contains_var(a, b.sym) == 1 { return nx_result_err(NX_ERR_INVALID_STATE) }
203 return nx_subst_add(s, b.sym, a)
204 }
205
206 // Both CONST: equal sym -> done; differ -> fail. (Already handled
207 // by structural equality above for equal CONST; reaching here means
208 // they differ.)
209 if a.kind == NX_TERM_CONST { return nx_result_err(NX_ERR_TAG_MISMATCH) }
210 if b.kind == NX_TERM_CONST { return nx_result_err(NX_ERR_TAG_MISMATCH) }
211
212 // Both APP: same head sym + arity?
213 if a.sym != b.sym { return nx_result_err(NX_ERR_TAG_MISMATCH) }
214 if a.n_args != b.n_args { return nx_result_err(NX_ERR_TAG_MISMATCH) }
215
216 // Unify children pairwise
217 var i: nx_int = 0
218 while i < a.n_args {
219 let r: *NxResult = nx_unify(nx_term_arg(a, i), nx_term_arg(b, i), s)
220 if nx_result_is_err(r) == 1 { return r }
221 i = i + 1
222 }
223 return nx_result_ok(s.n)
224}
225
226// ===== One-way matching =============================================
227// Extends substitution s so that pattern[s] = term. Only pattern's
228// variables are bound; term is treated as fixed (no recursion through
229// s on the term side). Used by subsumption + demodulation.
230//
231// Returns Result<nx_int, NX_ERR_*> with same error codes as nx_unify.
232func nx_match(pattern: *Term, term: *Term, s: *Subst) -> *NxResult {
233 if pattern.kind == NX_TERM_VAR {
234 let bound: *Term = nx_subst_lookup(s, pattern.sym)
235 if (bound as nx_int) != 0 {
236 if nx_term_eq(bound, term) == 1 { return nx_result_ok(s.n) }
237 return nx_result_err(NX_ERR_TAG_MISMATCH)
238 }
239 return nx_subst_add(s, pattern.sym, term)
240 }
241 if pattern.kind == NX_TERM_CONST {
242 if term.kind != NX_TERM_CONST { return nx_result_err(NX_ERR_TAG_MISMATCH) }
243 if pattern.sym != term.sym { return nx_result_err(NX_ERR_TAG_MISMATCH) }
244 return nx_result_ok(s.n)
245 }
246 // pattern is APP
247 if term.kind != NX_TERM_APP { return nx_result_err(NX_ERR_TAG_MISMATCH) }
248 if pattern.sym != term.sym { return nx_result_err(NX_ERR_TAG_MISMATCH) }
249 if pattern.n_args != term.n_args { return nx_result_err(NX_ERR_TAG_MISMATCH) }
250 var i: nx_int = 0
251 while i < pattern.n_args {
252 let r: *NxResult = nx_match(nx_term_arg(pattern, i), nx_term_arg(term, i), s)
253 if nx_result_is_err(r) == 1 { return r }
254 i = i + 1
255 }
256 return nx_result_ok(s.n)
257}