xlog_logic/hypergraph/fixpoint.rs
1//! Naive fixpoint evaluator for recursive hypergraph rules.
2//!
3//! Builds on PR 2's [`super::evaluate_rule`]: each iteration runs
4//! every supplied rule once against the union of supplied base
5//! relations and the target predicate's currently-derived rows,
6//! unions new rows into the derived set, sorts and deduplicates,
7//! and stops when an iteration produces zero new rows.
8//!
9//! Pure-Rust, deterministic, set-semantics. Built to be the
10//! recursive-WCOJ correctness oracle for PR 4+ mixed-execution
11//! kernels. Not optimized — a real engine would use semi-naive
12//! delta-driven evaluation; this slice prefers simplicity over
13//! speed.
14//!
15//! ## Algorithm
16//!
17//! 1. Validate that every supplied rule's head predicate equals
18//! the target. (The slice ships single-predicate fixpoint;
19//! multi-predicate SCCs are a later concern.)
20//! 2. Compute the target relation's schema by inferring per-vertex
21//! types from the *first* iteration's evaluation: each rule
22//! head's term shape gives an arity; every cell's [`RefValue`]
23//! variant gives a [`ScalarType`]. The first iteration that
24//! produces non-empty rows freezes the schema.
25//! 3. Loop up to `max_iterations` times:
26//! a. For each rule, run [`super::evaluate_rule`] against
27//! `base_relations ∪ {target → derived}`. Union new rows
28//! into a per-iteration scratch buffer.
29//! b. Merge scratch into `derived`, sort+dedupe.
30//! c. If `derived` is unchanged this iteration, return.
31//! d. Otherwise increment the iteration counter and continue.
32//! 4. If the loop exits without convergence, return
33//! [`FixpointError::MaxIterationsExceeded`].
34//!
35//! ## Schema seeding
36//!
37//! On iteration 1, rules referencing the target predicate would
38//! ordinarily fail with [`RefEvalError::MissingRelation`]. The
39//! evaluator pre-seeds an empty `target` relation whose schema is
40//! taken from the head arity of the first rule with a non-empty
41//! head. Once a real iteration produces tuples the schema is
42//! frozen against per-cell variant types — drift in later
43//! iterations surfaces as a
44//! [`RefEvalError::RelationValueTypeMismatch`] from PR 2's
45//! validation.
46
47use super::{evaluate_rule, RefEvalError, RefRelation, RefRelationStore, RefValue, VariableOrder};
48use crate::ast::Rule;
49use xlog_core::ScalarType;
50
51/// Configuration for [`evaluate_fixpoint`].
52#[derive(Debug, Clone, PartialEq, Eq)]
53pub struct FixpointConfig {
54 /// Hard cap on iteration count. Returns
55 /// [`FixpointError::MaxIterationsExceeded`] if convergence
56 /// is not reached within this many iterations. Must be ≥ 1.
57 pub max_iterations: usize,
58}
59
60impl Default for FixpointConfig {
61 /// Default cap is 32. Generous enough for typical
62 /// transitive-closure and Same-Generation tests; tight enough
63 /// that infinite-loop bugs surface fast.
64 fn default() -> Self {
65 Self { max_iterations: 32 }
66 }
67}
68
69/// Errors surfaced by [`evaluate_fixpoint`].
70#[derive(Debug, Clone, PartialEq)]
71pub enum FixpointError {
72 /// A rule's head predicate did not equal `target_predicate`.
73 /// The fixpoint evaluator only accepts rules that contribute
74 /// to the named target.
75 RuleNotForTarget {
76 /// Index of the offending rule in the input slice.
77 rule_index: usize,
78 /// Head predicate observed.
79 observed: String,
80 /// Expected target predicate.
81 expected: String,
82 },
83 /// Two rules disagreed on the target predicate's head arity.
84 /// Surfaced separately from the per-row arity check so the
85 /// caller sees the rule-level shape mismatch directly rather
86 /// than as a downstream `RelationRowArityMismatch`.
87 HeadArityMismatch {
88 /// Index of the offending rule in the input slice.
89 rule_index: usize,
90 /// Head arity observed on this rule.
91 observed_arity: usize,
92 /// Head arity established by the first non-empty-head rule.
93 expected_arity: usize,
94 },
95 /// `target_predicate` was already present in `base_relations`.
96 /// The fixpoint constructs the target relation; allowing
97 /// `base_relations` to seed it would silently shadow the
98 /// caller's seed on the first iteration. If you want a seed,
99 /// encode it as a base-case rule.
100 TargetPredicateInBaseRelations {
101 /// The target predicate name as supplied.
102 name: String,
103 },
104 /// A rule failed evaluation. Wraps the per-rule error from
105 /// [`evaluate_rule`] with the rule's index in the input slice
106 /// for diagnostic precision.
107 RuleEval {
108 /// Index in the input slice.
109 rule_index: usize,
110 /// The wrapped per-rule error.
111 source: RefEvalError,
112 },
113 /// The fixpoint did not converge within
114 /// [`FixpointConfig::max_iterations`].
115 MaxIterationsExceeded {
116 /// The configured cap.
117 limit: usize,
118 /// Size of the derived target relation at the cap.
119 observed_size: usize,
120 },
121 /// No supplied rule produced a head whose arity could be
122 /// inferred — caller supplied an empty rules slice or
123 /// every rule had an empty head.
124 TargetSchemaIndeterminable,
125 /// `max_iterations` was zero. Must be ≥ 1.
126 InvalidMaxIterations,
127}
128
129/// Evaluate a recursive set of rules to a fixpoint over a single
130/// target predicate.
131///
132/// Every supplied rule must have its head predicate equal to
133/// `target_predicate`. `base_relations` carries any non-target
134/// predicates referenced in rule bodies (e.g. `edge` for transitive
135/// closure, `parent` for Same Generation). The target predicate
136/// must NOT appear in `base_relations`; it is constructed by the
137/// fixpoint and shadowing would be ambiguous.
138///
139/// Returns the converged target relation. Set semantics: rows
140/// are sorted lexicographically and deduplicated. Same input →
141/// same output. Rule order in the input slice does not affect
142/// the result (locked by test).
143pub fn evaluate_fixpoint(
144 rules: &[Rule],
145 base_relations: &RefRelationStore,
146 target_predicate: &str,
147 order: &dyn VariableOrder,
148 config: &FixpointConfig,
149) -> Result<RefRelation, FixpointError> {
150 if config.max_iterations == 0 {
151 return Err(FixpointError::InvalidMaxIterations);
152 }
153
154 if base_relations.contains_key(target_predicate) {
155 return Err(FixpointError::TargetPredicateInBaseRelations {
156 name: target_predicate.to_string(),
157 });
158 }
159
160 // 1. Validate that every rule heads `target_predicate`.
161 for (i, rule) in rules.iter().enumerate() {
162 if rule.head.predicate != target_predicate {
163 return Err(FixpointError::RuleNotForTarget {
164 rule_index: i,
165 observed: rule.head.predicate.clone(),
166 expected: target_predicate.to_string(),
167 });
168 }
169 }
170
171 // 2. Establish the target's arity from the first non-empty
172 // rule head. Per-position scalar types are filled in by the
173 // first iteration that produces non-empty rows.
174 let target_arity = rules
175 .iter()
176 .find(|r| !r.head.terms.is_empty())
177 .map(|r| r.head.terms.len())
178 .ok_or(FixpointError::TargetSchemaIndeterminable)?;
179
180 // Every other non-empty-head rule must agree on that arity.
181 // Surfacing this as a rule-level error prevents downstream
182 // confusion: PR 2's per-row validation would catch the same
183 // problem on iteration 1 as `RelationRowArityMismatch`, but
184 // pointing at "row index N" instead of "rule index M" is two
185 // layers of indirection from the actual fixture problem.
186 for (i, rule) in rules.iter().enumerate() {
187 if rule.head.terms.is_empty() {
188 continue;
189 }
190 if rule.head.terms.len() != target_arity {
191 return Err(FixpointError::HeadArityMismatch {
192 rule_index: i,
193 observed_arity: rule.head.terms.len(),
194 expected_arity: target_arity,
195 });
196 }
197 }
198
199 // Seed schema: every column is U32 as a placeholder. As soon
200 // as the first iteration produces a non-empty row we replace
201 // the schema with the variant-derived types and re-validate
202 // future iterations against it.
203 let mut derived_schema: Option<Vec<ScalarType>> = None;
204 let mut derived_rows: Vec<Vec<RefValue>> = Vec::new();
205
206 for _iter in 0..config.max_iterations {
207 // 3a. Build the per-iteration relation store: base ∪ target.
208 let mut store = base_relations.clone();
209 let placeholder_schema = derived_schema
210 .clone()
211 .unwrap_or_else(|| vec![ScalarType::U32; target_arity]);
212 store.insert(
213 target_predicate.to_string(),
214 RefRelation {
215 schema: placeholder_schema,
216 rows: derived_rows.clone(),
217 },
218 );
219
220 // 3b. Run every rule and union new tuples.
221 let mut new_rows: Vec<Vec<RefValue>> = derived_rows.clone();
222 for (rule_index, rule) in rules.iter().enumerate() {
223 // On iter 0, rules that reference `target_predicate`
224 // see an empty target — that's fine; they contribute
225 // base tuples. On later iters, recursive rules see
226 // the derived set.
227 let rows = evaluate_rule(rule, &store, order).map_err(|e| FixpointError::RuleEval {
228 rule_index,
229 source: e,
230 })?;
231 new_rows.extend(rows);
232 }
233 new_rows.sort();
234 new_rows.dedup();
235
236 // 3c. On the first iteration that produced rows, freeze
237 // the schema from the cell variants of the first row.
238 if derived_schema.is_none() {
239 if let Some(first) = new_rows.first() {
240 derived_schema = Some(infer_schema(first));
241 }
242 }
243
244 // 3d. Convergence check: identical-to-previous → done.
245 if new_rows == derived_rows {
246 let schema = derived_schema.unwrap_or_else(|| vec![ScalarType::U32; target_arity]);
247 return Ok(RefRelation {
248 schema,
249 rows: derived_rows,
250 });
251 }
252
253 derived_rows = new_rows;
254 }
255
256 Err(FixpointError::MaxIterationsExceeded {
257 limit: config.max_iterations,
258 observed_size: derived_rows.len(),
259 })
260}
261
262fn infer_schema(row: &[RefValue]) -> Vec<ScalarType> {
263 row.iter()
264 .map(|v| match v {
265 RefValue::U32(_) => ScalarType::U32,
266 RefValue::U64(_) => ScalarType::U64,
267 RefValue::I32(_) => ScalarType::I32,
268 RefValue::I64(_) => ScalarType::I64,
269 RefValue::Bool(_) => ScalarType::Bool,
270 RefValue::Symbol(_) => ScalarType::Symbol,
271 })
272 .collect()
273}