I was trying to have a representation of mutually recursive functions.

How can that be done?

(This description is probably too vague, but am not sure how to say it properly...)

I was attempting the odd-even example like:

```
Require Import Vector.
Import VectorNotations.
Program Definition foo := fun (x:Vector.t (nat -> bool) 2) => [
(* Even function *)
fun n =>
match n with
| O => true
| S n' => (nth_order x (_:1<2)) n' (* odd n' *)
end;
(* Odd function *)
fun n =>
match n with
| O => false
| S n' => (nth_order x (_:0<2)) n' (* even n' *)
end
].
```

Not sure if this is even a way to go about it. But in case it is, how can I actually use it? AS in, how to use the `even`

function as `even 3`

.

I looked at this link for some inspiration: https://okmij.org/ftp/Computation/fixed-point-combinators.html

Basically, I wanted to have representation of mutually recursive function as a type. So that I can have a representation of the mutually recursive functions themselves as values of that type, which can then be given appropriate meanings.

Any pointers, anyone?

I wonder how mutual recursion is represented in coq itself. Where can we find that info? I guess it's in the coq source's repo, but couldn't pinpoint.

Julin S said:

I wonder how mutual recursion is represented in coq itself. Where can we find that info? I guess it's in the coq source's repo, but couldn't pinpoint.

In the kernel, mutually recursive functions are represented as a "block", ie a list of all the different, mutually defined functions, with their arguments, bodies, etc., together with an index telling you which function is the one currently considered.

Regarding your first question, I am not sure I understand it: what do you mean by "representation of mutually recursive function as a type"? Mutually recursive functions are just a special case of fuctions, so in Coq they will have some arrow/pi type, and you cannot really express as a typing constraint that they are defined in a certain specific way…

If you want to see how to define your example in Coq, I think the most standard way to write it down would be:

```
Fixpoint even (n : nat) : bool :=
match n with
| 0 => true
| S n' => odd n'
end
with odd (n : nat) : bool :=
match n with
| 0 => false
| S n' => even n'
end.
```

You can see when doing `Print even.`

that it really contains all of the mutually defined functions.

Maybe relevant: how do you define a mutually recursive functions using a fixpoint combinator? For simplicity, I suspect @Julin S should probably want to ignore termination, and then define a vector of functions as a fixpoint

If you change foo to return a vector of functions, you could then try to write a fueled fixpoint which just iterates the function.

Filling in the initial vector is trickier, and I'm now wondering if we'll need a partiality monad. (Haskell and EDIT: all "partial" languages let you cheat here!)

@Julin S have you picked an encoding for non-mutual recursive functions? Translating those examples to Coq isn't trivial either.

Last updated: Jun 14 2024 at 18:01 UTC