From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id CD269BB9C for ; Wed, 16 Nov 2005 07:52:54 +0100 (CET) Received: from smtp2-g19.free.fr (smtp2-g19.free.fr [212.27.42.28]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id jAG6qsKj028534 for ; Wed, 16 Nov 2005 07:52:54 +0100 Received: from [192.168.0.2] (rke75-3-82-229-183-156.fbx.proxad.net [82.229.183.156]) by smtp2-g19.free.fr (Postfix) with ESMTP id 54A49522BD; Wed, 16 Nov 2005 07:52:54 +0100 (CET) Message-ID: <437AD616.7060006@inria.fr> Date: Wed, 16 Nov 2005 07:47:50 +0100 From: Alain Frisch User-Agent: Debian Thunderbird 1.0.2 (X11/20050602) X-Accept-Language: en-us, en MIME-Version: 1.0 To: Keiko Nakata Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Recursive types References: <20050506044107.1698.70519.Mailman@yquem.inria.fr> <437A64C1.3000807@cs.jhu.edu> <20051116.084030.02302710.garrigue@math.nagoya-u.ac.jp> <20051116.112005.68539737.keiko@kurims.kyoto-u.ac.jp> In-Reply-To: <20051116.112005.68539737.keiko@kurims.kyoto-u.ac.jp> Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 437AD746.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; frisch:01 frisch:01 caml-list:01 recursive:01 nodes:01 datatype:01 recursive:01 coinductive:01 nodes:01 memoization:01 wrote:01 arbitrary:01 define:01 loops:02 implemented:02 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 Keiko Nakata wrote: > I am very interested in this subject. > Since 1) I can define type abbreviations almost artitrary, > as in type t = < m : t > ; and 2) type abbreviations can have parameters > as in type 'a t = < m : 'a > , > just keeping a list/set of visited nodes does not seem to be enough, > especially for structual types. Structural loops (those that don't cross a datatype) cannot be arbitrary. The parameters cannot change: # type 'a t = < m : 'a t >;; type 'a t = < m : 'a t > # type 'a t = < m : ('a * 'a) t>;; In the definition of t, type ('a * 'a) t should be 'a t The restriction ensures that structural recursive types are necessarily regular. So standard coinductive algorithms (implemented by keeping track of visited nodes or by memoization) are ok. -- Alain