Re: [Caml-list] "super-compaction" of values

[Markus Mottl <markus@mail4.ai.univie.ac.at>]

On Thu, 02 Aug 2001, Gregory Morrisett wrote:
> Similarly, Zhong Shao's Flint IL uses hash-consing for type terms
> quite effectively.  I can dig up the reference if you like.  In
> these two settings, one has to worry about the exponential blow
> up you can get by turning a DAG into a tree.

This is not a problem for me, because the trees really stay trees (as
datastructure), only that OCaml will represent them as DAGs in memory
after the transformation. Of course, if you want to print such a tree,
you'll have to cut exponentially many trees for the paper ;)

So there are really two kinds of DAGs: the explicitly constructed one that
uses (integer) indices to refer to subtrees, and the "normal" tree, which
uses sharing. Unfortunately, I can't use the sharing-tree representation
with memory addresses as indices alone, because the GC can move things,
which destroys any kind of order relation based on memory addresses to
search for matching subtrees... :(

> In addition, the hash-consing made structural equality tests quite cheap
> (O(1)) which is important for type checking or proof verification.

Well, one has to "hash-cons" a freshly generated tree at least once,
but then one can find equivalent (sub)trees very fast, because they'll be
pointer-equal. If they aren't, they cannot be structurally equivalent. The
algorithm I have in mind shouldn't require more than O(n*log(n)) time
(n being the number of nodes in the tree) for merging a fresh tree into
the hash-consing datastructure. Hm, let's see...

> For TAL, GC was not an issue, though we thought it might be.  For Flint,
> if memory serves, they periodically flushed the table or used some
> finalization/weak-pointer tricks.

In the first attempt I'll probably use "manual" removing of unneeded
trees from the hash-consing datastructure. Maybe then I'll play some
finalization tricks that remove unreachable trees automatically, only
leaving subtrees shared with not yet removed trees.

Thanks to all of you for your numerous answers!

Regards,
Markus Mottl

-- 
Markus Mottl                                             markus@oefai.at
Austrian Research Institute
for Artificial Intelligence                  http://www.oefai.at/~markus
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr