diff --git a/lib/datalog/builtins.sx b/lib/datalog/builtins.sx index 90d5faed..9989c1ad 100644 --- a/lib/datalog/builtins.sx +++ b/lib/datalog/builtins.sx @@ -179,6 +179,27 @@ vs) out)))) +;; Filter a list of variable-name strings to exclude anonymous-renamed +;; vars (`_` in source → `_anon*` by dl-rename-anon-term). Used by +;; the negation safety check, where anonymous vars are existential +;; within the negated literal. +(define + dl-non-anon-vars + (fn + (vs) + (let + ((out (list))) + (do + (for-each + (fn + (v) + (when + (not (and (>= (len v) 5) + (= (slice v 0 5) "_anon"))) + (append! out v))) + vs) + out)))) + (define dl-rule-check-safety (fn @@ -282,8 +303,14 @@ ((and (list? inner) (> (len inner) 0)) (dl-rel-name inner)) (else nil))) - (needed (dl-vars-of inner)) - (missing (dl-vars-not-in (dl-vars-of inner) bound))) + ;; Anonymous variables (`_` in source → `_anon*` after + ;; renaming) are existentially quantified within the + ;; negated literal — they don't need to be bound by + ;; an earlier body lit, since `not p(X, _)` is a + ;; valid idiom for "no Y exists s.t. p(X, Y)". Filter + ;; them out of the safety check. + (needed (dl-non-anon-vars (dl-vars-of inner))) + (missing (dl-vars-not-in needed bound))) (cond ((and (not (nil? inner-rn)) (dl-reserved-rel? inner-rn)) (set! err diff --git a/lib/datalog/scoreboard.json b/lib/datalog/scoreboard.json index b30f55a4..8f389f01 100644 --- a/lib/datalog/scoreboard.json +++ b/lib/datalog/scoreboard.json @@ -1,8 +1,8 @@ { "lang": "datalog", - "total_passed": 271, + "total_passed": 273, "total_failed": 0, - "total": 271, + "total": 273, "suites": [ {"name":"tokenize","passed":31,"failed":0,"total":31}, {"name":"parse","passed":23,"failed":0,"total":23}, @@ -10,11 +10,11 @@ {"name":"eval","passed":42,"failed":0,"total":42}, {"name":"builtins","passed":26,"failed":0,"total":26}, {"name":"semi_naive","passed":8,"failed":0,"total":8}, - {"name":"negation","passed":10,"failed":0,"total":10}, + {"name":"negation","passed":12,"failed":0,"total":12}, {"name":"aggregates","passed":23,"failed":0,"total":23}, {"name":"api","passed":22,"failed":0,"total":22}, {"name":"magic","passed":36,"failed":0,"total":36}, {"name":"demo","passed":21,"failed":0,"total":21} ], - "generated": "2026-05-11T08:44:12+00:00" + "generated": "2026-05-11T08:49:02+00:00" } diff --git a/lib/datalog/scoreboard.md b/lib/datalog/scoreboard.md index 3ea409b0..b13d97c0 100644 --- a/lib/datalog/scoreboard.md +++ b/lib/datalog/scoreboard.md @@ -1,6 +1,6 @@ # datalog scoreboard -**271 / 271 passing** (0 failure(s)). +**273 / 273 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| @@ -10,7 +10,7 @@ | eval | 42 | 42 | ok | | builtins | 26 | 26 | ok | | semi_naive | 8 | 8 | ok | -| negation | 10 | 10 | ok | +| negation | 12 | 12 | ok | | aggregates | 23 | 23 | ok | | api | 22 | 22 | ok | | magic | 36 | 36 | ok | diff --git a/lib/datalog/tests/negation.sx b/lib/datalog/tests/negation.sx index e4de6207..9a5aae3d 100644 --- a/lib/datalog/tests/negation.sx +++ b/lib/datalog/tests/negation.sx @@ -169,6 +169,27 @@ (list (quote q) (quote X))) (list)) + ;; Anonymous `_` in a negated literal is existentially quantified + ;; — it doesn't need to be bound by an earlier body lit. Without + ;; this exemption the safety check would reject the common idiom + ;; `orphan(X) :- person(X), not(parent(X, _))`. + (dl-nt-test-set! "negation with anonymous var — orphan idiom" + (dl-query + (dl-program + "person(a). person(b). person(c). parent(a, b). + orphan(X) :- person(X), not(parent(X, _)).") + (list (quote orphan) (quote X))) + (list {:X (quote b)} {:X (quote c)})) + + ;; Multiple anonymous vars are each independently existential. + (dl-nt-test-set! "negation with multiple anonymous vars" + (dl-query + (dl-program + "u(a). u(b). u(c). edge(a, x). edge(b, y). + solo(X) :- u(X), not(edge(X, _)).") + (list (quote solo) (quote X))) + (list {:X (quote c)})) + ;; Stratifiability checks. (dl-nt-test! "non-stratifiable rejected" (dl-nt-throws? diff --git a/plans/datalog-on-sx.md b/plans/datalog-on-sx.md index 2c65125c..75d49ba2 100644 --- a/plans/datalog-on-sx.md +++ b/plans/datalog-on-sx.md @@ -15,7 +15,7 @@ for rose-ash data (e.g. federation graph, content relationships). ## Status (rolling) -`bash lib/datalog/conformance.sh` → **271/271 across 11 suites** +`bash lib/datalog/conformance.sh` → **273/273 across 11 suites** (tokenize, parse, unify, eval, builtins, semi_naive, negation, aggregates, api, magic, demo). Source is ~3100 LOC, tests ~2900 LOC, public API documented in `lib/datalog/datalog.sx`. @@ -320,6 +320,18 @@ large graphs. _Newest first._ +- 2026-05-11 — Anonymous `_` in a negated literal was incorrectly + flagged by the safety check. The canonical idiom + `orphan(X) :- person(X), not(parent(X, _))` was rejected with + "negation refers to unbound variable(s) (\"_anon1\")" because the + parser renames each `_` to a fresh `_anon*` symbol and the negation + safety walk demanded all vars in the negated lit be bound by an + earlier positive body literal. Anonymous vars in negation are + existentially quantified — they shouldn't need outer binding. + Added `dl-non-anon-vars` filter; `dl-process-neg!` now strips + `_anon*` names from `needed` before the binding check. 2 new + regression tests; 273/273. + - 2026-05-11 — Compound terms in fact-arg / rule-head positions were silently stored as unreduced expressions. `p(+(1, 2)).` resulted in a tuple `(p (+ 1 2))` (dl-ground? sees no free variables, so it