Stream: Coq users

Topic: ✔ Recursion + mutual recursion

Nikola Katić (Aug 11 2022 at 19:36):

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

• there is a need for evaluating single expression of some type exp, but also for evaluating list exp
• let's call those functions eval and evals

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?

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

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.

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.

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.

Nikola Katić (Aug 11 2022 at 22:25):

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

Notification Bot (Aug 11 2022 at 22:25):

Nikola Katić has marked this topic as resolved.

Last updated: Apr 18 2024 at 07:02 UTC