datalog: anonymous _ in negation is existential, not unbound
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 23s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 23s
The canonical Datalog idiom for "no X has any Y": orphan(X) :- person(X), not(parent(X, _)). was rejected by the safety check with "negation refers to unbound variable(s) (\"_anon1\")". The parser renames each anonymous `_` to a fresh `_anon*` symbol so multiple `_` occurrences don't unify with each other, and the negation safety walk then demanded all free vars in the negated lit be bound by an earlier positive body lit — including the renamed anonymous vars. Anonymous vars in a negation are existentially quantified within the negation, not requirements from outside. Added dl-non-anon-vars to strip `_anon*` names from the `needed` set before the binding check in dl-process-neg!. Real vars (like `X` in the orphan idiom) still must be bound by an earlier positive body lit, just as before. 2 new regression tests (orphan idiom + multi-anon "solo" pattern); conformance 273/273. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This commit is contained in:
@@ -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?
|
||||
|
||||
Reference in New Issue
Block a user