From 4c70e61a147bc9d35cc964e2955ac9d121adc01b Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 30 May 2024 22:41:15 -0700 Subject: [PATCH] Write some more in combining lattices Signed-off-by: Danila Fedorin --- content/blog/01_spa_agda_lattices.md | 1 + .../blog/02_spa_agda_combining_lattices.md | 60 ++++++++++++++++++- 2 files changed, 60 insertions(+), 1 deletion(-) diff --git a/content/blog/01_spa_agda_lattices.md b/content/blog/01_spa_agda_lattices.md index 55cdf12..b11e9f6 100644 --- a/content/blog/01_spa_agda_lattices.md +++ b/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 diff --git a/content/blog/02_spa_agda_combining_lattices.md b/content/blog/02_spa_agda_combining_lattices.md index 6b131ee..5d292d8 100644 --- a/content/blog/02_spa_agda_combining_lattices.md +++ b/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": +}`.