bosatsu icon indicating copy to clipboard operation
bosatsu copied to clipboard

can we compute an upper bound on number of recursions?

Open johnynek opened this issue 4 years ago • 1 comments

Since bosatu is total, can we adapt the totality checking to compute a limit of the number of recursive calls made?

It seems like maybe yes, because we can look at the structure we are recursing on and see the depth of the tree. The depth is the recursion limit.

If we had this, we could potentially use it to compile to starlark or perhaps BPF both of which don't allow general recursion. We could also dynamically choose between stack-safe and non-stack-safe recursions based on the depth of the recursion (if there were cases that the non-stack-safe can be faster).

johnynek avatar Dec 03 '19 21:12 johnynek

you definitely can’t compute an upper bound statically since the number of steps depends on input. You could also always append a counter to any recursion and just return the total count. We could possibly also delete all the other logic.

But to be useful we need to be able to somehow avoid explicit recursion since the mentioned target languages don’t have recursion.

johnynek avatar Dec 23 '19 02:12 johnynek