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

Show the basic Nat lattice.

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-12 18:52:26 -07:00
parent a20fe07a56
commit 6179c86919
1 changed files with 18 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
content/blog/01_spa_agda_lattices.md
View File

@ -242,6 +242,7 @@ record IsSemilattice {a} (A : Set a) (_⊔_ : A → A → A) : Set a where
⊔-idemp : (x : A) → (x ⊔ x) ≡ x ⊔-idemp : (x : A) → (x ⊔ x) ≡ x
``` ```
Note that this is an example of the ["Is Something" pattern]({{< relref "agda_is_pattern" >}}).
It turns out to be convenient, however, to not require definitional equality It turns out to be convenient, however, to not require definitional equality
(`≡`). For instance, we might model sets as lists. Definitional equality (`≡`). For instance, we might model sets as lists. Definitional equality
would force us to consider lists with the same elements but a different would force us to consider lists with the same elements but a different
@ -260,7 +261,7 @@ 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\\).
Intuitively, 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 both of \\(s_1 \\sqcap s_2\\) means "combine two signs where you know both of
them to be true". For example, \\((+\ \\sqcap\ ?)\ =\ +\\), because a variable them to be true". For example, \\((+\ \\sqcap\ ?)\ =\ +\\), because a variable
@ -321,4 +322,19 @@ In Agda, we can therefore write a lattice as follows:
{{< codelines "Agda" "agda-spa/Lattice.agda" 153 163 >}} {{< codelines "Agda" "agda-spa/Lattice.agda" 153 163 >}}
### Concrete Example: ### 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
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
operators to easily define `IsLattice` for natural numbers. Notice that
since we're not doing anything clever, like considering lists up to reordering,
there's no reason not to use definitional equality `≡` for our equivalence relation.
{{< codelines "Agda" "agda-spa/Lattice/Nat.agda" 1 45 >}}
The definition for the lattice instance itself is pretty similar; I'll omit
it here to avoid taking up a lot of vertical space, but you can find it
on lines 47 through 83 of [my `Lattice.Nat` module]({{< codeurl "agda-spa/Lattice/Nat.agda" >}}).