Recursive Function Definition

Stream: general

[Greg Zelevinsky]

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]

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]

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

Thanks!

[Damiano Testa]

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]

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]

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

[Kyle Miller]

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

[Damiano Testa]

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.