Archive Notes

3. Loops and Constructing SLD-Resolution Trees

3 min read

Non-termination in Prolog

Since Prolog searches the tree using clauses in the order which they are written (in a depth-first matter), we must put base cases before recursive ones.

append([X | L], Y, [X | Z]) :- append(L, Y, Z).
append([], L, L).

This program produces no solutions and will result in an error because Prolog will attempt to construct an infinite branch by using the recursive step in each resolution step.

Variable renaming in Prolog

Consider the following fragment of program and goal:

% in the program
myappend([X | Y], Z, [X | W]) :- myappend(Y, Z, W).
 
% in the query
:- myappend(Y, [2], W).

In order to resolve the literal in the goal clause with the head of the program clause, we first need to solve the unification problem:

Formally [X | Y] is a shorthand for the expression '[|]'(X,Y) whose functor is '[|]'. According to rule (6) of the unification algorithm, cannot be solved because Y occurs in [X | Y]. (same for W and [X | W])

Constructing SLD-Resolution trees

Recall that:

  • each node in the tree represents the goal being operated on, may contain several literals
  • the selection function will pick the next one to resolve (always left-most in Prolog)
  • when resolving the selected literal with a clause in the program, Prolog will use order of appearance of these clauses (top-to-bottom)
  • each node has as many children as there are clauses in the program that can be unfiied with the literal selected in the goal; failed unifications are not depicted
  • order of resolution with program clauses is depicted left-to-right
  • “left-most child corresponds to result of the resolution of the selected literal in the goal with the first clause in the program whose head can be unified with the literal”
  • each child is connected to its parent with an arrow from the parent to the child whose label corresponds to the mgu used in the unification
  • if no clauses in the program can be unified with the literal selected in the goal, the current branch fails has no children; indicated with failure
  • if a goal node is empty, then it is represented by and ends a success branch
  • some goals do not need program clauses to be resolved; built-in predicates

Example SLD-resolution trees in Prolog

Graph View