Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
RE: [Caml-list] "super-compaction" of values
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2001-08-02 (15:56)
From: Markus Mottl <markus@m...>
Subject: Re: [Caml-list] "super-compaction" of values
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!

Markus Mottl

Markus Mottl                                   
Austrian Research Institute
for Artificial Intelligence        
Bug reports:  FAQ:
To unsubscribe, mail  Archives: