Transforming a function to use tail recursion - a formal study

Question

Has anyone written an official paper describing a method for (automatically) converting functions to tail recursion? I am looking for formal treatment at the university level, including restrictions (types of functions that can be transformed), conversion procedures and, if possible, proof of correctness? Examples in Haskell are bonuses.

Answer 1

method (automatically) convert functions to tail recursion?

So there are two parts:

• Recognizing that a given recursive function can be transformed into a tail recursive form and do this transformation
• efficient tail calls, so the conversion is worth it.

Convert recursion to tail recursion

Apparently relatively straightforward to syntactically recognize tail recursive definitions. In the end, "tail recursive" means that the call appears syntactically in the tail of the expression.

eg. Schema people describe:

just compile the appropriate self-language, since the transitions are not enough to achieve full tail recursion. Instead, we syntactically divide all subexpression positions in the source language into two classes: tail (or abbreviations) and subtasks. In a simple expression (if predicate consistent alternative), predicate is the position of the subtask, while both subsequent and alternative position reductions. This syntactic concept can easily be extended to arbitrarily nested subexpressions.

• Compiling higher order languages ​​into fully connected portable C

Convert functions to tail calls

The hard part of your question is optimization for identifying and transforming recursive computations of candidates into tail recursive ones.

The GHC uses one link, which uses a built-in and wide range of simplification rules to collapse recursive calls until their main recursive tail structure remains.

• Secrets of Inlineer GHC

Tail elimination

Once you have your functions in tail recursive form, you would like it to be implemented efficiently. If you can create a loop, this is a good start. If your target machine doesn’t do this, then tail tail removal will require a few tricks. To quote Odersky and Schinz below,

Over the years, various methods have been proposed to eliminate common (and not only recursive) tail calls, mainly for compilers targeting C.

... put the whole program in a large function and simulate function calls using direct jumps or switch statements inside that function.

... A popular method is to use a trampoline. Trampoline - external which repeatedly causes internal function. Each time an internal function wants the tail to call another function, it does not call it directly, but simply returns its identity (for example, as a closure) to the trampoline, which then performs calling itself. Thus, unlimited stack growth can be avoided, but some indicators are inevitably lost, mainly because all calls made by the trampoline are calls to statically unknown functions.

Another method is Henry Bakers "Cheney on M.T.A." With it, the program must first be converted to Continued Transfer (CPS), so the inclusion of all calls in tail calls, and then can be composed as usual. At run time, when the stack is about to overflow, the current continuation is built and returned (or longjmped) in the “Waiting” trampoline at the bottom of the call stack.

• Tail Exclusion in the Java Virtual Machine , Michelle Schinz Martin Odersky, 2001

• Henry G. Baker, Jr. CONS Should Not AGREE Its Arguments, Part II: Cheney's ATA Project, January 1994.

Answer 2

Mercury contains a couple of optimizations to automatically create a tail recursive. ( Mercury is a programming logic language of purity, so it talks about predicates, not functions, but many of the same ideas apply to a Mercury program with respect to Haskell. A much bigger difference than logic, not functionality, is that it strict, not lazy)

Introduction to Drive generates specialized predicate versions with an optional accumulator parameter to allow associative operations to be moved before a recursive call. Apparently, this optimization does not necessarily lead to tail recursive predicates per se, but often leads to a form that can be optimized using the second optimization:

The "last modulo call constructors" essentially allows a recursive call, followed only by constructor applications, which must be rewritten in such a way that a value containing a "hole" is created first, and then the recursive call returns its output directly to the memory address " hole "and not the use of a normal return agreement. I believe that Haskell will get this optimization for free just because of laziness, however.

Both of these optimizations are described in Recursive Implementation of Mercury Programs .