Evaluating Relations: the Least Fixpoint

Unification fired the second ancestor rule once, against the five parent facts and the five ancestor facts the first rule gives, and derived three new facts: ancestor("tom", "ann"), ancestor("tom", "pat"), and ancestor("bob", "jim"). One fact the family’s meaning contains was still missing. ancestor("tom", "jim") needs ancestor("bob", "jim") as a premise, and that fact did not exist until the firing produced it. Firing the rule again, with the new facts included, derives it.

A family tree cannot show what rules do over a cycle, since no one is their own ancestor. A course catalogue can contain one by mistake, so this chapter adds a second example, a catalogue in which requires(c, p) records that course c requires course p, and before(p, c) holds when p must be taken at some point before c:

relation requires : (String, String);
relation before   : (String, String);

rule before(p, c) :- requires(c, p);
rule before(p, c) :- requires(c, q) and before(p, q);

fn main() {
    add requires("compilers", "pl");
    add requires("pl", "data_structures");
    add requires("data_structures", "intro");
    println(solutions before(?p, "compilers"));
    println(solutions before(?c, ?c));
}

The first rule says a direct requirement comes before; the second says that whatever comes before one of c’s requirements comes before c. The program prints ["data_structures", "intro", "pl"], the courses to take before compilers, and []: no course has to be taken before itself. A catalogue in which some course did would be a mistake, and the second query is a check for one.

Suppose someone records that the introductory course requires compilers, add requires("intro", "compilers");. The requirements now run in a circle, and solutions before(?c, ?c) becomes ["compilers", "data_structures", "intro", "pl"]. Each course comes before itself, by way of the other three.

The two examples raise these questions:

• When does firing stop? Each firing can produce facts that let some rule fire again. What says the process ends, and that it ends at $M(P,\Delta )$ and not short of it or past it?
• What happens on a cycle? After the mistaken entry, every before fact can be followed around the circle to derive more. Why does evaluation not go around forever?
• How much work is repeated? A second firing of the ancestor rule re-derives the three facts the first one found, along with the new one. Can that be avoided without losing any fact?

The answers come from a result about logic programs from the mid-1970s, and from database research a decade later.

Fixpoints and logic programs

Maarten van Emden and Robert Kowalski’s “The Semantics of Predicate Logic as a Programming Language” (1976) gave Horn-clause programs three meanings and showed that they agree. The first is the one Declarative programming used: the least set of facts closed under the rules. The second is operational: the facts that can be proved from the program. The third describes the program as a function from sets of facts to sets of facts, the one-step consequences of the rules, and takes the meaning to be the least set this function maps to itself. That function has a least fixed point by a theorem of lattice theory published by Alfred Tarski in 1955, which guarantees one to every function of its kind with a property called monotonicity, defined below.

The third meaning is also a way to compute the first: apply the function repeatedly, starting from the recorded facts, until nothing changes. When deductive databases began evaluating Datalog over stored relations in the 1980s, this loop was the starting point, and the work went into doing it without redundant effort. François Bancilhon and Raghu Ramakrishnan’s “An Amateur’s Introduction to Recursive Query Processing Strategies” (1986) compares the strategies then known, among them the plain loop and the refinement this chapter builds.

The loop itself appeared in this book at its start. The paradigm branches wrote reachability functionally as a function step, which adds every node one edge away, and a function grow, which applies step until the set stops changing: until it reaches a fixed point.

One round of consequences

Write $P$ for the rules and $\Delta$ for the recorded facts. The immediate-consequence operator $T_P$ takes a set of facts $S$ and returns $\Delta$ together with every fact a single rule step derives from $S$:

$$T_P(S)=\Delta \cup \{H\theta \mid H\text{ :- }{B}_1\text{ and }\dots \text{ and }{B}_m\in P,\text{each }{B}_i\theta \in S\}$$

The substitutions $\theta$ are the ones unification finds by carrying a set of substitutions through a body; $T_P$ fires every rule once against $S$ and collects the heads. A rule with no body, a program fact, has $m=0$: the condition on its body holds vacuously, so $T_P$ yields its fact from every $S$.

Closure has a short statement in these terms. A set $S$ containing $\Delta$ is closed under the rules exactly when $T_P(S)\subseteq S$: firing every rule against $S$ produces nothing outside $S$. A fixed point is a set with $T_P(S)=S$, and the least closed set $M(P,\Delta )$ is the least fixed point of $T_P$.

$T_P$ is monotone: if $S\subseteq S^{\prime }$, then $T_P(S)\subseteq T_P(S^{\prime })$. A rule’s body only asks for facts to be present, and a substitution that finds them all in $S$ finds them all in the larger $S^{\prime }$, so every fact derived from $S$ is derived from $S^{\prime }$ too. A body that asked for a fact to be absent would break this, since adding a fact to $S$ could then remove a consequence; that case is set aside until Rule bodies and safety.

Rounds

Evaluation applies $T_P$ over and over. It starts from $S_0$, the recorded facts $\Delta$ together with the program’s own facts, which every application of $T_P$ yields anyway, and computes $S_{i+1}=T_P(S_i)$, one round per application, until a round adds nothing:

$$\Delta \subseteq S_0\subseteq S_1\subseteq S_2\subseteq \cdots \subseteq S_k=S_{k+1}$$

Each $S_{i+1}$ contains $S_i$: $S_1$ contains $S_0$, since $T_P$ always yields $\Delta$ and the program’s facts, and monotonicity carries each inclusion one round further. For the family, starting from the five parent facts:

Round 4 derives only facts already present, so $S_4=S_3$ and $S_3$ is a fixed point, with the nine ancestor facts the declarative reading gave.

The fixed point where the rounds stop is the least one, $M(P,\Delta )$. Every $S_i$ lies inside any closed set $C$ that contains $\Delta$: $S_0$ does, since $T_P(C)\subseteq C$ puts the program’s facts in $C$ alongside $\Delta$, and if $S_i\subseteq C$ then $S_{i+1}=T_P(S_i)\subseteq T_P(C)\subseteq C$, by monotonicity and then closure. So the last set, $S_k$, is inside every closed set containing $\Delta$, and it is closed itself, since $T_P(S_k)=S_k$. It is the least closed set. The rounds compute exactly the facts with derivations: a fact enters in round $i$ when its shortest derivation needs $i$ rule steps above the recorded and program facts.

Why the rounds stop

The rounds stop because there are only so many facts to add. A rule’s terms are variables and literals, so every value in a derived fact is a value that appears in $\Delta$ or in the program. There are finitely many such values, and a relation with $k$ columns over $n$ values has at most $n^k$ facts. Every round before the last adds at least one new fact, so the number of rounds is at most the number of possible facts, plus the final round that adds none.

The catalogue with the mistaken entry has four courses, so before holds at most $4\times 4=16$ facts. Its rounds go around the cycle one step at a time:

After round 4, before holds all sixteen pairs, and len(solutions before(?p, ?c)) is 16. A fifth step around the circle arrives at pairs already present. The cycle lets derivations grow without bound, but it cannot make the set of facts grow without bound, and evaluation ends as soon as the set stops growing.

Naive and semi-naive evaluation

Computing $T_P(S_i)$ in full re-fires every rule against every fact, including the facts that produced nothing new last time. This is naive evaluation, and it re-derives what it already knows. Counting the rule instances it finds for the family, one per complete substitution:

Thirty-one rule instances derive nine facts. The first rule finds the same five instances in every round, and the second re-derives every instance it found in earlier rounds each time it runs.

A rule instance that derives a fact new in round $i+1$ must use at least one premise that was new in round $i$. If every premise had been known before round $i$, the instance would have been found in round $i$ already, and its fact would not be new. So each round needs only the instances with at least one premise from the previous round’s new facts, called the delta. Semi-naive evaluation fires each rule once for each relation atom in its body, with that atom matched against the delta and the others against all the facts. The first round’s delta is all of $S_0$.

For the family, the first rule’s only atom reads parent, whose delta is empty after round 1, so the rule finds nothing after its first round. The second rule has two atoms, parent(x, y) and ancestor(y, z). No rule derives parent facts, so after round 1 the firing with parent(x, y) reading the delta finds nothing, and only the firing with ancestor(y, z) reading the delta can match: 3 instances in round 2, 1 in round 3, and 0 in round 4, which stops it. The total is 5 + 3 + 1 + 0, nine instances for nine facts. Both strategies compute the same rounds and the same $M(P,\Delta )$; semi-naive evaluation skips instances that can contribute nothing.

The counts depend on the strategy and not only on the program. Counting the steps of an evaluation is the subject of Cost semantics, and for relations the count is a property of the engine that computed the answer as well as of the query.

Bridger’s evaluation

A Bridger query reads $M(P,\Delta )$ for the $\Delta$ in force when it is asked. The engine starts from the facts add recorded and the program’s body-less rules, fires the rules with bodies round by round until a round adds nothing, and matches the query against the result. The rules apply to whatever facts are present at the time, so the same rules answer for a different family or a different catalogue, and for the catalogue before and after the mistaken entry.

Nothing between two changes to $\Delta$ changes $M(P,\Delta )$, so an engine may compute it once and answer every query until the next add or clear from that one computation. The language reference allows this explicitly. A rule body that could observe how often it ran would make the reuse visible, which is part of why the bodies are restricted, a restriction Rule bodies and safety spells out.

Building it

The engine is one method, solutions, which the query forms of eval_expr call:

pub fn solutions(&mut self, q: &Query, span: Span, env: &Env)
    -> Result<Vec<Subst>, Control>
{
    todo_m6!("solutions: least fixpoint of the rules over base + dynamic facts, …")
}

It returns every distinct assignment to the query’s named holes under which the query holds, in canonical order. The env and span are for the query itself, which is handled as add was in Building it: the relation’s name is resolved in env, where anything other than a relation is stuck with NotARelation, each QArg::Expr argument is evaluated in env to the constant it contributes, and an argument count other than the relation’s column count is stuck with ArityMismatch at span. The pieces come from the previous chapters and the provided runtime:

self.program().rules                 // every rule; a body-less one is a base fact
self.db.facts(relation) -> &[Tuple]  // Δ: the facts add recorded
self.db.derived()                    // a closure stored since the last add or clear
self.db.set_derived(closure)         // store one
Subst::unify(&self, pattern, fact)   // yours, from Unification

The work is to collect the facts in $\Delta$ and the program’s base facts, then run rounds: fire each rule with a body by carrying substitutions through its relation atoms with unify, apply each complete substitution to the head, and add what is new, stopping when a round adds nothing. The tables above collect all of a round’s heads before adding any, so each round fires against $S_i$ throughout; adding heads as they appear also reaches $M(P,\Delta )$, in rounds that no longer match the tables. Naive rounds are enough: the starter’s tests pass with them, and semi-naive rounds compute the same facts in fewer instances. Storing the closure with set_derived is optional; add and clear discard a stored closure themselves, and an engine that recomputes for every query is correct, only slower. The query is then matched against its relation’s facts, as in Unification. Each match is cut down to the query’s named holes, which drops the variables standing for anonymous holes, and duplicates are removed, so that solutions parent(?p, ?) has three solutions and not five. The provided compare, the canonical order on values, then sorts the solutions by their hole values, first hole first. A rule body may also contain conditions that are not relation atoms; Rule bodies and safety adds them to the rounds.

The design space

Searching from the query

Prolog evaluates from the query downward. It unifies the query with a clause head, then tries to establish the body’s atoms in order, depth first, backing up to try the next clause when an atom fails. On the catalogue with the cycle, asked whether compilers comes before itself, the search follows the second rule from compilers to pl, then to data_structures and intro, where it finds requires("intro", "compilers") and answers yes. Asked whether art, a course the catalogue does not mention, comes before compilers, the search follows the same rule from compilers to pl, data_structures, intro, back to compilers, and on around the circle without end. Nothing tells it that it has been there before, and so it can never conclude that the answer is no. The same rules, evaluated in rounds, stop after five, and before("art", "compilers") is false.

The search from the query has an advantage the rounds lack: it explores only what the query leads to. Asking whether pl comes before compilers in the catalogue without the cycle touches one fact, where the rounds compute all of before. Some Prolog systems combine the two by recording each subgoal they meet together with the answers found for it; a subgoal met again reuses the record instead of being searched again, and with that a cycle no longer loops. Datalog systems approach the same combination from the other side, rewriting the rules for a given query so that bottom-up rounds derive only the facts the query can reach.

Adding and clearing

Since $T_P$ is monotone, adding facts to $\Delta$ can only enlarge $M(P,\Delta )$: everything derived before is still derived. An engine could therefore answer the query after an add by continuing from the stored closure, with the added facts as the delta of one more semi-naive round, instead of starting over. clear gives no such shortcut. Removing a fact can remove facts derived from it, but a derived fact may have a second derivation that does not use the removed fact, and telling the two cases apart takes more than the closure records. Database systems that keep derived relations up to date as their inputs change do this bookkeeping. The reference engine recomputes after either change, which is correct for both.

Fixpoints elsewhere

Least fixpoints are not particular to relations. Part I’s grow computed one over sets of nodes. The language reference defines which Bridger functions are pure as a least fixpoint over the call graph, the analysis Rule bodies and safety depends on. Semantics that gives a recursive function’s definition a meaning as a mathematical function takes the least fixed point of the definition, read as a function from approximations to better approximations. The theory behind all of these is the subject of the further reading below.

Further reading

The semantics of logic programs: van Emden and Kowalski’s “The Semantics of Predicate Logic as a Programming Language” (1976) defines the immediate-consequence operator and proves that its least fixed point is the least model of a Horn-clause program. The argument is short and mostly set-theoretic.

Evaluating recursive queries: Bancilhon and Ramakrishnan’s “An Amateur’s Introduction to Recursive Query Processing Strategies” (1986) compares naive, semi-naive, and query-directed strategies on common examples. Abiteboul, Hull, and Vianu’s Foundations of Databases, freely available from the authors, develops naive and semi-naive evaluation in its chapter 13, “Evaluation of Datalog”.

Fixed points in semantics: Tarski’s “A Lattice-Theoretical Fixpoint Theorem and its Applications” (1955) is the theorem in its general form; the argument is carried in the algebra of lattices. Glynn Winskel’s The Formal Semantics of Programming Languages (MIT Press, 1993) builds the same idea into the meaning of recursive programs, with the mathematics introduced along the way.

Concept checks