Unfold/fold Transformations Preserving Termination Properties

Abstract

The unfold/fold framework constitutes the spine of many program transformation strategies. However, by unrestricted use of folding the target program may terminate less often than the source program. Several authors have investigated the problem of setting up conditions which guarantee preservation of termination properties. These conditions are often formulated in a way which makes it hard to grasp the basic intuition why they work. The aim of this paper will be to give a more unified treatment by setting up a model which enables us to reason about termination preservation in a cleaner and more algebraic fashion. The model resembles a logic language and is parametrized with respect to evaluation order.