From 388c23c376e5e98be159df95dde1855bc7dadc8f Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 5 Jul 2024 12:09:29 -0700 Subject: [PATCH] Write more on finite height lattices Signed-off-by: Danila Fedorin --- .../blog/02_spa_agda_combining_lattices.md | 2 +- content/blog/03_spa_agda_fixed_height.md | 230 +++++++++++++++++- 2 files changed, 229 insertions(+), 3 deletions(-) diff --git a/content/blog/02_spa_agda_combining_lattices.md b/content/blog/02_spa_agda_combining_lattices.md index c324f5f..4412a17 100644 --- a/content/blog/02_spa_agda_combining_lattices.md +++ b/content/blog/02_spa_agda_combining_lattices.md @@ -425,7 +425,7 @@ we can create the infinite chain: On the other hand, our sign lattice _is_ of finite height; the longest chains we can make have three elements and two `<` signs. Here's one: -{#sign-length-three} +{#sign-three-elements} {{< latex >}} \bot < + < \top diff --git a/content/blog/03_spa_agda_fixed_height.md b/content/blog/03_spa_agda_fixed_height.md index ba11c1b..5af54e1 100644 --- a/content/blog/03_spa_agda_fixed_height.md +++ b/content/blog/03_spa_agda_fixed_height.md @@ -21,8 +21,8 @@ infinitely long: There isn't a "biggest natural number"! On the other hand, we've seen that our [sign lattice]({{< relref "01_spa_agda_lattices#sign-lattice" >}}) has a finite height; the longest chain we can make is three elements long; I showed one -such chain (there are many chains of length three) in -[the previous post]({{< relref "02_spa_agda_combining_lattices#sign-length-three" >}}), +such chain (there are many chains of three elements) in +[the previous post]({{< relref "02_spa_agda_combining_lattices#sign-three-elements" >}}), but here it is again: {{< latex >}} @@ -38,11 +38,13 @@ chains have five elements. The following is one example: {{< latex >}} (\bot, \bot) < (\bot, +) < (\bot, \top) < (+, \top) < (\top, \top) {{< /latex >}} +{#sign-prod-chain} The fact that \(L_1\) and \(L_2\) are themselves finite-height lattices is important; if either one of them is not, we can easily construct an infinite chain of the products. If we allowed \(L_2\) to be natural numbers, we'd end up with infinite chains like this one: +{#product-both-finite-height} {{< latex >}} (\bot, 0) < (\bot, 1) < (\bot, 2) < ... @@ -76,6 +78,230 @@ talk about them in a subsequent post. In the meantime, let's dig deeper into the notion of finite height, and the Agda proofs of the properties I've introduced thus far. +### Formalizing Finite Height + +The formalization I settled on is quite similar to the informal description: +a lattice has a finite height of length \(h\) if the longest chain +of elements compared by \((<)\) is exactly \(h\). There's only a slight +complication: we allow for equivalent-but-not-equal elements in lattices. +For instance, for a map lattice, we don't care about the order of the keys: +so long as two maps relate the same set of keys to the same respective values, +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`). + +{{< codelines "agda" "agda-spa/Chain.agda" 3 7 >}} + +From there, the definition of the `Chain` data type is much like the definition +of a vector, but indexed by the endpoints, and containing witnesses of `R`/`<` +between its elements. The indexing allows for representing +the type of chains between particular lattice elements, and serves to ensure +concatenation and other operations don't merge disparate chains. + +{{< codelines "agda" "agda-spa/Chain.agda" 19 21 >}} + +In the `done` case, we create a single-element chain, which has no comparisons. +In this case, the chain starts and stops at the same element (where "the same" +is modulo our equivalence). The `step` case prepends a new comparison `a1 < a2` +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. + +{{< 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, +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. + +{{< codelines "agda" "agda-spa/Chain.agda" 47 48 >}} + +Finally, for a lattice to have a finite height, the type of chains formed by using +its less-than operator needs to have that height (satisfy the `Height h` predicate). +To avoid having to thread through the equivalence relation, congruence proof, +and more, I define a specialized predicate for lattices specifically. +I do so as a "method" in my `IsLattice` record. + +{{< codelines "agda" "agda-spa/Lattice.agda" 153 180 "hl_lines = 27 28">}} + +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 +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. +We can't make chains out of incomparable elements (since we can't compare them +using `<`); thus, we can only have one `<` from the new least element, and +one `<` from the new greatest element. + +The proof is a bit tedious, but not all that complicated. +First, a few auxiliary helpers; feel free to read only the type signatures. +They specify, respectively: +1. That the bottom element \(\bot\) of the above-below lattice is less than any + concrete value from the underlying set. For instance, in the sign lattice case, \(\bot < +\). +2. That \(\bot\) is the only element satisfying the first property; that is, + any value strictly less than an element of the underlying set must be \(\bot\). +3. That the top element \(\top\) of the above-below lattice is greater than + any concrete value of the underlying set. This is the dual of the first property. +4. That, much like the bottom element is the only value strictly less than elements + of the underlying set, the top element is the only value strictly greater. + +{{< codelines "agda" "agda-spa/Lattice/AboveBelow.agda" 315 335 >}} + +From there, we can construct an instance of the longest chain. Actually, +there's a bit of a hang-up: what if the underlying set is empty? Concretely, +what if there were no signs? Then we could only construct a chain with +one comparison: \(\bot < \top\). Instead of adding logic to conditionally +specify the length, I simply require that the set is populated by requiring +a witness + +{{< codelines "agda" "agda-spa/Lattice/AboveBelow.agda" 85 85 >}} + +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 +bound of all chains of `AboveBelow` elements requires systematically +rejecting all longer chains. Informally, suppose you have a chain of +three or more comparisons. + +1. If it starts with \(\top\), you can't add any more elements since that's the + greatest element (contradiction). +2. If you start with an element of the underlying set, you could add another + element, but it has to be the top element; after that, you can't add any + more (contradiction). +3. If you start with \(\bot\), you could arrive at a chain of two comparisons, + but you can't go beyond that (in three cases, each leading to contradictions). + +{{< codelines "agda" "agda-spa/Lattice/AboveBelow.agda" 342 355 "hl_lines=8-14">}} + +Thus, the above-below lattice has a length of two comparisons (or alternatively, +three elements). + +{{< codelines "agda" "agda-spa/Lattice/AboveBelow.agda" 357 358 >}} + +And that's it. + +### Fixed Height of the Product Lattice + +Now, for something less tedious. We saw above that for a product lattice +to have a finite height, +[its constituent lattices must have a finite height](#product-both-finite-height). +The proof was by contradiction (by constructing an infinitely long product +chain given a single infinite lattice). As a result, we'll focus this +section on products of two finite lattices `A` and `B`. Additionally, for the +proofs in this section, I require element equivalence to be decidable. + +{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 115 117 >}} + +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 +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), +the new components would need to be bigger. Suppose then that we came up +with \(a_2\) and \(b_2\), with \(a_1 < a_2\) and \(b_1 < b_2\). We could then +create a length-one chain: + +{{< latex >}} +(a_1, b_1) < (a_2, b_2) +{{< /latex >}} + +That works, but we can construct an even longer chain by increasing only one +element at a time: + +{{< latex >}} +(a_1, b_1) < (a_1, b_2) < (a_2, b_2) +{{< /latex >}} + +We can apply this logic every time; the conclusion is that when building +up a chain, we need to increase one element at a time. Then, how many times +can we increase an element? Well, if lattice `A` has a height of two (comparisons), +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. + +This gives us a recipe for constructing +the longest chain in the product lattice: take the longest chains of `A` and +`B`, and start with the product of their lowest elements. Then, increase +the elements one at a time according to the chains. The simplest way to do +that might be to increase by all elements of the `A` chain, and then +by all of the elements of the `B` chain (or the other way around). That's the +strategy I took when [constructing the \(\text{Sign} \times \text{Sign}\) +chain above](#sign-prod-chain). + +To formalize this notion, a few lemmas. First, given two chains where +one starts with the same element another ends with, we can combine them into +one long chain. + +{{< codelines "agda" "agda-spa/Chain.agda" 31 33 >}} + +More interestingly, given a chain of comparisons in one lattice, we are +able to lift it into a chain in another lattice by applying a function +to each element. This function must be monotonic, because it must not +be able to reverse \(a < b\) such that \(f(b) < f(a)\). Moreover, this function +should be injective, because if \(f(a) = f(b)\), then a chain \(a < b\) might +be collapsed into \(f(a) \not< f(a)\), changing its length. Finally, +the function needs to produce equivalent outputs when giving equivalent inputs. +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 +concatenating the results. This works because the first chain ends with +\((\top, \bot)\), and the second starts with it. + +{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 177 179 >}} + +This gets us the longest chain; what remains is to prove that this chain's +length is the bound of all other changes. To do so, we need to work in +the opposite direction; given a chain in the product lattice, we need to +somehow reduce it to chains in lattices `A` and `B`, and leverage their +finite height to complete the proof. + +The key idea is that for every two consecutive elements in the product lattice +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. + +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, +the length two chains has to bound the main one's. I give the signature below, +and will put the implementation in a collapsible detail block. One last +detail is that the need to decide which chain to grow --- and thus which element +has increased --- is what introduces the need for decidable equality. + +{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 158 158 >}} + +{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 158 172 "" "**(Click here for the implementation of `unzip`)**" >}} + +Having decomposed the product chain into constituent chains, we simply combine +the facts that they have to be bounded by the height of the `A` and `B` lattices, +as well as the fact that they bound the combined chain. + +{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 174 183 "hl_lines = 8-9" >}} + +This completes the proof! + {{< todo >}} The rest of this. {{< /todo >}}