Version française
Home     About     Download     Resources     Contact us    
Browse thread
[Caml-list] equi-recursive Fold isomorphism
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Alain Frisch <frisch@c...>
Subject: Re: [Caml-list] equi-recursive Fold isomorphism

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:

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;

[2] Efficient Hash-Consing of Recursive Types, Jeffrey Considine;

Hope this helps.


To unsubscribe, mail Archives:
Bug reports: FAQ:
Beginner's list: