8.1 Introduction

In the preceding chapter, we defined the result of applying a stratified logic program to a dataset in a constructive manner - starting with the dataset and successively applying the program's strata to produce an extension of the program as a whole. This definition readily translates to a practical method of computing such extensions known as bottom-up evaluation.

Although bottom-up evaluation is used in some Logic Programming systems, many evaluation engines use a top-down approach to answering questions. Instead of starting with data and working upward, such engines start with a query to be answered and work downward, using rules to reduce the goals to subgoals until they reach subgoals written entirely in terms of base relations.

The benefit of doing things this way is that such evaluation engines avoid the generation of large numbers of conclusions that have nothing to do with the question at hand. More significantly, in cases where there are infinitely many possible conclusions, they can often find answers to specific questions without doing infinitely much work.

One downside to top-down evaluation is that, for some people, it is more difficult to understand than bottom-up evaluation. There is also a danger of unnecessary infinite loops if rules are written badly. However, that danger can be minimized or eliminated by understanding how the procedure works. A little familiarity with top-down processing can help one understand how it works and can help one avoid writing bad rules.

In this chapter, we introduce a particular top-down evaluation procedure. We begin by defining a top-down, backtracking approach to processing goals and rules without variables. We then introduce the key process of unification. Finally, we put the two together in a top-down procedure for arbitrary goals and rules.

8.2 Top-Down Processing of Ground Goals and Rules

In this section, we begin our discussion of top-down evaluation by focussing on goals and rules without variables. In the next section, we look at a way of comparing expressions containing variables. In the section after that, we show how to combine that technique with the procedure described here to produce an evaluation procedure for arbitrary goals and rules.

Top-down evaluation is a recursive procedure. We start with a goal to be "proved". We either prove the goal directly or we reduce it to one or more subgoals and try to prove those subgoals. The way we process a goal depends on the type of the goal we are given.

1. If the goal is an atom and the predicate in the goal is a base relation, we simply check whether the goal is contained in our dataset. If it is there, we succeed. If not, we fail.


2. If the goal is a negative literal, we execute the procedure on the argument of the negation. If we succeed in proving the argument, then the negation as a whole is false, and the procedure fails. If we fail to prove the argument, then the negation as a whole is true, and so we succeed.


3. If our goal is a conjunction of literals, we first execute our procedure on the first conjunct. If we succeed in proving that goal, we move on to the next conjunct and so forth until we are done. If we fail to prove any one of the goals, then we fail to prove the conjunction as a whole.


4. If the goal is an atom and the predicate in the goal is a view relation, we examine all rules with our goal as head. For each such rule, we execute our procedure on the body of the rule. We succeed on our goal if and only if we can succeed on the body of some rule; otherwise, we fail.

As an example, consider the dataset shown on the left below and the rule set shown on the right. There are three base relations - p, q, r; and there are two view relations - s and t.

Now, imagine that we are asked whether to evaluate the goal s(b). Since s is a view relation, we examine the rules containing s(b) in the head and execute the procedure on the bodies of these rules, one after another until we find one that succeeds.

Using the first rule for s(b), we reduce our goal to the conjunction (p(a) & q(b) & r(c)) and evaluate this subgoal. Since p is a base relation, we simply check our dataset for the literal p(a). Since p(a) is in the dataset, that subgoal evaluates to true and we move on to the second conjunct q(b). Since q is a base relation, again we check our dataset for the literal q(b). Unfortunately, in this case, we fail since q(b) is not a member of the dataset. At this point, we terminate processing of the conjunction. (Since the conjunction as a whole is false, there is no point in check r(c).)

Having failed to prove the body of the first rule, we move on to the second rule and try again, this time with p(a) & ~q(b) & ~t(c) as our goal. As before, we find that p(a) is true and we move on to the second conjunct. In this case, we have a negation, so we execute the procedure recursively on q(b). As before, we fail. Therefore, the subgoal ~q(b) is true. The upshot is that this time we continue and execute the procedure on ~t(c). Since t is view relation, we execute the procedure on the bodies of the rules containing t(c) in the head. In this case, we first try r(c) and fail; then we try r(d) and fail once again. Having exhausted all of the rules defining t(c), we fail to prove t(c). This means that the negation ~t(c) is true. The upshot of that is that the conjunction (p(a) & ~q(b) & ~t(c)) is true; and, hence, our overall goal s(b) is true.

8.3 Unification

Unifcation is the process of determining whether two expressions can be unified, i.e. made identical by appropriate substitutions for their variables. As we shall see, making this determination is an essential part of top-down evaluation.

A substitution is a finite mapping of variables to terms. In what follows, we write substitutions as sets of replacement rules, like the one shown below. In each rule, the variable to which the arrow is pointing is to be replaced by the term from which the arrow is pointing. In this case, X is to be replaced by a, Y is to be replaced by f(b), and Z is to be replaced by V.

The result of applying a substitution σ to an expression φ is the expression φσ obtained from the original expression by replacing every occurrence of every variable in the domain of the substitution by the term with which it is associated.

A substitution σ is a unifier for an expression φ and an expression ψ if and only if φσ=ψσ, i.e. the result of applying σ to φ is the same as the result of applying σ to ψ. If two expressions have a unifier, they are said to be unifiable.

The expressions p(X,Y) and p(a,V) have a unifier, e.g. {X←a, Y←b, V←b} and are, therefore, unifiable. The results of applying this substitution to the two expressions are shown below.

Note that, although this substitution is a unifier for the two expressions, it is not the only unifier. We do not have to substitute b for Y and V to unify the two expressions. We can equally well substitute c or f(c) or f(W). In fact, we can unify the expressions without changing V at all by simply replacing Y by V.

In considering these alternatives, it should be clear that some substitutions are more general than others. We say that a substitution σ is as general as or more general than a substitution τ if and only if there is another substitution δ such that σδ=τ. For example, the substitution {X←a, Y←V} is more general than {X←a, Y←c, V←b} since there is a substitution {V←c} that, when applied to the former, gives the latter.

In top-down evaluation, we are interested only in unifiers with maximum generality. A most general unifier σ of two expressions has the property that it is general as or more general than any other unifier.

Although it is possible for two expressions to have more than one most general unifier, all of these most general unifiers are structurally the same, i.e. they are unique up to variable renaming. For example, p(X) and p(Y) can be unified by either the substitution {X←Y} or the substitution {Y←X}; and either of these substitutions can be obtained from the other by applying a third substitution. This is not true of the substitutions mentioned earlier.

See below for a version of a Javascript implementation of a procedure for computing a most general unifier of two expressions. The procedure assumes a representation of expressions as sequences of subexpressions. For example, the expression p(X,f(b)) can be thought of as a sequence with three elements, viz. the predicate p, the variable X, and the compound expression f(b).

The procedure also assumes that the two expressions have no variables in common. We can always assure this by renaming the variables in one of the expressions.

We start the procedure with two expressions and a substitution (initially the empty substitution). We then recursively process the two expressions, comparing the subexpressions at each point. Along the way, we extend the substitution with variable assignments as described below. If, we fail to unify any pair of subexpression at any point in this process, the procedure as a whole fails. If we finish this recursive comparison of the expressions, the procedure as a whole succeeds, and the accumulated substitution at that point is the most general unifier.

1. If the pattern and the instance are the same, then the procedure succeeds, returning the unmodified substitution as result.


2. If at least one expression is a variable, we proceed as follows. First, we check whether the other expression contains the variable. If the variable occurs within the other expression, we fail. Otherwise, we extend our substitution to include a binding of the variable to the other expression.


3. If either the pattern or the instance is a constant, then the procedure fails.


4. If the pattern and the instance have different lengths, we fail.


5. Otherwise, we iterate across the corresponding subexpressions of the two expressions. If we fail to match the subexpressions at any point in this process, the procedure as a whole fails. If we finish this recursive comparison of the expressions, the procedure as a whole succeeds and the accumulated substitution at that point is the resulting unifier.

As an example of this procedure in operation, consider the computation of the most general unifier for the expressions p(X,b) and p(a,Y) with the initial substitution {}. A trace of the execution of the procedure for this case is shown below. We show the beginning of a comparison with a line labelled "Compare" together with the expressions being compared and the input substitution. We show the result of each comparison with a line labelled "Result" (either a substitution where successful or "false" where unsuccessful). The indentation shows the depth of recursion of the procedure.

As another example, consider the process of unifying the expression p(X,X) and the expression p(a,Y). A trace is shown below. The main interest in this example comes in comparing the last argument in the two expressions, viz. X and Y. By the time we reach this point, X is bound to a, so we call the procedure recursively on a and Y, which results in a binding of Y to a.

One noteworthy part of the unification procedure is the test for whether a variable occurs within an expression before the variable is bound to that expression. This test is called an occur check since it is used to check whether or not the variable occurs within the term with which it is being unified. For example, in trying to unify p(X,X) and p(Y,f(Y)), we would not want to bind Y to f(Y), since these expressions can never be made to look alike by substituting and value for Y consistently throughout the expression.

8.4 Top-Down Processing of Non-Ground Queries and Rules

Using unification, we can convert our procedure for top-down evaluation for ground queries and rules to a procedure for evaluating arbitrary queries and rules. See below for a top-down view evaluation procedure encoded in Javascript. The procedure takes as arguments an answer pattern, a query expression, a dataset (a list of factoids), and a ruleset ( a list of rules). It calls a subroutine queryall to produce a list of substitutions that make the query true, substitutes the variable bindings into the answer pattern, and returns a list of the resulting instances.

As with simple query evaluation, the queryall procedure does all of the hard work in evaluating view queries. It takes as arguments a list of subgoals, a substitution (initially empty), a dataset, and a ruleset. It returns a list of all variable substitutions that make all of the given subgoals true on the basis of the given dataset and ruleset.

The procedure assumes that the subgoals in the query, the factoids in the dataset, and the rules in the ruleset are all represented as sequences of expressions. For example, the expression p(X,f(b)) can be thought of as a sequence with three elements, viz. the predicate p, the variable X, and the expression f(b).

The procedure processes the subgoals in order. If at any point there are no subgoals, then the procedure returns a list of the given substitution as answer. Otherwise, it processes the first subgoal to get a list of answers that make it true and then executes the procedure recursively on the remaining subgoals, once for each answer to the first subgoal.

1. If the first subgoal is a negation, the procedure calls itself on the argument of the negation and the given substitution. If the result is a non-empty set (i.e. there are any substitutions that work), then the negation is false and the procedure returns false as answer. If the result of the recursive execution is the empty set (i.e. there are no substitutions that work), then the negation as a whole is true and the procedure calls itself recursively with the remaining subgoals and the corresponding substitution and returns the result.


2. If the query is a conjunction, the procedure adds the conjuncts to the subgoal list and calls itself recursively.


3. If the predicate in the goal is a base relation, we iterate through our dataset comparing the goal to each factoid in turn. If there is an extension of the given substitution that unifies the goal and the factoid, we add that extended substitution to our list of answers. Once we have finished examining all relevant factoids, we return the list of substitutions we have accumulated along the way. (If we do not find any factoids that unify with the goal, we return an empty list.)


4. If our goal is an atom and the predicate is a view relation, we iterate through the rules in our program. We first copy each rule, replacing the variables by new variables (to avoid possible conflicts with variables in our goal). We then try to find a most general unifier for the given goal and the head of the rule starting with the given substitution. If we succeed, we call the procedure recursively on the body of the rule (together with the remaining subgoals) and the resulting unifier. We add all substitutions returned from this recursive call to our output list. When we have finished examining all of the rules, we return the substitutions we have collected along the way.

Once again, consider the dataset we saw earlier (repeated on the left below), and consider a version of the logic program with some of the object constants replaced by variables (shown on the right below).

To see our procedure in action, let's start with a simple case. Imagine that we want to find all objects that appear in both the p relation and the q relation. We call our procedure with p(X) & q(X) as goal and the empty substitution {} as initial substitution. Since our goal is a conjunction, we first call the procedure recursively on p(X) and {}. Our goal p(X) with initial substitution {} unifies all three of the p factoids in our dataset, and so the result of the recursive call is a list of the resulting substitutions, i.e. {X←a} and {X←b} and {X←c}. For each of these substitutions, we then call the procedure recursively on the second conjunct q(X). There is no factoid that unifies with q(X) given the {X←a} substitution, so in this case we return the empty list. In the second case, we are luckier. q(X) and q(b) do unify given the substitution {X←b}, so we return a list containing that substitution. The third case is similar to the first in that there is no unifiable factoid, so again we get an empty list. Having checked the second conjunct for each of the answers to the first conjunct, we return the list of substitutions we have accumulated along the way, in this case the list consisting of the single substitution {X←b}.

The procedure just described computes all answers to a given query. If we want just a few answers, we can use a "pipelined" version of the algorithm that returns one answer at a time. When processing a rule, rather than computing all answers to a subgoal before proceeding, once we have a single answer we check whether that solution leads to an answer to the remaining subgoals. If it does, we return that answer. If not, we generate another answer to our subgoal and try again.

Exercises

Exercise 8.1: Suppose we were to run our top-down evaluation method on the dataset shown below and the ruleset shown on the right. How many dataset accesses would be required to evaluate s(b). (Each time a factoid is looked up counts as one access.)

Exercise 8.2: For each of the following pairs of sentences, say whether the sentences are unifiable and give a most general unifier for those that are unifiable.

Exercise 8.3: Suppose we were to run our top-down evaluation method on the dataset shown below and the ruleset shown on the right with the goal r(a,d). Show a trace of subgoals in the order in which they are processed and the results.