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 variables being replaced together constitute the domain of the substitution, and the terms replacing them constitute the range. For example, in the preceding substitution, the domain is {X, Y, Z}, and the range is {a, f(b), 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.

Given two or more substitutions, it is possible to define a single substitution that has the same effect as applying those substitutions in sequence. For example, the substitutions {X←a, Y←U, Z←V} and {U←d, V←e} can be combined to form the single substitution {X←a, Y←d, Z←e, U←d, V←e}, which has the same effect as the first two substitutions when applied to any expression whatsoever.

Computing the composition of a substitution σ and a substitution τ is easy. There are two steps. (1) First, we apply τ to the range of σ. (2) Then we adjoin to σ all pairs from τ with different domain variables.

As an example, consider the composition shown below. In the right hand side of the first equation, we have applied the second substitution to the replacements in the first substitution. In the second equation, we have combined the rules from this new substitution with the non-conflicting rules from the second substitution.

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.

One good thing about our language is that there is a simple and inexpensive procedure for computing a most general unifier of any two expressions if it exists.

The procedure assumes a representation of expressions as sequences of subexpressions. For example, the expression p(a,b,Z) can be thought of as a sequence with four elements, viz. the predicate p, the symbol a, the symbol b, and the variable Z.

The procedure also assumes that the two expressions have no variables in common. As we shall see in the next section, we can assure this by renaming the variables in one of the expressions.

We start the procedure with two expressions and a substitution, which is initially the empty substitution. We then recursively process the two expressions, comparing the subexpressions at each point. Along the way, we expand 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.

In comparing two subexpressions, we first apply the substitution to each of the two expressions; and we then execute the following procedure on the two modified expressions.

1. If one expression is a symbol and the other expression is the same symbol, then the procedure succeeds, returning the unmodified substitution as result.


2. If one expression is a symbol and the other expression is a different symbol or a compound expression, then the procedure fails.


3. If one expression is a variable and the other expression is the same variable, then the procedure succeeds, returning the unmodified substitution as result.


4. If at least one expression is a variable and the other expression is any other expression, we proceed as follows. First, we check whether the other expression contains the variable. If the variable occurs within the other expression, we fail (for reasons described below). Otherwise, we update our substitution to the composition of the old substitution and a new substitution in which we bind the variable to the second modified expression.


5. If the two expressions are sequences of the same length, we iterate across the expressions, comparing as described above.


6. If the expressions are compound expressions of a different length, the procedure fails.

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. There are three salient changes. (1) The procedure is begun with a goal and a substitution. (2) Rather than checking whether a goal and a factoid or a rule head are identical, the procedure checks whether or not they are unifiable. (3) Instead of returning a Boolean value from each recursive call, the procedure returns a substitution that makes the given goal true and it uses this substitution in processing any remaining subgoals. The steps of the procedure are described below.

1. 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.)


2. If our goal is a negative literal, we execute the procedure on the argument of the negation and the given substitution. If the result is empty, we return a singleton list containing the given substitution. Otherwise, we return the empty list, indicating failure to prove the negation.


3. If our goal is a conjunction of literals, we first execute our procedure on the first conjunct and the given substitution to get a list of substitutions that satisfy that conjunct. We then iterate through the list of substitutions, calling the procedure recursively on the remaining conjuncts with each substitution in turn. We collect the answers from these recursive calls. We return the list of these answers as value of the procedure.


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 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}.

As a more interesting example, imagine that we want to evaluate the goal s(X), i.e. we want all objects that satisfy the s relation. We call our procedure with s(X) and the empty substitution {}. Since s is a view relation, we examine the rules where s appears in the head. We copy the first rule resulting in the new rule s(X1) :- p(X1) & q(X1) & r(c), and we try to unify our goal with the head of this rule. In this case, we succeed with the substitution {X←X1}. We then call the procedure recursively on the body of the rule and this substitution and proceed as before, resulting in a final answer containing the single substitution {X←b, X1←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.