Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Edit and publish part 3

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-08-08 17:30:17 -07:00
parent 21b2ff208e
commit bf9b0aedf9
1 changed files with 27 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

51
content/blog/03_spa_agda_fixed_height.md
View File

@ -2,8 +2,7 @@
title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 3: Lattices of Finite Height" title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 3: Lattices of Finite Height"
series: "Static Program Analysis in Agda" 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" 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 date: 2024-08-08T17:29:00-07:00
draft: true
tags: ["Agda", "Programming Languages"] 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 propositional equality (`_≡_`). Thus, we we need to generalize the definition
of a chain to support equivalences. I parameterize the `Chain` module 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`, 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`/`<` which we will set to `<` for our chains. The equivalence relation `_≈_` and the
are expected to play together nicely (if `a < b`, and `a` is equivalent to `c`, ordering relation `R`/`<` are expected to play together nicely (if `a < b`, and
then it should be the case that `c < b`). `a` is equivalent to `c`, then it should be the case that `c < b`).
{{< codelines "agda" "agda-spa/Chain.agda" 3 7 >}} {{< 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 a different-but-equivalent element `a2'`.
With that definition in hand, I define what it means for a type of 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 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 maximum. put, all chains must have length less than or equal to the bound.
{{< codelines "agda" "agda-spa/Chain.agda" 38 39 >}} {{< codelines "agda" "agda-spa/Chain.agda" 38 39 >}}
Though `Bounded` specifies _a_ bound on the length of chains, it doesn't Though `Bounded` specifies _a_ bound on the length of chains, it doesn't
specify _the_ (lowest) bound. Specifically, if the chains can only have 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 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). 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 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. height exists, and that this height bounds the length of all other chains.
@ -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 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 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 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 This gives us a recipe for constructing
the longest chain in the product lattice: take the longest chains of `A` and 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 >}} {{< codelines "agda" "agda-spa/Lattice.agda" 196 217 >}}
Given this, and two lattices of finite height, we construct the full product 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)\), 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, b)\), and 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 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 >}} {{< 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`. 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 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 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 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, and produces two chains made from its increases. By the logic we've described,
@ -306,7 +307,7 @@ This completes the proof!
### Iterated Products ### Iterated Products
The product lattice allows us to combine finite height lattices into a 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 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, \(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 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. 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 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: 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" 34 40 >}}
@ -374,7 +375,7 @@ as many element as there are keys.
\end{array} \end{array}
{{< /latex >}} {{< /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. 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 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\)) 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): this by providing something like an [isomorphism](https://mathworld.wolfram.com/Isomorphism.html):
a pair of functions that convert between the two representations, and a pair of functions that convert between the two representations, and
preserve the properties and relationships (such as \((\sqcup)\)) of lattice 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: extensive:
{{< codelines "agda" "agda-spa/Isomorphism.agda" 22 33 "hl_lines=8-12">}} {{< 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 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)\). 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 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 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\) 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 Intuitively, this works because of the structure-preserving properties
we required above. For instance (recall the 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 >}} {{< latex >}}
\begin{align*} \begin{array}{rcr}
a \leq b & \iff (\text{definition of less than})\\ a \leq b & \iff & (\text{definition of less than})\\
a \sqcup b \approx b & \iff (\text{conversions preserve equivalence}) \\ a \sqcup b \approx b & \implies & (\text{conversions preserve equivalence}) \\
f(a \sqcup b) \approx f(b) & \iff (\text{conversions distribute over binary operations}) \\ 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) \sqcup f(b) \approx f(b) & \iff & (\text{definition of less than}) \\
f(a) \leq f(b) f(a) \leq f(b)
\end{align*} \end{array}
{{< /latex >}} {{< /latex >}}
2. __Proving that longer chains can't exist in the second (e.g., tuple) lattice:__ 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 we've already seen the mechanism to port a chain from one lattice to