Why isn't closure just a formula?
Because a theorem says it can't be: no first-order formula with aggregates computes unbounded reachability. A bounded chain of lookups only fakes it until the graph gets one hop deeper — so the rulebook gives closure its own declared field type instead.
You can chain lookups: A → B, then B → C, then C → D. Three hops, three fields. But "is X reachable from Y through any number of hops" is a different kind of question, and the difference is not stylistic.
Hella, Libkin, Nurmonen & Wong (2001) proved transitive closure is not expressible in first-order logic with aggregates — the exact expressivity class of the rulebook's formula, lookup, and aggregation fields (and of SQL without WITH RECURSIVE). The proof is by locality: every such formula can only see a bounded neighborhood of each row, and reachability has no bound.
So there are only two honest designs:
-
Fake it with a bounded-depth lookup chain that silently breaks the day the real graph gets one hop deeper than the chain. Spreadsheets do this all the time. It is the single most common way "declarative" systems quietly lie.
-
Declare it. Closure becomes its own field type in the model —
"type": "closure"over a relationship — and each substrate emits it with its native recursion machinery, exactly as it emits a COUNTIFS with its native aggregation machinery.
The rulebook takes door two, and then does the thing frameworks usually skip: the conformance harness proves the independently-built emissions agree — Postgres's WITH RECURSIVE, OWL's reasoner, and the Python/Go/TypeScript traversals all produce the same closure, graded cell by cell, including on cyclic graphs where a step can reach itself.
The theorem is why the primitive exists. The harness is why you can trust it.