Type classes for Boolean ring and Boolean algebra without 1.
TomasMikula opened this issue · 24 comments
There are useful data types that are almost like Bool or BoolRing, except they don't have a top element. A good example is Set[A]—when A is a type with infinitely many inhabitants, we cannot have the top element (Set of all As), but it is still useful to view it as a Boolean algebra.
Naming
A suitable name for a BoolRing without identity seems to be BoolRng.
For Bool without top, the best I have so far is ToplessBool. I'm not completely satisfied with this name, because it might suggest Bool necessarily without top, while what we mean is Bool potentially without top.
Definitions
BoolRng is just a Rng with idempotent multiplication (a⋅a=a).
ToplessBool is a DistributiveLattice with bottom and for all elements a, b, there is an element b\a, called the relative complement of a in b, such that
- a ∧ b\a = 0
- a ∨ b\a = a ∨ b
Note that in the presence of 1, we can define ¬a = 1\a and the above laws give the familiar laws of Boolean algebra:
a ∧ ¬a = a ∧ 1\a = 0
a ∨ ¬a = a ∨ 1\a = a ∨ 1 = 1
Equivalence
BoolRng and ToplessBool are equivalent.
Given a ToplessBool, one can construct a BoolRng in the following way:
- 0 = 0
- a⋅b = a∧b
- a+b = a\b ∨ b\a
- -a = a
Given a BoolRng, one can construct a ToplessBool in the following way:
- 0 = 0
- a∧b = a⋅b
- a∨b = a+b+(a⋅b)
- a\b = (a+b)⋅a = a + a⋅b
Just glacing at this, I wonder if LowerBoundedBool is a reasonable name.
That might be a better name. Although it might make Bool look like it is not bounded.
I just learned that they are also called generalized Boolean algebras. Not a great name, either, since it is not the only possible generalization of a Boolean algebra (Heyting is a different one) and the name does not say what kind of generalization it is. But if it is an established name, maybe we should use that—GeneralizedBool or GenBool.
I wonder if we can back away from the top/bottom distinctions here, and come up with a name that connotes something like a limited boolean algebra? We can't assert that the algebra definitely does not have a top element (only that it might not), and we don't want to imply that Bool lacks a bottom element by mentioning it here.
Doing some research [1], it seems like some authors talk about semi-boolean algebras as those that are missing a top or bottom element. If we created SemiBool[A] and defined it as a lower semi-boolean algebra maybe that would work?
Looks like I missed @TomasMikula's recent comment when posting mine. I think I slightly prefer SemiBool[A] but would be open to GeneralizedBool[A] or GenBool[A] as well.
SemiBool seems to suggest that only one of meet or join is required. It is not immediately clear to me whether "lower semi-Boolean algebra" implies the existence of join for any two elements (although by definition it has joins at least in every principal ideal).
Another naming problem is with the relative complement. In symbolic notation, we write a\b or a-b, but it is read backwards: "relative complement of b in a". So, should
relativeComplement(a, b)
mean
a\bto match the argument order of the symbolic notation; orb\ato match the argument order in the pronunciation?
A way around this could be calling the operation something else that would match the argument order of symbolic notation, such as minus or without:
without(a, b) ≡ a\b
I like SemiBool and will also suggest my own colour for the bikeshed: OpenBool.
"open" again suggests necessarily open, instead of potentially open.
I tend to agree with @TomasMikula. In all our existing naming, semi seems to mean you are missing an operation: semigroup (well, missing - and 0), semiring (missing 1, -), semilattice (only one of either meet/join).
This would be the first semi- that is missing only an element/unit.
About LowerBoundedBool, wouldn't Bool extend this, so it is necessarily lower bounded (but also upper bounded)?
@johnynek Yes, it becomes clear once you look at the inheritance hierarchy. It is just that without that information, my intuition would tell me that LowerBoundedBool must be something stronger than Bool—it feels like "LowerBounded" adds some constraint on Bool, while in fact it relaxes a constraint that is not mentioned (namely, the upper bound).
You're right, the semi-boolean algebras there are only guaranteed to have meet or join but not both. So I agree that the terminology I proposed is probably not great.
How do folks feel about GenBool (or GeneralizedBool)? It seems better than a totally idiosyncratic name, won't confuse the issue, and isn't that bad to type.
GeneraliSedBlah
:) I guess I asked for it.
GeneralizedBool is fine with me, I guess. Although, I'd probably be happier to use the name of the first person we can find in a book that studied this case. FooBool, for instance.
Looks like maybe someone named Stone created that name?
EDIT: Here maybe:
https://www.jstor.org/stable/2371008?seq=1#page_scan_tab_contents
StoneBool or GeneralizedBool would be my votes.
Stone algebra already means something: https://en.wikipedia.org/wiki/Stone_algebra (also see https://en.wikipedia.org/wiki/Stone%27s_representation_theorem_for_Boolean_algebras)
If you have a bottom element but not necessarily a top, then the word I've seen used is "Pointed" (https://en.wikipedia.org/wiki/Complete_partial_order) although it's not clear to me that orderings are as important to the abstractions you care about as they are in Domain Theory.
The problem with "PointedX" is what is "X" here? PointedBool again suggests "Bool with an extra requirement", while in fact what we have is Bool with less requirements.
@eigenvariable so, StoneLattice might actually be something we'd want to add (I'd rather say Lattice than Algebra). What do you think of StoneBool though as a distinct thing? I assume the Stone here is the same person.
I'd expect CPO and PointedCPO to be a useful programming abstraction to someone, somewhere, although whether it's the exact abstraction you're going for here I can't actually say. Do you have a complete list of the properties you want this to have?
I agree that it's probably the same person, but I worry that, since Stone Algebras, Stone's Representation Theorem, Stone Spaces, and Stone Duality (https://en.wikipedia.org/wiki/Stone_duality) are all relatively famous things, many overlapping with the concept of "Bool", that StoneBool could easily be mistaken for one of the above (unless, of course, it actually is one of the concepts above, in which case that's great).
@eigenvariable I want all the properties of a distributive lattice, bounded join semilattice, plus the extra operation of relative complement a\b satisfying
a ∧ b\a = 0
a ∨ b\a = a ∨ b
And no, it is none of the other "Stone" things.
For some reason I was summoned here on Twitter. The established mathematical name is generalized Boolean algebra. I am afraid there isn't a good solution to your problem. I kind of like ToplessBool.
By the way, there is "bipointed" for the case of a thing having two points, but I'd avoid calling neutral elements 0 and 1 "points".
@andrejbauer thanks for chiming in.
I think my favorite candidate so far is GeneralizedBool.