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
Jan-Willem Maessen wrote:
> 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
Use observable sharing or one of the unsafe pointer equality primitives (?)
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
