Этюд об устранении рекурсии

Трансформационный подход к верификации программ был очень популярной темой исследований в первые десятилетия теории программирования. Многие выдающиеся пионеры теории программирования внесли свой вклад в разработку данного направления исследований: Джон Маккарти, Амир Пнуели, Дональд Кнут ... Много интересных примеров трансформационного подхода было тщательно изучено, что привело к методам устранения рекурсии, известным как хвостовая рекурсия и как ко-рекурсия. В данной работе мы подробно исследуем (мы надеемся, новый) пример устранения рекурсии, основанный на трансформациях программы и анализе задачи, решаемой этой программой. Наш пример является частным случаем нисходящего динамического программирования, но не является ни примером хвостовой рекурсии, ни кo-рекурсии. Этот пример можно рассмотреть с разных точек зрения: как пример преобразования нисходящего динамического программирования к восходящему (с использованием только статической памяти фиксированного размера), или как доказательство функциональной эквивалентности между рекурсивной и итеративной программами (которое в дальнейшем может послужить примером для автоматического доказательства), или как захватывающую алгоритмическую головоломку либо задачу дизайна, анализа и верификации алгоритмов. Статья публикуется в авторской редакции.

рекурсивные и стандартные схемы программ, рекурсивные и итеративные программы, функциональная эквивалентность программ и схем программ, восходящее и нисходящее динамическое программирование, устранение рекурсии, ассоциативные и стандартные массивы, статическая и динамическая память

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.