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

Add a sidenote about land and lor.

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-13 15:41:50 -07:00
parent e063ff6aa5
commit befcd3cf98
1 changed files with 15 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
content/blog/01_spa_agda_lattices.md
View File

@ -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 <a href="https://en.wikipedia.org/wiki/Boolean_algebra">
Boolean algebra</a>, 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?<br>
<br>
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 `-`?