Heyting#asCommutativeRing broken

[typelevel]

Heyting#asCommutativeRing broken

[non]

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.

[non]

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.

[TomasMikula]

That seems to work.

[TomasMikula]

Actually, I'm not sure. I realized that I just checked that for a Boolean algebra, not Heyting algebra.

[non]

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

[TomasMikula]

The tricky part IMO will be to prove the ring's distributive law.
On Oct 8, 2015 5:44 PM, "Erik Osheim" [email protected] 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
#89 (comment).

[TomasMikula]

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.

[non]

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.

[non]

Thanks again for your help @TomasMikula!

[TomasMikula]

I think the method should be moved from Heyting to Bool, where it is true. Or even make Bool extend CommutativeRing directly?

[non]

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.

[TomasMikula]

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

[non]

You can create a Bool[Int] using & and | which is different from the Ring[Int] one might normally expect.

[TomasMikula]

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.

[non]

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

[TomasMikula]

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].

[TomasMikula]

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).

[non]

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.

[TomasMikula]

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.

[TomasMikula]

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).

[non]

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.

[TomasMikula]

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.

[non]

Fixed by #94

[TomasMikula]

See my comment.