diff --git a/content/blog/01_spa_agda_lattices.md b/content/blog/01_spa_agda_lattices.md index 1006449..f54f396 100644 --- a/content/blog/01_spa_agda_lattices.md +++ b/content/blog/01_spa_agda_lattices.md @@ -138,7 +138,7 @@ Moreover, the value we'll get out of the fixed point algorithm will be the _least fixed point_. For us, this means that the result will be "the most specific result possible". -{{< codelines "Agda" "agda-spa/Fixedpoint.agda" 80 80 >}} +{{< codelines "Agda" "agda-spa/Fixedpoint.agda" 86 86 >}} The above explanation omits a lot of details, but it's a start. To get more precise, we must drill down into several aspects of what I've said so far. diff --git a/content/blog/03_spa_agda_fixed_height.md b/content/blog/03_spa_agda_fixed_height.md index 3a2e13d..22aa140 100644 --- a/content/blog/03_spa_agda_fixed_height.md +++ b/content/blog/03_spa_agda_fixed_height.md @@ -125,7 +125,7 @@ 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 >}} +{{< codelines "agda" "agda-spa/Chain.agda" 47 53 >}} 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). @@ -133,7 +133,7 @@ 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">}} +{{< codelines "agda" "agda-spa/Lattice.agda" 183 210 "hl_lines = 27 28">}} Thus, bringing the operators and other definitions of `IsLattice` into scope will also bring in the `FixedHeight` predicate. @@ -262,7 +262,7 @@ 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 >}} +{{< codelines "agda" "agda-spa/Lattice.agda" 226 247 >}} 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_2)\), @@ -270,7 +270,7 @@ 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_1, \bot_2)\), and the second starts with it. -{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 177 179 >}} +{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 169 171 >}} 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 @@ -292,15 +292,15 @@ 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" 149 149 >}} -{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 158 172 "" "**(Click here for the implementation of `unzip`)**" >}} +{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 149 163 "" "**(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" >}} +{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 165 175 "hl_lines = 8-9" >}} This completes the proof! @@ -326,7 +326,7 @@ lattices as input. {{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 7 11 >}} -{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 21 22 >}} +{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 23 24 >}} 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` @@ -347,18 +347,18 @@ To build up with the lattice instance and --- if possible --- the finite height 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 >}} +{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 40 55 >}} 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 >}} +{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 57 76 >}} 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)**" >}} +{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 78 120 "" "**(Click here to expand the inductive proof)**" >}} ### Fixed Height of the Map Lattice @@ -472,11 +472,11 @@ 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 >}} +{{< codelines "agda" "agda-spa/Isomorphism.agda" 52 64 >}} With that, we can prove the second lattice's finite height: -{{< codelines "agda" "agda-spa/Isomorphism.agda" 65 72 >}} +{{< codelines "agda" "agda-spa/Isomorphism.agda" 66 73 >}} The conversion functions are also not too difficult to define. I give @@ -485,12 +485,12 @@ 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 >}} +{{< codelines "agda" "agda-spa/Lattice/FiniteValueMap.agda" 68 85 >}} 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 >}} +{{< codelines "agda" "agda-spa/Lattice/FiniteMap.agda" 58 60 >}} Proving the remaining properties (which as I mentioned, I omit from the main body of the post) is sufficient to apply the isomorphism, @@ -500,7 +500,7 @@ 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. +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". diff --git a/content/blog/agda_hugo.md b/content/blog/agda_hugo.md index baa4bc2..e753403 100644 --- a/content/blog/agda_hugo.md +++ b/content/blog/agda_hugo.md @@ -92,7 +92,7 @@ as well as a surrounding "context" that says what file the code is from, which lines are listed, and where to find the full code (e.g., on my Git server). It looks something like this: -{{< codelines "Agda" "agda-spa/Language.agda" 20 27 >}} +{{< codelines "Agda" "agda-spa/Language/Base.agda" 12 20 >}} In summary: