Skip to main content

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}