For an illustration of the difference between building structure in the clause head and building structure in the clause body, we construct an AND/OR proof tree for the goal triple([1,2],Y) using the code described previously for the building structure in the clause head case in figure 6.1 and, in figure 6.2, an AND/OR proof tree for the goal triple([1,2],[],Y) for the case of building structure in the clause body.
The method used to rename the variables is to use an superscript to indicate different instances of a variable.
There is a slight cheat because the different instances of Y have not been distinguished. Really, there should be a succession of instances --- Y, Y
and so on. They are, however, all established as equivalent (via unification).
You will notice that they are extremely similar in shape.
The difference lies in the order of the construction of the variable bindings.
Note that, in figure 6.1, the binding for Y
is achieved after computing T2
and the binding for
T2
is achieved after computing T2
which is done through the clause
triple([],[]).
In the other case, in figure 6.2,
the binding for Y is achieved through the clause triple([],L,L).
The main point is that one computation leaves incomplete structure around (which is eventually completed) while the other does not do so.
Figure 6.1: The Proof Tree for triple([1,2],Y)
Figure 6.2: The Proof Tree for triple([1,2],[],Y)