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

[Neil Mitchell]

Hi

> 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:

Its accurate and pretty fast - indeed I don't do sharing, but it is a
lot more accurate than when expressed as a formula. In my algorithms,
its never been a bottleneck, so perhaps "fast enough that I don't
care" is a more reasonable way of saying it :)

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

Take a look at: A Purely Functional Implementation of ROBDDs in
Haskell (http://www.cs.nott.ac.uk/~nhn/TFP2006/Papers/09-ChristiansenHuch-APurelyFunctionalImplementationOfROBDDs.pdf)

It may have some of these flaws, but its pretty well thought out.

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

Plus you get simplification between terms, and an interface that makes
it look like a proposition.

If anyone does want to write a BDD library, link to one with FFI, or
contribute any more proposition implementations - i'm happy to add
them in. Think of this library as a nice interface to propositions
which both satisfies all the implementations and all the users.
Plugging in new implementations or users is designed to be easy enough
to do.

This library used to be a critical part of my PhD, now its not as
important (I use it, but in a very limited way and only on the way
from one thing to another) . I released it so others may find it
useful, and would very much like others to fix the flaws in the BDD
library - or create another BDD library based upon it.

Thanks

Neil





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