Particular case of mutually recursive function not working

[gabriel-barrett]

For some reason the following code does not work

(letrec ((odd?
          (letrec ((even? (lambda (n) (if (= n 0) 1 (odd? (- n 1))))))
            (lambda (n) (if (= n 0) 0 (even? (- n 1)))))))
  (odd? 3))

However, adding the letrec for even? inside the lambda works:

(letrec ((odd? (lambda (n)
                 (letrec ((even? (lambda (n) (if (= n 0) 1 (odd? (- n 1))))))
                   (if (= n 0) 0 (even? (- n 1)))))))
  (odd? 3))

[arthurpaulino]

Since this also happens on the Lean alternative implementation, we believe that this is a limitation of the expected behavior rather than a real bug. So we should address this issue later, with a more robust strategy to deal with a wider range of ways to express recursions.

For now, the rule of thumb is to define recursive calls as straightforward binds of symbols to lambdas in the letrec block.

[porcuquine]

Although I'm sure it's not exactly the same, something about this reminds me of #3 (lol, number three). The idea of an env becoming 'lost' may be conceptually useful as we work through this.

[porcuquine]

I think I know the issue. When we find a function in a recursive environment, then we extend its closure-environment at the time it is found. That is how we provide recursion currently.

What's happening in the bad example, is that the binding to odd? is an inner function. This does indeed get its environment extended as expected. However, this mechanism doesn't have any contract with the binding of even?. The associated function is not ever found as a 'recursive lookup', so there should be no expectation that its environment will be extended.

This is just an explanation which more clearly explains why the 'rule of thumb' @arthurpaulino describe is actually what should be expected based on an understanding of how Lurk's letrec does and is intended to function now.

[porcuquine]

In other words, the hypothesis that odd? should be available inside the definition of even is simply mistaken. You can reason through this by considering the bindings available lexically when even is defined. Clearly, odd? is not in scope — and the letrec only grants the extra, magical, scope to the function bound.

In fact, on consideration, this behavior is already documented in our tests. This test exists exactly to show the expected behavior (and happens to use the same examples…): https://github.com/lurk-lab/lurk-rs/blob/8fd97899fbf7776de650059d850d63ef7aacb1c5/src/proof/nova.rs#L1767-L1788

The only difference is that the example code uses the 'concise' form:

(letrec ((foo (lambda (…) …))
         (bar (lambda (…) …)))
   …)

whereas the example in this issue manually expands it (as evaluation itself does) to

(letrec ((foo (letrec ((bar (lambda (…))))
                (lambda (…) …)))
   …)

I think most of the confusion here comes because we're not used to reading code that avoids the concise form, so didn't recognize that this is a direct replication of the explanatory test case.

Another way to phrase the final response here is, "Yes, this issue demonstrates that Lurk's letrec still does not provide mutual recursion."

However, the more constructive observation is that there is indeed a clever way to obtain mutual recursion from the more limited self-recursion Lurk's letrec provides. This means we could actually implement mutual recursion as a macro (mutrec), as a 'built-in' macro (like the existing transformations, including the 'concise' form of letrec), or even perhaps as the new default expansion of letrec, replacing the current one and providing (it seems) strictly better behavior.

Interesting!

[porcuquine]

In other words, the interesting point about the original issue was not actually, "Mutual recursion is surprisingly broken in some case," which we always knew. But rather it is, "But Lurk is perfectly capable of expressing mutual recursion if we transform concise letrecs differently." Nice find, @gabriel-barrett.

[porcuquine]

Correcting myself slightly: It's not true that the first (bad) example is exactly the same as the test demonstrating the error. That would actually expand to

(letrec ((even (lambda (n)
                 (if (= 0 n)
                     t
                     (odd (- n 1))))))
  (letrec ((odd (lambda (n)
                  (even (- n 1)))))
    (odd 2)))

Nevertheless, the general point remains. There are many ways to misuse Lurk's focused self-recursion construct (letrec) in the hope of extracting mutual recursion. There is also a way (the second, 'good') example to accomplish that goal in a way that is simple and relatively efficient.

Since accomplishing this does require that all bindings be to lambda forms defining functions, I think maybe we should define mutrec as a construct which can only be used to do that. Then we can omit the lambda from the syntax.

An example like the original could then be written:

(mutrec ((even? (n) (if (= n 0) true (odd? (- n 1))))
         (odd? (n) (if (= n 0) false (even? (- n 1))))
  (odd? 3))

And it would then become

(letrec ((even? (lambda (n)
                  (letrec ((odd? (lambda (n)
                                   (if (= n 0) nil (even? (- n 1))))))
                    (if (= n 0) t (odd? (- n 1))))))
         (odd? (lambda (n)
                 (letrec ((even? (lambda (n)
                                   (if (= n 0) t (odd? (- n 1))))))
                   (if (= n 0) nil (even? (- n 1)))))))
  (odd? 3))

This example does highlight one annoying point about the idea. In order to make all of the bound functions available in the body, we would need to separately define each entry point. If it's okay to have only a single entry point, then that's not necessary.

However, I think we can probably come up with a way to build on this idea and also obtain all the bindings in one pass, probably by introducing new continuation types.

[porcuquine]

Alternately, maybe it will be better to pursue one of the other strategies. I think we can get the properties we want by making the recursive lookups smarter. This will still require some tweaks to the continuations, but basically, when searching a recursive env, we can hold on to the enclosing recursive env as we descend, then use that as the env with which to extend the closure.

In light of the above expansion, I now slightly lean toward that approach.

[porcuquine]

In that model (the one involving making recursive lookups smarter), we wouldn't even need a new construct. Then this

(lettrec ((even? (n) (if (= n 0) true (odd? (- n 1))))
         (odd? (n) (if (= n 0) false (even? (- n 1))))
  (odd? 3))

would 'just work'. The rule would be that all bindings within a single 'concise' letrec would have all other bindings available within the bodies of any functions directly defined as the value of those bindings. I think this is exactly what we want to express, and a change to the lookup and function-env-extension mechanism seems like the simplest and most direct way to effect it.