Datalog: Rules, the T_P Operator, and Least Fixpoint

📍 Where we are: Part IV · Datalog and the Chase — Chapter 12. Consequence-Based Reasoning showed a description-logic reasoner deriving subsumptions by growing two ledgers to a fixpoint; now we strip that engine down to its purest form — a rule language called Datalog — and prove the fixpoint is not a trick but the definition of what a rule program means.

Every reasoner in this volume so far has been the same loop in disguise: fire a fixed set of rules over the facts you have, collect what they conclude, and repeat until a round changes nothing. This chapter names the loop's home. Datalog is the small, exact rule language whose entire semantics is that loop, and it is worth meeting on its own because it is the common ancestor of forward chaining, the EL completion algorithm, and the query engines behind real knowledge graphs. We will decode one rule, define the operator that runs it, prove the loop reaches a unique answer, and then watch it rebuild the academic world atom for atom.

The simple version

Imagine a room full of clerks, each holding one small rule of the form "if these facts are on the board, write this new fact on the board." Nobody erases anything. You ring a bell; every clerk whose rule now applies steps up and writes their conclusion. You ring the bell again, and now clerks whose rule needed those new facts get to write too. You keep ringing until a whole round passes where no clerk has anything new to add. At that moment the board holds every fact the rules can ever produce — no more, no less. Datalog is exactly this room, the bell is the operator $T_P$, and "the board when the bell stops mattering" is the least fixpoint.

What this chapter covers

• A Datalog rule, decoded — the shape head :- body₁, …, bodyₙ, why the only terms allowed are constants and variables, and why banning function symbols makes the pool of derivable facts finite.
• The immediate-consequence operator $T_P$ — one round of reasoning as a function on fact sets: fire every rule whose body holds, add every head, and hand the enlarged set back.
• Least fixpoint = least model — iterating $T_P$ from the base facts until it stops growing, and why the answer is unique, guaranteed by Knaster–Tarski and equal to Volume 1's forward chaining.
• Running the academic world — the seven real Horn rules and the committed output: the least fixpoint in three waves, sizes [23, 41, 47, 47], 47 atoms total, 24 derived.
• Reading the derived relations — five researchers, three grandAdvisor pairs, three transitive citations, eight colleague pairs, and the neq guard that keeps colleague irreflexive.
• Why recursion needs the fixpoint — how citesTransitively(p3, p1) can only appear one wave after citesTransitively(p2, p1), so no fixed number of sweeps is safe.
• The unsolved part — Datalog can only recombine constants it already has; the moment a rule must assert that something exists without naming it, we need existential rules and the chase.

A Datalog rule, decoded

A Datalog program is a finite set of rules. Each rule is written

$$\underbrace{H}_{\text{head}} \;\text{:-}\; \underbrace{B_1, B_2, \ldots, B_n}_{\text{body}}.$$

Read the neck symbol :- as "holds if": the single atom $H$ on the left is concluded true whenever every atom $B_1, \ldots, B_n$ in the body on the right is true, for some consistent assignment of values to the variables. An atom is a predicate applied to arguments, like advises(alice, bob); a rule with an empty body ($n = 0$) is just a stored fact. Here is a rule from the companion file, the one that composes advising with itself:

(("grandAdvisor", "?x", "?z"),
 [("advises", "?x", "?y"), ("advises", "?y", "?z")]),

In ordinary Datalog notation that is grandAdvisor(?x, ?z) :- advises(?x, ?y), advises(?y, ?z) — read "$?x$ is the grand-advisor of $?z$ if $?x$ advises some $?y$ who in turn advises $?z$." Two features define the whole language. First, the only terms are constants and variables — nothing else. A constant names a fixed individual (alice, p1, mit); a variable is a placeholder that a rule firing binds to a constant. The companion marks variables by a leading ? so that capitalized concept names stay constants (datalog.py lines 43–46):

def is_var(t) -> bool:
    """A Datalog variable is a string beginning with ``?`` (so capitalised
    constants such as ``Professor`` are *not* mistaken for variables)."""
    return isinstance(t, str) and t.startswith("?")

Second — and this is the load-bearing restriction — Datalog is function-free: there are no function symbols, so no term can nest, and a rule can never build a brand-new structured object like $f(f(\text{alice}))$. Every head a rule produces is ground by substituting constants that were already in the program. Because the program has finitely many predicates and finitely many constants (the academic world has 13: five people, three papers, two institutions, three topics), only finitely many ground atoms can ever be formed. That finite pool is the Herbrand base $B_P$, and the fact that it is finite is the reason everything below terminates: reasoning can only ever add atoms drawn from $B_P$, and a set that only grows inside a finite ceiling must stop growing [1]. This is Datalog as function-free Horn logic — Horn because every rule has exactly one positive head and a conjunction of positive body atoms, no disjunction and no negation.

The immediate-consequence operator $T_P$

One round of reasoning is a function on sets of facts. Given the current facts, it fires every rule whose body is satisfied and returns those facts plus every head so derived. This function is the immediate-consequence operator, written $T_P$ — the subscript $P$ names the program of rules. In the companion it is eight lines including its docstring (datalog.py lines 93–100):

def t_p(facts: set, rules: list) -> set:
    """One application of the immediate-consequence operator T_P: the given facts
    plus every rule head derivable from them in a single step."""
    out = set(facts)
    for head, body in rules:
        for sub in _match_body(body, facts, {}):
            out.add(_apply(head, sub))
    return out

Line by line: out = set(facts) copies the current facts, so $T_P$ never deletes anything; the loop over rules tries each rule; _match_body yields every variable-to-constant substitution that makes the whole body true in the current facts; and out.add(_apply(head, sub)) fires the rule by adding the head under that substitution. Written as a set equation, for a set $S$ of atoms,

$$T_P(S) \;=\; S \,\cup\, \{\, H\sigma \;:\; (H \text{ :- } B_1, \ldots, B_n) \in P,\ B_i\sigma \in S \text{ for all } i \,\},$$

where $\sigma$ is a substitution of constants for the rule's variables and $H\sigma$ is the head with that substitution applied; the colon reads "such that" and $\cup$ is set union. The operator has one property everything hinges on: it is monotone — feed it a bigger set of facts and it can only give back a bigger result, $S \subseteq S' \Rightarrow T_P(S) \subseteq T_P(S')$. This holds precisely because every body atom is positive: adding facts can only satisfy more rule bodies, never switch one off. (Negation in a body would break this, which is why plain Datalog forbids it.)

Least fixpoint = least model

To reason with the program you apply $T_P$ over and over. A set $S$ with $T_P(S) = S$ is a fixpoint: firing every rule produces nothing you did not already have. The meaning of the program is the least fixpoint, written $\mathrm{lfp}(T_P)$ — the smallest such set — and the loop that reaches it is the plainest imaginable (datalog.py lines 103–114):

def least_fixpoint(edb, rules, trace: bool = False):
    """Iterate T_P from the EDB facts until it stops growing — the least fixpoint
    lfp(T_P), i.e. the least model. With ``trace=True`` also return the per-wave
    size list, exposing how the derivation grows."""
    current = set(edb)
    sizes = [len(current)]
    while True:
        nxt = t_p(current, rules)
        sizes.append(len(nxt))
        if nxt == current:
            return (current, sizes) if trace else current
        current = nxt

The seed current = set(edb) starts from the EDB (the extensional database — the base facts asserted directly, as opposed to the IDB, the intensional database of relations the rules derive). The line nxt = t_p(current, rules) is one application $S_{t+1} = T_P(S_t)$, and if nxt == current is the fixpoint test $T_P(S) = S$ turned into an if. Because seeding with the EDB is the same as treating those facts as empty-bodied rules and seeding from the empty set, the whole climb is captured by one display equation:

$$\mathrm{lfp}(T_P) \;=\; \bigcup_{n \ge 0} T_P^{\,n}(\varnothing),$$

where $T_P^{\,n}$ means "$T_P$ applied $n$ times," $\varnothing$ is the empty set, and $\bigcup$ collects the atoms that appear at any round. Two theorems from Volume 1 make this legitimate rather than hopeful. The Knaster–Tarski theorem guarantees a monotone operator on the complete lattice of subsets of the Herbrand base has a least fixpoint at all; the Kleene construction says iterating from $\varnothing$ reaches it, and since $B_P$ is finite the ascending chain $\varnothing \subseteq T_P(\varnothing) \subseteq T_P^2(\varnothing) \subseteq \cdots$ must halt after finitely many strict growth steps. The classical result of logic programming closes the loop: this least fixpoint equals the least model — the smallest set of facts making every rule true — so the procedure and the meaning coincide [1]. This is the identical engine as Volume 1's forward_chain.py; Datalog is just the name the database world gives it [2].

Running the academic world

Part A of the companion re-expresses the academic world's rules in the ?-variable convention and runs them from scratch. The seven rules are the whole intensional vocabulary — researcher, person, grandAdvisor, colleague, and transitive citation (datalog.py lines 121–132):

HORN_RULES = [
    (("researcher", "?x"), [("professor", "?x")]),
    (("researcher", "?x"), [("student", "?x")]),
    (("person", "?x"), [("researcher", "?x")]),
    (("grandAdvisor", "?x", "?z"),
     [("advises", "?x", "?y"), ("advises", "?y", "?z")]),
    (("colleague", "?x", "?y"),
     [("affiliated", "?x", "?i"), ("affiliated", "?y", "?i"), ("neq", "?x", "?y")]),
    (("citesTransitively", "?a", "?b"), [("cites", "?a", "?b")]),
    (("citesTransitively", "?a", "?c"),
     [("cites", "?a", "?b"), ("citesTransitively", "?b", "?c")]),
]

Running python3 datalog.py prints the climb and what it derived — this is the real, committed output:

Part A — academic-world Horn rules
  least fixpoint in 3 waves; sizes: [23, 41, 47, 47]
  47 atoms total, 24 derived
  researchers (5): ['alice', 'bob', 'carol', 'dave', 'erin']
  grandAdvisor (3): [('alice', 'carol'), ('alice', 'dave'), ('bob', 'erin')]
  citesTransitively (3): [('p2', 'p1'), ('p3', 'p1'), ('p3', 'p2')]
  colleague pairs: 8

Read [23, 41, 47, 47] as the ascending chain $S_0 \subseteq S_1 \subseteq S_2 \subseteq S_3$ with the size $\lvert S_t\rvert$ printed rung by rung. The final $47 = 47$ is the wave that changes nothing and so proves, by nxt == current, that the fixpoint is reached — three waves in all, two productive and the third merely confirming, exactly as in Volume 1. Here is which atoms enter on each wave and why:

wave $t$	$\lvert S_t\rvert$	atoms added this wave	rule(s) that fired
0	23	the 23 EDB facts (the seed)	none yet
1	41	+18: researcher×5, grandAdvisor×3, colleague×8, citesTransitively×2	every rule whose body reads a base fact
2	47	+6: person×5, citesTransitively(p3, p1)×1	the two rules that read a derived fact
3	47	+0	every firing repeats an atom already present

The 24 derived atoms split with no remainder as 5 researcher + 5 person + 3 grandAdvisor + 8 colleague + 3 citesTransitively, and $23 + 24 = 47$.

Datalog evaluation as an ascending chain: iterating $T_P$ from the 23 EDB facts grows the set along $S_0 \subseteq S_1 \subseteq S_2 \subseteq S_3$ (sizes 23, 41, 47, 47) and halts at the least fixpoint, with the two-hop citation p3 → p1 arriving one wave after the one-hop p2 → p1 it is built on. Original diagram by the authors, created with AI assistance.

Reading the derived relations

The printed relations are the intensional database, and each is a small argument you can check by eye. The five researchers are everyone who is a professor or a student, and every one of them is then a person in the next wave — a two-link chain professor/student ⟹ researcher ⟹ person. The three grandAdvisor pairs — (alice, carol), (alice, dave), (bob, erin) — are the advising chains alice → bob → carol, alice → bob → dave, and bob → carol → erin, composed by the role-chain rule. The three transitive citations close the chain p3 → p2 → p1: the two direct edges (p2, p1) and (p3, p2) plus the derived reachability (p3, p1).

The eight colleague pairs are the ordered same-institution pairs: two at mit (alice–bob, both directions) and six among the three cmu students. What keeps a person from being listed as their own colleague is the neq guard in the body. It is not a stored fact but a built-in the engine evaluates directly (datalog.py lines 81–86):

    if first[0] == "neq":
        x = sub.get(first[1], first[1])
        y = sub.get(first[2], first[2])
        if not is_var(x) and not is_var(y) and x != y:
            yield from _match_body(rest, facts, sub)
        return

The guard succeeds only when its two arguments have been bound to different constants, so colleague(carol, carol) is blocked before it can be added. Without it the relation would be reflexive and the count would balloon; with it, colleague is irreflexive, and the tally is exactly 8.

Why recursion needs the fixpoint, not one sweep

Most of the rules settle in a bounded number of waves — person waits for researcher, which waits for professor, a fixed three-layer chain you could unroll in advance. Recursion is different, and the transitive-citation rule is the reason the fixpoint machinery cannot be replaced by a fixed number of passes:

    (("citesTransitively", "?a", "?b"), [("cites", "?a", "?b")]),
    (("citesTransitively", "?a", "?c"),
     [("cites", "?a", "?b"), ("citesTransitively", "?b", "?c")]),

The second clause feeds its own head back into its own body. Watch what one sweep can and cannot do on the citation chain p3 → p2 → p1. In wave 1 the non-recursive base-case clause turns each direct cites edge into a citesTransitively edge, so citesTransitively(p2, p1) and citesTransitively(p3, p2) appear. But citesTransitively(p3, p1) cannot yet: the recursive clause needs citesTransitively(p2, p1) sitting in its body, and that atom did not exist when wave 1 began. Only in wave 2, with citesTransitively(p2, p1) now on the board, does the recursive clause fire to produce citesTransitively(p3, p1):

wave	citesTransitively atoms present	why
1	(p2, p1), (p3, p2)	base-case clause on the two direct cites edges
2	(p2, p1), (p3, p2), (p3, p1)	recursive clause: cites(p3, p2) ∧ citesTransitively(p2, p1)
3	unchanged	no new pair to compose; fixpoint confirmed

That single delayed atom is the whole point. A conclusion two hops deep is unreachable until the one-hop conclusion beneath it exists, and because a citation chain can be any length, no number of sweeps fixed in advance is safe — a chain of $k$ papers needs $k-1$ waves before its longest reachability atom appears. This is why transitive closure is the textbook example of genuine recursion that no fixed set of relational joins can express, and why Datalog's semantics must be a fixpoint rather than a bounded unrolling [3]. Reasoning here stops being a fixed computation and becomes reaching a limit.

The unsolved part

Datalog's guarantees — a unique least model, reached in finitely many waves — are bought entirely by the function-free restriction, and that same restriction is its ceiling. Datalog can only ever recombine constants it already has. Every atom in the 47-atom fixpoint is built from the 13 individuals named in the EDB; the rules shuffle those constants into new relations but never conjure a new one. This is exactly what keeps the Herbrand base finite and the climb terminating.

But real ontologies routinely need to say something exists without naming it: "every researcher has an advisor," even when no specific advisor is on record. A rule whose head asserts $\exists r.C$ — some unnamed witness must exist — cannot be Datalog, because firing it would have to invent a fresh individual, and that invented individual is itself a researcher who needs an advisor, so the rule fires again on the thing it just made. The forward-chaining process that chases these obligations is the chase, and its ascending chain need never reach a fixpoint at all: it can climb forever, minting an endless tower of anonymous witnesses. The finiteness argument fails at its one arithmetic move — the Herbrand base is no longer finite — so "just iterate until nothing changes" stops being a plan. Where that leaves decidability, and which restricted rule shapes claw it back, is the open question the next chapter takes up.

Why it matters

Datalog is the crisp specification that every heavier reasoner in this volume, and every learned reasoner in the volumes ahead, is measured against. Its least fixpoint is a canonical answer: there is exactly one least model, it is complete (nothing derivable is missed), and it is reproducible to the atom — the same [23, 41, 47, 47] every run. For neuro-symbolic AI that makes it the ideal yardstick. When a differentiable rule layer or a graph-embedding model claims to "reason with rules," the question is whether it reaches this fixpoint or merely a plausible-looking approximation of it, and the transitive-citation case is precisely the kind of multi-hop, recursive inference that soft models tend to truncate. Knowing that Datalog's answer is unique and exactly computable is what lets you say whether a neural approximation landed on the right limit or a nearby wrong one — the same "requirements are tests" discipline, now with the requirement pinned to a fixpoint.

Key terms

• Datalog — function-free Horn logic: a finite set of rules head :- body₁, …, bodyₙ whose only terms are constants and variables, no function symbols.
• Rule / head / body / fact — a rule concludes its head atom whenever every body atom holds under some substitution; a fact is a rule with an empty body.
• Herbrand base $B_P$ — the finite pool of every ground atom the program can form; finite precisely because Datalog has no function symbols, which is why evaluation terminates.
• Immediate-consequence operator $T_P$ — the monotone map that fires every rule whose body holds and adds the heads; one application is one wave.
• Least fixpoint / least model — the smallest set closed under $T_P$, equal to $\bigcup_n T_P^n(\varnothing)$; the unique meaning of the program, guaranteed by Knaster–Tarski and reached by the Kleene climb on a finite base.
• EDB / IDB — the extensional database of asserted base facts versus the intensional database of relations the rules derive.
• neq guard — a built-in that holds only when its two ground arguments differ; it keeps colleague irreflexive, holding the count at 8.
• Recursion — a rule whose head re-enters its own body (transitive citation); the reason a fixpoint, not a bounded number of sweeps, is required.

Where this leads

Datalog gives us a rule engine with a perfect guarantee — one canonical answer, always reached — bought by never letting a rule assert that a new thing exists. The next chapter, Existential Rules and the Chase, removes exactly that restriction. It lets a rule head demand an unnamed witness, follows the forward-chaining chase that invents one, and confronts the consequence head-on: the climb can now run forever, decidability is no longer free, and the whole study of which existential-rule shapes keep reasoning terminable — or at least decidable — begins. The finite, friendly world of Datalog is where that harder story starts.