diff --git a/lib/datalog/scoreboard.json b/lib/datalog/scoreboard.json index 33dd2a77..9fa459b9 100644 --- a/lib/datalog/scoreboard.json +++ b/lib/datalog/scoreboard.json @@ -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" } diff --git a/lib/datalog/scoreboard.md b/lib/datalog/scoreboard.md index ef47d2fd..40dd40ca 100644 --- a/lib/datalog/scoreboard.md +++ b/lib/datalog/scoreboard.md @@ -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 | diff --git a/lib/datalog/strata.sx b/lib/datalog/strata.sx index 0928c989..feaad46f 100644 --- a/lib/datalog/strata.sx +++ b/lib/datalog/strata.sx @@ -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))))) diff --git a/lib/datalog/tests/aggregates.sx b/lib/datalog/tests/aggregates.sx index a582ed8a..dbe2f643 100644 --- a/lib/datalog/tests/aggregates.sx +++ b/lib/datalog/tests/aggregates.sx @@ -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 diff --git a/plans/datalog-on-sx.md b/plans/datalog-on-sx.md index 2d7fca84..b3769e92 100644 --- a/plans/datalog-on-sx.md +++ b/plans/datalog-on-sx.md @@ -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