Zulip Chat Archive

Stream: general

Topic: Recursive Function Definition


Greg Zelevinsky (Oct 28 2022 at 02:12):

Hi,

I'm trying to define a recursive function from natural numbers to reals:

def f : ℕ → ℝ
| 0 := 1
| (n + 1) := f n + 1 / (f n)

It gives me an error:
"rec_fn_macro only allowed in meta definitions"

What does this mean, and what do I have to change to get it to work?

Thanks!

Damiano Testa (Oct 28 2022 at 02:56):

Try adding noncomputable:

noncomputable def f :   
| 0 := 1
| (n + 1) := f n + 1 / (f n)

I think that the inverse is causing some issue.

Greg Zelevinsky (Oct 28 2022 at 02:57):

oh cool ok yeah that works, haven't seen that before.

Thanks!

Damiano Testa (Oct 28 2022 at 02:58):

I am not sure why it is giving such a cryptic message. This is how I got to the answer:

def f_aux (α) [field α] :   α
| 0 := 1
| (n + 1) := f_aux n + 1 / (f_aux n)

def f :    := f_aux  -- now Lean says that you should add `noncomputable`.

Kyle Miller (Oct 29 2022 at 12:14):

I think the cryptic message should just be understood to be an internal error in the VM compiler and noncomputability checker. In this case, given what I know about the internals, putting "noncomputable" on a recursive definition causes the equation compiler in use a different strategy and it's a sort of accidental workaround.

Kyle Miller (Oct 29 2022 at 12:15):

Another workaround is the more insistent version noncomputable! if you run into a similar issue again.

Kyle Miller (Oct 29 2022 at 12:18):

This is one of those things that would ideally be fixed, but almost all effort is being put into Lean 4 development.

Damiano Testa (Oct 29 2022 at 16:14):

Kyle, thanks for the extra information!

I was confused by the message, but once realized that the issue was the noncomputability of division, the solution was easy.

Anyway, I agree that this is secondary with respect to the 3→4 change.


Last updated: Dec 20 2023 at 11:08 UTC