From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id VAA08208; Sat, 27 Jul 2002 21:44:01 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id VAA08222 for ; Sat, 27 Jul 2002 21:44:00 +0200 (MET DST) Received: from nef.ens.fr (nef.ens.fr [129.199.96.32]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id g6RJhED07612 for ; Sat, 27 Jul 2002 21:43:36 +0200 (MET DST) Received: from clipper.ens.fr (clipper-gw.ens.fr [129.199.1.22]) by nef.ens.fr (8.10.1/1.01.28121999) with ESMTP id g6RJhAo70406 ; Sat, 27 Jul 2002 21:43:10 +0200 (CEST) Received: from localhost (frisch@localhost) by clipper.ens.fr (8.12.3/jb-1.1) id g6RJh9YL021225 ; Sat, 27 Jul 2002 21:43:09 +0200 (MET DST) Date: Sat, 27 Jul 2002 21:43:09 +0200 (MET DST) From: Alain Frisch To: John Max Skaller cc: caml-list@inria.fr Subject: Re: [Caml-list] equi-recursive Fold isomorphism In-Reply-To: <3D42D920.2020800@ozemail.com.au> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Virus-Scanned: by amavisd-milter (http://amavis.org/) Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Hello, On Sun, 28 Jul 2002, John Max Skaller wrote: > Given a recursive type > > Fix 'a . T (where 'a occurs in T) > > we can unfold the type to T' = T['a -> Fix 'a.T], > we define unfold t = t, if t doesn't start with a fixpoint operator. > > Any ideas how to best implement fold, the inverse isomorphism? > > Brute force method: examine every subterm, and compare with > the main term using equi-recusive comparison .. this seems quadratic > in the number of nodes .. smarter method: only compare arguments > of fixpoint binders .. can we do any better? You can keep in each node of the term a hash value for the corresponding subterm; this hash value should be invariant by folding/unfolding (you can for instance look at a fixed depth to compute this hash value and unfold when necessary). These hash values avoid most equi-recursive comparisons (and elegate most of the remaining ones). My Recursive module uses the same technique; it may do what you want: http://www.eleves.ens.fr:8080/home/frisch/soft#recursive It helps manipulating recursive structures (and recursive types was indeed the main motivation) with maximal sharing and unique representation (that is: two terms that have the same infinite unfolding will be represented by the same value). You can also have a look at the following papers, which describe another solution: [1] Improving the Representation of Infinite Trees to Deal with Sets of Trees, Laurent Mauborgne; http://www.di.ens.fr/~mauborgn/publi/esop00.ps.gz [2] Efficient Hash-Consing of Recursive Types, Jeffrey Considine; http://www.cs.bu.edu/techreports/2000-006-hashconsing-recursive-types.ps.Z Hope this helps. Alain ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners