Stream: Coq users

Topic: Representing mutual recursion functions


view this post on Zulip Julin S (Mar 21 2023 at 04:54):

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?

view this post on Zulip Julin S (Mar 21 2023 at 05:00):

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.

view this post on Zulip Meven Lennon-Bertrand (Mar 21 2023 at 09:49):

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.

view this post on Zulip Meven Lennon-Bertrand (Mar 21 2023 at 09:51):

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…

view this post on Zulip Meven Lennon-Bertrand (Mar 21 2023 at 09:52):

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.

view this post on Zulip Paolo Giarrusso (Mar 21 2023 at 10:20):

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

view this post on Zulip Paolo Giarrusso (Mar 21 2023 at 10:24):

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

view this post on Zulip Paolo Giarrusso (Mar 21 2023 at 10:24):

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!)

view this post on Zulip Paolo Giarrusso (Mar 21 2023 at 10:31):

@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