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

[Derek Elkins]

> 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  (?)