-2

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,

kalaldi
  • 1
  • 3
    Why should tail recursion not be suitable for verification? – Frank Schmitt Jan 26 '14 at 07:07
  • 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

1 Answers1

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.

GS - Apologise to Monica
  • 28,466
  • 10
  • 89
  • 111