how to do well founded recursion without...

Stream: general

[Huỳnh Trần Khanh]

how to do well founded recursion without well founded recursion? this is my attempt so far... not successful...

inductive something (r : ℕ → ℕ → Prop) : ℕ → Prop
| intro (x : ℕ) (h : ∀ y : ℕ, r y x → something y) : something x

def less : ℕ → ℕ → Prop
| a b := a < b

def loglike : ∀ x : ℕ, something less x → ℕ
| value' (something.intro value h) :=
  if h1 : value = 0 then 0 else
  (loglike (value / 2) (h (value / 2) begin
    rw less,
    have : 0 < value := begin
      apply lt_of_le_of_ne (zero_le _),
      tauto,
    end,
    have := @nat.div_lt_self value 2 this begin
      norm_num,
    end,
    exact this,
  end) + 1)

[Huỳnh Trần Khanh]

someone on here said that well-founded recursion is just structural recursion, that's why I'm doing this

[Mario Carneiro]

You can't use the equation compiler for this, because it doesn't support recursion on inductive predicates without well founded recursion, which is what you are trying to avoid. Instead you can just call the recursor directly:

def loglike (x : ℕ) (h : something less x) : ℕ :=
something.rec_on h $ λ value h IH,
  if h1 : value = 0 then 0 else
  (IH (value / 2) (begin
    rw less,
    have : 0 < value := begin
      apply lt_of_le_of_ne (zero_le _),
      tauto,
    end,
    have := @nat.div_lt_self value 2 this begin
      norm_num,
    end,
    exact this,
  end) + 1)

[Huỳnh Trần Khanh]

Well, your implementation has a bug. And I'm not asking you to fix that bug because, well, what's the point :joy: I mean, I want to understand how rec_on works to fix that bug myself. I don't understand rec_on at all, how does it work?

[Huỳnh Trần Khanh]

This is the signature of rec_on:

Π {r : ℕ → ℕ → Prop} {C : ℕ → Sort l} {ᾰ : ℕ}, something r ᾰ → (Π (x : ℕ), (∀ (y : ℕ), r y x → something r y) → (Π (y : ℕ), r y x → C y) → C x) → C ᾰ

The first parameter is the relation obviously. And I guess the C is the result type, and ᾰ is a parameter in the introduction rule. something r ᾰ is the inductive predicate, and x is also a parameter in the introduction rule (???) and the (∀ (y : ℕ), r y x → something r y) is the hypothesis in the introduction rule (?). (Π (y : ℕ), r y x → C y) → C x means a function that outputs the result type and C ᾰ is the final result. I feel like I'm typing nonsense. Because to be honest I don't understand the parameters at all.

[Huỳnh Trần Khanh]

Oh, the explanation is here:

The implicit argument, C, is the codomain of the function being defined. In type theory it is common to say C is the motive for the elimination/recursion, since it describes the kind of object we wish to construct. The next argument, n : nat, is the input to the function. It is also known as the major premise. Finally, the two arguments after specify how to compute the zero and successor cases, as described above. They are also known as the minor premises.

It doesn't explain how the rec_on function itself is evaluated though. How is it evaluated then?

[Huỳnh Trần Khanh]

And why does your function output 0 when I run #eval loglike 1000000 (something.intro 1000000 (is_wf 1000000))? This is my is_wf lemma, it's gnarly but hey, I'm just goofing around!

lemma invent (x y : ℕ) (h : something less x) (h1 : less y x) : something less y := begin
  cases h,
  exact h_h y h1,
end

lemma is_wf (x : ℕ) : ∀ y : ℕ, less y x → something less y := begin
  intro y,
  intro h,
  induction y,
  {
    rw less at h,
    exact something.intro 0 begin
      intro y,
      intro h,
      rw less at h,
      linarith,
    end,
  },
  {
    exact something.intro y_n.succ begin
      intro y,
      intro hhh,
      rw less at hhh,
      have := nat.eq_or_lt_of_le (nat.le_of_succ_le_succ hhh),
      cases this,
      rw this at hhh,
      rw this.symm at y_ih,
      rw this.symm at h,
      exact y_ih begin
        rw less at h,
        rw less,
        have : y < y.succ := by rwa this,
        exact lt_trans this h,
      end,
      rw less at h,
      have : y_n < y_n.succ := begin
        apply nat.lt_succ_of_le,
        linarith,
      end,
      have := y_ih begin
        rw less,
        exact lt_trans this h,
      end,
      exact invent y_n y this begin
        rw less,
        assumption,
      end,
    end,
  }
end

[Huỳnh Trần Khanh]

My original function, on the other hand, outputs 20.

[Huỳnh Trần Khanh]

That is, when I stick the meta keyword in front of the function definition.

[Eric Wieser]

In your example C is just λ _, nat

[Mario Carneiro]

Huỳnh Trần Khanh said:

Well, your implementation has a bug. And I'm not asking you to fix that bug because, well, what's the point :joy: I mean, I want to understand how rec_on works to fix that bug myself. I don't understand rec_on at all, how does it work?

Could you be more specific? It compiles just fine. As for what it actually does, I didn't pay it much attention, I think the body of the function is on you

[Mario Carneiro]

Oh, you are right, you've found one of lean's dirty secrets. Here's a function that computes a value in the singleton type one_hundred:

inductive acc' {α} (r : α → α → Prop) : α → Prop
| intro (x : α) (h : ∀ y : α, r y x → acc' y) : acc' x

def one_hundred := {x : ℕ // x = 100}
def foo : one_hundred :=
@acc'.rec_on one_hundred (=) (λ _, one_hundred) ⟨100, rfl⟩ sorry $ λ x h IH, x

You won't guess what the value is though:

#eval foo.1 -- 0

[Mario Carneiro]

Change one character and it works:

def foo : one_hundred :=
@acc.rec_on one_hundred (=) (λ _, one_hundred) ⟨100, rfl⟩ sorry $ λ x h IH, x
#eval foo.1 -- 100

[Chris B]

Huỳnh Trần Khanh said:

It doesn't explain how the rec_on function itself is evaluated though. How is it evaluated then?

When you declare an inductive type, the kernel makes lambda functions that correspond to the type's constructors. When the whnf reduction procedure needs to apply the recursor, there's a kernel function that fishes out the appropriate lambda and just applies it like a regular function. You can see the procedure for making one of the computation rules here:
https://github.com/leanprover/lean4/blob/99e2a577910812726958303fd1deeae52f57684e/src/kernel/inductive.cpp#L639
https://github.com/ammkrn/nanoda_lib/blob/998ef68742d2ccc9f82442d70ae16802f44e33f2/src/inductive.rs#L1116

Mario's paper has a written description in 2.6.3/2.6.4

[Chris B]

I'm not sure if there's a way to get Lean to print the value level of the computation rule. Someone else might know.

[Chris B]

Or if you know any of the languages used in the type checkers you can use one of those to print out whatever kernel terms you want.

[Mario Carneiro]

Here's an example for nat.rec_on:

protected def nat.rec_on : Π {C : ℕ → Sort l} (n : ℕ), C 0 → (Π (n : ℕ), C n → C n.succ) → C n

variables (α : Type) (z : α) (s : ℕ → α → α)
#check (@nat.rec_on (λ _, α) : ℕ → α → (ℕ → α → α) → α)

example : @nat.rec_on (λ _, α) 0 z s = z := rfl
example (n) : @nat.rec_on (λ _, α) (n+1) z s = s n (@nat.rec_on (λ _, α) n z s) := rfl

So when given z as initial value and s as a successor function, it returns z when the input is 0, and when the input is n+1, it first calls itself recursively at n to produce a result IH, then calls s n IH

[Mario Carneiro]

When the inductive type contains a nested function, IH will itself be a function, which can be called by the provided user function:

inductive foo : Type
| mk : (ℕ → foo) → foo

variables (α : Type)
#check (@foo.rec (λ _, α) : ((ℕ → foo) → (ℕ → α) → α) → foo → α)

I'm simplifying to the nondependent case here but it still has a rather involved function signature. The recursor takes one "configuration" argument of type (ℕ → foo) → (ℕ → α) → α, which defines what we want to compute by recursion, and one "main" argument of type foo, which is what we are actually recursing over. When we define the body, we get two arguments, of types ℕ → foo and ℕ → α. The first argument is the contents of the current value after destructing the foo.mk: since it has one argument of type ℕ → foo the recursor gives it to us, and we can call this function to receive embedded values. The other function of type ℕ → α is the inductive hypothesis. We are trying to define a function returning values in α, so if we want to query the children of the current value we can use this function to do so.

[Eric Wieser]

Mario, can you expand what the "dirty secret" about acc is there? Having the VM produce a different answer to the one you have a proof of seems like a pretty big deal, even if it doesn't impact soundness.

[Mario Carneiro]

def f (x : ℕ → foo) (IH : ℕ → α) : α := IH 2

def rec_f {α} : foo → α := @foo.rec (λ _, α) (f α)

example (x : ℕ → foo) : rec_f (foo.mk x) = f α x (λ n, rec_f (x n)) := rfl

[Mario Carneiro]

@Eric Wieser Indeed, this is a bug in the VM that can cause programs to crash or compute wrong answers. The dirty secret is that because supporting large-eliminating propositions is complicated, the lean devs punted on the problem and only implemented it for two specific types: eq and acc. Luckily you can simulate all other large eliminating inductives using these, and the built in compilation strategy uses them, so people were none the wiser.

[Gabriel Ebner]

In case you were wondering where the 0 came from:

inductive acc' {α} (r : α → α → Prop) : α → Prop
| intro (x : α) (h : ∀ y : α, r y x → acc' y) : acc' x

def foo : string :=
@acc'.rec_on string (λ _ _, false) (λ _, string) "" ⟨_, by cc⟩ $ λ x h IH, x

#eval foo
/-
vm check failed: is_external(o) (possibly due to incorrect axioms, or sorry)
-/

[Mario Carneiro]

Actually there are a few more builtin inductive predicates, like and. This one gives a nice error message:

inductive and' (a b : Prop) : Prop
| mk : a → b → and'

def foo : and true true := ⟨⟨⟩, ⟨⟩⟩
#eval (@and.rec true true (one_hundred) (λ _ _, ⟨100, rfl⟩) foo).1 -- 100
def foo' : and' true true := ⟨⟨⟩, ⟨⟩⟩
#eval (@and'.rec true true (one_hundred) (λ _ _, ⟨100, rfl⟩) foo').1
-- code generation failed, inductive predicate 'and'' is not supported

[Mario Carneiro]

Amusingly, it seems the humble true was supported however:

inductive true' : Prop
| mk : true'

def foo : true := ⟨⟩
#eval (@true.rec (one_hundred) ⟨100, rfl⟩ foo).1 -- 100
def foo' : true' := ⟨⟩
#eval (@true'.rec (one_hundred) ⟨100, rfl⟩ foo').1 -- 100

[Mario Carneiro]

The recursor for true is very useless:

protected eliminator true.rec : Π {C : Sort l}, C → true → C

[Huỳnh Trần Khanh]

so the moral of the story is... lean codegen is a clownfest? :clown: this is honestly... intriguing. like... lean can do something entirely different if it doesn't understand how to interpret our code computationally...

[Huỳnh Trần Khanh]

what's the motivation for this quirk though? performance?

[Huỳnh Trần Khanh]

to be quite frank I've never intentionally introduced a bug before... it's kind of weird that the lean devs intentionally introduce a bug into their software for some reason, and I want to understand the reasoning

[Gabriel Ebner]

intentionally introduce a bug

Please don't accuse anyone of being malicious.

[Huỳnh Trần Khanh]

hmm I don't? it's just that I find this quirk intriguing :joy:

[Gabriel Ebner]

The story with all of these things is simply limited developer time. This is not an intentional limitation, just that nobody had the time and motivation to implement it.

[Kevin Buzzard]

People's efforts go into what the community wants. Lean has made it into Nature with some high-powered maths but in all that code there is no #eval at all, it's not what (those kinds of) mathematicians do. Because there is no big demand for getting the Lean 3 VM better, it stays as it is.

[Huỳnh Trần Khanh]

Alright. Thank you for taking the time to answer this extremely crazy question! I have to go to bed now, see you! And I learned an extremely crazy quirk of the Lean theorem prover too :heart:

[Huỳnh Trần Khanh]

One final question (because I can't sleep LOL): this quirk doesn't exist in Lean 4 right?

[Gihan Marasingha]

Well-founded recursion isn't structural recursion (except in the sense that it involves structural recursion on well_founded). To my (admittedly freshly-formed) understanding, it's about constructing a function via well_founded.fix, together with the proof, viawell_founded.fix_eq, that the function so constructed has the desired properties.

[Mario Carneiro]

Huỳnh Trần Khanh said:

One final question (because I can't sleep LOL): this quirk doesn't exist in Lean 4 right?

Lean 4 behavior is very slightly worse than lean 3 here:

def OneHundred := {x : Nat // x = 100}
def mk : OneHundred := ⟨100, rfl⟩

inductive True' : Prop
| intro : True'

def True.foo : True := ⟨⟩
#eval (@True.rec (λ _ => OneHundred) mk True.foo).1
-- code generator does not support recursor 'True.rec' yet, consider using 'match ... with' and/or structural recursion
def True'.foo : True' := ⟨⟩
#eval (@True'.rec (λ _ => OneHundred) mk True'.foo).1
-- code generator does not support recursor 'True'.rec' yet, consider using 'match ... with' and/or structural recursion

inductive And' (a b : Prop) : Prop
| intro : a → b → And' a b

def And.foo : And True True := ⟨⟨⟩, ⟨⟩⟩
#eval (@And.rec True True (λ _ => OneHundred) (λ _ _ => mk) And.foo).1 -- 100
def And'.foo : And' True True := ⟨⟨⟩, ⟨⟩⟩
#eval (@And'.rec True True (λ _ => OneHundred) (λ _ _ => mk) And'.foo).1
-- code generator does not support recursor 'And'.rec' yet, consider using 'match ... with' and/or structural recursion

inductive Eq' {α : Sort u} (a : α) : α → Prop
| refl : Eq' a a

def Eq.foo : Eq 0 0 := rfl
#eval (@Eq.rec Nat 0 (λ _ _ => OneHundred) mk 0 Eq.foo).1 -- 100
def Eq'.foo : Eq' 0 0 := ⟨⟩
#eval (@Eq'.rec Nat 0 (λ _ _ => OneHundred) mk 0 Eq'.foo).1
-- code generator does not support recursor 'Eq'.rec' yet, consider using 'match ... with' and/or structural recursion

inductive Acc' {α : Sort u} (r : α → α → Prop) : α → Prop
| intro (x : α) (h : (y : α) → r y x → Acc' r y) : Acc' r x

def Acc.foo : Acc Eq mk := sorry
#eval (@Acc.rec OneHundred Eq (λ _ _ => OneHundred) (λ x h IH => x) mk Acc.foo).1
-- code generator does not support recursor 'Acc.rec' yet, consider using 'match ... with' and/or structural recursion
def Acc'.foo : Acc' Eq mk := sorry
#eval (@Acc'.rec OneHundred Eq (λ _ _ => OneHundred) (λ x h IH => x) mk Acc'.foo).1
-- code generator does not support recursor 'Acc'.rec' yet, consider using 'match ... with' and/or structural recursion

This makes sense considering that even regular well founded recursion is not implemented yet. On the bright side, the error is uniformly reported instead of having a loophole that allows seeing behind the under construction sign

[Mario Carneiro]

Oops, spoke too soon:

inductive False' : Prop

def False.foo : False := sorry
#eval (@False.rec (λ _ => OneHundred) False.foo).1
-- server crash
def False'.foo : False' := sorry
#eval (@False'.rec (λ _ => OneHundred) False'.foo).1
-- code generator does not support recursor 'False'.rec' yet, consider using 'match ... with' and/or structural recursion

[Mario Carneiro]

although to be fair I think it's fine to say that evaluating False.rec is undefined behavior