Definitional well-founded recursion

Stream: Type theory

[Parth Shastri]

I have figured out how to use the failure of normalization to encode well-founded recursion that is definitionally equal to its unfolding:

-- https://arxiv.org/abs/1911.08174
def T : Prop := ∀ p, (p → p) → p → p
def δ (z : T) : T := fun p η h => η (z (T → T) id id z p η h)
def ω : T := fun _ _ h => propext ⟨fun _ => h, fun _ => id⟩ ▸ δ
def Ω : T := δ ω

noncomputable def WellFounded.fix' {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r) {C : α → Sort v} (F : ∀ x, (∀ y, r y x → C y) → C x) x : C x :=
  @Acc.rec α r (fun x _ => C x) (fun x _ => F x) x (Ω (∀ x, Acc r x) (fun wf x => ⟨x, fun y _ => wf y⟩) hwf.apply x)

theorem WellFounded.fix'_eq : @WellFounded.fix' α r hwf C F x = F x fun y _ => hwf.fix' F y := rfl

noncomputable def log2 : Nat → Nat := WellFounded.fix' (r := LT.lt) Nat.lt_wfRel.wf fun n log2 => if h : n ≥ 2 then log2 (n / 2) (by omega) + 1 else 0

example : log2 n = if n ≥ 2 then log2 (n / 2) + 1 else 0 := rfl

Notably, this implementation does not require reducing the given proof of well-foundedness, since it constructs a new (non-normalizing) proof to use instead.

[Aaron Liu]

how do make sure it doesn't run forever

[Kenny Lau]

that's the well founded part

[Robin Arnez]

Well, #reduce still runs forever but I suppose whnf gets you to the if statement

[Albert Smith]

#reduce still runs forever

Works fine in practice for me, I guess"by accident"

#time -- 25ms
#reduce log2 (2^64)

[Albert Smith]

even with (proofs := true), which blows up the equivalent with Nat.log2

[Joachim Breitner]

Neat!

Parth Shastri schrieb:

since it constructs a new (non-normalizing) proof to use instead.

Do these proofs grow in size? (If so, then this wouldn’t quite solve the problem that decision procedures by well-founded recursion are not well-suited for by decide) Or will the proof just always be Ω (∀ x, Acc r x) as the function reduces?

[Albert Smith]

I think they stay small, but I'm not an expert so don't take my word for it. At the very least it plays nice with decide:

noncomputable def sqrt (n : Nat) : Nat :=
  if n ≤ 1 then n else
  iter n (n / 2)
where
  iter n : Nat → Nat :=
    Nat.lt_wfRel.wf.fix'
      fun guess self =>
        let next := (guess + n / guess) / 2
        if _h : next < guess then
          self next _h
        else
          guess

-- works!!
example : sqrt (10^200) = 10^100 := by
  decide

[Junyan Xu]

Does that mean we won't need PRs like #24514, or will the Lean kernel block such hacks?

[Aaron Liu]

I tried some manual reduction and the proofs don't seems to be getting bigger

[Aaron Liu]

I did encounter some deep recursion in the kernel though

[Parth Shastri]

Joachim Breitner said:

Do these proofs grow in size?

No, and this fact is actually an important part of why the defeq succeeds. My initial attempt at achieving definitional well-founded recursion was to replace Acc.rec directly, like so:

noncomputable def Acc.rec' : type_of% @Acc.rec.{u_1, u} := @fun α r motive intro x h =>
  @Acc.rec α r motive intro x (Ω (∀ x, Acc r x → Acc r x) (fun ih x h => ⟨x, fun y ryx => ih y (h.inv ryx)⟩) (fun _ h => h) x h)

theorem Acc.rec'_eq {intro x h} : @Acc.rec' α r motive intro x h = intro x @h.inv fun y ryx => @Acc.rec' α r motive intro y (h.inv ryx) := rfl

noncomputable def log2 (n : Nat) : Nat :=
  @Acc.rec' Nat LT.lt (fun _ _ => Nat) (fun n _ log2 => if h : n ≥ 2 then log2 (n / 2) (by omega) + 1 else 0) n (Nat.lt_wfRel.wf.apply n)

#reduce log2 (2^64) -- 64

example : log2 n = if n ≥ 2 then log2 (n / 2) + 1 else 0 := rfl -- error: maximum recursion depth has been reached

With this approach, the proof term gets bigger. However, this doesn't seem to cause any problems for decide, as the reduction performance is not that much slower (Benchmark).
The actual problem with this approach is that defeq checking runs forever for well-founded definitions like log2 (both the elaborator and the kernel loop). The underlying issue is that (Nat.lt_wfRel.wf.apply n).inv (h : m < n) and Nat.lt_wfRel.wf.apply m are definitionally equal by proof irrelevance, but they are not syntactically equal, and the defeq algorithm will reduce the Acc.rec application indefinitely. WellFounded.fix' avoids this issue because the proofs do not grow in size and the defeq check terminates because the two sides become syntactically equal.

[Parth Shastri]

@Mario Carneiro Is the algorithmic definitional equality from #leantt actually decidable? It seems to me that fix'_eq holds definitionally according to the algorithmic definitional equality rules, which allows the same undecidability proof from #leantt to apply. If it is in fact undecidable, is there any other theoretical reason to prefer it over the ideal definitional equality?

[Aaron Liu]

Well it can run forever on this

[Mario Carneiro]

Parth Shastri said:

Mario Carneiro Is the algorithmic definitional equality from #leantt actually decidable? It seems to me that fix'_eq holds definitionally according to the algorithmic definitional equality rules, which allows the same undecidability proof from #leantt to apply. If it is in fact undecidable, is there any other theoretical reason to prefer it over the ideal definitional equality?

I don't think it is decidable. (Note that this paper was written before the Abel-Coquand counterexample.) However, I think it is still possible to have a relation which is decidable and whose transitive closure is ideal defeq. You should never reduce proof terms, but you still reduce Acc.rec applied directly to Acc.intro. Unfolding would proceed by a transitivity chain of defeq replacements using proof irrelevance and reductions until the next step.

[Kenny Lau]

why is the code above noncomputable?

[Parth Shastri]

Mario Carneiro said:

You should never reduce proof terms, but you still reduce Acc.rec applied directly to Acc.intro. Unfolding would proceed by a transitivity chain of defeq replacements using proof irrelevance and reductions until the next step.

If we would sacrifice kernel reducibility of WF recursion anyways, why not go all the way and make the (ideal) definitional equality decidable by removing large elimination from Acc?

[Mario Carneiro]

that would require huge code changes

[Mario Carneiro]

what I'm talking about is a change to the theory that impacts no users

[Mario Carneiro]

There is a difference between WF recursion not being provable by the kernel and WF recursion not even being true in theory

[Joachim Breitner]

Mario Carneiro schrieb:

that would require huge code changes

Would it? Assuming in practice already all users of well-founded recursion don’t rely on any defeqs, then making fix_eq an axiom should be rather smooth? (I thought you even suggested that once?)

Or are you thinking of manual uses of Acc independent of wfrec?

[Parth Shastri]

#lean4 > opaque recursion definitions break mergeSort decidability @ 💬

[Mario Carneiro]

well in any case it's for me a separate question from what should be documented in the paper. I want to document lean as it exists, and we can also talk about changing lean and the document will change to match if/when this becomes a clear plan of action