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

Finish up draft about lattices of finite height.

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-07-05 20:43:26 -07:00
parent 388c23c376
commit 861dafef70
2 changed files with 253 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
content/blog/01_spa_agda_lattices.md
View File

@ -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

258
content/blog/03_spa_agda_fixed_height.md
View File

@ -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 >}}