[Haskell-cafe] Re: [Haskell] ANN: Data.Proposition 0.1
Jan-Willem Maessen
jmaessen at alum.mit.edu
Wed Apr 18 09:05:16 EDT 2007
Hmm, your BDD implementation claims (in the comment at the top) that
"Equality is fast and accurate." But you don't do sharing
optimizations, and use derived Eq (rather than object identity), so
it's exponential in the number of nodes. Consider:
A
/ \
B |
\ /
C
/ \
D |
\ /
E
Here there are five nodes, but we will do two calls to see if C==C,
four calls to see if E==E. If I continue the diagram downwards I add
two nodes and double the number of equality calls on the leaf.
The sharing optimizations are rather important to making an efficient
BDD implementation. I haven't yet seen a Haskell-only BDD
implementation that didn't have one or more of the following flaws:
1) IO in all the result types, even though the underlying
abstraction is pure.
2) Inability to garbage collect unused nodes.
3) Loss of sharing leading to loss of fast equality.
Does anyone have a Haskell-only BDD library which avoids all these
problems? I wrote one with flaw #2, but was unable to make weak
pointers and finalization behave in anything like a sensible fashion
and gave up as it was a weekend project. The concurrency +
unsafePerformIO mix was trickier than I initially expected, too.
That said, this BDD implementation is pretty similar to the
performance & behavior you'd get from Data.IntSet (where the bits of
your int correspond to the True/False values of your variables).
-Jan-Willem Maessen
On Apr 16, 2007, at 9:07 AM, Neil Mitchell wrote:
> Hi,
>
> I am now releasing Data.Proposition. This library handles
> propositions, logical formulae consisting of literals without
> quantification. It automatically simplifies a proposition as it is
> constructed using simple rules provided by the programmer.
> Implementations of propositions in terms of an abstract syntax tree
> and as a Binary Decision Diagram (BDD) are provided. A standard
> interface is provided for all propositions.
>
> Website: http://www-users.cs.york.ac.uk/~ndm/proposition/
> Darcs: darcs get --partial http://www.cs.york.ac.uk/fp/darcs/
> proposition/
> Haddock: http://www.cs.york.ac.uk/fp/haddock/proposition/Data-
> Proposition.html
>
> The Haddock documentation also has a short example in it.
>
> This library is used substantially in the tool I have developed for my
> PhD, and has been extensively tested.
>
> Thanks
>
> Neil
> _______________________________________________
> Haskell mailing list
> Haskell at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2425 bytes
Desc: not available
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20070418/66568a85/smime.bin
More information about the Haskell-Cafe
mailing list