Etude on recursion elimination

N. V. Shilov

Modelirovanie i analiz informacionnyh sistem, Tome 25 (2018) no. 5, pp. 549-560

Résumé

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.

Détail

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.