Closed TomasMikula closed 8 years ago
Oops! You are right that this implementation is buggy.
I think that in this case, every element is its own inverse, since xor(x, x) = false
for any x
. In that case, negate(x) = x
.
I'll try to prepare a patch with laws, law-checking, and a correction. If I can't prove (and test) that this change is correct, we'll have to remove the method.
That seems to work.
Actually, I'm not sure. I realized that I just checked that for a Boolean algebra, not Heyting algebra.
From Heyting
:
def xor(a: A, b: A): A = or(and(a, complement(b)), and(complement(a), b))
xor(a, a)
// expand definition
or(and(a, complement(a)), and(complement(a), a))
// we know that and(a, complement(a)) is false even in just heyting algebras
or(false, false)
// we know this is false
false
So I'm pretty sure we know xor(a, a) = false
.
EDIT: See pseudo-complement here: https://en.wikipedia.org/wiki/Heyting_algebra#Formal_definition
The tricky part IMO will be to prove the ring's distributive law. On Oct 8, 2015 5:44 PM, "Erik Osheim" notifications@github.com wrote:
From Heyting:
def xor(a: A, b: A): A = or(and(a, complement(b)), and(complement(a), b))
xor(a, a)// expand definition or(and(a, complement(a)), and(complement(a), a))// we know that and(a, complement(a)) is false even in just heyting algebras or(false, false)// we know this is falsefalse
So I'm pretty sure we know xor(a, a) = false.
— Reply to this email directly or view it on GitHub https://github.com/non/algebra/issues/89#issuecomment-146694450.
Here's why it cannot be true. Suppose the object defined by Heyting#asCommutativeRing is a ring. Then it is a ring with a property a•a = a. A ring with this property is called a Boolean ring and is equivalent to a Boolean algebra (with xor
defined as ring addition, and or
defined in terms of xor
). Since we know that Heyting algebra is weaker than Boolean algebra, our assumption must have been wrong.
Ah yes, you are right of course. Let's just remove this method for now. Later on if someone discovers a useful structure (e.g. Semiring
) we can add a conversion.
Thanks again for your help @TomasMikula!
I think the method should be moved from Heyting
to Bool
, where it is true. Or even make Bool
extend CommutativeRing
directly?
Yeah let's move the method to Bool
, I think that makes the most sense. I'd rather not having it extend it directly because it would often conflict with other (possibly more natural) rings.
Do you have an example of a Boolean algebra that is also a ring different than the one given by a•b = a∧b
and a+b = a⊕b
(where ⊕ means xor)?
You can create a Bool[Int]
using &
and |
which is different from the Ring[Int]
one might normally expect.
If you don't want Bool
to extend CommutativeRing
directly, should there be a new trait BoolRing
and have asCommutativeRing
return that? BoolRing
can then have a method asBool
to get the Boolean algebra back.
Hm. My sense was that people were likely to want to use a [A: Bool]
constraint on their generic methods, and that they would be using asCommutativeRing
only when they were calling into code that was already parameterized on [A: Ring]
. I don't see an obvious situation where someone would need to recover the boolean algebra again where they couldn't just ask for it in the first place. Can you think of a situation where someone would need to talk about BoolRing
instead of just Bool
(or Ring
)?
I have a situation where I need to talk about a Boolean algebra (potentially) without a unit. I don't have a good name for it, but there is a good name for a Boolean ring without a unit - Boolean rng (see also my question on math.stackexchange). So I will have methods parameterized by [A: BoolRng]
. If someone has a Bool
, that should be good enough, except Bool#asCommutativeRing
only returns a CommutativeRing
, which is not enough. Anyway, this does not concern the current state of algebra
directly (since it has no BoolRng
), but this is the use case that I had in mind.
An example of a Boolean algebra without the top element is the set of finite subsets of an infinite set. For example, the type Set[String]
.
Also, in a Boolean algebra without unit, there will be no complement, but I'm still interested in the relative complement a\b
(set-theoretic difference). In Bool
, it could be implemented as a∧¬b
, but it can still be implemented even without ¬
. For Set
, it is a -- b
.
I think it would be nice to have this notion of a Boolean algebra without unit, but with relative complement, in algebra
(whether it would be called BoolRng
or something else).
Right, interesting.
I actually came up with a set data type that had a valid unit (i.e. the set containing everything) specifically to be able to use it in a boolean context. So I definitely see the value in something like that.
Interestingly, the link you gave defines Boolean Ring as the name for a boolean algebra with no "top" element, which sounds like what you actually want here.
Yeah, there doesn't seem to be consensus on whether ring assumes unit or not. But since Ring
in algebra
has a unit, it would be strange if BooleanRing
didn't.
What was your construction of a set type with unit? I constructed a type isomorphic to (Boolean, Set[A])
, where the Boolean
bit indicates whether the elements of Set
are meant to be included or excluded. However, if A
has a finite number of elements, this construction yields two representations for each subset of A
. If A
is infinite, then it represents only finite and co-finite subsets (which is better than just finite subsets represented by only Set
itself, but not much better).
I did something similar. I also used a type Universe[A]
to track the cardinality of A
(finite or infinite, etc) when I needed to be able to compare the two kinds of sets.
I can go ahead and move the method to Bool
if you want. Do you think it makes sense to rename it to just asRing
, where the fact that it is a commutative ring is captured by the return type? This way, we don't have to change the name again if in the future we decide that we want it to return a BoolRing
.
Fixed by #94
See my comment.
Heyting#asCommutativeRing
seems to be broken. The problem is with thenegate
method:complement
is not an inverse with respect toxor
.As an example, consider the usual interpretation of the type
Boolean = {false, true}
as a Boolean algebra.From the additive group, we have the law
Substituting
one
forx
we getAnd now replace
plus
byxor
,negate
by¬
,zero
byfalse
andone
bytrue
(as defined inasCommutativeRing
):i.e.
which is a contradiction.
FWIW, I don't immediately see how this could be fixed, i.e. I don't see how every Heyting algebra gives rise to a commutative ring.