is lattice a distributive lattice?
johnynek opened this issue · 3 comments
Here we say yes:
"Additionally, join and meet distribute:"
https://github.com/non/algebra/blob/master/core/src/main/scala/algebra/lattice/Lattice.scala#L16
But here we don't test this property:
https://github.com/non/algebra/blob/master/laws/shared/src/main/scala/algebra/laws/LatticeLaws.scala#L39
Lastly, a BoundedLattice is also a rig, right:
https://github.com/non/algebra/blob/master/core/src/main/scala/algebra/lattice/BoundedLattice.scala
we have the distributive + associative laws, we have 0, 1. Am I missing something?
So, the negation (which is identity, it looks like) is somehow only in Bool?
related to #89
/cc @TomasMikula
I think we shouldn't assume lattice to be distributive - there should be a separate DistributiveLattice type class for that. (Heyting would then extend DistributiveLattice.)
As to whether a bounded distributive lattice is a rig: it indeed seems that it is a rig (unless I'm missing something too), but a different one than the one that could be extended to a (Boolean) ring in case of Bool. The rig you have in mind defines plus as or, whereas the ring implied by Bool defines plus as xor. Since a xor a = 0, we can immediately define negate(a) = a. However, xor in Heyting is defined via complement (or relative complement in case of Bool without identity), so we don't have xor in a general bounded lattice.