An Interpreter For The Programming Languages Predicate Logic

Introduction

The development of programming languages has more and more relieved a programmer from machine control and details, giving him the power of ab­ stract reasoning and thus helped him to concentra­ te more on his problem. Kowalski [8,9) has convin­ cingly argued that predicate logic formalizes a man's thoughts and is a useful simple programming language for human problem solving. Consequently it is desirable to have predicate logic implemen­ ted on machines for practical programming. There is one implementation at the University of Aix­ Marseille, PROLOGUE [2). At the University of Stockholm we have implemented an interpreter in LISP 1.6 [11).

Syntax and Proof Procedure

TI1e syntax of the language consists of Kowalski's procedural form [7) plus a control structure consisting of an ordered procedure, or­ dered procedures and computational consequences (Tarnlund [14)). The proof procedure is based on Kowalski's cqnnection graph system [6).

Kowalski's procedure form

A procedure is the only type of statement in the language. It contains two special cases, a goal and an assertion. Two typical procedures are

which is read "x owns y if there is a z such that x owns z and y is a part of z", and

which is read "x divides y or x divides z if there is a w such that x divides w and x is a prime and y · z = w". The part to the left of the arrow is called procedure name and the part to the right is called procedure body consisting of procedure calls.

A goal statement is a procedure without a name e.g . ,

An assertion is a procedure without a body e.g. ·

A program is a set of procedures connected in a graph depending on how they match each other.

AN INTERPRETER FOR THE

PROGRAMMING LANGUAGE PREDICATE LOGIC

Sten-Ake Tarnlund Computer Science Department University of Stockholm

For example, the program

+ Part(finger,arm)

Part(x,y) + Part(x,z),Part(z,y)

Part(hand,arm) +

Part(finger,hand) + ,

gives rise to the following connection graph

The connection graph is indipendent of the order the programmer presents his statements. De­ pending on one's programming style (problem-sol­ ving) one can combine top-down, middle-out and bottom-up programming. The goal of the interpreter is to activate links (resolve corresponding atoms) in a way that eventually leads to the empty pro­ cedure 0 .

Control structure

The control structure transfers some decision­ making responsibility from the search strategy to the programmer and makes the decisions ex­ plicit. This is illustrated by a program that probes for a node to be deleted in a binary tree such that its remaining nodes are sorted when tra­ versed in symmetrical order. The program is based on a delete algorithm in Knuth [5). We use Knuth's zodiac example (sec. 6.2.2) to delete the node CAPRICORN from a binary tree. The initial goal is

Suppose that we have the binary tree in a data base

where A is an arbitrary predicate whose argument tree is equal to t(t(O,AQUARIUS,t(O,ARIES,t(O,CANCER,O))), (3) CAPRICORN,t(t(O,GEMINI,t(O,LEO,t(O,LIBRA,O))), PISCES,t(t(O,SCORPIO,O),TAURUS,t(O,VIRGO,O)))), This zodiac binary tree "tree" is an instantiation of the data structure

t(x,y,z)

denoting a binary tree with a root y and a left subtree x and a right subtree z. An empty tree is denoted 0. When we have picked up the binary tree from the data base and deleted the node CAPRICORN, we want to put the new tree back into the data base i.e.,

where u is the node to be deleted in a binary tree x, and z is the resulting binary tree. Note that Delete* and Delete are two different predicates. The predicate within the braces is a computational consequence not to be resolved upon during the computation, but to be put into the data base when the remaining part of procedure (4) is resolved to the empty clause. (Computational consequences may be viewed as a generalization of Green's answer predicate [3)). The angled brackets '<' and 1 > 1 tell us that procedure (4) is an ordered p~ocedure and is executed from left to right within the brackets.

In the delete algorithm we check each node in the binary tree to determine whether it is to be deleted or if we have to continue a binary tree search for the node to be deleted. The procedures for this algorithm are ordered among themselves and delimited by a pair of double angled brackets '<< 'and '>> 1 · This ordering controls the executi­ on of the procedures.

There are two cases when a node is deleted. The simpler case occurs when the left subtree of the right subtree of a node u is empty viz.,

« Delete(t(x,u,t(O,y 1 ,z')),u,t(x,y 1 ,z 1 )) + 1 (5)

where the new binary tree

is "the old tree with the root u deleted". The con­ trol structure attempts to execute this procedure first. In case we have to search for the successor node y of the deleted node u in symmetrical order, the procedure is more complicated viz.,

where

is the new binary tree in which the root y anq the left subtree x" are still unknown. They are de­ duced by the Successor procedures (9) and (10).

In case we have not found the node to delete we have to search for it viz . ,

Delete(t(x,y,z),u,t(x',y,z)) +

where the node u to be deleted is to be found in the left subtree x of y. The new binary tree he comes

where x' is the same tree as x but with a node de­ leted. When the probed node is in the right sub­ tree of y we have

where the node u to be deleted is found in the right subtree z. LE and Gr are "built-in" procedu­ res that determin~ alphabetic orderin&s (see below). The procedures (5) - (8) are ordered· among them­ selves, which means that a procedure call Delete(x,y,z) first will try procedure (5) ; if that procedure cannot be resolved to the empty procedure the call will try procedure (6) and so on.

To complete the program we write the recursive successor procedures that probe for a node y which is the successor in symmetric order of the deleted node u viz.,

where (10) is the recursion step and (9) the re­ cursion base which terminates the search for the successor node on the first root with an empty left subtree.

Procedures (5), (6), (9) and (10) with the goal

+ Delete (tree ,,CAPRICORN, z),

where tree is equal to the binary tree in (3), have been executed on the theorem prover of Allen & Luckham [1], at the Artificial Intelligence Labora­ tory, Stanford University, in 2.6 seconds (see appendix).

Procedure Evocation

A computation is mainly goal oriented i.e., the interpreter tries to find out a deduction top­ down from the goal. There are, however, some im­ portant deviations.

Bottom-up pre-processing

It is generally recognized that it is impor­ tant to find the "right" data structure for a prob­ lem and to make strong use of it. For predicate logic programs this can mean improvements of seve­ ral magnitudes. The reason for such improvements is that predicate logic programs can be very non­ deterministic but by making a bottom-up pre-proces­ sing of the data structure the program can become much more deterministic. We show this idea with a slight variation of an example from Kowalski [9] .

This program is written using the philosophy that a program should be separated from its data structure as much as possible, and leads to a highly non-deterministic and data independent pro­ gram. The data representation

t(x,u)

of a tower where x is a top block and u is the rest of the tower, is only used in the assertion Parts(x,u,t(x,u)) + · A bottom-up pre-processing of this assertion by activating the links 1, 2, 3 together with link 4 gives

---------

The program in fig.3 with the data structure pre-processed into the procedures seems to use the "right" data structure t(x,u) for this problem where x is a top block and u is either an empty tower or a tower t(v,y) where y is an empty tow­ er, denoted 0, or a non-empty tower. Notably, this more deterministic tower program is more than 15 times faster than the program in fig.2 for the goal

+ Tower(t(A,t(B,t(C,t(D,O))))),

when run on the theorem-prover at the Artificial Intelligence Laboratory, Stanford University (see appendix).

In a top-down execution the variable v of atom On(x,v) will always be bound to a block so the starred link in fig.3 will never be activated. Consequently we can erase it, which then implies that the recursive "On" procedure contains a pure literal and thus can be deleted from the graph. This reasoning about data types would be simplifi­ ed if the variables and their types were declared. Most of the pre-processing that we have seen follow a one link rule (see below).

One link evocation

Another important deviation from a top-down computation can occur from a one link evocation. The one link rule, however, is also useful during a top-down computation, because of the fact that a whole procedure can be deleted from a graph, if the procedure contains an atom connected with only one link, which is activated (Kowalski [6]). The following figures show a one link evocation.

c·p·----

There are two atoms connected with only one link in graph G. Selecting statement 1 gives a top­ down computation and a new goal

+ Own(x,z),Part(tyre,z)

in G'. This goal is non-deterministic in the sense that the interpreter is not told which subgoal to solve first. This problem is discussed qelow in the sections built-in procedures and instantiation evo­ cation. The old goal

+ Own(x,tyre)

in G, is deleted giving a cleaned up graph G'. The one link rule does not workinG'; how­ ever, the interpreter could have followed the one link rule in a bottom-up computation by evoking statement 3 giving G".

The one link rule is applicable again in G", this time middle-out, giving the new fact

Own(John,tyre) + ,

which is a recursion base. The problem is now sol­ ved top-down using the recursion base giving a solution x + John in the goal

+ Own (x, tyre).

The transformation from G to G" shows an efficient problem-solving sequence by the one link rule combining bottom-up, middle-out and top-down computation. Bottom-up and middle-out execution corresponds to PLANNER's (Hewitt [4]) antecedent theorem and top-down to a consequent theorem.

A matcher containing a unification algorithm (Robinson [12]) plays a major role, operating on the substitution sets corresponding to a link. The matcher computes the substitution set to a new link in a local area.

Instantiation evocation

The graph G' in fig.4 has no one link atom, however, in the goal

the second subgoal is more instantiated than the other. TI1is fact is a heuristic giving the inter­ preter a hint that a first attack on that goal could give a more deterministic computation (Minker et al. [10]). The interpreter recognizes also that the subgoals have common variables i.e., they are dependent. So when searching for soluti­ ons for z in Part(tyre,z), the interpreter checks these for compatibility with the subgoal

Built-in procedures

The interpreter also has built-in knowledge that makes it simpler to write programs. We are already familiar with the huilt-in predicates LE(u,y) and Gr(u,y) (the delete program above) which nrc true when the relations u < y and y > u are satisfied.

We can also use ordinary numbers like 0, 1, 2, ... instead of 0, s(O), s(s(O)), ... , where s

is a successor function.

The interpreter has a knowledge base of use­ ful LISP-functions [11] which can be used as pro­ cedures. The knowledge base can be increased by a programmer. Some useful LISP-functions e.g., add, difference and cons which can be represented as the following procedures: ADD(x,y,z), DIFF(x,y,z) and CONS(x,y,z), where x and yare input variables and z is an output variable. If the input variab­ les are instantiated with numbers then the ADD and DIFF predicates are solved directly e.g.,

is solved with z + 7. The procedure CONS(x,y,z) is even solved when the output variable z is bound to a list e.g.,

gives x +a and y + [b,c].

The matcher can solve more complex problems like the three dependent subproblems

from its knowledge base in LISP-code. The solution is equivalent to the following sequence of substi­ tutions, y + diff[z,l], and x + diff[z,2] giving add[diff[z,2],diff[z,l]] = 3, which gives

z + 3, y + 2 and x + 1.

Built-in procedures like LE and Gr are used frequently at decision points during a computation thus they are given high priority to be matched.

Function Transformation

In the section on pre-processing predicates were instantiated with a data structure (function). Sometimes, however, we want to do the opposite i.e., move a function out of a predicate and trans­ form it to a predicate. We explain this idea from Kowalski [9] with an example.

Suppose that we have to sort a list of three ele­ ments [c,b,a] i.e., the initial goal is

where z is the output variable and x is the first element and y the rest of the list cons(x,y). Assume further that we have a procedure

in the sort program. Procedures (1) and (2) do not unify though their first arguments denote a list. But let us transform the term 'list' in (2) to a predicate and also use two auxiliary procedures

1. e. ·

and

then the situation is changed and yields after some computational steps the intended goal

The transformation of a term into a predicate extends the domain of the unification algorithm and gives the opportunity to use a uniform proce­ dure for terms and predicates to determine which

of them to evoke.

Goal Variations

In problem-solving problem variation some­ times leads to a successful solution (Polya [13]). We show two ways to vary a problem i.e., problem generalization and problem specialization. In both cases logical consequence plays an important role.

Problem generalization

Perhaps the simpliest example that shows both oroblem generalization and specialization is a fa­ ~ily example from Kowalski [9].

Suppose that we have the following goal

+ Male(x),Parent(x,y),Father(x)

and the procedure

then by logical consequence we have the new goal

+ Male(x),Parent(x,y).

The problem is generalized in the way that the connection graph for the new goal contains less details in form of predicate(s) and link(s), yet still gives the same ~elution.

Problem specialization

A reasoning by logical consequence can also give a specialized problem in the way that we put in more details in form of link(s) and predicate(s)

into the connection graph.

Suppose we have the goal

and the procedure

Father(x) + Male(x),Parent(x,y),

then by logical consequence we have the new goal

+ Male(x),Parent(x,y),Father(x).

The idea of logical consequence can also be used in a heuristic reasoning.

Suppose that we have a goal to show that x is a parallelogram

and a procedure defining a parallelogram

and two rectangle procedures

Let us assume that the goal we obtain by resolving (1) and (2) is very non-deterministic; then we could use the idea of logical consequence in a heuristic reasoning and make the following assump­ tion.

Suppose that Rectangle(x) is a logical consequence of Parallelogram(x), then we have the new speci­ alized goal,

which by resolution, (4) and (5), gives the goal

which is more deterministic and could give a faster solution. This computation is, however, based on a heuristic assumption that could be

false and thus could be a wasted computation.

Whether or not it is favourable to generalize or specialize a problem depends basically on how much each can decrease the non-determinism of a problem.

Interactive Computation Control

Interactive control of a computation helps a programmer debug a program, as well as improve a program, and can give the programmer hints that he can use to trim the search strategy.

Program debugging

A computation is a deduction (a unique pro­ perty of predicate logic among programming langu­ ages), which means that each step in the computa­ tion is a logical step. This gives us a powerful mean to discover bugs e.g., misspellings, missed termination conditions (recursion bases) and bad­ ly expressed ideas.

Program improvements

Assume that we have a data base holding

and that we want to search in the data base for a special key k

which a priori can be matched with all elements in the data base, then this program is reasonable for very few elements only. If a programmer is told when the number of possible matches is more than a given threshold then he could start thinking of some program improvements.

A simple refinement of the given program is t o substitute goal (2) by goal

+ A(k,l)

(3)

and add the procedure

which gives a deterministic sequential search pro­ gram.

Conclusions

Our experience in predicate logic programming has only been positive. A program becomes structu­ red and transparent. All variables of a procedure are local variables of that procedure so we do not get side effects from global variables. Each step in a computation is a logical step, which supports debugging. A proof of an algorithm on a theorem­ prover has a different behaviour from, for example a proof in group theory where a proof of depth 9 is a surprise, though a proof of depth 42 for an algorithm has been fnund in 75 seconds (Ta"rnlund [14]).

Acknowledgement~

The design of the interpreter is very much inspired by Robert Kowalski of Imperial College who visited University of Stockholm in December 74. James McSkimin of University of Maryland and Ake Hansson of University of Stockholm have given many valuable comments on drafts of this paper. David Luckham, Jorge ~orales and Joachim Schreiber of Stanford University made the appendix possible.

NFR (Naturvetenskapliga Forskningsradet) and ITM (Institutet for Tillampad Matematik) have part­ ly supported this work.