Inspect Tail Recursion

Stream: lean4

[Scott Viteri]

Is there a quick way to check if Lean has recognized that a function is tail recursive? (Besides running it on large examples and trying to crash Lean)

[Mario Carneiro]

I did this:

set_option trace.compiler.ir.result true

def tail_recursive : Nat → Nat
  | 0 => 0
  | (n+1) => tail_recursive n

def not_tail_recursive : Nat → Nat
  | 0 => 0
  | (n+1) => not_tail_recursive n + 1

The trace.compiler.ir.result printout is pretty close to the lowest level that is still lean IR, but it's still fairly functional so the tail recursion is not explicit. But if you compile to C using

lean --c="test.c" test.lean

lean_object* l_tail__recursive(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3;
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_nat_dec_eq(x_1, x_2);
if (x_3 == 0)
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_unsigned_to_nat(1u);
x_5 = lean_nat_sub(x_1, x_4);
lean_dec(x_1);
x_1 = x_5;
goto _start;
}
else
{
lean_object* x_7;
lean_dec(x_1);
x_7 = lean_unsigned_to_nat(0u);
return x_7;
}
}
}

lean_object* l_not__tail__recursive(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3;
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_nat_dec_eq(x_1, x_2);
if (x_3 == 0)
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_4 = lean_unsigned_to_nat(1u);
x_5 = lean_nat_sub(x_1, x_4);
x_6 = l_not__tail__recursive(x_5);
lean_dec(x_5);
x_7 = lean_nat_add(x_6, x_4);
lean_dec(x_6);
return x_7;
}
else
{
lean_object* x_8;
x_8 = lean_unsigned_to_nat(0u);
return x_8;
}
}
}

you can see that the l_tail__recursive function contains a goto _start while l_not__tail__recursive contains a recursive call

[Scott Viteri]

wow, this is great

[Scott Viteri]

What do I need to do to view the result of the ir option once I set it to true

[Mario Carneiro]

on vscode it pops up in the output panel; in the console it prints to stdout

[Scott Viteri]

I'm finding it on emacs lsp::stderr

[Scott Viteri]

[result]
def tail_recursive.match_1._rarg (x_1 : @& obj) (x_2 : obj) (x_3 : obj) : obj :=
  let x_4 : obj := 0;
  let x_5 : u8 := Nat.decEq x_1 x_4;
  case x_5 : u8 of
  Bool.false →
    dec x_2;
    let x_6 : obj := 1;
    let x_7 : obj := Nat.sub x_1 x_6;
    let x_8 : obj := app x_3 x_7;
    ret x_8
  Bool.true →
    dec x_3;
    let x_9 : obj := ctor_0[PUnit.unit];
    let x_10 : obj := app x_2 x_9;
    ret x_10
def tail_recursive.match_1 (x_1 : ◾) : obj :=
  let x_2 : obj := pap tail_recursive.match_1._rarg._boxed;
  ret x_2
def tail_recursive.match_1._rarg._boxed (x_1 : obj) (x_2 : obj) (x_3 : obj) : obj :=
  let x_4 : obj := tail_recursive.match_1._rarg x_1 x_2 x_3;
  dec x_1;
  ret x_4
[result]
def tail_recursive (x_1 : obj) : obj :=
  let x_2 : obj := 0;
  let x_3 : u8 := Nat.decEq x_1 x_2;
  case x_3 : u8 of
  Bool.false →
    let x_4 : obj := 1;
    let x_5 : obj := Nat.sub x_1 x_4;
    dec x_1;
    let x_6 : obj := tail_recursive x_5;
    ret x_6
  Bool.true →
    dec x_1;
    let x_7 : obj := 0;
    ret x_7

is the ir result

[Scott Viteri]

the "def tail_recursive" part makes sense to me though it does not show tail recursion. What is the purpose of the other "match" functions here?

[Mario Carneiro]

tail_recursive.match_1 was generated by the equation compiler, and the compiler just compiled that definition too

def tail_recursive.match_1.{u_1} : (motive : Nat → Sort u_1) →
  (x : Nat) → (Unit → motive 0) → ((n : Nat) → motive (Nat.succ n)) → motive x :=
fun (motive : Nat → Sort u_1) (x : Nat) (h_1 : Unit → motive 0) (h_2 : (n : Nat) → motive (Nat.succ n)) =>
  Nat.casesOn x (h_1 Unit.unit) fun (n : Nat) => h_2 n

[Mario Carneiro]

the auxiliaries tail_recursive.match_1._rarg._boxed and tail_recursive.match_1._rarg were made by the compiler, but match_1 already existed

[Jakob von Raumer]

Is the compiled version of tail_recursive.match_1 optimized away or does it still exist in the fully compiled code?

[Mario Carneiro]

I believe the compiler will not use the definition of tail_recursive that lean sees but will directly compile an equation compiler definition to a general recursion

[Mario Carneiro]

In fact, right now the compiler doesn't know how to compile functions written directly by recursors:

def tail_recursive : Nat → Nat :=
  fun x => Nat.recOn (motive := λ _ => Nat) x 0 (fun _ ih => ih)
-- code generator does not support recursor 'Nat.recOn' yet, consider using 'match ... with' and/or structural recursion

So the equation compiler metadata is actually essential, at least for the present

[Scott Viteri]

#check tail_recursive.match_1 succeeds, but #check tail_recursive.match_1._rarg doesn't. So the generated functions are not one-to-one with the ir functions.

[Scott Viteri]

Oh that's what you mean by "match_1" already existed.

[Scott Viteri]

The Unit -> motive 0 part of match_1 is strange to me. Why is it not just motive 0 in the type signature?

[Scott Viteri]

Is the point of match_1 to create a lower level representation of your definition by removing match statements?

[Mario Carneiro]

There are definitions that are generated by the equation compiler, like tail_recursive.match_1, and definitions that are generated by the (lean-to-C) compiler, like tail_recursive.match_1._rarg.

• The first class of definitions are produced by macros, tactics, and constructs like match. They appear in the environment, are checked by the kernel, and are in that sense "real" definitions.
• The second class of definitions are created in the course of lowering code for generating machine code. Things like lifted lambda bodies will show up here as separate definitions because ultimately they will need to be separate functions in C. These are never touched by the kernel and are not added to the environment, although I don't think there is any fundamental reason why they couldn't be added; it's just not necessary. They are also not regular lean definitions - the IR syntax is not a term of type expr, even though it has a syntax that looks a lot like lean. (For example case x : u8 of ... is not a thing in lean, but it is in the IR.)

[Mario Carneiro]

Scott Viteri said:

The Unit -> motive 0 part of match_1 is strange to me. Why is it not just motive 0 in the type signature?

If I had to guess, I think this is to ensure that evaluating tail_recursive.match_1 (x+1) (fun _ => e1) (fun n => e2 n) does not require evaluating e1. This is handled by the evaluation semantics of Nat.casesOn directly, but for functions wrapping casesOn you get the default eager evaluation semantics, so it is important to introduce a thunk on any cases for constructors with no arguments, so that the case for that constructor is not unnecessarily evaluated.

[Scott Viteri]

This makes sense, thank you. Will match statements always turn into casesOn? Why not recOn?

[Scott Viteri]

hmm it also does support not rec directly

def tail_recursive'' : Nat → Nat :=
  fun x => Nat.rec (motive := λ _ => Nat) 0 (fun _ ih => ih) x

though casesOn uses rec under the hood.

[Scott Viteri]

Explained here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/type.20mismatch.20error