Stream: Coq users

Topic: ✔ Recursion + mutual recursion


view this post on Zulip Nikola Katić (Aug 11 2022 at 19:36):

Hi all,
I stumbled at the following problem when trying to make deeply embedded toy language:

Because of the nature of exp type:
1) both of them are recursive
2) both of them are mutually recursive

So if evals is defined locally (using let statement inside eval's function definition), recursion is not allowed.
There is a message saying that evals is not recognized:

Error: The reference evals was not found in the current environment.

How would you overcome this?

view this post on Zulip Paolo Giarrusso (Aug 11 2022 at 20:15):

you could define evals using fix, but it's simpler to write evals ls as map eval ls

view this post on Zulip Paolo Giarrusso (Aug 11 2022 at 20:16):

Essentially that error doesn't mean "recursion is not allowed" but "you have not enabled recursion"... Just like Definition does not enable recursion while Fixpoint does.

view this post on Zulip Nikola Katić (Aug 11 2022 at 20:35):

@Paolo Giarrusso Thanks for the help :+1:
I didn't know fix existed and didn't consider map at all -- will try with map first.

Regarding other comment -- I meant to say that having (for example) following function is not possible:

Fail Fixpoint f1 (n1 : nat) :=
  let f2 (n2 : nat) :=
    match n2 with
    | 0 => f1 0
    | S (n2') => f2 n2'
    end
  in match n1 with
     | 0 => 0
     | S (n1') => 1 + f2 n1'
     end.

Since it seems to me (based on the error message) that recursive references inside local function such as f2 are not permitted.

view this post on Zulip Paolo Giarrusso (Aug 11 2022 at 22:18):

Indeed let (like definition) does not enable recursion, but that's what fix is for. Fixpoint is mostly just a Definition that uses fix.

view this post on Zulip Nikola Katić (Aug 11 2022 at 22:25):

Thanks again for clarifications :smile:
fold_left did the job in my case.

view this post on Zulip Notification Bot (Aug 11 2022 at 22:25):

Nikola Katić has marked this topic as resolved.


Last updated: Jun 23 2024 at 23:01 UTC