RFC: kernel-irreducible well-founded recursion

[nomeata]

A long standing issue is that the kernel will happily try to reduce functions defined by well-founded recursion (#2171), and then this often fails with (kernel) deep recursion detected.

This leads to highly unpredictable behavior:

example : f 10000 = id f (id 10000) := rfl -- deep recusion
example : id f 10000 = id f (id 10000) := rfl -- fine
example : f 10000 + 0 = f (id 10000) + 0 := rfl -- deep recursion
example : f 10000 = f (id 10000) := rfl -- fine

It would be good to fix this. In #4061 we made functions defined by well-founded recursion irreducible by default, but this only affects the elaborator, not the kernel.

It might thus be desirable to prevent the kernel from unfolding these functions as well.

This can be achieved without changes to the kernel by inserting an opaque identity function into the definition of WellFounded.fix, as shown in #5182. This fixes the above issue.

One downside is that unseal f in doesn’t help anymore to make the function reduce after all. In #5182 and its mathlib adaption branch I could replace many rfl-proofs that needed unseal f by suitable proofs by rewriting (by simp [f] or variants). But two applications remain in mathlib where kernel-reduction of well-founded definitions are intentional and hard to replace:

• Nat.minFacAux finds the smallest factor of a number, and needs to be kernel reducible so that small prime numbers can be found.

  Arguably it could be rewritten to use structural recursion (or have a fuel argument), but it’s not a trivial change.

• The function

  /-- All steps of building the abstract filtered closure together with the realization function,
      as a function of `ℕ`.
  
     The function is defined by well-founded recursion, but we really want to use its
     definitional equalities in the proofs below, so lets make it semireducible.  -/
  @[semireducible] private noncomputable def bundledAbstractFilteredClosure :
      ℕ → Σ t : Type (max v w), t → C
    | 0 => ⟨ULift.{v} α, f ∘ ULift.down⟩
    | (n + 1) => ⟨_, inductiveStepRealization (n + 1) (fun m _ => bundledAbstractFilteredClosure m)⟩

  in Mathlib/CategoryTheory/Filtered/Small.lean also seems really need well-founded recursion and kernel reduction.

Here is one possible way forward:

• We define WellFounded.fix and WellFounded.reducibleFix. The former is as in feat: WellFounded.fix to be kernel-irreducible #5182 (no kernel reduction), the latter as it is now (kernel can reduce the Acc argument).
• By default, recursive functions are compiled using WellFounded.fix and are thus irreducible.
• If the user specifies @[semireducible], then it is compiled using WellFounded.reducibleFix

This way, special cases like the two above continue working, while in general well-founded definitions do not reduce, as desired.

Alternatives

• Live with the status quo.
• Wait until maybe eventually the kernel adheres to the transparency hints used by the elaborator.
• Wait for the module system to fix this for us (but would it do that even within a module)?

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[nomeata]

Ok, minNatFac can be rewritten to be structurally recursive (with fuel), and it’s much faster (minFacAux2 is the version in mathlib).

import Mathlib

open Nat

def minFacAux1 (n : ℕ) (fuel : ℕ) (k : ℕ) (_ : 2 * fuel > sqrt n + 2 - k) : ℕ :=
  match fuel with
  | 0 => by exfalso; omega
  | fuel+1 =>
    if h : n < k * k then n
    else
      if k ∣ n then k
      else
        minFacAux1 n fuel (k + 2) (by
          push_neg at h
          have : sqrt n ≥ k := by exact le_sqrt.mpr h
          omega
          )
          
def minFacAux2 (n : ℕ) : ℕ → ℕ
  | k =>
    if n < k * k then n
    else
      if k ∣ n then k
      else
        minFacAux2 n (k + 2)
termination_by k => sqrt n + 2 - k
decreasing_by simp_wf; apply minFac_lemma n k; assumption

/--
info: 449
---
info: time: 15ms
-/
#guard_msgs in
#time
#reduce minFacAux1 449 449 3 (by norm_num)

/--
info: 449
---
info: time: 1882ms
-/
#guard_msgs in
#time
#reduce minFacAux2 449 3

So maybe the conclusion should be that one simply should not use well-founded recursion when one wants kernel reduction.

[digama0]

I'd really rather we fix well founded recursion to not be so broken rather than pile on more hacks.

[nomeata]

Well, it’s not broken, but it’s just too slow when you try to reduce it. So it seems unless we can make it reduce as efficient as it looks, we should avoid reducing it?

What are our options at making well-founded recursion reduce efficiently? If we are willing to give up termination I guess we can just not reduce Acc terms, and it’s going to be reasonably fast, but my sense is that that isn’t great either, is it?

[digama0]

We shouldn't be reducing proofs in the first place. This is the source of all of the problems. It's possible to reduce the recursor without reducing the proof, because it can only unfold to one thing. This is described in my thesis. But I think we want something a bit more specialized to well founded recursion in this case, so that the kernel can actually just run the function which is what users want anyway. Never running the function is not a solution, it's causing more problems because it means that lean can't evaluate all expressions in its language so people have to just avoid a key feature of lean entirely when using kernel reduction. That's not a sustainable path forward.

Re: "If we are willing to give up termination": We already gave up termination a long time ago. Lean has been known to have theoretical termination issues for a while, and we also have concrete examples of code that fails to terminate in practice. I think you don't even need Acc to do it, reducing proofs is enough to create the counterexample.

[nomeata]

If we can get away with not reducing these proofs, I would be happy!

But I don't see not reducing certain definition as bleak.

it means that lean can't evaluate all expressions in its language so people have to just avoid a key feature of lean entirely when using kernel reduction

I expect we'll have more variants of Isabelle-style “here is a specification of a function, construct it under hood for me and prove it satisfies these equations” function definitions. I'm in particular thinking of tail-recursive and monadic functions, or more general fix points in partial order. Maybe others that just prove the existence of a certain function. I don't expect these will have any useful DefEqs, but aren't they still useful features in a theorem prover?

[digama0]

I expect we'll have more variants of Isabelle-style “here is a specification of a function, construct it under hood for me and prove it satisfies these equations” function definitions. I'm in particular thinking of tail-recursive and monadic functions, or more general fix points in partial order. Maybe others that just prove the existence of a certain function. I don't expect these will have any useful DefEqs, but aren't they still useful features in a theorem prover?

The trouble is that lean currently leans hard on defeq as a method for evaluating arbitrary functions, in #eval and rfl proofs. We currently don't have anything like that for functions defined by propositional equality clauses. Isabelle has a mechanism to evaluate these functions, but we don't, unless we make sure it's all defeqs. There are a bunch of important use cases in the "proof by reflection" regime where kernel evaluation forms a key part of the proof process, and I'm getting mixed messages from the FRO on whether they want to support kernel evaluation better or worse.

[nomeata]

I'd say we have the same mechanism as Isabelle: rewriting with simp. You can do a lot of useful work without any defeq.

Proof by reflection is something I, too, want to be well-supported by Lean, and plan to work on soon. But as long as reduction of well-founded recursive functions is horribly slow I'd rather prevent it from happening (so that users know that it isn't something that's supported) then having unhappy users due to slow reductions.

If we ever do get reduction of fix without having to reduce the proof objects we can change that again.

[nomeata]

Here might be a way to have our cake and eat it too.

The majority of functions defined by well-founded recursion have a termination_by function that maps the arguments to a value in Nat. At least for these functions, lean could use a different construction: Do not use WellFounded.fix with the invImage metric, but use the following fixed-point combinator that uses structural recursion and fuel:

def Nat.fix {motive : α → Sort u} (h : α → Nat) (F : (x : α) → ((y : α) → h y < h x → motive y) → motive x) : (x : α) → motive x :=
  let rec go : ∀ (fuel : Nat) (x : α), (h x < fuel) → motive x := Nat.rec 
    (fun _ hfuel => (not_succ_le_zero _ hfuel).elim)
    (fun _ ih x hfuel => F x (fun y hy => ih y (Nat.lt_of_lt_of_le hy (Nat.le_of_lt_add_one hfuel))))
  fun x => go (h x + 1) x (Nat.lt_add_one _)

theorem Nat.fix.go_fuel_congr {motive : α → Sort u} (h : α → Nat) (F : (x : α) → ((y : α) → h y < h x → motive y) → motive x)
    (fuel1 fuel2 : Nat) (x : α) (hfuel1 : h x < fuel1) (hfuel2 : h x < fuel2) :
    Nat.fix.go h F fuel1 x hfuel1 = Nat.fix.go h F fuel2 x hfuel2 := by
  induction fuel1 generalizing fuel2 x hfuel2 with
  | zero => contradiction
  | succ fuel1 IH => cases fuel2 with
    | zero => contradiction
    | succ fuel2 => show F .. =  F ..; congr; ext y hy; apply IH

theorem Nat.fix_eq  {motive : α → Sort u} (h : α → Nat) (F : (x : α) → ((y : α) → h y < h x → motive y) → motive x)
    (x : α) : Nat.fix h F x = F x (fun y _ => Nat.fix h F y) := by
  show F .. =  F ..; congr; ext y hy
  apply Nat.fix.go_fuel_congr

It’s about bedtime here, so I didn’t measure the reduction speed, but I expect its similarly good as with minFacAux1.

One worry is that the kernel, even though it won’t have to reduce proofs, it will build large unevaluated proof terms in each step and that this will kill performance.

[nomeata]

but I expect its similarly good as with minFacAux1.

And my expectation was proven wrong, it’s about as bad as the well-founded definition:

def minFacAux3 (n : ℕ) : ℕ  → ℕ :=
  Nat.fix (fun k => sqrt n + 2 - k) fun k ih =>
    if h : n < k * k then n
    else
      if k ∣ n then k
      else
        ih (k + 2) (by simp_wf; apply minFac_lemma n k; assumption)

/--
info: 449
---
info: time: 1914ms
-/
#guard_msgs in
#time
#reduce minFacAux3 449 3

Maybe diagnostics can help? We have

-- manual structural recursion with fuel
[reduction] unfolded declarations (max: 42, num: 4): ▼
  Decidable.rec ↦ 42
  dite ↦ 32
  Bool.rec ↦ 32
  rec ↦ 22

-- well-founded recursion
[reduction] unfolded declarations (max: 34787, num: 10): ▼
  Nat.rec ↦ 34787
  Or.rec ↦ 17217
  Acc.rec ↦ 259
  Nat.eq_or_lt_of_le ↦ 223
  Acc.inv ↦ 208
  Eq.rec ↦ 158
  rfl ↦ 144
  Decidable.rec ↦ 56
  dite ↦ 55
  Bool.rec ↦ 46
  
-- my Nat.fix experiment
[reduction] unfolded declarations (max: 34367, num: 10): ▼
  Nat.rec ↦ 34367
  Or.rec ↦ 17017
  Acc.rec ↦ 216
  Nat.eq_or_lt_of_le ↦ 203
  Acc.inv ↦ 198
  Eq.rec ↦ 128
  rfl ↦ 124
  Decidable.rec ↦ 56
  Bool.rec ↦ 46
  dite ↦ 45

This is strange. I wonder if I made a silly mistake somewhere.

---

Yes, I did! The expensive thing isn’t minFacAux, but it’s the sqrt computation:

/--
info: 21
---
info: time: 1880ms
-/
#guard_msgs in
#time 
#reduce Nat.sqrt 449

Above I accidentially initialized fuel with a simpler term than sqrt 449 and that was much faster. If I change the fuel condition in minFacAux1 to (_ : fuel > sqrt n + 2 - k) and call it as

#reduce minFacAux1 449 (sqrt 449 + 2 - 3  + 1) 3 (by norm_num)

then it is just as slow.

So much for barking up the wrong tree.

---

Now I wonder if I can speed up the definition by well-founded recursion if I avoid sqrt, and this definition is accepted

def minFacAux4 (n : ℕ) : ℕ → ℕ
  | k =>
    if h : n < k * k then n
    else
      if k ∣ n then k
      else
        minFacAux4 n (k + 2)
termination_by k => 2*n + 1 - k
decreasing_by
  simp_wf
  push_neg at h
  have : k ≤ n := k.le_mul_self.trans h
  omega

But it’s not faster either. I am confused.

---

I’ll just continue using this as a note-taking post…

It seems that #reduce doesn’t use the kernel’s whnf implementation, but that’s easily fixed

elab "#kernel_reduce" t:term : command => Lean.Elab.Command.runTermElabM fun _ => do
  let e ← Lean.Elab.Term.elabTermAndSynthesize t none
  let e' ← Lean.ofExceptKernelException <| Lean.Kernel.whnf (← Lean.getEnv) (← Lean.getLCtx) e
  Lean.logInfo m!"{e'}"

I am slowly making sense of this. Nat.sqrt is itself defined by well-founded recursion, and thus slow. This means that using Nat.sqrt somewhere where the kernel has to reduce it already kills performance. For example

def minFacAux1 (n : ℕ) (fuel : ℕ) (k : ℕ) (_ : fuel > sqrt n + 2 - k) : ℕ :=
  -- explicit fuel
#kernel_reduce (minFacAux1 449 449 3 (by norm_num))                     -- 13ms
#kernel_reduce (minFacAux1 449 (sqrt 449 + 2 - 3  + 1) 3 (by norm_num)) -- 1500ms

Note that having sqrt n in the precondition is fine, it seems that norm_num does not reduce Nat.sqrt here.

So my simple benchmarking shows this

Implementation	Timing
manual fuel, sqrt in initial fuel	1500ms
manual fuel, no sqrt in fuel	13ms
wf, like in mathlib	1500ms
Nat.fix, sqrt in size function	1850ms
wf, avoiding sqrt in measure	1500ms
Nat.fix, avoiding sqrt in size function	3ms (!)

Why is the last one faster than the manual fuel version? I suspected the .brecOn construction, but rewriting the manual fuel version using Nat.rec does not speed it up, with either of the two measure functions above. Strange, this looks almost like the fast version with just Nat.fix inlined.

---

Looking at Nat.sqrt, if I replace the existing definition

def sqrt1 (n : Nat) : Nat :=
  if n ≤ 1 then n else
  iter n (n / 2)
where
  /-- Auxiliary for `sqrt`. If `guess` is greater than the integer square root of `n`,
  returns the integer square root of `n`. -/
  iter (n guess : Nat) : Nat :=
    let next := (guess + n / guess) / 2
    if _h : next < guess then
      iter n next
    else
      guess
  termination_by guess

with one using Nat.fix, namely

def sqrt2 (n : Nat) : Nat :=
  if n ≤ 1 then n else
  iter (n / 2)
where
  /-- Auxiliary for `sqrt`. If `guess` is greater than the integer square root of `n`,
  returns the integer square root of `n`. -/
  iter : Nat → Nat := Nat.fix (fun guess => guess) (fun guess ih =>
    let next := (guess + n / guess) / 2
    if _h : next < guess then
      ih next (by decreasing_tactic)
    else
      guess
  )

then calculating the square root of 441 speeds up from 1409ms to 2ms.

This improvement seems to just too good to leave on the table!

Source code

[nomeata]

Another user bitten by accidentially reducing a function defined with well-founded recursion:
https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/An.20interval.20tactic.20for.20constant.20real.20inequalities/near/468279684

This increases my confidence that at least with the current status quo, we should block reduction of wf-rec functions, at least until when and if we can evaluate them efficiently.

[nomeata]

It seems actually likely that the Lean kernel will at some point do this kind of fast reduction of Acc.rec without looking at the proof term. This is also what you preferred, @digama0, right? Would you be interested to write a short RFC for it with a precise specification?

Also, it’s not unlikely that eventually the kernel will have more fine-grained transparency controls, like the elaborator now.

The timeline for both isn’t clear, though, and until then I am still in favor of removing the footgun of kernel-reduction of WellFounded.fix, as proposed here, with the per-function opt-out.

[nomeata]

In issue #5321 someone again stumbled over this.

But I noticed that since #3772 (merged two weeks ago) rfl will no longer use Kernel.whnf, so most users currently affected by kernel-reduces-wf will now be shielded from the issue because the elaborator won’t even accept the terms.

There might be corner cases where the elaborator manages to type-check the terms without reducing the wf term, but then the kernel tries to, but I’d like to see evidence of that before jumping into action.

Hence lowering the priority of this to low.