🚀 go-pugleaf

I've received a couple of messages expressing interest in my
toy unfold/folder, so here's a longer description.




Here's a description of my little program: please remember that
it is only a first attempt at applying the Unfold/Fold transformation 
automatically, and that as I note at the bottom of the article,
I think it can be improved considerably.

Even so, it is capable of performing the following Unfold/Fold transformations
on programs like (naive) reverse, the program "string" shown below,
and other "simple" recursive programs to yield their difference list 
counterparts.

string(n(X,Y),S) :- string(X,SX), string(Y,SY), append(SX,SY,S).
string(X,[X]) :- terminal(X).

terminal(a).   terminal(b).   terminal(c).

It consists of 3 major predicates. To make things simpler, I describe
each predicates' application to naive reverse as a running example:

Example Input program (as assertions in data base).

  reverse([],[]) <- [].
  reverse([E|Es],Rs) <- [ reverse(Es,Ms), append(Ms,[E],Rs) ].

1.  foldDefn(GoalToFold,FoldDef)

 This proposes a definition clause FoldDef for the folding process
 based on the clauses for GoalToFold.  FoldDef is currently computed
 by examining the recursive clauses for GoalToFold. 
 
foldDefn(reverse(_,_),FoldDef).
FoldDef = reverse_f(_2,_820,_8)<-[reverse(_2,_14),append(_14,_820,_8)] ;
FoldDef = reverse_f(_2,_0,_8)<-[reverse(_2,_14),append(_14,[_0],_8)] ;
FoldDef = reverse_f(_2,_0,_830,_8)<-[reverse(_2,_14),append(_14,[_0 | _830],_8)] ;

2.  unfoldFoldDefn(FoldDef,GoalToFold,Unfoldeds)
 
 This unfolds all instances of the GoalToFold in FoldDef to yield the
 unfolded clauses. It also performs some elementary simplifications on
 the result.
 
unfoldFoldDefn(reverse_f(_2,_820,_8)<-[reverse(_2,_14),append(_14,_820,_8)],
	reverse(_,_),Unfoldeds).

Unfoldeds = [ 
    reverse_f([],_4,_4)<-[],
    reverse_f([_62 | _64],_4,_6)<-
        [reverse(_64,_74),
         append(_74,[_62],_12),
         append(_12,_4,_6)]] ;

3.  fold(Unfolded,Folders,Folded)
 
 This folds the body of Unfolded by the bodies of Folders to yield Folded.
 Folders includes equivalences which may be useful in the folding process
 as well as FoldDef itself.
 
 In our example, note that there is nothing to fold in the first clause of
 Unfoldeds.  Note the equivalences involving append that are given to the
 folder: only the first of these is used here, the second is required when
 folding the unfolded body of the FoldDef for the "string" predicate defined
 above.
 
fold(reverse_f([_62 | _64],_4,_6)<- 
      [reverse(_64,_74),append(_74,[_62],_12),append(_12,_4,_6)], 
     [ [reverse_f(A1,B1,C1)]<-[reverse(A1,D1),append(D1,B1,C1)],
       [append(X,[A|V],W)] <- [ append(X,[A],Y), append(Y, V, W) ],
       [append(B,D,X),append(A,X,E)] <- [append(A,B,C),append(C,D,E)] ],
     Folded).

Folded = reverse_f([_0 | _2],_8,_10)<-[append(_28,_8,_10),reverse_f(_2,[_0],_28)] ;
Folded = reverse_f([_0 | _2],_8,_10)<-[reverse_f(_2,[_0 | _8],_10)] ;
Folded = reverse_f([_0 | _2],_8,_10)<-[append(_16,[_0 | _8],_10),reverse(_2,_16)] ;
Folded = reverse_f([_0 | _2],_8,_10)<-[reverse_f(_2,_254,_10),append([_0],_8,_254)] ;
Folded = reverse_f([_0 | _2],_8,_10)<-
	[append(_16,_254,_10),append([_0],_8,_254),reverse(_2,_16)] ;
Folded = reverse_f([_0 | _2],_8,_10)<-
	[append(_28,_8,_10),append(_16,[_0],_28),reverse(_2,_16)] ;

 The second of these answers is the preferred one, because it does not contain
 either the original program predicate we are trying to redefine, or the
 predicate "append".


The program might be improved in the following ways.  First, step 1,
ie. choosing a FoldDef, should incorporate the constraint that
the FoldDef actually be capable of computing the relation to be
folded!  This would rule out all but the first proposed FoldDef in step 1 
of the example above, and more importantly, may prove useful as a way of
generating possible FoldDefs.

Second, the unfolding step (step 2) could be modified so that it
doesn't just do a single unfold of the FoldDef head, but instead
unfolds all goals that contain a "recursive argument" of the FoldDef.
With this extension, the procedure may be able to Unfold/Fold programs
that are more complicated than the simple "one-level" recursive ones 
that it can deal with now.