From bf9b0aedf986d37c69bb81bef81d2ea6cebd20b7 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 8 Aug 2024 17:30:17 -0700 Subject: [PATCH] Edit and publish part 3 Signed-off-by: Danila Fedorin --- content/blog/03_spa_agda_fixed_height.md | 53 ++++++++++++------------ 1 file changed, 27 insertions(+), 26 deletions(-) diff --git a/content/blog/03_spa_agda_fixed_height.md b/content/blog/03_spa_agda_fixed_height.md index ca70421..3a2e13d 100644 --- a/content/blog/03_spa_agda_fixed_height.md +++ b/content/blog/03_spa_agda_fixed_height.md @@ -2,8 +2,7 @@ title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 3: Lattices of Finite Height" series: "Static Program Analysis in Agda" description: "In this post, I describe the class of finite-height lattices, and prove that lattices we've alread seen are in that class" -date: 2024-07-06T17:37:45-07:00 -draft: true +date: 2024-08-08T17:29:00-07:00 tags: ["Agda", "Programming Languages"] --- @@ -91,9 +90,9 @@ we will consider them equal. This, however, is beyond the notion of Agda's propositional equality (`_≡_`). Thus, we we need to generalize the definition of a chain to support equivalences. I parameterize the `Chain` module in my code by an equivalence relation, as well as the comparison relation `R`, -which we will set to `<` for our chains. The equivalence relation and `R`/`<` -are expected to play together nicely (if `a < b`, and `a` is equivalent to `c`, -then it should be the case that `c < b`). +which we will set to `<` for our chains. The equivalence relation `_≈_` and the +ordering relation `R`/`<` are expected to play together nicely (if `a < b`, and +`a` is equivalent to `c`, then it should be the case that `c < b`). {{< codelines "agda" "agda-spa/Chain.agda" 3 7 >}} @@ -112,15 +111,16 @@ to an existing chain; once again, we allow for the existing chain to start with a different-but-equivalent element `a2'`. With that definition in hand, I define what it means for a type of -chains between elements of the lattice `A` to have a maximum height; simply -put, all chains must have length less than or equal to the maximum. +chains between elements of the lattice `A` to be bounded by a certain height; simply +put, all chains must have length less than or equal to the bound. {{< codelines "agda" "agda-spa/Chain.agda" 38 39 >}} Though `Bounded` specifies _a_ bound on the length of chains, it doesn't specify _the_ (lowest) bound. Specifically, if the chains can only have length three, they are bounded by both 3, 30, and 300. To claim a lowest -bound, we need to show that a chain of that length actually exists (otherwise, +bound (which would be the maximum length of the lattice), we need to show that +a chain of that length actually exists (otherwise, we could take the previous natural number, and it would be a bound as well). Thus, I define the `Height` predicate to require that a chain of the desired height exists, and that this height bounds the length of all other chains. @@ -210,7 +210,7 @@ proofs in this section, I require element equivalence to be decidable. Let's think about how we might go about constructing the longest chain in a product lattice. Let's start with some arbitrary element \(p_1 = (a_1, b_1)\). -We need to find another value that isn't equal to \(p_1\), because we'rebuilding +We need to find another value that isn't equal to \(p_1\), because we're building chains of the less-than operator \((<)\), and not the less-than-or-equal operator \((\leq)\). As a result, we need to change either the first component, the second component, or both. If we're building "to the right" (adding bigger elements), @@ -235,7 +235,8 @@ can we increase an element? Well, if lattice `A` has a height of two (comparison then we can take its lowest element, and increase it twice. Similarly, if lattice `B` has a height of three, starting at its lowest element, we can increase it three times. In all, when building a chain of `A × B`, we can -increase an element five times. +increase an element five times. Generally, the number of `<` in the product chain +is the sum of the numbers of `<` in the chains of `A` and `B`. This gives us a recipe for constructing the longest chain in the product lattice: take the longest chains of `A` and @@ -264,10 +265,10 @@ The result is the following lemma: {{< codelines "agda" "agda-spa/Lattice.agda" 196 217 >}} Given this, and two lattices of finite height, we construct the full product -chain by lifting the `A` chain into the product via \(a \mapsto (a, \bot)\), -lifting the `B` chain into the product via \(b \mapsto (\top, b)\), and +chain by lifting the `A` chain into the product via \(a \mapsto (a, \bot_2)\), +lifting the `B` chain into the product via \(b \mapsto (\top_1, b)\), and concatenating the results. This works because the first chain ends with -\((\top, \bot)\), and the second starts with it. +\((\top_1, \bot_2)\), and the second starts with it. {{< codelines "agda" "agda-spa/Lattice/Prod.agda" 177 179 >}} @@ -282,7 +283,7 @@ chain, we know that at least one of their components must've increased. This increase had to come either from elements in lattice `A` or in lattice `B`. We can thus stick this increase into an `A`-chain or a `B`-chain, increasing its length. Since one of the chains grows with every consecutive pair, the -number of consecutive pairs can't exceed the length of the `A` and `B` chains. +number of consecutive pairs can't exceed the combined lengths of the `A` and `B` chains. I implement this idea as an `unzip` function, which takes a product chain and produces two chains made from its increases. By the logic we've described, @@ -306,7 +307,7 @@ This completes the proof! ### 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 +new finite height lattice. From there, we can use this newly created 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 @@ -343,7 +344,7 @@ 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 +instance, I needed to allow for the constituent lattices being either finite or infinite. I supported this by defining a helper type: {{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 34 40 >}} @@ -374,7 +375,7 @@ as many element as there are keys. \end{array} {{< /latex >}} -This is why I introduced the [iterated product](#iterated-products) earlier; +This is why I introduced [iterated products](#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\)) @@ -412,7 +413,7 @@ 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 +elements. In fact, the list of the conversion functions' properties is quite extensive: {{< codelines "agda" "agda-spa/Isomorphism.agda" 22 33 "hl_lines=8-12">}} @@ -432,7 +433,7 @@ extensive: 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 +3. Finally, the functions must be inverses of each other. If you convert a 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\) @@ -448,16 +449,16 @@ Given this, the high-level proof is in two parts: 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\)): + [definition of \((\leq)\) given by Lars Hupel](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}) \\ + \begin{array}{rcr} + a \leq b & \iff & (\text{definition of less than})\\ + a \sqcup b \approx b & \implies & (\text{conversions preserve equivalence}) \\ + f(a \sqcup b) \approx f(b) & \implies & (\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*} + \end{array} {{< /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