Improving programs which recurse over multiple inductive structures
Leonidas Fegaras · 2018
This paper considers generic recursion schemes for programs which recurse over multiple inductive structures simultaneously, such as equality, zip and the nth element of a list function. Such schemes have been notably absent from previous work. This paper defines a uniform mechanism for defining such programs and shows that these programs satisfy generic theorems. These theorems are the basis for an automatic improvement algorithm. This algorithm is an improvement over the algorithm presented earlier [15] because, in addition to inducting over multiple structures, it can be incorporated into any algebraic language and is no longer restricted to a "safe" subset. 1 Introduction In previous work [15, 16] we have shown how programming algebraically with generic recursion schemes provides a theory amenable to program calculation [14]. This theory provides a basis for automatic optimization techniques which capture many well-known transformations. Unfortunately, these recursion schemes may ...