Materialization versus Rewriting: Two Ways to Scale

📍 Where we are: Part IV · Scale and Systems — Chapter 9. Abstention closed Part III by pricing the right to say "I don't know"; Part IV opens the other ledger of the frontier, scale, and starts with its oldest question: pay for inference once at load time, or again at every query?

Every volume of this series has computed consequences: Volume 1 ran a fixpoint, Volume 2 saturated an ontology, Volume 4 differentiated through query answering. None of them asked when the computing should happen. That question sounds like an implementation detail, and it is the opposite: it is the axis along which the entire deductive-database and ontology-reasoning systems literature is organized, and it is governed by a piece of arithmetic simple enough to write in one line. Materialization pays at load time: run the rules to their least fixpoint once, store every consequence, and answer each query by lookup. Rewriting pays at query time: store nothing but the base facts, and unfold each query backward through the rules into a union of queries that the raw data can answer directly. Both return the same certain answers, the answers guaranteed by the facts and rules in every possible completion of the data, not merely in one; the companion module asserts exactly that, three ways, on every query it runs. What differs is the bill, and this chapter counts the bill probe by probe on the academic world: the load cost of the closure, the per-query cost of each strategy, the crossover workload where the winner flips, the maintenance cost that the headline identity hides, and finally the deepest fact in the chapter, that the choice is not always yours to make, because the logic fragment you reason in decides whether rewriting is even possible.

The simple version

Imagine a restaurant deciding when to chop vegetables. One kitchen preps everything at dawn: every onion diced, every sauce reduced, so each order is assembled in seconds. The other kitchen keeps whole ingredients and cooks each dish from scratch when the ticket arrives. If two hundred orders come in, dawn prep wins enormously; if three orders come in, it wasted a morning chopping food nobody asked for. Now add the hidden cost: a supplier recalls one crate of tomatoes. The from-scratch kitchen shrugs and stops using them. The prep kitchen must hunt through every prepared sauce asking "did this batch use that crate, and if so, could another crate have made it?", which is real, careful work. And one dish, the slow-simmered stock, cannot be made to order at all: no amount of last-minute effort replaces hours of simmering, so the from-scratch kitchen simply cannot serve it. Materialization is dawn prep, rewriting is cooking to order, the recall is deletion, and the stock is recursion.

What this chapter covers

• The accounting identity: total inference cost as load cost plus per-query cost times the workload size, each term decoded, and the crossover claim it implies: the winner is a function of how many queries you will ever ask.
• Materialization, counted: the naive fixpoint implemented with a visible probe counter (23 facts close to 47 in 2 waves for 236 probes), the naive strategy's waste named, and the semi-naive delta rule derived from scratch: only rule instances touching a new fact can derive anything new, so no instance ever fires twice.
• Rewriting, counted: backward unfolding of a query atom through Horn rules into a union of conjunctive queries over base predicates, the recursion quoted, termination proved for the non-recursive rule shapes by a rank argument, and the honest boundary at the one recursive rule.
• The crossover, computed: the committed per-query probe counts assembled into the identity, the break-even workload solved for exactly (thirteen passes of the five-query ledger), and the identical-answers assert that makes this a controlled experiment about cost, never about semantics.
• Maintenance, the third pole: adding one advising fact costs a 12-probe semi-naive delta on the materialized side and nothing on the rewriting side; deleting one citation forces DRed's overdelete-then-rederive dance, whose counted run (overdelete 2, restore 1) exhibits exactly why deletion is harder than insertion.
• The fragment dependence: the committed 8-hop recursion wall, the theorem that DL-Lite queries rewrite completely into first-order queries while EL's PTIME-complete reasoning (PTIME: the class of problems solvable in polynomial time, time bounded by a fixed power of the input size) cannot, and what that means when you choose a logic: you are choosing your systems options.

The accounting identity

Fix a knowledge base and a workload. Write $q$ for the workload size: the number of queries the store will answer over its lifetime (a plain count, one per query asked). Write $C_{\text{load}}$ for the one-time cost a strategy pays when the data is loaded, before any query arrives, and $C_{\text{query}}$ for the cost it pays per query. Then the total cost of serving the workload is one line:

$$\mathrm{Total}(q) \;=\; C_{\text{load}} \;+\; q \cdot C_{\text{query}}.$$

Read it as a line in the plane whose horizontal axis is $q$ and whose vertical axis is total work: $C_{\text{load}}$ is the intercept, $C_{\text{query}}$ is the slope. Materialization is a high-intercept, shallow-slope line: it pays the whole fixpoint up front so that each query is a lookup. Rewriting is a zero-intercept, steep-slope line: load is free (the base facts are stored as they arrive, nothing is derived), and every query pays for the reasoning it needs. Two lines with different intercepts and slopes cross at exactly one point. To find it, set the totals equal, with superscripts $m$ for materialization and $r$ for rewriting:

$$C^{m}_{\text{load}} + q\, C^{m}_{\text{query}} \;=\; q\, C^{r}_{\text{query}} .$$

Subtract $q\, C^{m}_{\text{query}}$ from both sides, then factor $q$ out of the right-hand side:

$$C^{m}_{\text{load}} \;=\; q\,\bigl(C^{r}_{\text{query}} - C^{m}_{\text{query}}\bigr).$$

Dividing both sides by the bracketed difference gives the crossover:

$$q^{*} \;=\; \frac{C^{m}_{\text{load}}}{C^{r}_{\text{query}} - C^{m}_{\text{query}}},$$

valid whenever rewriting's per-query cost exceeds materialization's, so the bracketed denominator is positive; the companion asserts, query by query, that the lookup never out-probes the rewriting, and strictly so whenever the rewriting actually joins, which is what makes the ledger's denominator positive. Below $q^{*}$ queries, rewriting has done less total work; above it, the load cost has amortized (been repaid in per-query savings) and materialization wins forever after. Everything else in this chapter is a careful measurement of the three constants, plus two complications the identity hides: the data changes (maintenance is a cost the identity has no term for), and for one rule shape the rewriting side of the comparison does not exist at all.

The instrument is the companion module mat_vs_rewrite.py, which runs both strategies on Volume 1's academic world, imported and never retyped: the 23 base facts and 7 Horn rules of examples/logic/kb.py, with forward_chain.least_fixpoint as the materializer and the SLD (Selective Linear Definite-clause resolution) prover of examples/logic/sld.py, the backward-chaining engine Volume 1 built, as an independent oracle that both strategies are checked against. Its one cost unit is the probe: the store is indexed by predicate, and evaluating a query charges one probe per candidate fact scanned under an atom's predicate index, plus one per ground disequality check (mat_vs_rewrite.py lines 37–40). No wall-clock numbers appear anywhere; probes stand in for the I/O and join cost that dominate at real scale, and the run is deterministic to the byte.

One identity, two poles: materialization buys a high intercept and a shallow slope, rewriting a zero intercept and a steep slope, and the committed probe counts put their crossing at about twelve and a half passes of the query ledger. Original diagram by the authors, created with AI assistance.

Materialization: pay once, look up forever

Materialization computes the least fixpoint of the rules over the base facts: the smallest set of atoms that contains the base and is closed under every rule. Volume 1 built the engine; here it becomes a cost center. Recall the operator. Write $P$ for the rule program, $I$ for a set of ground atoms (the current store), and $\sigma$ for a substitution, a mapping from variables to constants. The immediate-consequence operator $T_P$ maps a store to the store plus everything derivable in one step:

$$T_P(I) \;=\; I \,\cup\, \{\, h\sigma \;:\; (h \leftarrow b_1, \ldots, b_m) \in P,\;\; b_1\sigma, \ldots, b_m\sigma \in I \,\},$$

read: for every rule with head $h$ and body atoms $b_1$ through $b_m$ (the letter $m$ counts the body atoms of that rule), and every substitution $\sigma$ that makes all $m$ instantiated body atoms $b_i\sigma$ members of $I$, add the instantiated head $h\sigma$. Iterating $T_P$ from the base facts climbs a chain $I_0 \subseteq I_1 \subseteq I_2 \subseteq \cdots$ (the symbol $\subseteq$ says each store contains everything in the one before it: nothing is ever removed, only added) that stops growing after finitely many waves, because everything added is built from the finite supply of constants already present. The stable set is the closure. The companion's counted implementation is deliberately the naive version, so its waste is visible (mat_vs_rewrite.py lines 128–142):

    store = set(edb)
    waves = probes = 0
    while True:
        new: set[tuple] = set()
        for head, body in rules:
            subs, p = eval_cq(body, index(store))
            probes += p
            for s in subs:
                h = apply_sub(head, s)
                if h not in store:
                    new.add(h)
        if not new:
            return store, waves, probes
        store |= new
        waves += 1

Every wave re-evaluates every rule body over the whole store. That is correct and wasteful in a precise way: a rule instance whose body was already satisfied at wave $t$ is re-discovered at wave $t+1$, and at every later wave, deriving a head that is already stored. On the academic world the waste is affordable, and the committed run reports the whole bill:

[1] one closure, two bills — load once vs rewrite per query
  materialize: 23 facts → 47 (24 derived) in 2 waves, 236 probes at LOAD time
  rewrite    : store stays 23 facts; every query below pays at QUERY time

Two numbers deserve a pause. First, storage: the closure is 47 facts against 23 base facts, so this rule set slightly more than doubles the store. That ratio is the rent materialization pays forever, and it is not a toy artifact: the strategy's production line accepts it by design, building whole closures in main memory [1], and at benchmark scale the same discipline turns the 6.7 billion explicit triples of LUBM-50K (the Lehigh University Benchmark scaled to 50,000 universities) into 9.2 billion stored ones [2]. Second, the 236 probes are paid before the first query arrives, which is exactly the intercept $C^{m}_{\text{load}}$ of the identity. The harness then asserts that this counted closure equals, fact for fact, the closure Volume 1's own engine computes (mat_vs_rewrite.py lines 343–344), so the counting instrumentation changed nothing but visibility. The materialized store answers a query with a single atom lookup: match the query atom against its predicate index and collect the substitutions (mat_vs_rewrite.py lines 224–229). For grandAdvisor(alice, Z) that is 3 probes, one per stored grandAdvisor fact.

The delta rule, derived

Real engines do not run the naive loop; they run semi-naive evaluation, and its correctness is a two-line theorem worth proving rather than asserting. Define the delta at wave $t$ as the newly derived atoms, $\Delta_t = I_t \setminus I_{t-1}$ (the set-difference symbol $\setminus$ means "members of the first set that are not in the second"). The claim: any rule instance that fires for the first time at wave $t+1$ has at least one body atom in $\Delta_t$. Proof by contraposition. Take an instance $(h \leftarrow b_1, \ldots, b_m)\sigma$ all of whose body atoms lie in $I_t$ but none in $\Delta_t$. Then every $b_i\sigma$ lies in $I_t \setminus \Delta_t = I_{t-1}$, so the instance's body was already satisfied one wave earlier, the instance already fired at wave $t$, and its head is already in $I_t$: it is not a first-time firing. Contraposition gives the delta rule: to find every genuinely new consequence at wave $t+1$, it suffices to enumerate, for each rule and each body position $i$ (an index running from 1 to $m$), the instances whose $i$-th atom matches a fact in $\Delta_t$, joining the remaining $m-1$ atoms against the full store. No rule instance ever fires twice, a guarantee the RDFox line of work later named the non-repetition property, and the whole parallel engine is built around it, partitioning work by newly derived fact rather than by rule so that threads balance themselves [1]. The companion implements exactly this discipline in its incremental-addition procedure, seeding each body position with a delta fact and joining the rest (mat_vs_rewrite.py lines 249–261):

    while delta:
        idx = index(total)
        new: set[tuple] = set()
        for head, body in rules:
            for i, pat in enumerate(body):
                for d in sorted(delta):
                    s = unify(pat, d, {})
                    if s is None:
                        continue
                    probes += 1  # the delta seed is itself one probe
                    rest = body[:i] + body[i + 1:]
                    subs, p = eval_cq(rest, idx, sub=s)
                    probes += p

We will read its counted numbers in the maintenance section, where the delta is a single inserted fact and the contrast with the 236-probe from-scratch closure becomes stark. The industrial anchor for this pole is RDFox, whose lock-light, by-fact-partitioned semi-naive engine materialized the LUBM-50K closure, deriving its 2.5 billion new triples at a rate of 6.1 million triples per second, running 15.7 times faster than its own single thread with 16 threads and 69.6 times faster with 128 [2]: near-linear multicore scaling at commodity core counts, on exactly the loop quoted above, grown up.

Rewriting: resolution at query time

Rewriting stores nothing but the base facts and moves all reasoning into the query. The base predicates, those that appear in the data, are the EDB (extensional database); the derived predicates, exactly the rule heads, are the IDB (intensional database); the companion computes the split in one line, IDB: frozenset[str] = frozenset(head[0] for head, _ in RULES) (mat_vs_rewrite.py line 69). A query atom over an IDB predicate cannot be looked up, because nothing with that predicate is stored. It must be unfolded: replaced by the bodies of the rules that could derive it, recursively, until only EDB atoms remain. The result is a union of conjunctive queries (UCQ): a finite list of ordinary joins over base predicates, each one a conjunctive query (CQ), whose union of answers is the answer to the original query.

One unfolding step is precisely a resolution step, run at query time instead of load time. Take a partial query $A_1, \ldots, A_i, \ldots, A_n$ (a conjunction of $n$ atoms, where $A_i$ is the leftmost atom whose predicate is IDB), and a rule $H \leftarrow B_1, \ldots, B_m$ whose variables have been renamed fresh so they cannot collide with the query's. If $A_i$ and $H$ unify, let $\sigma$ be their most general unifier (mgu), the least-committal substitution making them identical. The step replaces the atom by the body under $\sigma$:

$$A_1 \ldots A_i \ldots A_n \;\;\leadsto\;\; (A_1 \ldots A_{i-1}\; B_1 \ldots B_m\; A_{i+1} \ldots A_n)\,\sigma .$$

Soundness of the step is the logic of the rule read right to left: any store satisfying the new conjunction under some substitution satisfies the rule body, hence the rule head $H\sigma = A_i\sigma$, hence the old conjunction. Completeness over Horn rules is completeness of SLD resolution, which Volume 1 established for this exact rule format; what is new here is only the bookkeeping that collects every fully unfolded branch into a UCQ instead of racing to one answer. This is the reformulation step of PerfectRef, the rewriting algorithm at the heart of the DL-Lite family, in Horn clothing [3]. The companion's implementation is a breadth-first frontier over partial queries (mat_vs_rewrite.py lines 185–206):

    frontier: list[tuple[int, tuple, list[tuple]]] = [(0, goal, [goal])]
    seen: set[tuple] = set()
    ucq: list[tuple[tuple, tuple]] = []
    while frontier:
        d, g, cq = frontier.pop(0)
        i = next((j for j, a in enumerate(cq) if a[0] in IDB), None)
        if i is None:
            key = _canon(g, cq)
            if key not in seen:
                seen.add(key)
                ucq.append((key[0], list(key[1])))
            continue
        if d == max_unfold:
            continue  # truncated: this branch's answers are given up
        for rule in rules:
            head, body = rename(rule, counter)
            s = unify(head, cq[i], {})
            if s is None:
                continue
            new_cq = [apply_sub(a, s) for a in cq[:i] + body + cq[i + 1:]]
            frontier.append((d + 1, apply_sub(g, s), new_cq))
    return ucq

A partial query with no IDB atom left is finished and joins the UCQ (deduplicated by canonical renaming); answering the goal then means evaluating each CQ over the base index and unioning the instantiated goals (mat_vs_rewrite.py lines 209–221).

Does the frontier empty? For the non-recursive predicates, yes, and the argument is a rank induction worth making explicit. Assign every EDB predicate rank 0, and every non-recursive IDB predicate the rank one more than the largest rank appearing in any of its rule bodies: researcher has rank 1 (its bodies mention only the base predicates professor and student), person has rank 2 (its body mentions researcher), grandAdvisor and colleague have rank 1. Each unfolding step removes one atom of some rank $r \ge 1$ and inserts finitely many atoms of rank strictly below $r$. Since no rank here exceeds 2, track the pair (number of rank-2 atoms in the partial query, number of rank-1 atoms). A step on a rank-2 atom lowers the first count by one; it may raise the second count, which will not matter. A step on a rank-1 atom leaves the first count unchanged and lowers the second by one, since only rank-0 atoms come in. Every step therefore strictly decreases the pair in dictionary order: either the first count drops, or it stays put and the second drops. No infinite sequence of steps is possible: along such a sequence the first count, a non-negative integer that never increases, would eventually stop changing, and from that point on the second count would have to decrease forever, which a non-negative integer cannot do. So every branch of the unfolding halts, the frontier empties on its own, and the UCQ is finite and complete. The rule citesTransitively(A, C) ← cites(A, B), citesTransitively(B, C) breaks the assignment: its head predicate appears in its own body, no finite rank exists, and each unfolding of the recursive atom produces another copy of it, one hop further out. The implementation is honest about this: the max_unfold cap truncates such branches, and a truncated branch's answers are simply given up. For the base academic world the module runs the rewriter with a cap of 3, which exceeds the citation chain's diameter of 2, so the truncation costs nothing there; the recursion-wall section measures exactly what it costs when the data outgrows the cap.

The crossover, computed from the committed constants

The experiment's discipline comes first, because without it the cost comparison would be meaningless: both strategies must return identical answers on every query, so that cost is the only thing being traded. The harness runs a five-query ledger, one query per rule family, and for each goal checks the materialized lookup against the rewritten UCQ against Volume 1's SLD prover, an independent backward-chaining engine in a different file (mat_vs_rewrite.py lines 352–356):

        a_mat, p_mat = answers_mat(goal, index(mat))
        a_rew, n_cq, p_rew = answers_rewrite(goal, base_idx, RULES, 3)
        a_sld = set(sld.answers(goal))
        # Three-way agreement: lookup, UCQ, and the backward-chaining oracle.
        assert a_mat == a_rew == a_sld, f"{goal}: strategies disagree"

Three-way agreement, never a self-comparison: if the materializer and the rewriter shared a bug, the oracle would catch it. With semantics pinned, the committed ledger is pure accounting:

  query                              answers  CQs  probes mat  probes rew
  person(X)                                5    2          5           5
  researcher(X)                            5    2          5           5
  grandAdvisor(alice, Z)                   2    1          3           8
  colleague(carol, Y)                      2    1          8          13
  citesTransitively(p3, X)                 2    3          3          12

Read the rows, because each teaches something different. The two unary queries tie at 5 probes each: their UCQs (person unfolds through researcher to the union of professor and student) contain only single-atom CQs, so evaluating them scans exactly the same base facts a closure lookup would scan in the derived index. Rewriting loses nothing when the unfolding eliminates all joins. The three binary queries are where the join cost lands: grandAdvisor(alice, Z) is one CQ, advises(alice, Y), advises(Y, Z), and its left-to-right join scans the 4-fact advises index once to bind Y and once more per binding, 8 probes against the lookup's 3. The harness asserts the pattern in general, p_mat <= p_rew always, and strictly whenever some CQ in the rewriting has more than one atom (mat_vs_rewrite.py lines 359–361): the join did not disappear under materialization, it was paid at load time and its result stored.

Now assemble the identity. One pass of the whole ledger costs materialization $5+5+3+8+3 = 24$ probes and rewriting $5+5+8+13+12 = 43$ probes; materialization also carries its intercept of 236 load probes. Treat one ledger pass as the workload unit $q$ (the module prints the per-query constants; the totals below are arithmetic on those committed numbers, not a separate experiment):

$$\mathrm{Total}^{m}(q) = 236 + 24\,q, \qquad \mathrm{Total}^{r}(q) = 43\,q,$$

and the crossover of the two lines is

$$q^{*} \;=\; \frac{236}{43 - 24} \;=\; \frac{236}{19} \;\approx\; 12.42 .$$

ledger passes $q$	materialize: $236 + 24q$	rewrite: $43q$	cheaper strategy
1	260	43	rewriting, by 6×
5	356	215	rewriting
12	524	516	rewriting, barely
13	548	559	materialization, barely
100	2,636	4,300	materialization, by 1.6×

The table is the chapter's thesis in five rows. Ask the ledger once and materialization has done six times too much work: it derived colleague facts and person facts nobody asked about, the dawn-prep kitchen chopping onions for orders that never came. Ask it a hundred times and rewriting has re-derived the same grandAdvisor join a hundred times while the materialized store served each repeat for 3 probes. The flip sits at thirteen passes, and its location is the tunable insight: a bigger closure or costlier rules raise the intercept and push $q^{*}$ right; heavier queries with deeper joins widen the slope gap and pull it left. Query-light, data-heavy, update-heavy regimes live left of the crossing and want rewriting; query-heavy, read-mostly regimes live right of it and want materialization. Nothing about the miniature's scale changes this shape, only the constants: at the billion-triple scale the intercept is hours of single-threaded work, minutes on 128 cores, rather than 236 probes [2], and cold data that will be queried once, or never, is exactly the case where paying that intercept is a mistake, which is why rewriting engines advertise that load is free and cold data stays cold.

Maintenance: the cost the identity hides

The identity $\mathrm{Total}(q) = C_{\text{load}} + q\,C_{\text{query}}$ has no term for change, and change is where the two strategies stop being mirror images. Modern materialization engines treat incremental update as a first-class algorithmic problem, since re-running the fixpoint from scratch on every edit would forfeit the amortization the whole strategy exists to buy [4]. The companion prices both directions of change on the academic world:

[2] updates break the symmetry
  add advises(alice, carol):
    materialized: semi-naive delta, 1 round, 12 probes → +1 derived grandAdvisor(alice, erin)
    rewriting   : ZERO maintenance — the same UCQ over the grown
                  base already answers grandAdvisor(alice, erin)
  delete cites(p3, p2) with the diamond cites(p3, p1) asserted:
    naive drop leaves a STALE fact: citesTransitively(p3, p2)
    DRed overdeletes 2 derived facts (both citesTransitively above p3) ...
    ... and re-derives 1: citesTransitively(p3, p1) has a second proof via the diamond
    result == the from-scratch fixpoint, fact for fact

Insertion is the easy direction, and the delta rule already derived is the reason. Adding advises(alice, carol) seeds $\Delta_0$ with one fact; the semi-naive loop quoted earlier joins it against the store, derives grandAdvisor(alice, erin) (alice now advises carol, who advises erin), finds nothing further, and stops: 1 round, 12 probes, against the 236 the original closure cost from scratch, and the harness asserts the incrementally maintained closure equals the from-scratch fixpoint of the grown base exactly (mat_vs_rewrite.py lines 366–368). Monotonicity does all the work: Horn rules only ever add consequences, so old derivations stay valid and the new fact's consequences are a pure top-up. The rewriting side is even better: there is nothing to maintain, because nothing derived is stored. The same UCQ evaluated over the grown base sees the new composition immediately, which the harness also asserts against the oracle (mat_vs_rewrite.py lines 375–380).

Deletion is the hard direction, and the reason is a counting fact the module engineers on purpose: a derived fact may have more than one derivation. Before deleting, the module asserts the extra base fact cites(p3, p1), giving citesTransitively(p3, p1) two independent proofs: the direct edge, and the two-hop path through p2. Now delete the base fact cites(p3, p2). Naively dropping it from the closure leaves the store stale: citesTransitively(p3, p2) is still sitting in the index though no surviving derivation supports it, and the harness pins this exact fact as the unique stale survivor (mat_vs_rewrite.py lines 386–390). A materialized store cannot just forget a base fact; it must decide, for every derived fact downstream, whether some other support keeps it alive. The classical answer is DRed, delete-and-rederive [5], an overdelete-then-repair discipline (mat_vs_rewrite.py lines 291–308):

    old_idx = index(closure)
    deleted: set[tuple] = {fact}
    while True:
        new: set[tuple] = set()
        for head, body in rules:
            subs, _ = eval_cq(body, old_idx)
            for s in subs:
                if any(apply_sub(a, s) in deleted
                       for a in body if a[0] != "neq"):
                    h = apply_sub(head, s)
                    if h not in deleted:
                        new.add(h)
        if not new:
            break
        deleted |= new
    survivors = closure - deleted
    final = fc.least_fixpoint(survivors, rules)
    return final, deleted, final & deleted

Phase one closes the deleted set upward: any head with some one-step derivation over the old closure using a deleted fact joins the set. This over-approximates on purpose. Its correctness direction is an induction on derivation height: if every derivation of a fact uses the deleted base fact, then at the top of each derivation some body atom is (inductively) deleted, so the fact enters the set; hence nothing that truly lost all support survives phase one. But the converse fails, and the diamond shows it failing: both citesTransitively(p3, p2) and citesTransitively(p3, p1) have a derivation through the deleted edge, so both are overdeleted, even though the second still has an intact alternative proof. Phase two repairs the collateral damage: re-run the rules to fixpoint from the survivors, and every overdeleted fact with an independent derivation comes back. The committed counts are the exhibit: overdelete 2, re-derive 1, final closure equal to the from-scratch fixpoint fact for fact, with all three sets asserted exactly (mat_vs_rewrite.py lines 391–401). Note the pleasant economy in the last two lines of the excerpt: the repair phase is Volume 1's own least_fixpoint (examples/logic/forward_chain.py lines 52–63), the maintenance algorithm literally reusing the load-time engine.

The overdelete-and-repair churn is DRed's known weakness when facts are richly supported, and the field's sharper answer inverts the phases: the Backward/Forward algorithm checks, before deleting a candidate, whether an alternative derivation from surviving facts exists, by running a backward search for support combined with forward checks, and deletes only when none is found [4]. The diamond fact is precisely the case it is built for: one backward probe would find the surviving edge cites(p3, p1) and spare citesTransitively(p3, p1) the round trip through deletion and resurrection. The companion implements DRed alone and cites Backward/Forward; what its counted run contributes is the why: a measured instance of the round trip that the alternative-derivation check exists to avoid. On the rewriting side, deletion, like insertion, is free: drop the base fact, and the next query's UCQ simply no longer finds it. The maintenance column of the trade therefore reads: rewriting pays nothing ever; materialization pays a small delta for insertions and a genuinely subtle algorithm for deletions. An update-heavy workload shifts the crossover right just as surely as a query-light one does.

The recursion wall and the fragment dependence

Everything so far has treated the two strategies as interchangeable in meaning and different only in cost. The chapter's deepest point is that this symmetry is a property of the logic, and it breaks. The companion builds the breaking point as a synthetic citation chain, a one-parameter scaling axis (mat_vs_rewrite.py lines 316–318):

CHAIN_M: int = 8
CHAIN_FACTS: list[tuple] = [
    ("cites", f"c{i}", f"c{i + 1}") for i in range(CHAIN_M)]

Eight facts, $c_0 \to c_1 \to \cdots \to c_8$, so the goal citesTransitively(c0, X) has eight answers, the farthest of which needs recursion depth 8. Materialization does not notice: the same two Datalog rules close the chain at any length, because the fixpoint runs until it is done, however deep "done" turns out to be. Rewriting, by contrast, must fix its unfolding depth $k$ before seeing the data, and each unfolding of the recursive rule reaches exactly one hop further. The committed sweep over $k$:

[3] the recursion wall — citesTransitively(c0, ?) on the 8-hop chain
  a depth-k UCQ holds one CQ per path length ≤ k: sound at every
  k, complete only when k reaches the data's diameter
     k   CQs  answers/8  probes  complete?
     1     1      1/8       8   no
     2     2      2/8      24   no
     3     3      3/8      48   no
     4     4      4/8      80   no
     5     5      5/8     120   no
     6     6      6/8     168   no
     7     7      7/8     224   no
     8     8      8/8     288   yes

The harness asserts each row's shape: a depth-$k$ UCQ holds one CQ per path length up to $k$, returns exactly the $k$ nearest answers (sound, never inventing one), and is complete only at $k = 8$, the data's diameter (mat_vs_rewrite.py lines 411–423). Grow the chain and the wall moves with it: no fixed $k$ chosen in advance survives every dataset. This is the finite shadow of a real theorem. Theorem (imported) [6]: transitive closure is not first-order expressible: there is no first-order formula $\varphi(x, y)$ over a binary relation symbol $E$ such that, on every finite graph, $\varphi$ holds of exactly the pairs connected by a directed $E$-path. Decoded: "first-order" means quantifying over individuals only, which is exactly the expressive power of a UCQ, and indeed of a plain SQL query without recursion; the theorem says no such query, however large, computes reachability on all inputs. The proof, a locality argument of finite model theory showing that any fixed first-order formula can only see a bounded-radius neighborhood of its arguments while reachability needs unbounded radius, is beyond this volume; what the companion demonstrates instead is the exhibit a finite instance can give, the depth-$k$ rewriting failing at every $k$ below the diameter, which illustrates the theorem and does not prove it.

The systems consequence is the fragment dependence, and it deserves a precise statement on each side. Theorem (imported) [3]: for every DL-Lite TBox $\mathcal{T}$ (the terminology axioms) and every conjunctive query $q$, the PerfectRef algorithm computes a finite UCQ $q_{\mathcal{T}}$ such that for every ABox $\mathcal{A}$ (the assertional data) consistent with $\mathcal{T}$, the certain answers of $q$ over $(\mathcal{T}, \mathcal{A})$ equal the answers of $q_{\mathcal{T}}$ evaluated directly over $\mathcal{A}$ stored as a plain database. (The consistency proviso costs nothing: whether a DL-Lite knowledge base is consistent is itself decided by evaluating one fixed first-order query over the data, so the whole task stays first-order.) This property is FO-rewritability: the TBox compiles into the query, completely, so query answering in DL-Lite runs as ordinary SQL over ordinary tables with zero load-time reasoning, and its data complexity (the cost measured as the data grows, with the query and the TBox held fixed) falls into the class evaluable by fixed relational queries. That is a designed outcome, not a lucky one: DL-Lite's axiom shapes were chosen to be exactly what first-order rewriting can absorb, and OWL 2 QL, the web-ontology profile built on it, forbids transitivity and recursion for precisely the reason the chain exhibits, while OWL 2 RL, the profile built for rule engines, keeps them because materialization handles them. On the other side, the same source delimits the boundary: enrich the axioms with EL-style constructs (qualified existentials on the left of subsumptions) and query answering becomes PTIME-hard in data complexity [3], while Volume 2 already showed EL classification is PTIME-complete. A PTIME-hard problem cannot be solved by a fixed first-order query, whose evaluation sits in $\mathrm{AC}^0$, the class of constant-depth boolean circuits that captures fixed first-order queries and is provably weaker than PTIME; the proof of that separation is likewise beyond the volume. The upshot is the sentence this chapter exists to earn: choosing a logic chooses your systems options. In DL-Lite, rewriting is complete by theorem and you may sit at either pole as the workload dictates. In EL and richer Horn fragments, pure query rewriting is insufficient in principle, materialization (or a hybrid that materializes a bounded core and rewrites over it, the "combined approach" family) is mandatory for completeness, and the whole maintenance apparatus of the previous section comes with it.

The systems anchors

Each pole of the miniature has a production system standing on it, and the numbers already quoted are theirs. The materialization pole is anchored by RDFox: the semi-naive, non-repeating discipline derived above, made parallel by partitioning work by newly derived fact so that load balance is emergent rather than scheduled [1], and reported at scale on LUBM-50K: 6.7 billion explicit triples closing to 9.2 billion, a materialization rate of 6.1 million triples per second, and a 128-thread run 69.6 times faster than one thread [2]. The rewriting pole is anchored twice. In the DL-Lite lane, PerfectRef-style engines (the ontology-based data-access, OBDA, family) compile the TBox into SQL and ship every query to an unmodified relational database, the strategy whose completeness is the theorem above [3]; their home regime is query-light, update-heavy, data-behind-someone-else's-firewall. In the expressive-DL lane, Konclude, a tableau reasoner for logics far beyond Horn, leans on absorption: preprocessing that rewrites general axioms into a triggered form, so that each applies deterministically, and only when an individual's known memberships make it relevant, instead of forcing a speculative case split everywhere [7]. The source presents absorption as a tableau optimization; read through this chapter's lens, it is the same accounting instinct wearing different machinery: do not pay for axioms that nobody's individuals touch.

pole	anchor	design signature	home regime
materialize	RDFox [1] [2]	parallel semi-naive closure, by-fact partitioning, incremental maintenance	read-mostly, query-heavy, recursion-bearing (OWL 2 RL / Datalog)
rewrite	PerfectRef / OBDA engines [3]	TBox compiled into a UCQ, evaluated as SQL over the raw data	query-light, update-heavy, FO-rewritable (DL-Lite / OWL 2 QL)
rewrite (expressive)	Konclude [7]	absorption: axioms rewritten to trigger lazily, only when relevant	expressive DLs where full materialization is impossible

The NeSy echo: the same trade wearing vectors

Volume 4 ran this exact trade without naming it. QTO (Query computation Tree Optimization), the training-free query optimizer of the fuzzy and training-free complex logical query answering (CLQA) chapter, precomputed its neural adjacency matrices, one dense entity-by-entity score table per relation, before answering anything: a load-time closure of the 1-hop predictor's beliefs, paid once so that every multi-hop query becomes tensor lookups and max-products over stored scores. That is materialization in embedding space, intercept and all (the memory footprint of those matrices is the closure's storage rent). CQD (Continuous Query Decomposition), from the same chapter, did the opposite: it kept only the trained link predictor and unfolded each query at answering time into a sequence of 1-hop calls glued by t-norms, paying per query and storing nothing derived. That is rewriting in embedding space, steep slope and all (deep queries cost it dearly, exactly where the ledger's join rows hurt). Even the maintenance column carries over: swap in a retrained predictor and CQD picks it up on the next query for free, while QTO must re-materialize every adjacency matrix, and nothing smarter than from-scratch recomputation is on offer. The classical accounting identity, it turns out, does not care whether the consequences being bought are crisp facts or scores.

The unsolved part

The clean two-pole picture is a pedagogical kindness; practice lives between the poles, and the between has no clean theory. Partial materialization asks which derived predicates, or which fragments of them, deserve storage: materialize grandAdvisor because the workload hammers it, rewrite colleague because nobody asks. Formally this is view selection, choosing a set of materialized views to minimize the identity's total under a storage budget, and it is a workload-dependent combinatorial optimization whose inputs (the future workload, the future update stream) are exactly what a system does not know in advance. Engines ship heuristics; nobody ships a theorem. Streaming and time-varying data stress both poles at once: a materialized store faces a deletion per expiring fact (Volume 3's temporal annotations, read as validity intervals, make every fact a scheduled deletion), while a rewriting engine faces re-executing its UCQs against data that changed mid-answer. And this volume's own trajectory adds the newest open front: when the "rules" are network weights, as they were for QTO's precomputed adjacencies, there is no DRed. A fine-tune that shifts the 1-hop predictor invalidates an unknown, unstructured subset of every materialized score, no derivation graph records which, and the only sound maintenance known is total recomputation. A delete-and-rederive discipline for learned closures, some analogue of the diamond exhibit's bookkeeping for gradients instead of derivations, does not exist yet, and the systems chapters ahead keep colliding with its absence.

Why it matters

This chapter is the hinge between the series' semantics and its systems. Volume 1's fixpoint, Volume 2's EL completion, and Volume 4's grounded circuits were all, in this chapter's vocabulary, materialization decisions taken silently; Volume 4's CQD was a rewriting decision taken silently. Naming the axis turns those defaults into choices with prices, and the prices are the ones your own research will pay: if your benchmark asks a million queries against a frozen knowledge graph, you are at $q \gg q^{*}$ (the symbol $\gg$ reads "much greater than": a workload far above the crossover) and precomputation is not cheating, it is arithmetic; if your system ingests a live stream and answers occasional questions, you are at small $q$ and every materialized tensor is rent on storage plus an unbudgeted maintenance liability. The fragment dependence is the deeper research instrument. It says expressiveness claims and systems claims are the same claim: adding one axiom shape to your logic can move query answering from "compiles to SQL, by theorem" to "requires a maintained closure, by theorem," and a NeSy architecture that fixes its unfolding depth in advance, as every fixed-layer network does, has taken a position on this axis whether its authors noticed or not. The next two chapters make that observation quantitative, first for the reasoner and then for the transformer.

Key terms

• Materialization: computing and storing the least fixpoint of the rules over the base facts at load time, so queries become index lookups; the OWL 2 RL / Datalog engine strategy.
• Query rewriting: unfolding a query backward through the rules into a union of conjunctive queries over base predicates, evaluated against the raw data; load-free, paid per query.
• Union of conjunctive queries (UCQ): a finite disjunction of joins; the target format of rewriting, and exactly the expressive power of first-order queries without recursion.
• EDB / IDB: the extensional database (predicates stored as base facts) versus the intensional database (predicates defined by rule heads); rewriting terminates when only EDB atoms remain.
• Semi-naive evaluation / delta rule: the discipline of joining only rule instances with at least one newly derived body fact, proved above to find every first-time firing; the non-repetition property is its guarantee that no instance fires twice.
• Amortization: repayment of the load-time intercept through per-query savings; complete at the crossover workload $q^{*} = C^{m}_{\text{load}} / (C^{r}_{\text{query}} - C^{m}_{\text{query}})$.
• DRed (delete-and-rederive): deletion maintenance that overdeletes everything with some derivation through the deleted fact, then re-derives survivors from the remainder; correct, and wasteful exactly when facts have alternative derivations.
• Backward/Forward algorithm: deletion maintenance that searches for an alternative derivation before deleting a candidate, avoiding DRed's overdelete-and-repair round trip.
• FO-rewritability: the property that TBox reasoning compiles completely into a finite first-order (UCQ) rewriting of every query; holds for DL-Lite by theorem, fails for EL and for transitive closure in principle.
• Probe: the companion's cost unit: one candidate fact scanned under a predicate index, or one ground disequality check.

Where this leads

Materialization won the right half of every table in this chapter, which makes its intercept the next bottleneck: if the closure is what you pay, how fast can the closure itself be built? GPU Reasoning takes Volume 2's EL completion, re-expresses the whole rule calculus as boolean matrix algebra, and batches the fixpoint across a hundred ontologies at once, with the semi-naive delta discipline of this chapter reappearing as a matrix mask and every closure checked cell for cell against the symbolic oracle.

---

Companion code: examples/frontier/mat_vs_rewrite.py implements the counted naive fixpoint, the resolution-based UCQ rewriter, the semi-naive addition delta, DRed deletion, and the recursion wall, on top of Volume 1's examples/logic/kb.py, forward_chain.py, sld.py, and unify.py. Run python3 examples/frontier/mat_vs_rewrite.py to reproduce every number in this chapter; the run is deterministic and every claim is guarded by an assert, with the query ledger checked three-way against the independent SLD oracle.