Unification

The previous chapter gave the meaning of a set of rules as the facts that have derivations. One step of the derivation for ancestor("tom", "jim") used the second ancestor rule,

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

with x as tom, y as bob, and z as jim. The chapter wrote those values down without saying where they came from. An interpreter has only the rule and the facts it knows, and it has to find the values itself.

Suppose the facts known so far are the five parent facts of the family and the five ancestor facts that the first rule gives from them, one for each parent pair. Firing the second rule means finding every assignment of values to x, y, and z under which both atoms of the body are known facts. A few attempts show what is involved:

The first row succeeds, and the rule’s head with those values is a new fact, ancestor("bob", "jim").

The attempts raise these questions:

• How is an atom with variables matched against a fact? In the first column, both of parent(x, y)’s variables take their values from the fact. In the third, y already has a value, and the fact has to agree with it.
• What makes the two atoms of a body agree? y appears in both atoms of the body. The second row fails because the fact puts tom where y already stands for pat.
• How are all the assignments found? One success gives one new fact. Firing the rule means finding every assignment, and the table above tried three.

The operation in each cell, making an atom with variables identical to a fact by choosing values for the variables, has a name from automated theorem proving. Part VI used it on types.

Unification in logic programming

A type checker introduced J. A. Robinson’s unification algorithm (1965): given expressions containing variables, find a substitution for the variables that makes them identical. Robinson built it for resolution, his single inference step for proving theorems, which combines two clauses when an atom of one and a negated atom of the other can be made identical. Unification finds the substitution that makes them so, and the combined clause carries that substitution forward. Milner later used the same algorithm to solve equations between types, which is how Part VI’s checker infers them.

Logic programming made unification the whole of its data handling. In Kowalski’s procedural reading of a clause, establishing a goal means unifying it with the head of a clause and then establishing the body. The unification does the work a function call’s parameter passing does elsewhere: values in the goal flow into the clause’s variables, and values the clause’s variables receive flow back out to the goal. A goal whose arguments are all values tests a fact. A goal with variables in some positions computes values for them. Which positions are inputs is settled by each goal and not fixed by the clause, and this is the source of the direction-free queries of the previous chapter.

Prolog unifies at every step of its search, between terms that may contain variables on both sides and may be built from other terms. To keep that step fast, Prolog systems have generally left out the occurs check Part VI’s checker needed, and accepted the consequences. Datalog’s evaluation proceeds the other way round, from known facts to new ones. The facts contain no variables, so there unification always meets a variable on one side only.

Substitutions

A substitution maps logic variables to values. Writing $\theta$ for one, the first row of the table found

$$\theta =\{x\mapsto \text{bob},y\mapsto \text{pat},z\mapsto \text{jim}\}$$

Applying a substitution to an atom replaces each variable it binds with its value, written $A\theta$. For the second rule’s head, $ancestor(x,z)\theta$ is $ancestor(\text{bob},\text{jim})$. An atom with no variables left is ground. Every fact is ground, and a substitution that binds all of a rule’s variables makes every atom of the rule ground.

Matching an atom against a fact

Matching an atom against a fact, under a substitution $\theta$ that may already bind some of the atom’s variables, finds the substitution ${\theta }^{\prime }$ that extends $\theta$ and makes the atom equal the fact, or fails. The atom and the fact must belong to the same relation, so they have the same number of positions, and matching compares them position by position:

• A constant in the atom must equal the fact’s value in that position.
• A variable already bound by the substitution must have the fact’s value in that position.
• A variable not yet bound becomes bound to the fact’s value in that position.

If every position passes, the result is $\theta$ extended by the new bindings. The first two cases test and change nothing. The third binds and cannot fail. A single position is one or the other depending on the substitution it is matched under, and the atom says nothing about which.

Matching parent(x, y) under the empty substitution binds both variables, so every parent fact matches and each gives a different substitution. The same atom matched under $\{y\mapsto \text{pat}\}$ binds only x, and only the facts with pat in the second position match: parent("bob", "pat"), giving $\{x\mapsto \text{bob},y\mapsto \text{pat}\}$.

A constant in a rule tests in the same way. In

rule toms(c) :- parent("tom", c);

the first position of the body atom matches only facts whose parent is tom, so toms holds bob and liz.

The cases also apply within a single atom. A variable written twice is bound at its first position and tested at its second. Matching parent(x, x) against parent("tom", "bob") binds x to tom in the first position and fails in the second, where x is tom and the fact has bob. Nobody in the family is their own parent, so no parent fact matches.

Matching a rule body

A body’s atoms are matched one after another, each under the substitution the ones before it produced. That is how a variable shared between atoms comes to mean the same value in each. The first atom that contains it binds it, and every later atom tests it. In the table above, parent(x, y) bound y, and ancestor(y, z) then accepted only facts that agreed.

To find every assignment, the interpreter carries a set of substitutions through the body instead of a single one. It starts with the set holding only the empty substitution. Each atom then builds a new set: for each substitution in the old set and each fact the atom matches under it, the extended substitution goes into the new set. A substitution under which the atom matches no fact drops out, and one under which it matches several facts gives several extensions. After the last atom, the set holds every assignment that makes the whole body true, and applying each to the head gives the facts the rule derives.

For the second ancestor rule, with the five parent facts and the five ancestor facts the first rule gives, parent(x, y) turns the empty substitution into five:

Two of the five substitutions are extended by the second atom, the first in two ways and the fourth in one. That gives three complete substitutions and three ancestor facts that were not known before. One more is missing from the meaning: ancestor("tom", "jim") needs ancestor("bob", "jim"), which this firing has just produced. Firing the rule again, with the new facts included, finds it. Evaluating relations repeats the firing until nothing new appears.

Carrying a set of substitutions through a conjunction of atoms is, in database terms, a join: the rows of one relation are combined with the rows of another wherever they agree on a shared column, here y. The body’s order changes the work done and never the result. Matching ancestor(y, z) first binds y and z from every ancestor fact, and parent(x, y) then tests y and binds x, which leaves the same three complete substitutions at the end. A conjunction is the same in either order, and so is the set of substitutions that satisfies it.

Queries

A query is matched in the same way, against the facts in $M(P,\Delta )$. Its holes are variables, and its other arguments are evaluated to values and become constants. ancestor(?a, "jim") is the atom $ancestor(a,\text{jim})$. Matched under the empty substitution against each ancestor fact, it binds a wherever the second position is jim, and each match is a solution. A hole written twice is one variable, so parent(?x, ?x) asks for the facts with the same value in both positions, and solutions parent(?x, ?x) is []. An anonymous hole ? is a variable that no other position shares and no solution reports. solutions parent(?p, ?) lists each parent once, ["bob", "pat", "tom"], though bob and tom have two children each.

Bridger’s matching

Bridger’s matching is the one-sided case. Every value a variable can be bound to comes from a fact, and a fact holds values, never variables: the facts add records are ground, and every fact a rule derives is ground because every head variable is bound by its body, the condition that Rule bodies and safety calls safety. So a variable is only ever bound to a value, and never to another variable or to a term containing one.

Set beside Part VI’s unify, the operation has the same cases with less in each:

Part VI’s checker needed the occurs check to stop $\alpha$ from being solved as a type containing $\alpha$. A logic variable here is bound to a value, and a value contains no logic variables, so the binding can never refer back to the variable it binds. Bridger’s matching has no occurs check because nothing could fail it.

Matching compares values with ==. Every column type of a relation is one that admits equality, as Declaring relations required, and that requirement exists for this comparison.

Building it

The engine’s terms and substitutions are provided. A Term is a logic variable or a constant value, the form both a rule’s atoms and a query’s arguments take once they reach the engine:

enum Term {
    Var(Name),   // a logic variable: x in a rule, ?x in a query
    Val(Value),  // a constant: a literal, or an evaluated query argument
}

impl Subst {
    fn new() -> Self;                         // the empty substitution
    fn get(&self, x: &str) -> Option<&Value>; // x's value, if bound
    fn bind(&mut self, x: Name, v: Value);    // bind x (overwrites)
    fn apply(&self, t: &Term) -> Term;        // Aθ, one term at a time
}

Matching is yours, as one method on Subst:

pub fn unify(&self, pattern: &[Term], fact: &[Value]) -> Option<Subst> {
    todo_m6!("Subst::unify: match terms against a ground tuple, …")
}

pattern is an atom’s arguments and fact a tuple of the relation. The method returns the extended substitution, or None when some position disagrees or the two have different lengths. It leaves self unchanged either way, so the caller can try the same substitution against the next fact, which is how one substitution becomes several. Within one call, a variable bound at one position counts as bound at every later position of the same atom, so parent(x, x) against parent("tom", "bob") binds x at the first position and fails at the second. bind overwrites, so a variable that is already bound has to be checked with get before anything is bound.

Once a body has been matched, applying each complete substitution to the head’s terms, with apply, gives the tuple of the derived fact. A query’s anonymous holes reach the engine as variables too, each given a name that no other position uses, so it binds nothing that any other position tests and is left out of the solutions. The engine that carries the set of substitutions through a body and fires the rules is built in Evaluating relations, and it calls unify for every pairing of an atom and a fact.

The design space

Two-sided unification

Prolog unifies terms that have variables on both sides and that may be built from other terms. Its lists are compound terms, [H|T] for a list with head H and tail T, and appending two lists is two clauses:

append([], L, L).
append([H|T], L, [H|R]) :- append(T, L, R).

Asked append([1], [2], X), Prolog binds X to [1, 2]. Asked append(X, Y, [1, 2]), it runs the other way and gives every way of splitting the list: X = [] and Y = [1, 2], then X = [1] and Y = [2], then X = [1, 2] and Y = []. Each step unifies the goal with a clause head, binding variables to terms that themselves contain variables, such as [1|R], to be filled in by later steps. This takes the full algorithm of Part VI applied to terms instead of types: two-sided, recursive through compound terms, and in need of the occurs check.

When Bridger’s relations give up compound terms, they give up this power too. Without terms built from other terms, a variable meets only values, and matching is a loop over positions with a comparison in each. A list in Bridger is computed by functions, and a relation can hold one as a column value but cannot take it apart in a rule.

The occurs check

Unifying X with f(X) would bind X to a term containing X. The occurs check rejects this, at a cost: before binding a variable to a term, it looks through the whole term, so binding a variable to a large term costs time proportional to the term’s size. Most Prolog systems skip the check by default and provide a separate, checked unification for when it matters; without it, X = f(X) succeeds and builds a term that contains itself. Colmerauer’s later Prolog II took that outcome as intended and treated such terms as infinite trees, which its unification was designed to handle. Robinson’s algorithm, Part VI’s checker, and checked unification in Prolog all reject the binding. Bridger never meets the case.

General unification has a cost even with the check, since terms that share subterms can make a direct implementation of Robinson’s algorithm do far more work than the terms’ size suggests, and later algorithms, Martelli and Montanari’s among them, were designed to avoid it. One-sided matching against a fact costs one comparison per column.

Which atom first

Since the order of a body’s atoms does not change its substitutions, an engine may choose the order. The choice decides how many facts are tried. In the firing above, starting with parent(x, y) binds y, after which ancestor(y, z) need consider only the ancestor facts whose first position is that value. An engine that keeps each relation indexed by column finds those facts directly instead of trying every one. Database systems choose join orders and indexes for each query; Prolog leaves the order to the programmer, who writes it; Bridger’s meaning ignores the order, and its engine is free to pick one.

Further reading

Unification: Kevin Knight’s “Unification: A Multidisciplinary Survey” (1989) follows unification through theorem proving, logic programming, type inference, and natural-language processing, and covers the algorithms and their costs. Alberto Martelli and Ugo Montanari’s “An Efficient Unification Algorithm” (1982) presents unification as solving a set of equations by transformation rules and gives the efficient algorithm.

Unification without the occurs check: Alain Colmerauer’s “Prolog and Infinite Trees” (in Logic Programming, ed. Clark and Tärnlund, Academic Press, 1982) gives the theory behind treating the terms built by omitting the check as infinite trees.

Joins and their evaluation: Abiteboul, Hull, and Vianu’s Foundations of Databases, freely available from the authors, treats evaluating Datalog rules as joins in its chapter 13, “Evaluation of Datalog”.

Concept checks