Preserving termination when rewriting recursive programs Powerful program transformations like partial evaluation, deforestation and supercompilation are based on applying three kinds of transformations:


Rewrite using axioms, e.g. a+b = b+a.
Unfolding/inlining: replace a function call with the body of the function.
Folding/un-inlining: replace a subexpression that matches the body of a function with a call to the function.


Each of these transformations will not change the result of a computation if it still terminates, but rule #3 may introduce non-termination. Here is a simple example of this. We have this program:

f(x) = x+1


We apply transformation #3 to the expression (x+1) and replace it with an equivalent function call:

f(x) = f(x)


Now the program doesn't terminate any more (infinite recursion). Rule #3 is however essential for powerful program transformations (see example below).

Transformations like deforestation and supercompilation ensure that termination behavior is not changed as a side effect of how these algorithms work. However, whether or not a sequence of transformations preserves the termination behavior is a property of the sequence itself, independent of any algorithm that generated it. My question is: how can we limit the application of the rules in such a way that a terminating program is never turned into a non-terminating program, but is still sufficiently general to allow useful program transformations, like deforestation and supercompilation (and hopefully, more)?

Algorithms like deforestation and supercompilation intertwine in their execution the search for good program transformations with ensuring that they preserve termination. I'm looking for a way to separate that into two problems: (1) characterizing a class of transformations that preserve termination (2) the search for good transformations in that class.



Here is an example. Suppose we have an append function in a language like Haskell:

app xs ys = case xs of
            [] -&gt; ys
            x:xs' -&gt; x:(app xs' ys)


And we have a function that appends three lists:

app3 a b c = app (app a b) c


The problem with this is that the outer app copies the (app a b), so the newly constructed list immediately becomes garbage. We can avoid this with a transformation:

Step 1. Unfold the inner app:

 app3 a b c = app (case a of 
                  [] -&gt; b
                  x:a' -&gt; x:(app a' b)) c


Step 2. Apply an axiom that distributes a function over a case expression:

app3 a b c = case a of 
             [] -&gt; app b c
             x:a' -&gt; app (x:(app a' b)) c


Step 3. Unfold the outer app:

app3 a b c = case a of 
             [] -&gt; app b c
             x:a' -&gt; case x:(app a' b)
                     [] -&gt; c
                     x:d -&gt; x:(app d c)


Step 4. Apply axiom to eliminate dead case alternative:

app3 a b c = case a of 
             [] -&gt; app b c
             x:a' -&gt; x:(app (app a' b) c)


Note that this is the step where the needless allocation is eliminated! We eliminate the pair x:(app a' b), because it then is immediately destructured again.

Step 5. Fold the expression app (app a' b) c:

app3 a b c = case a of 
             [] -&gt; app b c
             x:a' -&gt; x:(app3 a' b c)


This function is equivalent to the original one, but more efficient because it does not construct an intermediate list. Note that the after step 4, only a single node allocation is eliminated. By folding in step 5, we generalize that to eliminating the allocation of the entire list (supercompilation can do this transformation automatically).
The standard presentation of program transformation ideas is unsound, quite unfortunately.  They usually think of program transformation as forward deduction.  Using equational reasoning, you can deduce new facts from the old program, and lo and behold, it gives a better program!  While the new facts are quite clearly facts, nothing guarantees that they constitute a program.  The problem you have spotted is this naive presentation of the program transformation ideas.

However, it is possible to think of very much the same process as a backward deduction.  We think of the old program as a specification, and derive a new program that satisfies the specification.  Since equational reasoning is often bidirectional, you would see very similar steps in deriving the new program.  However, the meaning of these steps is opposite to what the naive methods imply.  When you use this "correct" method, you reason about termination while introducing recursion, and always derive a correct program.

For a paper describing the technique, see Deductive and inductive synthesis of equational programs (PDF).  This was done for first-order "equational" programs, but very similar ideas should be applicable to terminating functional programs.  If you are interested in non-terminating programs, I think you could use coinduction techniques (an off-the-cuff intuition).  However, my efforts to apply domain theory techniques to do these kinds of transformations did not bear fruit.  It might still be possible, but I haven't seen anything written on it.