Edit and publish part 2

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

content/blog/00_spa_agda_intro.md

@@ -97,3 +97,4 @@ Here are the posts that I’ve written so far for this series:
 * {{< draftlink "Lattices" "01_spa_agda_lattices" >}}
 * {{< draftlink "Combining Lattices" "02_spa_agda_combining_lattices" >}}
 * {{< draftlink "Lattices of Finite Height" "03_spa_agda_fixed_height" >}}
+* {{< draftlink "Part 4: The Fixed-Point Algorithm" "04_spa_agda_fixedpoint" >}}

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