Loop checking in logic programming
Roland N. Bol · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1995
Given an implication or clause A~B 1, ... ,Bn, its logical meaning (declarative interpretation) is: ifB1 is true and ... and Bn is true then A is true.An obvious procedural interpretation can be derived from this: if the user requests a proof of A, try to prove B1 and ... and 8 0 • This very popular control mechanism is known as top-down interpretation, because it corresponds to the top-down construction of a proof tree for A.Unfortunately, programmers often over-use these extra-logical features of PROLOG, especially the cut.The result is 'imperative PROLOG': a program that consists mainly of control information and that has no declarative meaning.Additional control information is often provided to improve the efficiency of a logic program.The most extreme form of inefficient behaviour of a program is nontermination. NonterminationAlthough every solution is present in an SLD-tree, it is not guaranteed that it is also found by an interpreter.When a logic program is interpreted by a PROLOG-like interpreter, the result is often a nonterminating computation.This does not mean that the program is logically incorrect.It is caused by the fact that the interpreter employs a depth-first search through the SLD-tree.Consequently it can enter an infinite branch and miss a solution.The problem of detecting such a possibility of nontermination is generally undecidable as logic programming has the full power of recursion theory.Programmers have developed a number of useful heuristics to enforce termination.Sometimes it suffices to give a more complex set of logical rules.However, the resulting program can be very different from the original one.More often than not, the programmer decides to add explicit control primitives to the program, thereby destroying its declarative meaning.In both cases the burden of avoiding nontermination rests with the programmer.Another possible approach to this problem is based on modifying the interpreter that searches through the SLD-tree by adding a capability of pruning.Pruning an SLD-tree means that at some point the interpreter is forced to stop its search through a certain part of the tree, typically an infinite branch.Every method of pruning SLD-trees considered so far has been based on excluding some kind of repetition in the SLD-derivations, because such a repetition can make the interpreter enter an infinite loop.That is why pruning SLD-trees has been called loop checking. Ext,mpleTo better understand the relevance of the problems studied here, consider the following example.Let P be the following simple-minded logic program computing in the relation tc the transitive closure of the relation r: P = { tc(x,y) ~ r(x,y).tc(x,y) ~ r(x,z),tc(z,y).} .Suppose we add to P the following facts about r: r(a,a)~.r(a,b)~.r(b,c)~.r(d,a)~.Then we can interpret Pas a PROLOG program, but if we ask:2.1 + 2.2 5.1 + 5.2 Logic Programming Chapter I A positive literal is just an atom (A), a negative literal is the negation of an atom (-.A).Literals are denoted by L1, L2, ....In Chapter 5 we shall encounter general clause.v:constructs of the form A1v ... vA111 f--L1A ... ALn, where AJ, ... ,Am are atoms but L1, .. ,,Ln are (not necessarily positive) literals.Again, such a general clause is called a general goal if m = 0, a general program clause if m = 1.(General) goals are denoted by G, H, G1, G2, ... , (general) program clauses by C1, C2, ....For a (general) program clause Af--LJ, ... ,Ln, A is called the head of the clause and L1, ... ,Lm the body.For a goal G, IGI denotes its length, i.e., the number of atoms in it.A logic program (or just a program) is a finite nonempty set of program clauses.A general logic program (or just a general program) is a finite nonempty set of general program clauses.With each (general) program P we can uniquely associate a first-order language Lp whose constants, functions and predicates are those occurring in P. P isfunction{ree if P contains no function symbols.An expression is a term, literal, sequence of literals, clause or program, and is d•!noted by E. For an expression E, var(E) denotes the set of variables that oc:ur in E. If var(E) = 0 then E is called ground.Substitutions Consider now a fixed first-order language.A substitution is a finite mapping from variables to terms, and is written as 8 = {x1/tJ, ... ,xn/tn}, It is to be read: the variables XJ, .. ,,Xn are mapped (bound) to t1, ... ,tn re.-.pectively.The notation implies that the variables XJ, .. ,,Xn are different.We also assume that Xi t, ti (i = l, ... ,n).A pair Xi/li is called a binding.(x1, ... ,xnl is tailed the domain of 8 (dom(O)), {tt,•••,tn} the range of 8 (ran(O)).If 8 is a bijection, that is if dom(8) = ran(9), then 8 is called a renaming.Thus a renaming is simply a permutation of a finite nummu-of variables.The empty substitution or uhntity substitution is denoted by E: E = dom(E) = ran(E) = 0. Substitutions operate on expressions.For an expression E and a sub.,t1tution 8, E0 stands for the re.,ult of applying 8 to E, whic::h is obtained by sintul.tlineouslyreplacing each occurrenee in E of a variable from dom(8) by the corresponding term.A substitution 8 is ground (in a given context) if E8 is ground for all expressions E that occur in that context.Section I.I Syntax 13 Substitutions can be composed.Given substitutions 8 and 11, their composition 811 is defined as 1108 (regarding substitutions as functions).Alternatively, if 8 = {x1/t1, ... ,xn/tn} and 11 = {y1/u1, ... ,yn/un}, then 811 is obtained by removing from the set {x1/t111, ... ,xnllnll,Y1lu1, ... ,yn/un} the pairs x/till for which Xi = till as well as the pairs y/ui for.which Yi E { x 1 , ... ,Xn}.Thus for an expression E and substitutions O", 8 and 11, (E8)11 = E(811) and can be written as E811; (cr8)11 = 0"(011) and can be written as 0811.A substitution 0 is idempotent if 80 = 0.It is easy to see that a substitution 0 is idempotent if and only if dom(8) n var(ran(8)) = 0.So the only idempotent renaming is£.For two expressions E and F, E is an instance of F (F is more general than E, notation F ~ E) if for some substitution 0, E = F0.E and Fare variants if E = F0 for some renaming 0. A substitution 0 is more general than 11 if 11 = 0y for some substitution y. 0 and 11 are variants if 11 = 0y for some renaming y.For a program P, ground(P) denotes the set of all ground instance of clauses in Pin the language Lp.Notice that ground(P) can be infinite. Un(ficationConsider two atoms A and B. If for some substitution 0 we have A0 = B8, then 8 is called a un(fier of A and B and we say then that A and B are unifiable.A unifier 0 of A and Bis called their most general un!fier (or mgu in short) if it is more general than any other unifier of A and B. A unifier 8 of A and Bis called relevant if dom(0) ~ var(A) u var(B).It is easy to prove that every idempotent mgu of A and Bis relevant.The following theorem is due to Robinson [Ro].THEOREM 1.1.1(Unification Theorem).There exists a unification algorithm which for any two atoms produces an idempotent most general unifier (f they are unifiable and reports nonexistence of a unifier otherwise.PROOF.The unification algorithm we give here was first presented by Martelli & Montanari ([MM]).Two atoms can only be unified if they have the same predicate symbol.When p(s1, ... ,sn) and p(t1, ... ,tn) are to be unified, first the set of equations { s 1 = t 1, ... , Sn = tn} is constructed.This set is then transformed according to the following six rules: Logic Programming Chapter I COROLLARY 1.2.7.Let iJ = (Go =>c J,6/ G J => ... => G;_J =>c;,6; G; => ... ) be a normal SW-derivation c,,61 G J => ... => G;_, =>c;,6; G; => ...