# Preserving termination when rewriting recursive programs

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

-
I have an issue with your example. If you just use folds to define concat, then fusion (and, thus, inlining) is enough to get rid of the intermediate structure. Proof: app a b = (\ cons nil -> (a cons (b cons nil))) (concats 2 lists represented as their folds). app3 a b c = (app a (app b c)). Normalizing app3, we get: (a b c cons nil -> (a cons (b cons (c cons nil)))) which clearly makes no intermediate structure. – Viclib Oct 21 '15 at 14:15

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.

-
Backwards deduction is a great insight! It's a somewhat disappointing result though that you have to supply inductive proofs with the transformations, instead of doing something simple syntactic, but in retrospect it's obvious that that was a naive thing to hope for. I've accepted this answer as the answer to my question. – Jules Mar 6 '13 at 13:09
@Jules. Well, the transformation methods are still quite "syntactic". Inductive proof enters the picture in proving the soundness of the method. As far as the method is concerned, all that is needed is to make sure that the folding steps are applied to smaller arguments. That can again be done by "syntactic" means most of the time. – Uday Reddy Mar 6 '13 at 22:06

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.

-
Yes, however these program transformations rely on introducing recursion for them to do their job. In the meantime I have added an example of this at the end of the question. Note how a non-recursive function like app3 = app (app a b) c is turned into a recursive function. – Jules Feb 20 '13 at 15:22
Hmmm, interesting. A small correction: all function definitions in Haskell are recursive. So what you are doing is that a recursive definition which does not call itself is transformed into one that does. – Andrej Bauer Feb 20 '13 at 15:27
This gets more complicated. – Andrej Bauer Feb 20 '13 at 15:32
Yes, that's another way to view it. Operationally, I don't think it makes any difference whether a function that does not call itself is considered recursive or not (to my knowledge, marking a function as recursive or not is mainly a type system issue, and these kind of transformations work just as well on dynamically typed programs). – Jules Feb 20 '13 at 15:33
We need a theorem which tells us when two functions have the same least fixed point. I don't have time to do this right now, but if I think of anything, I will let you know. This looks like domain theory to me. – Andrej Bauer Feb 20 '13 at 15:45

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.

-
Thanks! Folding is only useful if it results in a cycle. I have added an example to illustrate this. Applying a generic termination checker is an interesting idea! However, program transformations like deforestation and supercompilation work without proving that the programs terminate. In fact they also work on non-terminating programs, they just don't introduce non-termination. Generic termination checking is a very hard problem, and I was hoping that there would be an easier and simpler method in this special case. – Jules Feb 20 '13 at 14:55
Thanks for the clarification. My knowledge about termination checking for functional languages is basically non-existing, but I assume that it is much easier to design heuristics that try to infer variant/ranking function candidates from a given program, because the variants can only depend on the function arguments and not on a shared heap. Dafny (research.microsoft.com/en-us/projects/dafny) has such heuristics, but I don't know how they work. Such heuristics could limit the use of folding to cases where a variant can be inferred and termination can be proved. – Malte Schwerhoff Feb 20 '13 at 15:09