How can `WellFounded.fix` be noncomputable?

Stream: lean4

[Leni Aniva]

e.g.

def g : Nat → Nat
  | 0 => 0
  | (s+1) => 1 + g ((s+1) / 2)
#print g

gives

@[irreducible] def g : ℕ → ℕ :=
g.proof_1.fix fun a a_1 => ...

but WellFounded.fix is marked noncomputable. How can g be computable if its definition contains noncomputable parts?

[Aaron Liu]

g can be computable because the code generator generates code for it.
WellFounded.fix is noncomputable because the code generator does not generate code for it.

The code for g is based off the recursive definition written, not the compiled nonrecursive definition using WellFounded.fix.

[Leni Aniva]

Aaron Liu said:

g can be computable because the code generator generates code for it.
WellFounded.fix is noncomputable because the code generator does not generate code for it.

The code for g is based off the recursive definition written, not the compiled nonrecursive definition using WellFounded.fix.

so this is a special case in the code generator?

[Aaron Liu]

The code generator will always use the written definition, the compiled definition is the one for proof purposes and is not relevant to the code generator. Even if your g was compiled with Nat.brecOn, the code generator would still use the written definition.

[Aaron Liu]

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

-- uses `Nat.brecOn`
#print fib

-- the code generator generates a double recursive algorithm and this makes it slow
#eval fib 32

-- the kernel sees `Nat.brecOn`, whose reduction is linear
#reduce fib 32

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Also if you #print g and then try to use the printed term as the definition, Lean will complain that it cannot compile it.

[Leni Aniva]

Is there a way to #print the written recursive definition instead of the WellFounded.fix definition?

[Aaron Liu]

set_option trace.compiler.ir.result true in
def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fib (n + 1) + fib n

#print fib

#print fib._cstage1
#print fib._cstage2