Preserving termination when rewriting recursive programs

Question

Powerful program transformations like partial evaluation, deforestation and supercompilation are based on applying three kinds of transformations:

1. Rewrite using axioms, e.g. a+b = b+a.

2. Unfolding/inlining: replace a function call with the body of the function.

3. 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).

Answer 1

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.

Answer 2

If you are a bit more careful about definitions, and in particular recursive definitions, then such confusion cannot arise. In your example, we must first decide whether

f(x) = x + 1

is supposed to be a recursive definition or not. This cannot be discovered by looking for recursive calls in the body of the definition. Defining a function by recursion is a completely different thing than defining a function by abstraction. Most programming languages tend to bury the distinction and just assume that all function definitions are recursive. Some languages are more careful about this, for example OCaml, ML and Coq. If you do fancy stuff like program transformation then the difference matters. Anyhow:

1. If the above definition is not recursive, then it is really a shorthand for (I am switching to OCaml notation to make things a bit less ambiguous):

   let f = fun x => x + 1
   

   The suggested transformation of x + 1 into f(x) is illegal because f is not in the scope of the body of the function, so it cannot be mentioned.

2. If it is a recursive definition then the question is more interesting, but the transformation is still invalid. The recursive definition

   let rec f x = x + 1 
   

   is really an ordinary definition involving the fixpoint operator fix:

   let f = fix (fun g => fun x => x + 1)
   

   Now the suggested transformation is to replace x + 1 with g(x) (and not by f(x) because f again is not in the scope of the body of the function, but g is). But now we get stuck because we cannot prove that g(x) equals x + 1. After all, the only thing we know about g is that it is an argument in a function abstraction.

   We could transform x + 1 into fix (fun h => fun y => y + 1) x if we wanted to, but I cannot think of a good reason to do so.

You may be tempted to hate the fixpoint operator. But it is better to learn to live with it because it helps clarify confusing points about recursion.

Answer 3

You could maintain a static call graph and, for a given subexpression such as (x + 1), apply the third transformation only if it does not yield a cycle in the graph. Thus, if the original program had no infinite recursion, the transformed version shouldn't have one, either.

A next step could be to allow the introduction of new cycles if a static analyses (such as used by Terminator) guarantees that the newly added recursion eventually terminates.