[Haskell-cafe] Re: [Haskell] ANN: Data.Proposition 0.1
derek.a.elkins at gmail.com
Wed Apr 18 09:16:34 EDT 2007
> On Apr 16, 2007, at 9:07 AM, Neil Mitchell wrote:
>> 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/
>> 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.
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:
> / \
> B |
> \ /
> / \
> D |
> \ /
> 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 (?)
More information about the Haskell-Cafe