Etude on Recursion Elimination

Transformation-based program verification was a very important topic in early years of theory of programming. Great computer scientists contributed to these studies: John McCarthy, Amir Pnueli, Donald Knuth ... Many fascinating examples were examined and resulted in recursion elimination techniques known as tail-recursion and co-recursion. In the paper, we examine just a single example (but new we hope) of recursion elimination via program manipulations and problem analysis. The recursion pattern of the example matches descending dynamic programming but is neither tail-recursion nor corecursion pattern. Also, the example may be considered from different perspectives: as a transformation of a descending dynamic programming to ascending one (with a fixed-size static memory), or as a proof of the functional equivalence between recursive and iterative programs (that can later serve as a casestudy for automatic theorem proving), or just as a fascinating algorithmic puzzle for fun and exercising in algorithm design, analysis, and verification. The article is published in the author’s wording.

recursive and standard program schemata, recursive and iterative programs, functional equivalence of programs and program schemata, ascending and descending dynamic programming, recursion elimination, static and dynamic memory, associative and standard arrays

1. Olver P. J., Applications of Lie groups to differential equations, Springer-Verlag, New York, 1993.

2. Bellman R., “The theory of dynamic programming”, Bulletin of the American Mathematical Society, 60 (1954), 503-516.

3. Berry G., “Bottom-up computation of recursive programs”, RAIRO — Informatique Theorique et Applications (Theoretical Informatics and Applications), 10:3 (1976), 47¬82.

4. Cowles J., Computer-Aided reasoning: ACL2 case studies, Kluwer Academic Publishers, 2000.

5. Cowles J., Gamboa R., “Contributions to the Theory of Tail Recursive Functions”, 2004, http://www.cs.uwyo.edu/~ruben/static/pdf/tailrec.pdf, accessed September 26, 2018.

6. Cormen T. H. et al., Introduction to Algorithms (3rd ed.), The MIT Press, 2009.

7. De Moor O., Sittampalam G., “Generic Program Transformation”, Lecture Notes in Computer Science, 1608, 1999, 116-149.

8. Ershov A.P., “Mixed computation: potential applications and problems for study”, Theor. Comp. Sci., 18:1 (1982), 41-67.

9. Greibach S. A., Theory of Program Structures: Schemes, Semantics, Verification, Lecture Notes in Computer Science, 36, Springer, 1975.

10. Jones N. D. et al., Partial Evaluation and Automatic Program Generation, Prentice Hall International, 1993.

11. KnuthD.E., Textbook Examples of Recursion, 1991, arXiv:cs/9301113[cs.CC], accessed September 26, 2018.

12. Kotov V. E., Sabelfeld V. K., Theoriya Schem Programm, Nauka, 1991.

13. Liu Y. A., Stoller S.D., “Program optimization using indexed and recursive data structures”, Proceedings of the 2002 ACM SIGPLAN workshop on Partial evaluation and semantics-based program, manipulation, 2002, 108-118.

14. Liu Y. A., Systematic Program Design: From Clarity to Efficiency, Cambridge University Press, 2013.

15. Manna Z., Pnueli A., “Formalization of Properties of Functional Programs”, Journal of the ACM, 17:3 (1970), 555-569.

16. Manna Z., McCarthy J., “Properties of programs and partial function logic”, Machine Intelligence, 5 (1970), 79-98.

17. Paterson M.S., Hewitt C.T., “Comperative Schematology”, Proc. of the ACM Conf. on Concurrent Systems and Parallel Computation, 1970, 119-127.

18. Shilov N.V., “Unifying Dynamic Programming Design Patterns”, Bulletin of the Novosibirsk Computing Center (Series: Computer Science), 34 (2012), 135-156.

19. Shilov N. V., “Algorithm Design Patterns: Program Theory Perspective”, Proc. of Fifth Int. Valentin Turchin Workshop on Metacomputation (META-2016), 2016, 170-181.

20. Wand M., “Continuation-Based Program Transformation Strategies”, Journal of the ACM, 27:1 (1980), 164-180.

21. “McCarthy 91 function”, https://en.wikipedia.org/wiki/McCarthy_91_function, accessed September 26, 2018.