Embedding: a unifying concept for recursive program design

The concept of embedding one function into another is used to get a unified view of some well-known design techniques, such as loop derivation using inveriants, recursion removal, or folding-unfolding. A design method for recursive functions based on embedding is presented and its relation to those techniques stated. Efficiency transformations are also formalized using embedding. A few examples will clarify and complement the proposed technique