From 4938cdaecdb2447391a1094ab16d2a4aed05ac37 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 20 May 2024 22:46:18 -0700 Subject: [PATCH] Work some more on lattices 2 Signed-off-by: Danila Fedorin --- content/blog/01_spa_agda_lattices.md | 2 +- .../blog/02_spa_agda_combining_lattices.md | 36 +++++++++++++++++++ 2 files changed, 37 insertions(+), 1 deletion(-) diff --git a/content/blog/01_spa_agda_lattices.md b/content/blog/01_spa_agda_lattices.md index c747e48..ee7f305 100644 --- a/content/blog/01_spa_agda_lattices.md +++ b/content/blog/01_spa_agda_lattices.md @@ -422,7 +422,7 @@ only thing we needed is to be able to check and see if two elements are equal or not; this is called _decidable equality_. Since that's the only thing we used, this means that we can define an "above/below" lattice like this for any type for which we can check if two elements are equal. In Agda, I encoded -this using a parameterized module: +this using a [parameterized module](https://agda.readthedocs.io/en/latest/language/module-system.html#parameterised-modules): {{< codelines "Agda" "agda-spa/Lattice/AboveBelow.agda" 5 8 >}} diff --git a/content/blog/02_spa_agda_combining_lattices.md b/content/blog/02_spa_agda_combining_lattices.md index 54a1214..5a80506 100644 --- a/content/blog/02_spa_agda_combining_lattices.md +++ b/content/blog/02_spa_agda_combining_lattices.md @@ -29,3 +29,39 @@ challenging, but for for a two-level map like \(\text{info}\) above, we'd need to do a lot more work. We need tools to build up such complicated lattices! The way to do this, it turns out, is by using simpler lattices as building blocks. +To start with, let's take a look at a very simple way of combining lattices: +taking the Cartesian product. + +### The Cartesian Product Lattice + +Suppose you have two lattices \(L_1\) and \(L_2\). As I covered in the previous +post, each lattice comes equipped with a "least upper bound" operator \((\sqcup)\) +and a "greatest lower bound" operator \((\sqcap)\). Since we now have two lattices, +let's use numerical suffixes to disambiguate between the operators +of the first and second lattice: \((\sqcup_1)\) will be the LUB operator of +the first lattice \(L_1\), and \((\sqcup_2)\) of the second lattice \(L_2\). + +Then, let's take the Cartesian product of the elements of \(L_1\) and \(L_2\); +mathematically, we'll write this as \(L_1 \times L_2\), and in Agda, we can +just use the standard [`Data.Product`](https://agda.github.io/agda-stdlib/master/Data.Product.html) +module. In Agda, I'll define the lattice as another [parameterized module](https://agda.readthedocs.io/en/latest/language/module-system.html#parameterised-modules). Since both \(L_1\) and \(L_2\) +are lattices, this parameterized module will require `IsLattice` instances +for both types: + +{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 1 7 >}} + +Elements of \(L_1 \times L_2\) are in the form \((l_1, l_2)\), where +\(l_1 \in L_1\) and \(l_2 \in L_2\). The first thing we can get out of the +way is define what it means for two such elements to be equal. That's easy +enough: we have an equality predicate `_≈₁_` that checks if an element +of \(L_1\) is equal to another, and we have `_≈₂_` that does the same for \(L_2\). +It's reasonably to say that _pairs_ of elements are equal if their respective +first and second elements are equal: + +{{< latex >}} + (l_1, l_2) \approx (j_1, j_2) \iff l_1 \approx_1 j_1 \land l_2 \approx_2 j_2 +{{< /latex >}} + +In Agda: + +{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 39 40 >}}