🚀 go-pugleaf

In article <3005@mulga.oz> harald@mulga.oz (Harald Sondergaard) writes:
>     There seem to be two approaches to transformation using
>difference-lists, "folk" and "unfold" (no, no misprints there :-).
>The former is exemplified in Sterling and Shapiro's book, the latter
>in a recent ECAI paper by Zhang and Grant.
>     The example transformation suggested by Richard seems to be of
>the "unfold" school.

I have not seen the paper by Zhang and Grant, but I am also of the
"unfold" school (I have tried to convert Kim and Harald without
success, so far at least :-).  Fold/unfold transformations are fairly
well understood and provide a good theoretical framework.  I think it
can be automated quite easily also, as long as the "eureka" steps are
known.  For the list-> difference list/pair transformation, the first
trick (at least to my mind), is to spot occurrences of
	.... p(...X...), append(X, Y, Z)....
where X doesn't appear anywhere else and "fold" this into
	....p'(...Y, Z...)....

The definition of p' can be obtained from the definitions of p and
append.  Often this definition can be simplified, using the
transitivity of append (another "eureka"), then folded to get a
recursive p' predicate which uses difference pairs rather than simple
lists.

This last step is the problem as far as preserving semantics is
concerned.  The two versions have the same least model but in the
transformed version generally makes p' true in more models of (the
completion of) the program.  It is a more complex version of
replacing p:-fail by p:-p.  This causes infinite loops.  Goals which
where false in all models in the original version (and hence finitely
failed if the computation rule was fair) are true in some but not all
models in the transformed version (so they loop).

Here is what we get with reverse:

% original, after simplifying append(E, [A], F), append(F, C, D)
reverse'([], A, A).
reverse'(A.B, C, D) :- reverse(B, E), append(E, A.C, D).

% folded version
reverse'([], A, A).
reverse'(A.B, C, D) :- reverse'(B, A.C, D).

The first version finitely fails with the goal reverse'(X, [a], [b]),
assuming a fair computation rule.  The second version loops with the
same goal.  The reason is that there is a (non-Herbrand) model in
which an instance of the goal is true.  This also explains why O(N)
reverse causes loops when run backwards.

I (with Kim and Harald) looked for a transformation which preserves
all models without much luck.  If you use the trick of keeping the
"length" of the difference list around it works for some cases (for
reverse you get something like the version which calls same_length and
can run backwards).  For tree traversals, the benefit of difference
lists was lost however (the algorithm was O(N^2) due to manipulation
of lengths).   I tried using integers and "successor" notation and
neither seemed to work.  Any ideas, anyone?  Also if anyone would like
to verify my claim that the d-list "fold" style transformation can be
automated, I would encourage it (are you listening Richard? :-).

	lee