transforming tail recursion into non tail recursion

Question

I would like to know if there is any method that converts tail-recursive function into a non tail recursive one. I know, tail recursive functions are better than no tail recursive functions if one's focus is on efficiency, but in verification tail-recursion is not suitable.

thanks,

do you mean to recover the original recursive function from a tail-recursive one transformed with the *accumulator argument*? i.e. get rid of this *accumulator argument*, is that what you're after??? — Will Ness, Jan 26 '14 at 18:58
translating a tail-recursive function into a non tail recursive one seems to be a good challenge for many reasons. for example, in reverse engineering, one could be interested in recovering the function in a more clear and suitable form; as you know no tail recursive functions are more easy to understand than their tail recursive form. — kalaldi, Jan 26 '14 at 19:46
Also, if you want to prove by induction this property, for example: factorial(n)=factorialTerminale(n, 0) using any theorem prover, you will not succeed because of the initial value 0. this is why I said tail recursive functions are not suitable for verification. I am not interested in program efficiency at all. — kalaldi, Jan 26 '14 at 19:47
translation from tail recursion to recursion is a no-op. tail recursion is already a recursion. end of story. as for ease of understanding, YMMV. So can mine. :) So unless you give us examples, full code and all, your answer is unclear. — Will Ness, Jan 26 '14 at 19:49
suppose you translate a function f into its tail recursive form, how can guarantee that your mechanized transformation is correct? — kalaldi, Jan 26 '14 at 19:59
recursion first analyzes its argument while building a stack going towards the base case, then the actual calculation of the result is performed by the stack unwinding. explicate this unwinding of the stack, abstracting away the initial argument, the starting point of the analysis, which becomes the end point of the synthesis (or "accumulation"), whose start point is the recursion's base case. cf. [this](http://stackoverflow.com/a/19951540/849891). How to formalize this I have no idea. — Will Ness, Jan 27 '14 at 09:01
but if you have a mechanized transformation procedure already you should use it only if it is proven to be correct. Do ask a concrete question please. Also, check out other sites in SE network, e.g. http://cs.stackexchange.com/tour where a more theoretical questions might be more appropriate. :) — Will Ness, Jan 27 '14 at 17:42

score 0 · Answer 1 · answered Jan 26 '14 at 10:56

0

I doubt this question is well posed, because tail recursion elimination is an optimisation that you could simply ignore or turn off for the purposes of verification if you need to. (I guess that replacing a call with a jump might confuse it or damage certain security properties.)

However, if you do really want to do this, you need to change your source code so that the recursive function call is no longer in tail position. The tricky part will be making sure that the optimiser does not change your code back again.

Consider this F# tail-recursive factorial function:

let rec fact n v =
    if n <= 1
        then v
        else fact (n-1) (n*v)

Now, let's add a function that does nothing at all unless you set some global variable to true:

// we'll never set this to true, but the compiler doesn't know this
let mutable actuallyDoSomething = false
let doNothing() =
    if actuallyDoSomething then failwith "Don't set actuallyDoSomething!"

Now we can change the tail call in fact:

let rec fact n v =
    if n <= 1
        then v
        else
            let res = fact (n-1) (n*v)
            doNothing()
            res

Similar tricks should work in other languages.

answered Jan 26 '14 at 10:56

Ganesh Sittampalam

28,821
4
79
98

I am not interested in program optimization. Tail recursive programs are sometime difficult to understand, and in reverse engineering, for example, I have to be able to recover the initial non tail recursive program in a more suitable form. – kalaldi Jan 26 '14 at 19:54
1

Some algorithms are naturally tail recursive, so tail recursive version might be the simplest form as well. – Ganesh Sittampalam Jan 26 '14 at 20:18
we have to be able to do this transformation whatever the reason. – kalaldi Jan 27 '14 at 06:28
My answer will apply in all circumstances. – Ganesh Sittampalam Jan 27 '14 at 06:29
ok, suppose you did the reverse direction, translate a non tail recursive function f to a tail recursive function g. how can you prove that g is correct? – kalaldi Jan 27 '14 at 08:21
That's a very general question. It would at least depend on how you knew `f` was correct in the first place and what your transformation was. – Ganesh Sittampalam Jan 27 '14 at 08:46

transforming tail recursion into non tail recursion

1 Answers1