From 8656985885ee66b9eb83febd2c2956e26d52533d Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 16 Jun 2024 20:12:39 -0700 Subject: [PATCH] Introduce "join" and "meet" as terms Signed-off-by: Danila Fedorin --- content/blog/01_spa_agda_lattices.md | 4 +++- content/blog/02_spa_agda_combining_lattices.md | 4 ---- 2 files changed, 3 insertions(+), 5 deletions(-) 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