3 ms·
Well, if the compiler will also report error for recursive calls not in tail position... There are strategies to prove various things about recursive calls. Se
by pmahoney 12y ago
Well, if the compiler will also report error for recursive calls not in tail position...
There are strategies to prove various things about recursive calls. See Ada/Spark's explanation for Rule 17.2 in [1].
I'm not familiar with Coq and Agda, but I believe they allow recursive calls if they can prove termination, though "termination" may be different than "using too much stack".
[1] http://www.spark-2014.org/entries/detail/misra-c-2012-vs-spark-2014-the-subset-matching-game http://www.spark-2014.org/entries/detail/misra-c-2012-vs-spa...
- Tyr42 12y agoAs a rule of thumb, they permit recursion where one parameter "obviously" is getting smaller each time, with a base case at 0 or the empty list or whatever. You can annotate the program in ways to make the compiler see that a parameter is actually getting smaller.