datalog: stratified negation (Phase 7, 124/124)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 54s

New lib/datalog/strata.sx: dl-build-dep-graph (relation -> deps with
:neg flag), Floyd-Warshall reachability, SCC-via-mutual-reach for
non-stratifiability detection, iterative dl-compute-strata, and
dl-group-rules-by-stratum.

eval.sx refactor:
- dl-saturate-rules! db rules — semi-naive worker over a rule subset
- dl-saturate! db — stratified driver. Rejects non-stratifiable
  programs at saturation time, then iterates strata in order
- dl-match-negation — succeeds iff inner positive match is empty

Order-aware safety in dl-rule-check-safety (Phase 4) already
required negation vars to be bound by a prior positive literal.
Stratum dict keys are strings (SX dicts don't accept ints).

Phase 6 magic sets deferred — opt-in path, semi-naive default
suffices for current workloads.
This commit is contained in:
2026-05-08 08:20:56 +00:00
parent d964f58c48
commit caec05eb27
7 changed files with 626 additions and 24 deletions

View File

@@ -55,13 +55,24 @@
results)))))
;; Naive matcher (for dl-saturate-naive! and dl-query post-saturation).
(define
dl-match-negation
(fn
(inner db subst)
(let
((walked (dl-apply-subst inner subst))
(matches (dl-match-positive inner db subst)))
(cond
((= (len matches) 0) (list subst))
(else (list))))))
(define
dl-match-lit
(fn
(lit db subst)
(cond
((and (dict? lit) (has-key? lit :neg))
(error "datalog: negation not yet supported (Phase 7)"))
(dl-match-negation (get lit :neg) db subst))
((dl-builtin? lit)
(let
((s (dl-eval-builtin lit subst)))
@@ -194,7 +205,7 @@
(options
(cond
((and (dict? lit) (has-key? lit :neg))
(error "datalog: negation in semi-naive (Phase 7)"))
(dl-match-negation (get lit :neg) db subst))
((dl-builtin? lit)
(let
((s (dl-eval-builtin lit subst)))
@@ -281,14 +292,14 @@
candidates)))
(define
dl-saturate!
dl-saturate-rules!
(fn
(db)
(db rules)
(let
((delta (dl-snapshot-facts db)))
(do
(define
dl-sn-step
dl-sr-step
(fn
()
(let
@@ -300,14 +311,50 @@
(for-each
(fn (cand) (append! pending cand))
(dl-collect-rule-candidates rule db delta)))
(dl-rules db))
rules)
(dl-commit-candidates! db pending new-delta)
(cond
((dl-delta-empty? new-delta) nil)
(else (do (set! delta new-delta) (dl-sn-step))))))))
(dl-sn-step)
(else (do (set! delta new-delta) (dl-sr-step))))))))
(dl-sr-step)
db))))
;; Stratified driver: rejects non-stratifiable programs at saturation
;; time, then iterates strata in increasing order, running semi-naive on
;; the rules whose head sits in that stratum.
(define
dl-saturate!
(fn
(db)
(let
((err (dl-check-stratifiable db)))
(cond
((not (nil? err)) (error (str "dl-saturate!: " err)))
(else
(let
((strata (dl-compute-strata db)))
(let
((grouped (dl-group-rules-by-stratum db strata)))
(let
((groups (get grouped :groups))
(max-s (get grouped :max)))
(do
(define
dl-strat-loop
(fn
(s)
(when
(<= s max-s)
(let
((sk (str s)))
(do
(when
(has-key? groups sk)
(dl-saturate-rules! db (get groups sk)))
(dl-strat-loop (+ s 1)))))))
(dl-strat-loop 0)
db)))))))))
;; ── Querying ─────────────────────────────────────────────────────
(define