From 861dafef70f6112b1ca4c99edc70a31adab2bd0d Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 5 Jul 2024 20:43:26 -0700 Subject: [PATCH] Finish up draft about lattices of finite height. Signed-off-by: Danila Fedorin --- content/blog/01_spa_agda_lattices.md | 1 + content/blog/03_spa_agda_fixed_height.md | 258 ++++++++++++++++++++++- 2 files changed, 253 insertions(+), 6 deletions(-) diff --git a/content/blog/01_spa_agda_lattices.md b/content/blog/01_spa_agda_lattices.md index 68bee16..98e0741 100644 --- a/content/blog/01_spa_agda_lattices.md +++ b/content/blog/01_spa_agda_lattices.md @@ -333,6 +333,7 @@ A lattice is made up of two semilattices. The operations of these two lattices, however, must satisfy some additional properties. Let's examine the properties in the context of `min` and `max` as we have before. They are usually called the _absorption laws_: +{#absorption-laws} * `max(a, min(a, b)) = a`. `a` is either less than or bigger than `b`; so if you try to find the maximum __and__ the minimum of `a` and diff --git a/content/blog/03_spa_agda_fixed_height.md b/content/blog/03_spa_agda_fixed_height.md index 5af54e1..d120290 100644 --- a/content/blog/03_spa_agda_fixed_height.md +++ b/content/blog/03_spa_agda_fixed_height.md @@ -61,9 +61,10 @@ an infinite chain of map lattice elements in general: As long as we have infinite keys to choose from, we can always keep adding new keys to make bigger and bigger maps. But if we fix the keys in -the map -- say, we use only `a` and `b` -- then suddenly our heights are once +the map --- say, we use only `a` and `b` --- then suddenly our heights are once again fixed. In fact, for the two keys I just picked, one longest chain is remarkably similar to the product chain above. +{#fin-keys} {{< latex >}} \{a: \bot, a: \bot\} < \{a: \bot, b: +\} < \{a: \bot, b: \top\} < \{a: +, b: \top\} < \{a: \top, b: \top\} @@ -138,7 +139,7 @@ Thus, bringing the operators and other definitions of `IsLattice` into scope will also bring in the `FixedHeight` predicate. ### Fixed Height of the "Above-Below" Lattice -We've already seen intuitive evidence that the sign lattice --- which is an instance of +We've already seen intuitive evidence that the sign lattice --- which is an instance of the ["above-below" lattice]({{< relref "01_spa_agda_lattices#the-above-below-lattice" >}}) --- has a fixed height. The reason is simple: we extended a set of incomparable elements with a single element that's greater, and a single element that's lower. @@ -173,7 +174,7 @@ I use this witness to construct the two-`<` chain. {{< codelines "agda" "agda-spa/Lattice/AboveBelow.agda" 339 340 >}} -The proof that the length of two -- in terms of comparisons -- is the +The proof that the length of two --- in terms of comparisons --- is the bound of all chains of `AboveBelow` elements requires systematically rejecting all longer chains. Informally, suppose you have a chain of three or more comparisons. @@ -302,6 +303,251 @@ as well as the fact that they bound the combined chain. This completes the proof! -{{< todo >}} -The rest of this. -{{< /todo >}} +### Iterated Products + +The product lattice allows us to combine finite height lattices into a +new finite height lattice. From there, we can use this newly lattice +as a component of yet another product lattice. For instance, if we had +\(L_1 \times L_2\), we can take a product of that with \(L_1\) again, +and get \(L_1 \times (L_1 \times L_2)\). Since this also creates a +finite-height lattice, we can repeat this process, and keep +taking a product with \(L_1\), creating: + +{{< latex >}} +\overbrace{L_1 \times ... \times L_1}^{n\ \text{times}} \times L_2. +{{< /latex >}} + +I call this the _iterated product lattice_. Its significance will become +clear shortly; in the meantime, let's prove that it is indeed a lattice +(of finite height). +To create an iterated product lattice, we still need two constituent +lattices as input. + +{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 7 11 >}} + +{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 21 22 >}} + +At a high level, the proof goes by induction on the number of applications +of the product. There's just one trick. I'd like to build up an `isLattice` +instance even if `A` and `B` are not finite-height. That's because in +that case, the iterated product is still a lattice, just not one with +a finite height. On the other hand, the `isFiniteHeightLattice` proof +requires the `isLattice` proof. Since we're building up by induction, +that means that every recursive invocation of the function, we need +to get the "partial" lattice instance and give it to the "partial" finite +height lattice instance. When I implemented the inductive proof for +`isLattice` independently from the (more specific) inductive proof +of `isFiniteHeightLattice`, Agda could not unify the two `isLattice` +instances (the "actual" one and the one that serves as witness +for `isFiniteHeightLattice`). This led to some trouble and inconvenience, +and so, I thought it best to build the two up together. + +To build up with the lattice instance and --- if possible --- the finite height +instance, I needed to allow for the constituent lattices either finite +or infinite. I supported this by defining a helper type: + +{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 34 40 >}} + +Then, I defined the "everything at once" type, in which, instead of +a field for the proof of finite height, has a field that constructs +this proof _if the necessary additional information is present_. + +{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 42 55 >}} + +Finally, the proof by induction. It's actually relatively long, so I'll +include it as a collapsible block. + +{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 57 95 "" "**(Click here to expand the inductive proof)**" >}} + +### Fixed Height of the Map Lattice + +We saw above that [we can make a map lattice have a finite height if +we fix its keys](#finite-keys). How does this work? Well, if the keys +are always the same, we can think of such a map as just a tuple, with +as many element as there are keys. + +{{< latex >}} +\begin{array}{cccccc} + \{ & a: 1, & b: 2, & c: 3, & \} \\ + & & \iff & & \\ + ( & 1, & 2, & 3 & ) +\end{array} +{{< /latex >}} + +This is why I introduced the [iterated product](#iterated-products) earlier; +we can use them to construct the second lattice in the example above. +I'll take one departure from that example, though: I'll "pad" the tuples +with an additional unit element at the end. The unit type (denoted \(\top\)) +--- which has only a single element --- forms a finite height lattice trivially; +I prove this in [an appendix below](#appendix-the-unit-lattice). +Using this padding helps reduce the number of special cases; without the +adding, the tuple definition might be something like the following: + +{{< latex >}} +\text{tup}(A, k) = +\begin{cases} +\top & k = 0 \\ +A & k = 1 \\ +A \times \text{tup}(A, k - 1) & k > 1 +\end{cases} +{{< /latex >}} + +On the other hand, if we were to allow the extra padding, we could drop +the definition down to: + +{{< latex >}} +\text{tup}(A, k) = \text{iterate}(t \mapsto A \times t, k, \bot) = +\begin{cases} +\top & k = 0 \\ +A \times \text{tup}(A, k - 1) & k > 0 +\end{cases} +{{< /latex >}} + +And so, we drop from two to three cases, which means less proof work for us. +The tough part is to prove that the two representations of maps --- the +key-value list and the iterated product --- are equivalent. We will not +have much trouble proving that they're both lattices (we did that last time, +for both [products]({{< relref "02_spa_agda_combining_lattices#the-cartesian-product-lattice" >}}) and [maps]({{< relref "02_spa_agda_combining_lattices#the-map-lattice" >}})). Instead, what we need to do is prove that +the height of one lattice is the same as the height of the other. We prove +this by providing something like an [isomorphism](https://mathworld.wolfram.com/Isomorphism.html): +a pair of functions that convert between the two representations, and +preserve the properties and relationships (such as \((\sqcup)\)) of lattice +elements. In fact, list of the conversion functions' properties is quite +extensive: + +{{< codelines "agda" "agda-spa/Isomorphism.agda" 22 33 "hl_lines=8-12">}} + +1. First, the functions must preserve our definition of equivalence. Thus, + if we convert two equivalent elements from the list representation to + the tuple representation, the resulting tuples should be equivalent as well. + The reverse must be true, too. +2. Second, the functions must preserve the binary operations --- see also the definition + of a [homomorphism](https://en.wikipedia.org/wiki/Homomorphism#Definition). + Specifically, if \(f\) is a conversion function, then the following + should hold: + + {{< latex >}} + f(a \sqcup b) \approx f(a) \sqcup f(b) + {{< /latex >}} + + For the purposes of proving that equivalent maps have finite heights, it + turns out that this property need only hold for the join operator \((\sqcup)\). +3. Finally, the functions must be inverses of each other. If you convert + list to a tuple, and then the tuple back into a list, the resulting + value should be equivalent to what we started with. In fact, they + need to be both "left" and "right" inverses, so that both \(f(g(x))\approx x\) + and \(g(f(x)) \approx x\). + +Given this, the high-level proof is in two parts: + +1. __Proving that a chain of the same height exists in the second (e.g., tuple) + lattice:__ To do this, we want to take the longest chain in the first + (e.g. key-value list) lattice, and convert it into a chain in the second. + The mechanism for this is not too hard to imagine: we just take the original + chain, and apply the conversion function to each element. + + Intuitively, this works because of the structure-preserving properties + we required above. For instance (recall the + [definition of \((\leq)\) explained by Lars Huple](https://lars.hupel.info/topics/crdt/03-lattices/#there-), which in brief is \(a \leq b \triangleq a \sqcup b = b\)): + + {{< latex >}} + \begin{align*} + a \leq b & \iff (\text{definition of less than})\\ + a \sqcup b \approx b & \iff (\text{conversions preserve equivalence}) \\ + f(a \sqcup b) \approx f(b) & \iff (\text{conversions distribute over binary operations}) \\ + f(a) \sqcup f(b) \approx f(b) & \iff (\text{definition of less than}) \\ + f(a) \leq f(b) + \end{align*} + {{< /latex >}} +2. __Proving that longer chains can't exist in the second (e.g., tuple) lattice:__ + we've already seen the mechanism to port a chain from one lattice to + another lattice, and we can use this same mechanism (but switching directions) + to go in reverse. If we do that, we can take a chain of questionable length + in the tuple lattice, port it back to the key-value map, and use the + (already known) fact that its chains are bounded to conclude the same + thing about the tuple chain. + +As you can tell, the chain porting mechanism is doing the heavy lifting here. +It's relatively easy to implement given the conditions we've set on +conversion functions, in both directions: + +{{< codelines "agda" "agda-spa/Isomorphism.agda" 51 63 >}} + +With that, we can prove the second lattice's finite height: + +{{< codelines "agda" "agda-spa/Isomorphism.agda" 65 72 >}} + + +The conversion functions are also not too difficult to define. I give +them below, but I refrain from showing proofs of the more involved +properties (such as the fact that `from` and `to` are inverses, preserve +equivalence, and distribute over join) here. You can view them by clicking +the link at the top of the code block below. + +{{< codelines "agda" "agda-spa/Lattice/FiniteValueMap.agda" 67 84 >}} + +Above, `FiniteValueMap ks` is the type of maps whose keys are fixed to +`ks`; defined as follows: + +{{< codelines "agda" "agda-spa/Lattice/FiniteMap.agda" 50 52 >}} + +Proving the remaining properties (which as I mentioned, I omit from +the main body of the post) is sufficient to apply the isomorphism, +proving that maps with finite keys are of a finite height. + + +### Using the Finite Height Property + +Lattices having a finite height is a crucial property for the sorts of +static program analyses I've been working to implement. +We can create functions that traverse "up" through the lattice, +creating larger values each time. If these lattices are of a finite height, +then the static analyses functions can only traverse "so high". +Under certain conditions, this +guarantees that our static analysis will eventually terminate with +a [fixed point](https://mathworld.wolfram.com/FixedPoint.html). Pragmatically, +this is a state in which running our analysis does not yield any more information. + +The way that the fixed point is found is called the _fixed point algorithm_. +We'll talk more about this in the next post. + +{{< seriesnav >}} + +### Appendix: The Unit Lattice + +The unit lattice is a relatively boring one. I use the built-in unit type +in Agda, which (perhaps a bit confusingly) is represented using the symbol `⊤`. +It only has a single constructor, `tt`. + +{{< codelines "agda" "agda-spa/Lattice/Unit.agda" 6 7 >}} + +The equivalence for the unit type is just propositional equality (we have +no need to identify unequal values of `⊤`, since there is only one value). + +{{< codelines "agda" "agda-spa/Lattice/Unit.agda" 17 25 >}} + +Both the join \((\sqcup)\) and meet \((\sqcap)\) operations are trivially defined; +in both cases, they simply take two `tt`s and produce a new `tt`. +Mathematically, one might write this as \((\text{tt}, \text{tt}) \mapsto \text{tt}\). +In Agda: + +{{< codelines "agda" "agda-spa/Lattice/Unit.agda" 30 34 >}} + +These operations are trivially associative, commutative, and idempotent. + +{{< codelines "agda" "agda-spa/Lattice/Unit.agda" 39 46 >}} + +That's sufficient for them to be semilattices: + +{{< codelines "agda" "agda-spa/Lattice/Unit.agda" 48 54 >}} + +The [absorption laws]({{< relref "01_spa_agda_lattices#absorption-laws" >}}) +are also trivially satisfied, which means that the unit type forms a lattice. + +{{< codelines "agda" "agda-spa/Lattice/Unit.agda" 78 90 >}} + +Since there's only one element, it's not really possible to have chains +that contain any more than one value. As a result, the height (in comparisons) +of the unit lattice is zero. + +{{< codelines "agda" "agda-spa/Lattice/Unit.agda" 102 117 >}}