diff --git a/content/blog/01_spa_agda_lattices.md b/content/blog/01_spa_agda_lattices.md index 16fe024..2a0079c 100644 --- a/content/blog/01_spa_agda_lattices.md +++ b/content/blog/01_spa_agda_lattices.md @@ -202,6 +202,7 @@ similar function for our signs. We call this function "[least upper bound](https 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\)). +The \((\sqcup)\) symbol is also called the _join_ of \(a\) and \(b\). We can define it for our signs so far using the following [Cayley table](https://en.wikipedia.org/wiki/Cayley_table). {{< latex >}} @@ -264,7 +265,8 @@ 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\). +that's smaller than both inputs". Such a function is denoted as \(a\sqcap b\), +and often called the "meet" of \(a\) and \(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 diff --git a/content/blog/02_spa_agda_combining_lattices.md b/content/blog/02_spa_agda_combining_lattices.md index 0be1311..70454e0 100644 --- a/content/blog/02_spa_agda_combining_lattices.md +++ b/content/blog/02_spa_agda_combining_lattices.md @@ -449,10 +449,6 @@ The same is true for maps, under certain conditions. The finite-height property is crucial to lattice-based static program analysis; we'll talk about it in more detail in the next post of this series. -{{< todo >}} -I started using 'join' but haven't introduced it before. -{{< /todo >}} - ### Appendix: Proof of Uniqueness of Keys I will provide sketches of the proofs here, and omit the implementations