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  -> ys x:xs' -> 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  -> b x:a' -> 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  -> app b c x:a' -> app (x:(app a' b)) c
Step 3. Unfold the outer app:
app3 a b c = case a of  -> app b c x:a' -> case x:(app a' b)  -> c x:d -> x:(app d c)
Step 4. Apply axiom to eliminate dead case alternative:
app3 a b c = case a of  -> app b c x:a' -> 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  -> app b c x:a' -> 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).