[Haskell-cafe] Re: [Haskell] ANN: Data.Proposition 0.1

[Jan-Willem Maessen]

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




  2) Inability to garbage collect unused nodes.
  3) Loss of sharing leading to loss of fast equality.





-Jan-Willem Maessen


On Apr 16, 2007, at 9:07 AM, Neil Mitchell wrote:

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. 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).

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
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

smime.p7s
Description: S/MIME cryptographic signature

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe