Write some more in combining lattices

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

content/blog/01_spa_agda_lattices.md

@@ -70,6 +70,7 @@ things we're trying to rank depend on the sort of analysis we're trying to
 perform. Since I introduced sign analysis, we're ranking signs like `+` and `-`.
 For other analyses, the elements will be different. The _comparison_, however,
 will be a permanent fixture.
+{#specificity}
 
 Suppose now that we have some program analysis, and we're feeding it some input
 information. Perhaps we're giving it the signs of variables `x` and `y`, and

content/blog/02_spa_agda_combining_lattices.md

@@ -85,7 +85,16 @@ corresponding operators from \(L_1\) and \(L_2\) seems quite natural as well.
 (l_1, l_2) \sqcap (j_1, j_2) \triangleq (l_1 \sqcap_1 j_1, l_2 \sqcap_2 j_2)
 {{< /latex >}}
 
-In Agda:
+As an example, consider the product lattice \(\text{Sign}\times\text{Sign}\),
+which is made up of pairs of signs that we talked about in the previous
+post. Two elements of this lattice are \((+, +)\) and \((+, -)\). Here's
+how the \((\sqcup)\) operation is evaluated on them:
+
+{{< latex >}}
+(+, +) \sqcup (+, -) = (+ \sqcup + , + \sqcup -) = (+ , \top)
+{{< /latex >}}
+
+In Agda, the definition is written very similarly to its mathematical form:
 
 {{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 50 54 >}}
 
@@ -106,3 +115,52 @@ proving lattice properties boils down to applying the lattice properties of
 \(L_1\) and \(L_2\) to individual components.
 
 {{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 84 96 >}}
+
+This concludes the definition of the product lattice, which is made up of
+two other lattices. If we have a type of analysis that can be expressed as
+{{< sidenote "right" "pair-note" "a pair of two signs," >}}
+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
+\(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
+the smallest pieces that make up the bundles are themselves lattices.
+
+Products will come very handy a bit later in this series. For now though,
+our goal is to create another type of lattice: the map lattice. We will
+take the same approach we did with products: assuming the elements of the
+map are lattices, we'll prove that the map itself is a lattice. Then, just
+like we could put products inside products when building up lattices, we'll
+be able to put a map inside a map. This will allow us to represent the
+\(\text{Info}\) lattice, which is a map of maps.
+
+### The Map Lattice
+
+When I say "map", what I really means is something that associates keys with
+values, like [dictionaries in Python](https://docs.python.org/3/tutorial/datastructures.html#dictionaries).
+This data structure need not have a value for every possible key; a very precise
+author might call such a map a "partial map". We might have a map
+whose value (in Python-ish notation) is `{ "x": +, "y": - }`. Such a map states
+that the sign of the variable `x` is `+`, and the sign of variable `y` is
+`-`. Another possible map is `{ "y": +, "z": - }`; this one states that
+the sign of `y` is `+`, and the sign of another variable `z` is `-`.
+
+Let's start thinking about what sorts of lattices our maps will be. 
+The thing that [motivated our introduction]({{< relref "01_spa_agda_lattices#specificity" >}})
+of lattices was comparing them by "specificity", so let's try figure out how
+to compare maps. For that, we can begin small, by looking at singleton maps.
+If we have `{"x": +}` and `{"x": ⊤}`, which one of them is smaller? Well, wehave previously established that `+` is more specific (and thus less than) `⊤`. Thus, it shouldn't be too much of a stretch
+to say that for singleton maps of the same key, the one with the smaller
+value is smaller.
+
+Now, what about a pair of singleton maps like `{"x": +}` and `{"y": ⊤}`? Among
+these two, each contains some information that the other does not. Although the
+value of `y` is larger than the value of `x`, it describes a different key, so
+it seems wrong to use that to call the `y`-singleton "larger". Let's call
+these maps incompatible, then. More generally, if we have two maps and each one
+has a key that the other doesn't, we can't compare them.
+
+If only one map has a unique key, though, things are different. Take for
+instance `{"x": +}` and `{"x": +, "y": +}`.