maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2018-5-549-560mais-756Research ArticleОригинальные статьиArticlesЭтюд об устранении рекурсииEtude on Recursion Eliminationhttps://orcid.org/0000-0001-7515-9647ШиловНиколай ВячеславовичShilovNikolay

канд. физ.-мат. наук, доцент.

ул. Университетская, 1, г. Иннополис, Республика Татарстан, 420500.

PhD.

Universitetskaya str., Innopolis, Tatarstan Republic, 420500.

shiloviis@mail.ruАвтономная некоммерческая организация высшего образования “Университет Иннополис”.РоссияAutonomous noncommercial organization of higher education "Innopolis University".Russian Federation201828102018255549560Copyright © Шилов Н.В., 20182018Шилов Н.В.Shilov N.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/756

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

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 schematarecursive and iterative programsfunctional equivalence of programs and program schemataascending and descending dynamic programmingrecursion eliminationstatic and dynamic memoryassociative and standard arraysReferencesOlver P. J., Applications of Lie groups to differential equations, Springer-Verlag, New York, 1993.Olver P. J., Applications of Lie groups to differential equations, Springer-Verlag, New York, 1993.Bellman R., “The theory of dynamic programming”, Bulletin of the American Mathematical Society, 60 (1954), 503-516.Bellman R., “The theory of dynamic programming”, Bulletin of the American Mathematical Society, 60 (1954), 503-516.Berry G., “Bottom-up computation of recursive programs”, RAIRO — Informatique Theorique et Applications (Theoretical Informatics and Applications), 10:3 (1976), 47¬82.Berry G., “Bottom-up computation of recursive programs”, RAIRO — Informatique Theorique et Applications (Theoretical Informatics and Applications), 10:3 (1976), 47¬82.Cowles J., Computer-Aided reasoning: ACL2 case studies, Kluwer Academic Publishers, 2000.Cowles J., Computer-Aided reasoning: ACL2 case studies, Kluwer Academic Publishers, 2000.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.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.Cormen T. H. et al., Introduction to Algorithms (3rd ed.), The MIT Press, 2009.Cormen T. H. et al., Introduction to Algorithms (3rd ed.), The MIT Press, 2009.De Moor O., Sittampalam G., “Generic Program Transformation”, Lecture Notes in Computer Science, 1608, 1999, 116-149.De Moor O., Sittampalam G., “Generic Program Transformation”, Lecture Notes in Computer Science, 1608, 1999, 116-149.Ershov A.P., “Mixed computation: potential applications and problems for study”, Theor. Comp. Sci., 18:1 (1982), 41-67.Ershov A.P., “Mixed computation: potential applications and problems for study”, Theor. Comp. Sci., 18:1 (1982), 41-67.Greibach S. A., Theory of Program Structures: Schemes, Semantics, Verification, Lecture Notes in Computer Science, 36, Springer, 1975.Greibach S. A., Theory of Program Structures: Schemes, Semantics, Verification, Lecture Notes in Computer Science, 36, Springer, 1975.Jones N. D. et al., Partial Evaluation and Automatic Program Generation, Prentice Hall International, 1993.Jones N. D. et al., Partial Evaluation and Automatic Program Generation, Prentice Hall International, 1993.KnuthD.E., Textbook Examples of Recursion, 1991, arXiv:cs/9301113[cs.CC], accessed September 26, 2018.KnuthD.E., Textbook Examples of Recursion, 1991, arXiv:cs/9301113[cs.CC], accessed September 26, 2018.Kotov V. E., Sabelfeld V. K., Theoriya Schem Programm, Nauka, 1991.Kotov V. E., Sabelfeld V. K., Theoriya Schem Programm, Nauka, 1991.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.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.Liu Y. A., Systematic Program Design: From Clarity to Efficiency, Cambridge University Press, 2013.Liu Y. A., Systematic Program Design: From Clarity to Efficiency, Cambridge University Press, 2013.Manna Z., Pnueli A., “Formalization of Properties of Functional Programs”, Journal of the ACM, 17:3 (1970), 555-569.Manna Z., Pnueli A., “Formalization of Properties of Functional Programs”, Journal of the ACM, 17:3 (1970), 555-569.Manna Z., McCarthy J., “Properties of programs and partial function logic”, Machine Intelligence, 5 (1970), 79-98.Manna Z., McCarthy J., “Properties of programs and partial function logic”, Machine Intelligence, 5 (1970), 79-98.Paterson M.S., Hewitt C.T., “Comperative Schematology”, Proc. of the ACM Conf. on Concurrent Systems and Parallel Computation, 1970, 119-127.Paterson M.S., Hewitt C.T., “Comperative Schematology”, Proc. of the ACM Conf. on Concurrent Systems and Parallel Computation, 1970, 119-127.Shilov N.V., “Unifying Dynamic Programming Design Patterns”, Bulletin of the Novosibirsk Computing Center (Series: Computer Science), 34 (2012), 135-156.Shilov N.V., “Unifying Dynamic Programming Design Patterns”, Bulletin of the Novosibirsk Computing Center (Series: Computer Science), 34 (2012), 135-156.Shilov N. V., “Algorithm Design Patterns: Program Theory Perspective”, Proc. of Fifth Int. Valentin Turchin Workshop on Metacomputation (META-2016), 2016, 170-181.Shilov N. V., “Algorithm Design Patterns: Program Theory Perspective”, Proc. of Fifth Int. Valentin Turchin Workshop on Metacomputation (META-2016), 2016, 170-181.Wand M., “Continuation-Based Program Transformation Strategies”, Journal of the ACM, 27:1 (1980), 164-180.Wand M., “Continuation-Based Program Transformation Strategies”, Journal of the ACM, 27:1 (1980), 164-180.“McCarthy 91 function”, https://en.wikipedia.org/wiki/McCarthy_91_function, accessed September 26, 2018.“McCarthy 91 function”, https://en.wikipedia.org/wiki/McCarthy_91_function, accessed September 26, 2018.

The authors declare that there are no conflicts of interest present.