Resolution Step

To later understand the available optimizations, we must first understand how an interpreter frame is further structured into sub objects. Interpreter frames are required to represent a successful resolution step and they should also accommodate for the undoing and the continuation of a resolution step. Both capabilities are needed in the backtracking algorithm.

The resolution step is based on the following input:

A :- B1, .., Bn   The old answer term and old list

C :- D1, .., Dm   The picked clause

The answer term can be viewed as a list of the variables from the initial query. It is carried around so that we can display the answer substitution when the initial query has been successfully solved.

Now suppose that r is a substitution that will rename the variables of the picked clause by new fresh variables. Further suppose that q is the most general unifier of B1 and rC. Then the resolution step will yield the following new current answer term and current goal list:

qA :- qrD1, .., qrDm, qB2, .., qBn    The new answer term and goal list

The above can be efficiently implemented by means of skeleton and display pairs. Displays serve the purpose of providing fresh un-instantiated variables for a clause. They are thus capable of representing the substitution r. The variable place holders inside a display are then modified during unification. They are thus also capable of representing the most general unifier q. Therefore the dominant structure of a frame will be the display.

But with the display alone we could not implement backtracking, since it will not allow us the undoing and the continuation of a resolution step. For undoing the resolution step it is not enough to simply forget the current display, since unification might also have modified previously allocated displays. Therefore the unification will produce a trail which records the modified variable place holders and which can later be used to undo the unification.

Besides the trail we will also need a pointer into the input list of the clauses. The pointer will refer to the currently picked clause. This will allow us to continue our search with the next clause upon backtracking. Besides that a further continuation structure will be needed. Namely instead of building the new goal list by appending the old goal list and the picked clause body, we simply store the old goal list as a later continuation in the display. And the search continues immediately with the picked clause body.

In summary an interpreter frame is structured as follows. The fields stemming from the resolution step are marked by an asterisk (*). All other fields have been introduced to provide further functionality needed by the Jekejeke Prolog implementation:

Display Choice Point

It should be noted, that we divert from the architecture of the Warren Abstract Machine (WAM) in two respects. The first difference can be seen in the way goals of a clause are invoked.  In the WAM machine the skeleton display pointer pair approach is broken for goals. It is explicitly noted in [4] that goal invocations are dynamically created by assembling the arguments and then invoking the predicate. In our architecture we stick to the skeleton display pointer pair approach. Each goal in a clause is simply a different skeleton pointer which is completed by the display pointer of the clause instantiation.

Sticking to the skeleton display pointer pair approach for goals can be very efficient when there are efficient means to move from one skeleton pointer to the other. This is archived by turning each body of a clause into a goal list representation. But Prolog would not be complete if it would only be based on an efficient resolution step. What is typically also needed is a construct that allows the pruning of the search tree. The usual predicate for this is the cut and which will destroy any choice points up to its own frame.

The second difference is now found in the way how we deal with the cut. Jekejeke Prolog differs from other Prolog as far as we allow naked variables and cut transparent predicates. For this purpose the frame also contains a prune field, which points to the true frame that will belong to a cut. As a result we can invoke cuts inside meta-predicates with the desired result. Eventually this could also be realized inside a WAM, but the default mode of analysis and execution is that a cut is statically recognized inside a clause and that the cut will only prune its own frame and not an eventually inherited frame.

We have already explained most of the fields of the interpreter frame. The remaining “number”, “perms” and “clause” fields have various purposes. The “number” field is used by the body variable elimination optimization to notice whether the intermediate goals were deterministic, i.e. whether they have not created any new choice points. The “perms” field is used to determine whether the current execution belongs to the user or the system, and also to avoid double work in the stack frame elimination optimization. The “clause” field is simply used to provide source file and line number information in a stack trace.

Comments