datalog: stratifier rejects recursion through aggregation (165/165)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 53s

Bug: dl-check-stratifiable iterated body literals looking only for
explicit :neg literals, missing aggregate cycles. Now also walks
aggregates via dl-aggregate-dep-edge — q(N) :- count(N, X, q(X))
correctly errors out at saturation time.

3 new tests cover:
- recursion-through-aggregation rejected
- negation + aggregation coexist when in different strata
- min over empty derived relation produces no result
This commit is contained in:
2026-05-08 09:13:10 +00:00
parent a63d67247a
commit b95d8c5a63
5 changed files with 76 additions and 18 deletions

View File

@@ -1,8 +1,8 @@
{
"lang": "datalog",
"total_passed": 162,
"total_passed": 165,
"total_failed": 0,
"total": 162,
"total": 165,
"suites": [
{"name":"tokenize","passed":26,"failed":0,"total":26},
{"name":"parse","passed":18,"failed":0,"total":18},
@@ -11,9 +11,9 @@
{"name":"builtins","passed":19,"failed":0,"total":19},
{"name":"semi_naive","passed":8,"failed":0,"total":8},
{"name":"negation","passed":10,"failed":0,"total":10},
{"name":"aggregates","passed":13,"failed":0,"total":13},
{"name":"aggregates","passed":16,"failed":0,"total":16},
{"name":"api","passed":9,"failed":0,"total":9},
{"name":"demo","passed":13,"failed":0,"total":13}
],
"generated": "2026-05-08T09:05:25+00:00"
"generated": "2026-05-08T09:12:57+00:00"
}

View File

@@ -1,6 +1,6 @@
# datalog scoreboard
**162 / 162 passing** (0 failure(s)).
**165 / 165 passing** (0 failure(s)).
| Suite | Passed | Total | Status |
|-------|--------|-------|--------|
@@ -11,6 +11,6 @@
| builtins | 19 | 19 | ok |
| semi_naive | 8 | 8 | ok |
| negation | 10 | 10 | ok |
| aggregates | 13 | 13 | ok |
| aggregates | 16 | 16 | ok |
| api | 9 | 9 | ok |
| demo | 13 | 13 | ok |

View File

@@ -197,18 +197,33 @@
(for-each
(fn
(lit)
(when
(and (dict? lit) (has-key? lit :neg))
(let ((tgt (dl-rel-name (get lit :neg))))
(when
(and (not (nil? tgt))
(dl-reach-cycle? reach head-rel tgt))
(set!
err
(str "non-stratifiable: relation " head-rel
" transitively depends through negation on "
tgt
" which depends back on " head-rel))))))
(cond
((and (dict? lit) (has-key? lit :neg))
(let ((tgt (dl-rel-name (get lit :neg))))
(when
(and (not (nil? tgt))
(dl-reach-cycle? reach head-rel tgt))
(set!
err
(str "non-stratifiable: relation " head-rel
" transitively depends through negation on "
tgt
" which depends back on " head-rel)))))
((dl-aggregate? lit)
(let ((edge (dl-aggregate-dep-edge lit)))
(when
(not (nil? edge))
(let ((tgt (get edge :rel)))
(when
(and (not (nil? tgt))
(dl-reach-cycle? reach head-rel tgt))
(set!
err
(str "non-stratifiable: relation "
head-rel
" aggregates over " tgt
" which depends back on "
head-rel)))))))))
(get rule :body)))))
(dl-rules db))
err)))))

View File

@@ -227,6 +227,39 @@
(list {:L (list)}))
;; Aggregate vs single distinct.
;; Stratification: recursion through aggregation is rejected.
(dl-at-test! "agg recursion rejected"
(dl-at-throws?
(fn ()
(let ((db (dl-make-db)))
(do
(dl-add-rule! db
{:head (list (quote q) (quote N))
:body (list (list (quote count) (quote N) (quote X)
(list (quote q) (quote X))))})
(dl-saturate! db)))))
true)
;; Negation + aggregation in the same body — different strata.
(dl-at-test-set! "neg + agg coexist"
(dl-query
(dl-program
"u(a). u(b). u(c). banned(b).
active(X) :- u(X), not(banned(X)).
cnt(N) :- count(N, X, active(X)).")
(list (quote cnt) (quote N)))
(list {:N 2}))
;; Min over a derived empty relation: no result.
(dl-at-test-set! "min over empty derived"
(dl-query
(dl-program
"s(50). s(60).
score(N) :- s(N), >(N, 100).
low(M) :- min(M, X, score(X)).")
(list (quote low) (quote M)))
(list))
(dl-at-test-set! "distinct counted once"
(dl-query
(dl-program

View File

@@ -273,6 +273,16 @@ large graphs.
_Newest first._
- 2026-05-08 — Bug fix: `dl-check-stratifiable` now rejects recursion
through aggregation (e.g., `q(N) :- count(N, X, q(X))`). The
stratifier was already adding negation-like edges for aggregates,
but the cycle scan only looked at explicit `:neg` literals. Added
the matching aggregate branch to the body iteration. Also adds
doc-only `lib/datalog/datalog.sx` with the public-API surface
(since `load` is an epoch command and can't recurse from within an
`.sx` file). 3 new aggregate tests cover recursion-rejection,
negation-and-aggregation coexistence, and min-over-empty-derived.
- 2026-05-08 — Phase 10 demo + canonical query. Added the "cooking
posts by people I follow (transitively)" example from the plan:
`dl-demo-cooking-rules` defines `reach` over the follow graph