From 21b2ff208e64127dc2f83be8e83e4dfd5e7f382a Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 8 Aug 2024 16:45:13 -0700 Subject: [PATCH] Edit and publish part 2 Signed-off-by: Danila Fedorin --- .../blog/02_spa_agda_combining_lattices.md | 22 ++++++++++--------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/content/blog/02_spa_agda_combining_lattices.md b/content/blog/02_spa_agda_combining_lattices.md index 4286d55..04ac3a1 100644 --- a/content/blog/02_spa_agda_combining_lattices.md +++ b/content/blog/02_spa_agda_combining_lattices.md @@ -2,8 +2,7 @@ title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 2: Combining Lattices" series: "Static Program Analysis in Agda" description: "In this post, I describe how lattices can be combined to create other, more complex lattices" -date: 2024-07-06T17:37:44-07:00 -draft: true +date: 2024-08-08T16:40:00-07:00 tags: ["Agda", "Programming Languages"] --- @@ -30,8 +29,8 @@ 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](https://mathworld.wolfram.com/CartesianProduct.html). +To start with, let's take a look at a very simple way of combining lattices +into a new one: taking the [Cartesian product](https://mathworld.wolfram.com/CartesianProduct.html). ### The Cartesian Product Lattice @@ -50,11 +49,11 @@ module. Then, I'll define the lattice as another [parameterized module](https:// are lattices, this parameterized module will require `IsLattice` instances for both types: -{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 1 7 >}} +{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 1 7 "hl_lines=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 defining what it means for two such elements to be equal. Recall that +\(l_1 \in L_1\) and \(l_2 \in L_2\). Knowing that, let's define what it means +for two such elements to be equal. Recall that we opted for a [custom equivalence relation]({{< relref "01_spa_agda_lattices#definitional-equality" >}}) instead of definitional equality to allow similar elements to be considered equal; we'll have to define a similar relation for our new product lattice. @@ -122,7 +121,7 @@ two other lattices. If we have a type of analysis that can be expressed as Perhaps the signs are the smallest and largest possible values of a variable. {{< /sidenote >}} for example, we won't have to do all the work of proving the (semi)lattice properties of those pairs. In fact, we can build up -even bigger data structures. By taking a product a product twice, like +even bigger data structures. By taking a product twice, like \(L_1 \times (L_2 \times L_3)\), we can construct a lattice of 3-tuples. Any of the lattices involved in that product can itself be a product; we can therefore create lattices out of arbitrary bundles of data, so long as @@ -196,7 +195,7 @@ requires that each key in the smaller map be present in the larger one; as a result, \(m_1 \sqcup m_2\) should contain all the keys in \(m_1\) __and__ all the keys in \(m_2\). So, we could just take the union of the two maps: copy values from both into the result. Only, what happens if both \(m_1\) -and \(m_2\) have a value mapped to a particular key? The values in the two +and \(m_2\) have a value mapped to a particular key \(k\)? The values in the two maps could be distinct, and they might even be incomparable. This is where the second part of the condition kicks in: the value in the combination of the maps needs to be bigger than the value in either sub-map. We already know how @@ -248,7 +247,7 @@ on values. {{< /latex >}} Turning once again to set theory, we can think of this operation like the -extension of the intersection operator \((\cup)\) to maps. This can be +extension of the intersection operator \((\cap)\) to maps. This can be motivated in the same way as the union operation above; the \((\sqcap)\) operator combines lattice elements in such away that the result represents both of them, and intersections of sets contain elements that are in __both__ @@ -269,6 +268,9 @@ transliteration: {{< codelines "Agda" "agda-spa/Lattice/Map.agda" 530 531 >}} +Defining equivalence more abstractly this way helps avoid concerns about the +precise implementation of our maps. + Okay, but we haven't actually defined what it means for one map to be a subset of another. My definition is as follows: if \(m_1 \subseteq m_2\), that is, if \(m_1\) is a subset of \(m_2\), then every key in \(m_1\) is also present