Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

Maude does not implement hash consing for normal term rewriting. There is 
some 
opportunistic sharing of subterms but term comparison cannot rely on it so 
term comparison is not guaranteed to be constant time.

You might be interested to know that Maude itself makes extensive use of BDDs 
- for Buchi Automata construction, ACU unification and unification sort 
calculations. Also general DDs are used for rewriting sort calculations and 
free theory discrimination nets.

Steven

On Tuesday 22 February 2011 02:13:31 am Alban Linard wrote:
> Hello,
> 
> In the SMV group (see signature), people think that Decision Diagram
> operations can be viewed as term rewriting, so i plan to try
> implementing a DD library in Maude.
> 
> But Decision Diagrams heavily rely on unique representation of their
> representation. If a DD is encoded as a term, can Maude check equality
> between two DDs/terms in constant time ? Is there a mechanism like
> hash-consing/flyweight/unicity-table for Maude terms ?
> 
> If it does not exist, is there a way to avoid deep comparison of two
> terms ?
> Do you know other similar projects ?
> 
> Moreover, is there an easy way to implement the operation cache ? Or
> should it be given explicitly together with the operations' terms ?
> 
> Thanks,
> 
> Alban Linard,
> Software Modeling and Verification Group,
> University of Geneva
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help
>