How is Nat.below and Nat.brecOn compiled

Stream: lean4

[Joachim Breitner]

When I elaborate a function using structural recursion, like in

def foo : Nat → Bool
 | 0 => true
 | n+1 => foo n

#print foo

I see it’s using Nat.brecOn to compile it:

def foo : Nat → Bool :=
fun x =>
  Nat.brecOn x fun x f =>
    (match (motive := (x : Nat) → Nat.below x → Bool) x with
      | 0 => fun x => true
      | Nat.succ n => fun x => x.fst.fst)
      f

The argument of Nat.brecOn here is (n : Nat) → Nat.below n → Bool, and @Nat.below motive n is a dependent vector of size n, (inductively defined and isomorphic to (i : Fin n) → motive i).

This looks like it would perform memoization, if the Nat.below n argument contains all the various for i < n, but it doesn't seem to be compiled that way.

So I wonder: How does the compiler turn the x.fst.fst into a normal recursive function calls? And why go through this detour in the first place?

(RTFM with pointers are welcome too :-))

[Joachim Breitner]

I may be able to answer the “why”: This way function definitions that are not just primitively recursive can be expressed using this kind of structural recursion, e.g. the typical fib function

def fib : Nat → Bool
 | 0 => true
 | 1 => true
 | n+2 => fib n && fib (n + 1)

#print fib

doesn't need to resort to well-founded recursion.

[Joachim Breitner]

Ok, and the answer of “how is it compiled” might simply be “not at all”. If I manually write a function using Nat.brecOn in a way that I might try to tease the code generator with, like

def sum_below : (n : Nat) → @Nat.below (fun _ => Nat) n → Nat
  | 0, .unit => 0
  | n+1, ⟨⟨i, b⟩, .unit⟩ => i + sum_below n b

def foo (n : Nat) : Nat :=
  Nat.brecOn (motive := fun _ => Nat) 0 sum_below

which would look at _all_ the previous values in the Nat.below, it says

code generator does not support recursor 'Nat.brecOn' yet, consider using 'match ... with' and/or structural recursion

So I conclude that the input to the code generator is _not_ the form I see with #print, with recursion replaced with Nat.brecOn, but some earlier, not-yet-elaborated-to-recursers-form of the function definition? Is that correct?

[Sebastian Ullrich]

Yes, that is exactly right. And the potentially unexpected memoization from brecOn that would otherwise happen is one of the and perhaps the main reason for that.

[Joachim Breitner]

Thanks! What is the “earlier, not-yet-elaborated” form that is then compiled?

[Sebastian Ullrich]

Just a direct recursive call, which the compiler understands in contrast to the kernel

[Joachim Breitner]

Browsing the code a bit it seems that “earlier” state, where recursion is still explicit, is a PreDefinition and addPreDefinitions in src/Lean/Elab/PreDefinition/Main.lean tries various strategies to turn this into a Declaration with recursers which can be added to the environment.

For example in def structuralRecursion then it produces a preDefNonRec which is added to the kernel’s environment with addNonRec, and it also produces a let preDef ← eraseRecAppSyntax preDefs[0]! with arbitrary recursion, which is compiled using addAndCompilePartialRec #[preDef].
Oddly, addAndCompilePartialRec via addAndCompileUnsafe calls eraseRecAppSyntax, but why not, doppelt hält besser.
addAndCompileUnsafe creates a Declaration.mutualDefnDecl, which I understand can be compiled. I am a bit surprised that this declaration (which the kernel can’t handle, can it) is still passed to addDecl decl…

Ok, that goes into C++ land, and there it checks that mutual definitions are always partial or unsafe… makes sense.
But why is there no name clash now between the recurser-based non-recursive definition, and the mutually recursive one, when both are added to the environment? Does one of them get a mangled name?

[Sebastian Ullrich]

I believe mutualDefnDecl is used basically by the compiler only, so there is no interaction or clash with defnDecls