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: Oct 13 2024 at 01:02 UTC