diff --git a/content/blog/01_spa_agda_lattices.md b/content/blog/01_spa_agda_lattices.md index a87afa4..bfe9208 100644 --- a/content/blog/01_spa_agda_lattices.md +++ b/content/blog/01_spa_agda_lattices.md @@ -198,7 +198,7 @@ but what we're looking for is something similar. Instead, we simply require a similar function for our signs. We call this function "[least upper bound](https://en.wikipedia.org/wiki/Least-upper-bound_property)", since it is the "least (most specific) element that's greater (less specific) than either `s1` or `s2`". Conventionally, -this function is written as \\(a \\sqcup b\\) (or in our case, \\(s_1 \\sqcup s_2\\)). +this function is written as \(a \sqcup b\) (or in our case, \(s_1 \sqcup s_2\)). We can define it for our signs so far using the following [Cayley table](https://en.wikipedia.org/wiki/Cayley_table). {{< latex >}} @@ -212,7 +212,7 @@ We can define it for our signs so far using the following [Cayley table](https:/ \end{array} {{< /latex >}} -By using the above table, we can see that \\((+\ \\sqcup\ -)\ =\ ?\\) (aka `unknown`). +By using the above table, we can see that \((+\ \sqcup\ -)\ =\ ?\) (aka `unknown`). This is correct; given the four signs we're working with, that's the most we can say. Let's explore the analogy to the `max` function a little bit more, by observing that this function has certain properties: @@ -220,18 +220,18 @@ that this function has certain properties: * `max(a, a) = a`. The maximum of one number is just that number. Mathematically, this property is called _idempotence_. Note that by inspecting the diagonal of the above table, we can confirm that our - \\((\\sqcup)\\) function is idempotent. + \((\sqcup)\) function is idempotent. * `max(a, b) = max(b, a)`. If you're taking the maximum of two numbers, it doesn't matter which one you consider first. This property is called _commutativity_. Note that if you mirror the table along the diagonal, - it doesn't change; this shows that our \\((\\sqcup)\\) function is + it doesn't change; this shows that our \((\sqcup)\) function is commutative. * `max(a, max(b, c)) = max(max(a, b), c)`. When you have three numbers, and you're determining the maximum value, it doesn't matter which pair of numbers you compare first. This property is called _associativity_. You - can use the table above to verify the \\((\\sqcup)\\) is associative, too. + can use the table above to verify the \((\sqcup)\) is associative, too. -A set that has a binary operation (like `max` or \\((\\sqcup)\\)) that +A set that has a binary operation (like `max` or \((\sqcup)\)) that satisfies the above properties is called a [semilattice](https://en.wikipedia.org/wiki/Semilattice). In Agda, we can write this definition roughly as follows: ```Agda @@ -260,10 +260,10 @@ and the "least upper bound" function can be constructed from one another. As it turns out, the `min` function has very similar properties to `max`: it's idempotent, commutative, and associative. For a partial order like 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 +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 +\(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, @@ -277,7 +277,7 @@ 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 +{{< /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 `-`? @@ -289,8 +289,8 @@ out that this "impossible" value is the least element of our set (we added it to be the lower bound of `+` and co., which in turn are less than `unknown`). Similarly, `unknown` is the largest element of our set, since it's greater than `+` and co, and transitively greater than `impossible`. In mathematics, -it's not uncommon to define the least element as \\(\\bot\\) (read "bottom"), and the -greatest element as \\(\\top\\) (read "top"). With that in mind, the +it's not uncommon to define the least element as \(\bot\) (read "bottom"), and the +greatest element as \(\top\) (read "top"). With that in mind, the following are the updated Cayley tables for our operations. {{< latex >}} @@ -338,7 +338,7 @@ In Agda, we can therefore write a lattice as follows: ### Concrete Example: Natural Numbers Since we've been talking about `min` and `max` as motivators for properties -of \\((\\sqcap)\\) and \\((\\sqcup)\\), it might not be all that surprising +of \((\sqcap)\) and \((\sqcup)\), it might not be all that surprising that natural numbers form a lattice with `min` and `max` as the two binary operations. In fact, the Agda standard library writes `min` as `_⊓_` and `max` as `_⊔_`! We can make use of the already-proven properties of these