Re: [Caml-list] equi-recursive Fold isomorphism

[Alain Frisch <frisch@clipper.ens.fr>]

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