Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Introduce "join" and "meet" as terms

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-06-16 20:12:39 -07:00
parent 3be523b79e
commit 8656985885
2 changed files with 3 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
content/blog/01_spa_agda_lattices.md
View File

@ -202,6 +202,7 @@ similar function for our signs. We call this function "[least upper bound](https
since it is the "least (most specific) since it is the "least (most specific)
element that's greater (less specific) than either `s1` or `s2`". Conventionally, 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\)).
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). We can define it for our signs so far using the following [Cayley table](https://en.wikipedia.org/wiki/Cayley_table).
{{< latex >}} {{< 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`: As it turns out, the `min` function has very similar properties to `max`:
it's idempotent, commutative, and associative. For a partial order like it's idempotent, commutative, and associative. For a partial order like
ours, the analog to `min` is "greatest lower bound", or "the largest value 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 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`), 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

4
content/blog/02_spa_agda_combining_lattices.md
View File

@ -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; 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. 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 ### Appendix: Proof of Uniqueness of Keys
I will provide sketches of the proofs here, and omit the implementations I will provide sketches of the proofs here, and omit the implementations