Derek Elkins 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:
>
>> 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/
>>
>> 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  (?)
```