The Coq mailing list

[Coq User <coquser AT googlemail.com>]

The CoFixpoint operator seems to work.

On Wed, Jul 29, 2009 at 7:46 PM, Cedric Auger <Cedric.Auger AT lri.fr> wrote:

Coq User a écrit :

In the (very simplified) example below some coinductive types are defined for a Parent and Child relationship.  How can a Parent or Child be instantiated since they both co-refer to each other?  Can it be done as in object oriented programming where a Parent would be defined with a 'null' child first and similarly the Child be defined with 'null' and later the fields be updated to refer to each other?  How?

Require Import String.
CoInductive Parent:Set :=
| Build_Parent (fatherOrMother:string)(child:Child)
with
Child:Set :=
| Build_Child (father:Parent)(mother:Parent).
(*Functions for Parent fields.*)
Definition fatherOrMother:Parent -> string :=                   (fun p:Parent =>
        match p with
        | (Build_Parent fm ch) => fm
        end).
Definition child:Parent -> Child :=                   (fun p:Parent =>
        match p with
        | (Build_Parent fm ch) => ch
        end).
(*Functions for Child*)
Definition father:Child -> Parent :=                   (fun p:Child =>
        match p with
        | (Build_Child f m) => f
        end).
Definition mother:Child -> Parent :=                   (fun p:Child =>
        match p with
        | (Build_Child f m) => m
        end).

(*Instantiate a Parent*)
Definition father:Parent := Build_Parent "father"
(
  (Build_Child ( (*Father ??? How to refer to the same father Instance being defined here???*)) ((*Mother*)))
).

(*Same problem if we try to instantiate the Child first.*)

Here is a solution, but it will probably be a pain in the neck to use it.

CoFixpoint father2 : Parent :=
 Build_Parent "father" (Build_Child father2 mother2)
with mother2 : Parent :=
 Build_Parent "mother" (Build_Child father2 mother2).

Forget OOprogramming in Coq, and above all forget those tricks, you are in a purely functionnal language you CANNOT do side effects,
you can define Monads as in Haskell, or "emulate" the memory with a list (or a map), which is probably a bad idea, for example
have a positive map:

parents:
1 -> ("father", 1)
10 ->  ("mother", 1)

childs:
 1 -> (1, 10)

--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
        http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club