Rule Bodies and Safety

Unification ended with a sibling rule that listed ann as ann’s own sibling. Nothing in the rule said that its two people had to differ, and a relation atom has no way to say it. The program below adds that condition. age(p, a) records that person p is a years old, and each rule ends with a condition that is an ordinary Bridger expression:

relation parent  : (String, String);
relation age     : (String, Int);
relation sibling : (String, String);
relation adult   : (String);

rule sibling(x, y) :- parent(p, x) and parent(p, y) and x != y;
rule adult(p)      :- age(p, a) and a >= 18;

fn main() {
    add parent("tom", "bob");  add parent("tom", "liz");
    add parent("bob", "ann");  add parent("bob", "pat");
    add parent("pat", "jim");
    add age("tom", 71);  add age("bob", 44);  add age("liz", 40);
    add age("pat", 19);  add age("ann", 17);  add age("jim", 1);

    println(solutions sibling(?x, ?y));
    println(solutions adult(?p));
}

It prints:

[("ann", "pat"), ("bob", "liz"), ("liz", "bob"), ("pat", "ann")]
["bob", "liz", "pat", "tom"]

If a body can hold any expression, other rules come to mind. note below prints a name and returns true. With next_age, related, noted, and childless declared as relations, these rules all parse, but Bridger rejects each of them before main runs:

fn note(p: String) -> Bool { println(p); true }

rule next_age(p, b)  :- age(p, a) and b == a + 1;
rule related(x, y)   :- parent(x, z);
rule noted(p)        :- age(p, a) and note(p);
rule childless(p)    :- age(p, a) and not parent(p, ?);

next_age is rejected because logic variable b “is not bound by any generator in this rule”, and related with the same message for y. noted and childless are rejected with “this filter is not pure”. These rejections raise the following questions:

• What gives a variable its values? x != y uses values that parent(p, x) and parent(p, y) found. b == a + 1 looks as if it could supply a value for b, yet it is rejected.
• What would a rule mean if a head variable had no source of values? related says nothing about y, so which facts would it derive?
• What may a condition do? A condition can run many times, in an order and a number of rounds that the engine chooses. What would a program see if a condition printed or read a ref cell?
• Why can a body ask for a fact to be present and never for one to be absent? Whether someone is childless looks like a simple question to ask of parent.

The problem with related first surfaced in logic-based database query languages, before Datalog-style rules were introduced.

Queries with no finite answer

A query written in the predicate calculus describes the values it wants. Nothing in the notation limits what that description may be, so it can ask for every $x$ that is not a parent:

$$\{x\mid \neg \exists y.parent(x,y)\}$$

If $x$ ranges over all strings, the answer is infinite. If $x$ ranges over the values in the database, the answer is finite but depends on facts unrelated to the question: recording the age of a new person adds that person to the answer. Abiteboul, Hull, and Vianu’s Foundations of Databases trace this concern in the database literature back at least to Kuhns’s work of 1967, which studied the formulas whose answers depend only on the stored relations.

No test can pick out exactly those formulas. Di Paola proved in 1969 that the question is undecidable. The response was a series of syntactic conditions, each accepting only formulas with the property and each turning away some others that have it too. Codd’s relational calculus of 1972 restricted its variables to ranges over stored relations. Jeffrey Ullman’s Principles of Database Systems defined safe formulas. Jean-Marie Nicolas’s range-restricted formulas (1982) require each variable to be tied to a relation in a form that can be read off the formula. Allen Van Gelder and Rodney Topor compared several of these classes in 1991 and gave translations from the formulas they accept into the relational algebra.

Datalog’s definition carries the same idea. Each variable in a rule’s head must also appear in its body, so a rule with no body must have a ground head. The word safety has stayed attached to conditions of this kind.

Generators and filters

A conjunct in a rule body is one of two things. A generator is a relation atom, such as parent(p, x). Matching it against the facts binds its variables, as in Unification. A filter is any other expression, such as x != y. It is evaluated under a substitution and yields true or false, which keeps or drops that substitution. A filter binds no variable, whatever its shape, and that is why b == a + 1 leaves b without a value. Here == is the comparison it is everywhere else in the language: it needs both sides to have values already.

Firing a rule therefore works as it did in the last two chapters, with one extra step. Carry the substitutions through the generators, then keep the ones under which every filter is true. The operator from Evaluating relations gains one condition. Writing a rule’s generators as $G_i$ and its filters as $F_j$:

$$T_P(S)=\Delta \cup \{H\theta \mid \text{a rule of }P\text{ has head }H,\text{each }{G}_i\theta \in S,\text{each }{F}_j\text{ is }\text{true}\text{ under }{\rho }_0[\theta ]\}$$

${\rho }_0[\theta ]$ is the program’s top-level environment extended by the substitution. For sibling, the generators produce nine substitutions, ann paired with ann among them, and x != y keeps the four whose two people differ. Applying each to the head gives the four facts the program printed.

The filter does not disturb the argument for monotonicity. If $S\subseteq S^{\prime }$, a substitution that finds its generators’ facts in $S$ finds them in $S^{\prime }$. A filter’s result depends on $\theta$ and nothing else, so a filter that accepted $\theta$ for $S$ accepts it for $S^{\prime }$. Every fact derived from $S$ is derived from $S^{\prime }$, and $T_P$ is still monotone. This argument assumes that a filter’s result depends only on $\theta$, a requirement that Purity enforces.

Binding belongs to the body as a whole, and the position of a filter does not limit what it can see. This rule has the filter first and derives the same four facts:

rule sibling(x, y) :- x != y and parent(p, x) and parent(p, y);

Wherever x != y sits in the body, the generators supply the substitutions before any filter runs. The order of filters among themselves can still matter when one of them can get stuck, as Conjunct order shows.

Safety

A rule is range-restricted when every variable in its head and every variable in its filters is bound by a generator of that rule. A filter may also refer to top-level constants and functions, which are visible everywhere. Writing $bound$ for the variables a rule’s generators mention, and $top$ for the top-level names, the conditions are:

$$vars(H)\subseteq boundfree(F_j)\subseteq bound\cup top\text{for each filter }{F}_j$$

A rule that meets them is safe. related fails the first condition: y appears in the head but in no generator. rule big(n) :- n > 100; fails it too, and so does a rule with no body and a variable in its head, rule everyone(x);.

What an unsafe rule would mean

Reading related(x, y) :- parent(x, z) logically gives: for all x, y, and z, if x is a parent of z then related(x, y). Taken at its word, related("tom", y) holds for every string y, so the relation would have infinitely many facts, which solutions cannot list.

Limiting y to the strings in the database makes the set finite, but at the price the calculus query paid: unrelated facts change the answer. add age("sue", 3) would then add related("tom", "sue"), related("bob", "sue"), and related("pat", "sue"), from a fact about someone’s age in a rule that mentions neither ages nor sue.

An engine computing $T_P$ has a more immediate problem. Applying a substitution to related(x, y) leaves y in place, but Bridger’s matching depends on every fact being ground.

What safety guarantees

Take a safe rule and any substitution that satisfies its body. Every variable in the head is bound by a generator, so it has a value taken from a fact. Every other term in the head is a literal. So the derived fact is ground, and each value in it was already in a fact or written in the program. By induction over the rounds, every value in $M(P,\Delta )$ appears in $\Delta$ or in the head of a rule.

That is the premise of the count in Why the rounds stop: finitely many values, so finitely many possible facts, so finitely many rounds. Filters add nothing to the count, since they contribute no values. The bound comes from the rule’s shape, and it holds for any facts the program may add while it runs.

Purity

The meaning of a query is a set determined by $P$ and $\Delta$. The engine is free to compute it in naive or semi-naive rounds, to choose the order of a body’s generators, and to reuse a closure until the next add or clear. Each of those freedoms relies on filters having no effect and depending on nothing except the substitution.

Suppose this rule were accepted, with limit a top-level ref:

ref limit = 18;
rule adult(p) :- age(p, a) and a >= deref limit;

After limit := 65, $\Delta$ is unchanged. An engine that reuses its closure would give the old answer, while one that recomputes for every query would give a new one. Since the filter’s result depends on the store, $T_P$ is no longer a function of its set of facts. A filter that printed would print once for each substitution the strategy happened to try. The previous chapter counted 31 rule instances for naive rounds and 9 for semi-naive ones on the same rules, and an effect in a filter would turn that difference into visible output.

A filter must therefore be pure: free of effects, and a deterministic function of the variables the generators bind.

The purity judgment

The judgment $\Phi ⊢e\mathbf{pure}$ reads: given the set $\Phi$ of functions known to be pure, $e$ is pure. Literals and variables are pure, an operator is pure when its operands are, and a call is pure when it names a function in $\Phi$ and its arguments are pure:

$$\frac{}{\Phi ⊢n\mathbf{pure}}(\text{P-Lit})\frac{}{\Phi ⊢x\mathbf{pure}}(\text{P-Var})\frac{\Phi ⊢e_1\mathbf{pure}\Phi ⊢e_2\mathbf{pure}}{\Phi ⊢e_1\oplus e_2\mathbf{pure}}(\text{P-Op})$$

$$\frac{f\in \Phi \Phi ⊢e_i\mathbf{pure}(1\le i\le n)}{\Phi ⊢f(e_1,\dots ,e_n)\mathbf{pure}}(\text{P-Call})$$

The other effect-free forms, such as if, match, tuples, and field access, are pure when their parts are. Some forms have no purity rule, so any expression containing one is impure: ref, deref, :=, while, for, add, clear, solutions, and a query. Calls to input and output primitives are impure as well, and so is to_string, because converting a ref cell to a string reads its current contents. A call through a parameter, a local, or a computed closure has no $\text{P-Call}$ instance, because the analysis cannot tell what it will run. The language reference has the complete list.

Which functions are pure

$\Phi$ comes from the program. Let $I$ be the smallest set of function names such that $f\in I$ whenever f’s body contains a form with no purity rule, or calls a function in $I$; $\Phi$ is every function outside it. This is another least fixpoint: start from the empty set, add what the condition requires, and stop when nothing changes. Take these functions:

fn plain(a: Int) -> Bool = a > 1;
fn note(p: String) -> Bool { println(p); true }
fn check(p: String) -> Bool = note(p);
fn both(a: Int, p: String) -> Bool = plain(a) and check(p);

plain stays out, so $\Phi$ holds only plain, and a > 1 and plain(a) are acceptable filters. A rule whose filter is both(a, x) is rejected, and the error follows the calls that put both in $I$:

the effect is reached through `both` → `check` → `note` → `println`

The steps in the table are the rounds of a relational program. has_effect records the functions whose bodies directly contain an impure form, as note’s contains println, and calls records the call graph. The rules have the same shape as ancestor:

relation calls      : (String, String);
relation has_effect : (String);
relation impure     : (String);

rule impure(f) :- has_effect(f);
rule impure(f) :- calls(f, g) and impure(g);

fn main() {
    add has_effect("note");
    add calls("check", "note");
    add calls("both", "plain");
    add calls("both", "check");
    println(solutions impure(?f));
}

It prints ["both", "check", "note"], the set in the table. Datalog’s use in program analysis rests on this correspondence. The checker you build computes the same set directly and also keeps the path for the error.

Filters must finish

A pure function can still run forever. fn spin(n: Int) -> Bool = spin(n); has no effects, but calling it in a filter would hang the engine, whose rounds rely on every filter returning. So no function a filter reaches may recurse, directly or through others, and Bridger rejects this filter with is recursive, so a filter calling it might not terminate:

fn is_even(n: Int) -> Bool = if n == 0 { true } else { is_odd(n - 1) };
fn is_odd(n: Int) -> Bool = if n == 0 { false } else { is_even(n - 1) };

rule even_aged(x) :- age(x, a) and is_even(a);

Like the conditions in the calculus, this check accepts only some of the programs that would work. On the ages above, is_even always returns, but on a negative argument it counts away from zero. The check looks at the call graph and never at the arguments. a % 2 == 0 tests the same thing with no recursion. For the same reason, a filter may not reach a function that takes a function-typed parameter, since the analysis cannot follow what such a function will call. The prelude’s own map, filter, fold, and the functions written over them are trusted to finish.

A filter can still get stuck: 100 / (a - 1) > 0 divides by zero when a is 1. Termination and reaching a value are separate properties, and these checks establish only the first. A filter that gets stuck makes the query, and the program, stuck.

Bridger’s rule bodies

Telling generators from filters

parent(p, x) and is_adult(a) have the same syntax, so the parser cannot sort them. The distinction comes from name resolution: a conjunct is a generator when it is a whole call whose callee names a declared relation, and every other conjunct is a filter. Bridger’s single namespace for top-level names guarantees that no name is both a relation and a function.

A body is its and-chain however it is bracketed, so age(x, a) and (parent(x, y) and a > 18) has three conjuncts. A generator’s arguments must be variables or literals, as a head’s must, so age(p, a - 1) is rejected with a relation's argument in a rule body must be a variable or a literal.

A relation applied anywhere else is a query, and a query is impure. So a body reads the database only through generators standing as whole conjuncts. (a < 18 or a >= 65) is a good filter, and with the facts above it selects ann, jim, and tom. parent(x, y) or parent(y, x) is a single conjunct and therefore a filter, with no generator to bind x. Two rules say the same thing and are accepted, since a relation with several rules reads as an “or”:

rule related(x, y) :- parent(x, y);
rule related(x, y) :- parent(y, x);

What a filter can see

A rule is a top-level definition and closes over the top-level environment, as a fn body does. It sees the variables its generators bind and the program’s top-level names, but never the locals where a query is asked:

let voting_age = 18;
rule adult(p) :- age(p, a) and a >= voting_age;

Moving voting_age into main as a let makes the rule an error, since no generator binds voting_age. If a rule could read a query’s locals, one set of facts and rules could have a different meaning at each query site. A generator-bound variable of the same name as a top-level definition shadows it inside the rule.

Typing a rule

Rules are checked by the same type checker as the rest of the program. A generator gives each of its variables the type of that column. Where a variable appears in several columns, those types must agree, so age(x, a) and parent(x, a) is rejected at the second a with type mismatch: expected String, found Int. The column’s declared type is the expected type, and the type a already has in the rule’s context is the found type. Head terms are checked against the head relation’s columns. Each filter is checked against Bool with the rule’s variables in the context, so a > "ten" and a filter of a + 1 are both type errors.

Conjunct order

Generators and filters can be written in any order without changing which facts a body derives. Filters evaluate left to right, as operands do everywhere else in the language: for each substitution the generators produce, the language reference runs a rule’s filters in the order written and stops at the first that yields false. Since a substitution that fails one filter derives nothing, this order makes no difference when no filter gets stuck. It does matter when one can. With jim at age 1, this rule finds its answer, because a != 1 removes jim before the division runs:

rule r(x) :- age(x, a) and a != 1 and 100 / (a - 1) > 0;

With the two filters swapped, the query is stuck with division by zero.

Building it

The checks are yours, in relations/check.rs. The provided driver calls them once per rule when the program is loaded, before main:

struct Rule { head: Atom, body: Vec<Expr>, span: Span }

pub fn check_generators(program: &Program, rule: &Rule)
    -> Result<Vec<bool>, RuleError>;
pub fn check_range_restriction(program: &Program, rule: &Rule, generators: &[bool])
    -> Result<(), RuleError>;
pub fn check_pure(program: &Program, rule: &Rule, generators: &[bool])
    -> Result<(), RuleError>;

body holds every conjunct as an ordinary Expr, so a generator is an Expr::Call that has not yet been recognised as one. check_generators classifies the conjuncts, answering with one bool per conjunct, and checks that the head and each generator name a declared relation with the right number of arguments and that each generator’s arguments are terms. The driver hands that answer to the other two checks, so neither has to resolve relation names again. check_range_restriction collects the variables the generators bind and compares the head’s and the filters’ variables against them. check_pure computes the impure set over the program’s call graph, then judges each filter, and also rejects a filter that reaches a recursive function or one with a function-typed parameter. The failures are the RuleError variants in the language reference. Checker::check_rule, in types/check.rs, gives the rule its types as in Typing a rule.

The engine from Evaluating relations gains the filter step. After the generators have been joined, the filters are evaluated by eval_expr left to right for each remaining substitution, in the program’s root environment (env.root()) extended with that substitution’s bindings. true moves on to the next filter, and false drops the substitution without evaluating the filters after it. A rule with filters and no generators starts from the one empty substitution, so rule r(1) :- 2 > 1; derives its fact once; a join that began with no substitutions at all would derive nothing. Filters read no facts, so semi-naive rounds choose a delta among a rule’s generators alone.

The design space

Absence in a body

Bridger’s rejected childless rule asks for a fact to be absent. To see what that does to the rounds, suppose person holds recorded facts for the six people, and suppose this version were accepted:

rule has_child(x) :- parent(x, y);
rule childless(x) :- person(x) and not has_child(x);

Run the rounds of the previous chapter on the family:

The rounds stop with childless("tom") in the set beside has_child("tom"). Rounds only add, so nothing withdraws the fact derived too early. $T_P$ has lost its monotonicity: a larger set of facts can give fewer consequences, and the chain $S_0\subseteq S_1\subseteq \cdots$ no longer leads to the intended meaning.

Some programs lose the meaning itself. With a person named tom, consider:

rule stays(x)  :- person(x) and not leaves(x);
rule leaves(x) :- person(x) and not stays(x);

The set holding person("tom") and stays("tom") is closed: tom stays, so the second rule does not fire. The set holding person("tom") and leaves("tom") is closed for the mirror-image reason. Neither contains the other, and the only set inside both, person("tom") alone, is not closed, since it fires both rules. With two minimal closed sets and nothing closed inside both, these rules have no least closed set to serve as $M(P,\Delta )$.

Stratification separates the two programs. Give each relation a layer number such that a rule’s head is in a layer at least as high as each relation it uses positively, and strictly higher than each relation it negates. childless can go above has_child. stays would have to be above leaves and leaves above stays, so no numbering exists for them. A program with a numbering is stratified: a cycle among its relations never passes through a negation. Evaluation computes one layer at a time, each to its own least fixpoint, so a negated relation is complete before anything reads its absence. Several researchers proposed this independently in the 1980s, among them Chandra and Harel and Apt, Blair, and Walker, who showed that the meaning does not depend on which numbering is chosen. Negated atoms also need safety: x must be bound by a positive generator, or not has_child(x) asks for every string that has no child, the calculus query from the start of this chapter.

Reading absence as falsehood was itself a decision. Keith Clark’s negation as failure and Raymond Reiter’s closed-world assumption, both published in 1978, examine when a system may conclude that what it cannot derive is false. Prolog’s \+ succeeds when the search for its goal fails. Datalog systems such as Soufflé offer stratified negation and reject a program with no numbering. SQL restricts recursion in a similar direction: SQLite, for example, rejects a recursive query that refers to itself inside NOT IN. Other semantics assign a meaning to programs like stays and leaves, at the cost of a meaning that is no longer a plain least fixpoint.

Bridger leaves negation over relations out of rules, but a host program can do the layering itself. A query in ordinary code is free to be negated, because the closure it reads is complete by the time it is asked:

relation person    : (String);
relation has_child : (String);
relation childless : (String);

rule person(x)    :- age(x, a);
rule has_child(x) :- parent(x, y);

fn find_childless() {
    clear childless;
    for person(?x) {
        if not has_child(x) { add childless(x); }
    }
}

After find_childless(), solutions childless(?x) is ["ann", "jim", "liz"]. Host code’s statement order is exactly the order between layers. The result is a snapshot: after add parent("jim", "sue") the query still lists jim, until find_childless() runs again and gives ["ann", "liz"]. A stratified rule would stay current by itself. The host version keeps every rule’s meaning a least fixpoint and places the sequencing where a program already has sequence.

Computing values in a body

next_age asks a body to compute a value. Datalog systems such as Soufflé read something like b == a + 1 as a binding, with = giving a new variable the result of the arithmetic. That reading gives up the bound on values. From the single fact person("tom"), this rule, were it allowed, would derive "tomtom", then "tomtomtomtom", doubling the string each round until memory ran out:

rule person(x) :- person(y) and x == y ++ y;

Arithmetic gives a slower version of the same problem: b == a + 1 would add a new integer each round, stopping only when the 64-bit integers wrapped around. A filter that limited the string’s length would make the rule stop, but telling those two apart is a harder problem than checking that a variable appears in a generator. Ramakrishnan, Bancilhon, and Silberschatz (1987) studied conditions under which recursive rules over such computed relations are safe. Prolog’s is evaluates arithmetic during the search and leaves termination to the programmer, as with its other control.

Bridger’s terms remain variables and literals, and the computation happens in host code:

for age(?p, ?a) { add next_age(p, a + 1); }

That for runs once over a fixed set of solutions and adds six facts. A host loop around it could still run forever, but that keeps non-termination in the part of the language where it already exists. The rules themselves keep the guarantee.

Aggregates

A rule that counted a person’s descendants would run into both of the preceding problems. Suppose a rule could hold count in its head, and watch tom’s descendants arrive in the rounds of the previous chapter: two after round 1, four after round 2, five after round 3. Facts are never withdrawn, so descendants("tom", 2), descendants("tom", 4), and descendants("tom", 5) would all hold. A count of a set that can grow is not monotone unless the count waits for the set to be complete. The counts are also values no fact contains, so they fall outside the finite set of values safety establishes.

Systems that allow aggregates usually place them under the layering discipline, so that a counted relation is complete first. SQL’s GROUP BY works over a complete input, and SQLite rejects an aggregate over a query’s own recursive reference with recursive aggregate queries not supported. Other work keeps recursion through an aggregate by asking which aggregates can be treated as growing. Kenneth Ross and Yehoshua Sagiv’s monotonic aggregation (1992) gave such an account, and Flix lets rules compute over ordered values that climb toward a fixed point, alongside sets of facts. Datafun records monotonicity in its types, so that a checker can confirm a recursive definition grows.

Bridger declines aggregates in rules and computes them in host code over a finished answer: len(solutions ancestor("tom", ?d)) is 5. Querying relations covers that style.

When order decides safety

Prolog has no static check of this kind, and the order of a clause’s conditions determines whether they have values to work with. These two clauses differ only in order:

sibling(X, Y) :- parent(P, X), parent(P, Y), X \= Y.
sibling(X, Y) :- X \= Y, parent(P, X), parent(P, Y).

The first behaves like Bridger’s rule. In the second, X \= Y runs first, on two unbound variables, and it succeeds only when they cannot be unified. Unbound variables can, so the clause finds nothing and reports no error. N is M + 1 with M unbound raises an error at run time. Prolog programmers learn which conditions need which variables bound.

Bridger’s check is made once, before the program runs, and asks only whether a generator somewhere binds the variable. In return, a query that finishes derives the same facts wherever its filters are written; reordering them can only change whether a stuck filter is reached. The check also rejects more than Prolog would: a program cannot use == to bind.

Tracking effects

Prolog’s clause bodies may call write, and a condition re-run on backtracking prints again. Programmers use this for tracing, and accept that the output describes the search. Bridger’s analysis takes the opposite position for rule bodies, and its form is a choice too. Function types record no effects, so the checker works out purity from the whole program’s call graph, for the one place the semantics needs it. Languages such as Haskell record effects in types, which makes purity visible at every call and requires every signature in a chain to say so. Bridger’s $I$ needs no annotations and reports a witness path, though a programmer reading a signature cannot tell from it whether the function may be used in a filter.

Further reading

Safety in query languages: Abiteboul, Hull, and Vianu’s Foundations of Databases, freely available from the authors, treats the problem and its syntactic conditions in chapter 5, “Adding Negation: Algebra and Calculus”, whose exercises work through several of the classes. Van Gelder and Topor’s “Safety and Translation of Relational Calculus” (1991) compares the conditions and translates accepted queries into the algebra.

Negation: chapter 15 of Foundations of Databases develops stratified semantics and the well-founded semantics, which gives a meaning to programs with no stratification, using three truth values. Clark’s “Negation as Failure” and Reiter’s “On Closed World Data Bases” both appear in Gallaire and Minker’s Logic and Data Bases (1978).

Beyond sets of facts: Madsen, Yee, and Lhoták’s “From Datalog to Flix” (2016) defines rules over lattices and applies them to program analysis. Arntzenius and Krishnaswami’s “Datafun: A Functional Datalog” (2016) combines a typed functional language with least fixed points, tracking monotonicity in the type system.

Concept checks