🚀 go-pugleaf

Occasionally postings appearing in this newsgroup move to expel
difference-lists from the Herbrand Elysium.  It is not quite
clear what this means, but the allegation seems to be that they
do not qualify as terms, or are somehow second-class objects.
     Perhaps the reason for this discriminating attitude is that
on the surface they promise to represent lists, but when we start
unifying them, they are sometimes not faithful representatives.
Unification of two difference-lists should correspond to unification
of the lists they represent.  However, there are cases where this is
not so.  Here are two examples that illustrate the problems:

1) The difference-lists nil\nil and a.nil\a.nil are not unifiable.
   But the lists they represent, nil and nil, are unifiable.

2) The difference-lists a.X\Y and Z\Z are unifiable.
   But the lists they represent, a.X and nil, are not unifiable.

(Note that difficulties with difference-lists are often ascribed to
the occur check problem, but the examples show that they are
independent).
     In the light of the above, it is a bit of a miracle that the
"folk" transformation from programs using lists to programs using
difference-lists seems to work.  In fact, sometimes it doesn't.
Consider the program

   double(X,Y) :- append(X,X,Y).                              (*)

The transformation yields

   double(X,Y) :- double'(X\nil,Y\nil).
   double'(X\X',Y\Y') :- app(X\X',X\X',Y\Y').
   app(X\Y,Y\Z,X\Z).

Unfolding the calls to double' and app, we get the program

   double(nil,nil).

This program is rather different to (*).
     This does not mean that difference-lists are second-class
objects.  It just means that we must be careful using them in the
"folk" transformation.
     A discussion of the problems with using difference-lists
and how they can be avoided by dataflow analysis can be found in:

Marriott, K. & H. Sondergaard,
Prolog program transformation by introduction of difference-lists,
Proc. Int. Computer Science Conf. '88, Hong Kong (1988) to appear.
Preliminary version as TR 88/14, Dept. of Computer Science, Univ.
of Melbourne (1988).

--- Kim Marriott & Harald Sondergaard