diff --git a/content/blog/01_spa_agda_lattices.md b/content/blog/01_spa_agda_lattices.md index 655ee83..a87afa4 100644 --- a/content/blog/01_spa_agda_lattices.md +++ b/content/blog/01_spa_agda_lattices.md @@ -263,8 +263,21 @@ ours, the analog to `min` is "greatest lower bound", or "the largest value that's smaller than both inputs". Such a function is denoted as \\(a\\sqcap b\\). As for what it means, where \\(s_1 \\sqcup s_2\\) means "combine two signs where you don't know which one will be used" (like in an `if`/`else`), -\\(s_1 \\sqcap s_2\\) means "combine two signs where you know both of -them to be true". For example, \\((+\ \\sqcap\ ?)\ =\ +\\), because a variable +\\(s_1 \\sqcap s_2\\) means "combine two signs where you know +{{< sidenote "right" "or-join-note" "both of them to be true" -7 >}} +If you're familiar with +Boolean algebra, this might look a little bit familiar to you. In fact, +the symbol for "and" on booleans is \(\land\). Similarly, the symbol +for "or" is \(\lor\). So, \(s_1 \sqcup s_2\) means "the sign is \(s_1\) or \(s_2\)", +or "(the sign is \(s_1\)) \(\lor\) (the sign is \(s_2\))". Similarly, +\(s_1 \sqcap s_2\) means "(the sign is \(s_1\)) \(\land\) (the sign is \(s_2\))". +Don't these symbols look similar?
+
+In fact, booleans with \((\lor)\) and \((\land)\) satisfy the semilattice +laws we've been discussing, and together form a lattice (to which I'm building +to in the main body of the text). The same is true for the set union and +intersection operations, \((\cup)\) and \((\cap)\). +{{< /sidenote >}}". For example, \\((+\ \\sqcap\ ?)\ =\ +\\), because a variable that's both "any sign" and "positive" must be positive. There's just one hiccup: what's the greatest lower bound of `+` and `-`?