Geodesic
Etude on recursion elimination
Modelirovanie i analiz informacionnyh sistem, Tome 25 (2018) no. 5, pp. 549-560.

Voir la notice de l'article provenant de la source Math-Net.Ru

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 co-recursion 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 case-study 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.
Keywords: 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. 
@article{MAIS_2018_25_5_a7,
     author = {N. V. Shilov},
     title = {Etude on recursion elimination},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {549--560},
     publisher = {mathdoc},
     volume = {25},
     number = {5},
     year = {2018},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2018_25_5_a7/}
}
TY  - JOUR
AU  - N. V. Shilov
TI  - Etude on recursion elimination
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2018
SP  - 549
EP  - 560
VL  - 25
IS  - 5
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2018_25_5_a7/
LA  - en
ID  - MAIS_2018_25_5_a7
ER  - 
%0 Journal Article
%A N. V. Shilov
%T Etude on recursion elimination
%J Modelirovanie i analiz informacionnyh sistem
%D 2018
%P 549-560
%V 25
%N 5
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2018_25_5_a7/
%G en
%F MAIS_2018_25_5_a7
N. V. Shilov. Etude on recursion elimination. Modelirovanie i analiz informacionnyh sistem, Tome 25 (2018) no. 5, pp. 549-560. http://geodesic.mathdoc.fr/item/MAIS_2018_25_5_a7/

[1] P. J. Olver, Applications of Lie groups to differential equations, Springer-Verlag, New York, 1993 | MR | Zbl

[2] R. Bellman, “The theory of dynamic programming”, Bulletin of the American Mathematical Society, 60 (1954), 503–516 | DOI | MR

[3] G. Berry, “Bottom-up computation of recursive programs”, RAIRO — Informatique Théorique et Applications (Theoretical Informatics and Applications), 10:3 (1976), 47–82

[4] J. Cowles, “Knuth's generalization of McCarthy's 91 function”, Computer-Aided reasoning: ACL2 case studies, Kluwer Academic Publishers, 2000, 283–299 | DOI

[5] J. Cowles, R. Gamboa, Contributions to the Theory of Tail Recursive Functions, , 2004 (accessed September 26, 2018) http://www.cs.uwyo.edu/r̃uben/static/pdf/tailrec.pdf

[6] T. H. Cormen et al., Introduction to Algorithms, 3rd ed., The MIT Press, 2009 | MR

[7] O. De Moor, G. Sittampalam, “Generic Program Transformation”, Lecture Notes in Computer Science, 1608, 1999, 116–149 | DOI

[8] A. P. Ershov, “Mixed computation: potential applications and problems for study”, Theor. Comp. Sci., 18:1 (1982), 41–67 | DOI | MR | Zbl

[9] S. A. Greibach, Theory of Program Structures: Schemes, Semantics, Verification, Lecture Notes in Computer Science, 36, Springer, 1975 | DOI | MR | Zbl

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

[11] D. E. Knuth, Textbook Examples of Recursion, 1991, arXiv: (accessed September 26, 2018) cs/9301113 [cs.CC] | MR

[12] V. E. Kotov, V. K. Sabelfeld, Theoriya Schem Programm, Nauka, 1991 | MR

[13] Y. A. Liu, S. D. Stoller, “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 | DOI

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

[15] Z. Manna, A. Pnueli, “Formalization of Properties of Functional Programs”, Journal of the ACM, 17:3 (1970), 555–569 | DOI | MR | Zbl

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

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

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

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

[20] M. Wand, “Continuation-Based Program Transformation Strategies”, Journal of the ACM, 27:1 (1980), 164–180 | DOI | MR | Zbl

[21] McCarthy 91 function, (accessed September 26, 2018) https://en.wikipedia.org/wiki/McCarthy_91_function