diff --git a/docs/rfc/002-bounded-recursion.md b/docs/rfc/002-bounded-recursion.md index 01aadcb208..7a7d9c7c7f 100644 --- a/docs/rfc/002-bounded-recursion.md +++ b/docs/rfc/002-bounded-recursion.md @@ -8,7 +8,7 @@ The Aleo Team. FINAL -# Summary +## Summary This proposal provides support for recursion in Leo, via a user-configurable limit to the allowed depth of the recursion. @@ -26,7 +26,7 @@ User-configurable limits may be also appropriate for other compiler transformations that are known to terminate but could result in a very large number of R1CS constraints. -# Motivation +## Motivation Leo currently allows functions to call other functions, but recursion is disallowed: @@ -34,9 +34,9 @@ a function cannot call itself, directly or indirectly. However, recursion is a natural programming idiom in some cases, compared to iteration (i.e. loops). -# Background +## Background -## Function Inlining +### Function Inlining Since R1CS are flat collections of constraints, compiling Leo to R1CS involves _flattening_ the Leo code: @@ -71,7 +71,7 @@ function main(a: u32) -> u32 { } ``` -## Constants and Variables +### Constants and Variables A Leo program has two kinds of inputs: constants and variables; both come from input files (which represent blockchain records). @@ -125,7 +125,7 @@ it is the case that, due to the aforementioned partial evaluation, the `const` arguments of function calls have known values when the flattening transformations are carried out. -# Design +## Design After exemplifying how inlining of recursive functions may terminate or not, we discuss our approach to avoid non-termination. @@ -133,7 +133,7 @@ Then we discuss future optimizations, and how the approach to avoid non-termination of recursion may be used for other features of the Leo language. -## Inlining Recursive Functions +### Inlining Recursive Functions In the presence of recursion, attempting to exhaustively inline function calls does not terminate in general. @@ -340,7 +340,7 @@ function main() { ... ``` -## Configurable Limit +### Configurable Limit Our proposed approach to avoid non-termination when inlining recursive functions is to @@ -388,7 +388,7 @@ as discussed later. In Aleo Studio, this compiler option is presumably specified via GUI preferences and build configurations. -## Circularity Detection +### Circularity Detection Besides the depth of the inlining call stack, the compiler could also keep track of @@ -401,7 +401,7 @@ and the compiler can show to the user the trace of circular calls. This approach would readily reject the `forever` example given earlier. -## Termination Analysis +### Termination Analysis In general, a recursive function (a generic kind of function, not necessarily a Leo function) @@ -460,7 +460,7 @@ If the recognition fails, the compiler falls back to inlining until either inlining terminates or the limit is reached. -## Application to Loops +### Application to Loops Loops are conceptually not different from recursion. Loops and recursion are two ways to repeat computations, @@ -483,7 +483,7 @@ which in particular would readily recognize the currently allowed loop forms to terminate. All of this should be the topic of a separate RFC. -## Application to Potentially Slow Transformations +### Application to Potentially Slow Transformations Some flattening transformations in the Leo compiler are known to terminate, but they may take an excessively long time to do so. @@ -496,18 +496,18 @@ not only for flattening transformations that may not otherwise terminate, but also for ones that may take a long time to do so. This is a broader topic that should be discussed in a separate RFC. -# Drawbacks +## Drawbacks This proposal does not appear to bring any real drawbacks, other than making the compiler inevitably more complex. But the benefits to support recursion justifies the extra complexity. -# Effect on Ecosystem +## Effect on Ecosystem This proposal does not appear to have any direct effects on the ecosystem. It simply enables certain Leo programs to be written in a more natural style. -# Alternatives +## Alternatives An alternative approach, hinted at in the above discussion about loops, is to take a similar approach to the current one for loops.