Declarative Programming

Part VI checked programs before running them, but how a Bridger program computes has not changed since Part V: a function receives arguments and works out a result from them, step by step. The program below answers a question about a family. The family is a list of pairs (p, c), each saying that p is a parent of c. parents_of(family, c) keeps the pairs whose second component is c and returns their first components. ancestors(family, who) collects who’s parents and, after each parent, that parent’s ancestors, in a list held in a ref cell:

fn parents_of(family: [(String, String)], child: String) -> [String] =
    map(filter(family, |p| p.1 == child), |p| p.0);

fn ancestors(family: [(String, String)], who: String) -> [String] {
    ref found = [];
    for p in parents_of(family, who) {
        found := deref found ++ [p] ++ ancestors(family, p);
    }
    deref found
}

fn main() {
    let family = [("tom", "bob"), ("tom", "liz"), ("bob", "ann"),
                  ("bob", "pat"), ("pat", "jim")];
    println(ancestors(family, "jim"));
}

It prints ["pat", "bob", "tom"]: jim’s parent, that parent’s parent, and so on up.

ancestors answers one question, who a given person’s ancestors are. Asking for tom’s descendants takes a second function, which filters on the first component and recurses on the second. Asking whether tom is an ancestor of jim takes a third, or a search through the first function’s result. The family is the same in all three, and so is what it means to be an ancestor: a parent is an ancestor, and so is a parent’s ancestor. Each function encodes that definition again, walking the pairs in its own direction.

Bridger’s relations let a program state the definition once. In the program below, relation declares a relation and the types of its columns, each add records one fact, and the two rules define ancestor:

relation parent   : (String, String);
relation ancestor : (String, String);

rule ancestor(x, y) :- parent(x, y);
rule ancestor(x, z) :- parent(x, y) and ancestor(y, z);

fn main() {
    add parent("tom", "bob");
    add parent("tom", "liz");
    add parent("bob", "ann");
    add parent("bob", "pat");
    add parent("pat", "jim");

    println(solutions ancestor(?a, "jim"));
    println(solutions ancestor("tom", ?d));
    println(ancestor("tom", "jim"));
}

The rules read as sentences: x is an ancestor of y if x is a parent of y; x is an ancestor of z if x is a parent of some y and y is an ancestor of z. A query names a relation and marks the place an answer goes with a hole, ?a or ?d. solutions lists the values that fill the holes, and a query with no holes is a yes-or-no question. The program prints:

["bob", "pat", "tom"]
["ann", "bob", "jim", "liz", "pat"]
true

One pair of rules answers all three questions. No line of the program chooses a person to visit first or a direction to walk the pairs in.

Replacing the functions with rules raises these questions:

What does a rule mean, if it does not say how to compute anything? The rules state when a fact holds. Which facts does that make true, and how is it decided?
Why are these five people tom’s descendants, and no others? A relation that named everyone as an ancestor of everyone would satisfy both rules too. What picks out the answer the program printed?
How do facts and rules fit inside a language of expressions and a store? In the program above, ordinary code in main adds the facts, and the answers come back as ordinary values.

Programming by stating what holds, and leaving a system to work out what follows, took shape in the early 1970s, where automated theorem proving met natural-language processing.

Logic as a program

The theorem provers of the 1960s took a set of logical statements and searched for a proof that some further statement followed from them. J. A. Robinson’s resolution principle (1965) gave them a single inference step to search with, together with the matching operation it depends on, the subject of the next chapter. A prover’s search was its own business: the statements said what was true, and the prover decided which inferences to try and in what order.

In 1974, Robert Kowalski argued that a restricted form of such statements could be read as a program. The restriction is to clauses with a single conclusion and a conjunction of conditions, B if A₁ and … and Aₙ. Alfred Horn had studied that form in 1951, and such clauses are called Horn clauses after him. Kowalski read the clause as a procedure: to establish B, establish A₁, then the rest. Over the same years Alain Colmerauer’s group in Marseille, building a system that answered questions put to it in French, wrote its reasoning as such clauses and built Prolog (1972) to run them. Kowalski’s later “Algorithm = Logic + Control” (1979) set out the division this made possible. A program’s logic states what is true, its control states how the search for consequences proceeds, and the two can be written and changed separately.

Databases arrived at relations from a different direction. Edgar Codd’s relational model (1970) stored data as relations, sets of rows of equal length, and asked queries by describing the rows wanted, leaving the system to find them. The query languages built on it could join, select, and project, but no query among them could compute an ancestor relation of unbounded depth. Alfred Aho and Jeffrey Ullman showed (1979) that the relational algebra cannot express transitive closure, the very construction ancestor performs, and proposed adding a fixpoint operator to supply it.

The two lines met in work on deductive databases, gathered in Hervé Gallaire and Jack Minker’s Logic and Data Bases (1978): stored relations as in Codd’s model, plus Horn-clause rules that derive further relations from them. The fragment of Prolog that suits this use keeps the rules but restricts their arguments to constants and variables, so a rule can relate values it is given and never constructs new ones. By the mid-1980s that fragment was called Datalog; Ceri, Gottlob, and Tanca’s survey (1989) collected what was known about it.

Relations, facts, and rules

A relation is a set of tuples, all with the same number of components. parent is a relation with two columns, both strings, and the program above gave it five tuples:

parent	child
tom	bob
tom	liz
bob	ann
bob	pat
pat	jim

Each tuple is a fact: parent("bob", "pat") says that bob is a parent of pat. Because a relation is a set, its facts have no order, and recording the same fact twice leaves the relation as it was. A query’s answer is a set as well: in a family where two lines of descent meet at one person, ancestors would list that person once for each line, and a query lists them once.

A rule derives facts from facts. It has a head, the atom to the left of :-, and a body, the conjunction of atoms to the right; read logically, the head holds whenever the body does. Each variable in a rule stands for every value at once, so the second ancestor rule says: for all x, y, and z, if parent(x, y) and ancestor(y, z) then ancestor(x, z). The variable y appears in the body and not in the head, and the reading is the same as “if x is a parent of some y, and that y is an ancestor of z”. A rule is a Horn clause, with one conclusion and a conjunction of conditions.

A rule has the shape of the inference rules used since Program semantics: premises above a horizontal bar, the conclusion below it. Written that way, the two ancestor rules are:

$\frac{parent ( x , y )}{ancestor ( x , y )} (Anc-Parent) \frac{parent ( x , y ) ancestor ( y , z )}{ancestor ( x , z )} (Anc-Step)$

and a fact is a rule with no premises. A fact holds when it has a derivation, a tree of rule instances whose leaves are facts. This is the tree for ancestor("tom", "jim"):

$\frac{parent ( tom , bob ) \frac{parent ( bob , pat ) \frac{parent ( pat , jim )}{ancestor ( pat , jim )}}{ancestor ( bob , jim )}}{ancestor ( tom , jim )}$

Each step instantiates a rule: the bottom step is $Anc-Step$ with x as tom, y as bob, and z as jim. An evaluation derivation $e ⇓ v$ in Part II showed that an expression has a value. This one shows that a fact follows from the facts recorded and the rules.

The facts a program means

The relational program’s meaning is the set of facts that have derivations. For the family, that is the five parent facts and nine ancestor facts: each of the five parent pairs, together with tom–ann, tom–pat, tom–jim, and bob–jim.

The same set can be described without derivations, and the description answers the question of why the answer is exactly this set. Call a set of facts closed under the rules when every rule whose body holds in the set has its head in the set too. Many sets are closed. The set that contains every parent fact and every possible ancestor pair of the six people is closed, since it has every head a rule could ask for. It also holds ancestor("jim", "tom"), which no derivation produces. The meaning is the least closed set: the one that contains the recorded facts, is closed under the rules, and is contained in every other set with those two properties.

The set of derived facts is that least closed set, and the argument has two halves. First, take any closed set that contains the recorded facts. A derivation starts from recorded facts, which are in the set, and each step applies a rule to facts already in the set, which a closed set answers with the rule’s head. So every derived fact is in every such set. Second, the set of derived facts is itself closed: if every premise of a rule instance has a derivation, placing the rule beneath those derivations gives one for its head. The derived facts form a closed set contained in every other, which makes them the least.

Writing $P$ for a program’s rules and $Δ$ for its recorded facts, this least set is written $M (P, Δ)$ , as in the language reference. It is the meaning of the rules and facts together. Changing a rule or a fact can change it. The order of the rules, the order of the conditions in a body, and the order in which facts were recorded cannot. How an interpreter computes $M (P, Δ)$ , and why that computation always ends, is the subject of Evaluating relations.

Queries

A query asks about $M (P, Δ)$ . A query ancestor(?a, "jim") has one hole, and a solution is a value for the hole that makes the query a member of the set: ?a as bob, as pat, or as tom. ancestor("tom", ?d) puts the hole in the other column and finds five solutions. A query with no holes, ancestor("tom", "jim"), has one solution with nothing to fill in when the fact is in the set and none when it is not, which makes it a yes-or-no question. The holes go wherever the question needs them, because $M (P, Δ)$ is a set of facts, and a set has no direction to walk it in.

Stored and derived relations

The family program splits its relations two ways. parent holds facts recorded one at a time; it is defined by listing its members, its extension, and the recorded facts are called the extensional database, or EDB. ancestor holds facts derived by rules; it is defined by a condition its members meet, its intension, and the relations defined by rules are called the intensional database, or IDB. The terms come from the deductive-database work above.

The rules for ancestor mention no person. Recording a different family’s parent facts and asking the same queries gives that family’s ancestors, with no change to the rules.

Bridger’s relations

Bridger takes Datalog’s restriction and embeds the result in the rest of the language. Relations and rules are top-level definitions; facts arrive from ordinary code with add; and the answers to queries come back as ordinary values. The grammar gives the forms.

Declaring relations

A declaration names a relation and the types of its columns:

relation parent : (String, String);

The types are checked like any other. add parent("tom", 3) is rejected before the program runs, with type mismatch: expected String, found Int at the 3. Answering a query compares column values for equality, so a column’s type must be one that admits equality, which rules out a function type. Rule bodies are typed by the same checker, and Rule bodies and safety gives their rules.

Rules and program facts

A rule is a top-level definition, so its position in the file does not matter, as for every other definition. Lowercase names in a rule are its logic variables; each term, an argument of an atom in a rule, is a logic variable or a literal and nothing else. A relation with several rules holds the facts derived by any of them, so two rules for one relation read as an “or”.

Because a term is only a variable or a literal, a rule cannot compute a new value. The grammar has no place for n + 1 as a term, and this rule is a parse error at the +:

rule nat(n + 1) :- nat(n);

A rule with no body is a fact that belongs to the program. These two give the program a family to start from, with no add needed:

rule parent("tom", "bob");
rule parent("bob", "ann");

Adding and clearing facts

The arguments of add are ordinary expressions, unlike a rule’s terms: add R(e₁, …, eₙ) evaluates each eᵢ, which may be n + 1 or a function call, and records the fact made of the resulting values. clear R removes the facts add recorded for R. A program’s own facts, from body-less rules, are part of $P$ , and clear leaves them. With the two program facts above, this main:

fn main() {
    add parent("ann", "sue");
    println(solutions ancestor(?a, "sue"));
    clear parent;
    println(solutions ancestor(?a, "sue"));
    println(solutions ancestor(?a, "ann"));
}

prints ["ann", "bob", "tom"], then [], then ["bob", "tom"]: once the added fact is gone, sue has no ancestors, and ann keeps the two that the program’s own facts give her.

The recorded facts are the $Δ$ of $M (P, Δ)$ : the relation database, which add and clear change and every query reads. It becomes a third component of the evaluation judgment, beside the store, going in and coming out of every rule:

$ρ ⊢ ⟨ e, σ, Δ ⟩ ⇓ ⟨ v, σ^{'}, Δ^{'} ⟩$

Every rule from earlier chapters passes $Δ$ through unchanged, threading it in evaluation order as it threads the store. add and clear are the rules that change it:

$\frac{ρ ⊢ ⟨ e _{i} , σ _{i - 1} , Δ _{i - 1} ⟩ ⇓ ⟨ v _{i} , σ _{i} , Δ _{i} ⟩ ( 1 \leq i \leq n )}{ρ ⊢ ⟨ add R ( e _{1} , \dots , e _{n} ) , σ _{0} , Δ _{0} ⟩ ⇓ ⟨( ) , σ _{n} , Δ _{n} \cup { R ( v _{1} , \dots , v _{n} )}⟩} (E-AddFact)$

$ρ ⊢ ⟨ clear R , σ , Δ ⟩ ⇓ ⟨( ) , σ , Δ ∖ { R ( v ) ∣ v }⟩ (E-Clear)$

E-AddFact takes a union, so adding a fact already present changes nothing. Neither rule removes a single fact: between one clear and the next, $Δ$ only grows, and the facts a query can see are the facts recorded so far. A query reads $Δ$ and never changes it.

The relation database is kept apart from the store for that reason. A store cell holds one value at a time, and := replaces it, so what a cell held earlier is gone. The facts in $Δ$ accumulate, and the meaning of a query is a fixed set, $M (P, Δ)$ , that the query’s own evaluation cannot alter.

Asking queries

The family program used a query in each of the three places one may appear. solutions q is a list of the hole values of every solution, a single value for each solution when the query has one hole and a tuple when it has more. A hole whose value is not needed can be left unnamed, as a bare ?: ancestor("bob", ?) asks whether bob has any descendant. A query where a Bool is expected is true when it has a solution. And for q { … } runs its body once for each solution with the holes bound as variables:

for ancestor(?a, "ann") {
    println(a ++ " is an ancestor of ann");
}

prints bob’s line and then tom’s. The solutions come in a fixed canonical order, sorted by their hole values, which is why the family program printed ["bob", "pat", "tom"] where the ancestors function printed ["pat", "bob", "tom"]. A query’s meaning is a set, and the canonical order gives that set one listing that does not depend on the order the facts were added or derived. The rules for the three forms are in Querying relations.

Building it

The query forms all need $M (P, Δ)$ , which Evaluating relations computes. What can be built now is the relation database and the two forms that change it, add and clear. The provided runtime keeps $Δ$ as a RelationDb on the interpreter, beside the store. Like the store, it is mutated in place, so its two operations are the step from $Δ$ to $Δ^{'}$ :

impl RelationDb {
    fn add(&mut self, relation: &str, tuple: Tuple) -> bool; // E-AddFact
    fn clear(&mut self, relation: &str);                     // E-Clear
}

The relation forms reach eval_expr as the Relation variant of Expr, holding a Rel:

enum Rel {
    Add(Query),        // add R(a, …)
    Clear(Name),       // clear R
    Solutions(Query),  // solutions R(a, …)
    Query(Query),      // a bare query R(a, …)
}

struct Query { name: Name, args: Vec<QArg> }   // R(a, …)

enum QArg {
    Expr(Expr),          // a ground argument
    Hole(Option<Name>),  // a hole: ?x (named) or ? (anonymous)
}

A relation’s name is resolved like any other name. The initial environment binds each declared relation to a Value::Relation(name), so add and clear look the name up in the environment; a name bound to anything else is stuck, with NotARelation. add evaluates its arguments left to right as E-AddFact does. Because Add holds a Query, its arguments are QArgs, and one of them may be a hole. A hole has no value to record: the type checker rejects it before the program runs, and the evaluator, given one anyway, is stuck with HoleInAdd. When the number of arguments differs from the relation’s declared number of columns, the evaluator is stuck with ArityMismatch, the same error a function call with the wrong number of arguments gives. The Add and Clear cases each yield Value::Unit. The Solutions, Query, and ForQuery cases wait until $M (P, Δ)$ can be computed.

The design space

Rules that build values

Prolog’s terms can be compound: a rule may build a structure from its variables, and a structure may appear inside a fact. Numbers in the style of Peano are two rules, one for zero and one for a successor:

nat(z).
nat(s(N)) :- nat(N).

The second rule derives nat(s(z)) from nat(z), then nat(s(s(z))), and so on without end, so the set of facts these rules mean is infinite. Lists, trees, and every other data structure in Prolog are compound terms of this kind, which is what makes Prolog a general-purpose language.

Datalog gives them up. Without compound terms, the only values a rule can put in a head are values already present in the facts, and finitely many facts contain finitely many values. A relation with two columns over six people can hold at most thirty-six facts, and so $M (P, Δ)$ is finite for every program. Bridger makes the same choice by limiting a term to a variable or a literal, which is why rule nat(n + 1) :- nat(n); does not parse: it would derive a new integer from each one it had. A program that needs a new value, such as the result of arithmetic, computes it in ordinary Bridger code, which can loop over a query’s solutions and add facts holding the results.

Search order

Prolog runs a query by searching from the query backwards, trying the clauses for a relation in the order they are written and the conditions of a body from left to right. With the conditions of the second rule swapped, the logic is unchanged:

ancestor(X, Y) :- parent(X, Y).
ancestor(X, Z) :- ancestor(X, Y), parent(Y, Z).

Asked for tom’s descendants, Prolog finds each of them, and then, asked for one more, enters the second clause again, whose first condition is again an ancestor query with tom as its first argument. The search recurses until it runs out of stack. A query with no solution, such as whether jim is an ancestor of tom, never answers at all. In Kowalski’s terms, the logic is the same and the control has changed, and a Prolog programmer orders clauses and conditions so the search terminates.

The same swap in Bridger, rule ancestor(x, z) :- ancestor(x, y) and parent(y, z);, prints exactly what the original printed. A query’s answer is $M (P, Δ)$ , which the order of rules and conditions does not affect, and Bridger computes the whole set, which is finite. The cost is that it computes all of it: to answer whether tom is an ancestor of jim, it derives all nine ancestor facts, where a search backwards from the query visits only the people on the way up from jim. Datalog systems recover much of that saving by rewriting a program’s rules, given a query, so that computing the whole set derives only the facts relevant to that query.

Where the facts come from

SQL, the query language of most relational databases, has been able since its 1999 standard to define a relation by recursion. This query, run against a parent table holding the family, returns bob, pat, and tom:

WITH RECURSIVE ancestor(anc, des) AS (
    SELECT parent, child FROM parent
  UNION
    SELECT p.parent, a.des
    FROM parent p JOIN ancestor a ON p.child = a.anc
)
SELECT anc FROM ancestor WHERE des = 'jim';

The UNION combines a base case and a recursive step, the two ancestor rules in another syntax. In SQL the facts live in a database, filled and changed by statements outside the query.

Standalone Datalog systems such as Soufflé read their facts from input files and write derived relations out, and they declare a type for each column, as Bridger does. One of their main uses is program analysis: the facts describe a program’s statements, and the rules derive facts about how its values flow. Prolog keeps facts and rules in one database that a program can change while it runs, adding clauses with assert and removing them with retract, in the middle of a search that reads them.

Bridger puts the facts in the hands of the host language. Imperative or functional code computes them and adds them; the rules are fixed when the program is written; and a query’s answer arrives as a list, a Bool, or a loop variable for the host code to keep working with. Facts accumulate between clears, so a query is always asked of a fixed set.

Concept checks

Add ancestor("liz", "jim") to the fourteen facts the family program means. Is the new set closed under both rules? Why is it not the program's meaning?

It is closed. The only rule that could use the new fact is $Anc-Step$ , with ancestor("liz", "jim") as its second premise, and it needs a parent of liz: tom. Its head, ancestor("tom", "jim"), is already in the set. So the set contains the recorded facts and is closed, but it is not the least such set: the set without ancestor("liz", "jim") is closed too and smaller. No derivation ends in ancestor("liz", "jim"), and the meaning holds only facts that have one.

Write a rule for grandparent(x, z) over parent. Which pairs does it give for the family, and is grandparent part of the EDB or the IDB?

rule grandparent(x, z) :- parent(x, y) and parent(y, z);

solutions grandparent(?g, ?c) is [("bob", "jim"), ("tom", "ann"), ("tom", "pat")], in canonical order. The rule is not recursive: a grandparent is exactly two parent steps up. grandparent is defined by a rule, so it is part of the IDB; parent, whose facts are added, is the EDB.

Swapping the conditions of the second ancestor rule changes nothing in Bridger and sends Prolog into unbounded recursion. What does each language take the order of conditions to mean?

To Prolog, the order is control: conditions are tried left to right, so ancestor(X, Y), parent(Y, Z) starts by asking a new ancestor query with the same first argument, which starts the same way, without end. To Bridger, the order means nothing: a body is a conjunction, a query’s answer is the least closed set $M (P, Δ)$ , and a conjunction is the same in either order. Bridger pays for that by computing the whole of $M (P, Δ)$ ; Prolog’s search, when it terminates, visits only what the query leads it to.

Bridger rejects rule nat(n + 1) :- nat(n); at parse time. What guarantee would accepting it give up?

That the values in the program’s facts and rules limit how many facts can be derived, and so how long computing $M (P, Δ)$ takes. With rule nat(0); as a program fact, the rule would derive nat(1), then nat(2), and so on, a new fact each round. Bridger’s integers wrap at $2^{64}$ , so the rounds would end only after about $2^{64}$ of them, and solutions nat(?n) would not return in any practical sense. With terms limited to variables and literals, every value in a derived fact already appears in the program’s facts or rules, and a finite set of values can be arranged into only finitely many facts.

ancestors returned ["pat", "bob", "tom"], while solutions ancestor(?a, "jim") returned ["bob", "pat", "tom"]. Why does Bridger sort solutions rather than list them in the order they were found?

The order a function returns is the order its code visits the pairs. A query has no code of its own: its answer is the set $M (P, Δ)$ , and the order in which facts are derived depends on how an interpreter computes that set, and on the order the facts were added, neither of which changes the set. Sorting by hole values gives every correct interpreter the same list for the same facts, so the order a program prints in, and anything it computes from that order, depends on the facts alone.

A Practical Introduction to Programming Language Design