blog-static/content/blog/03_spa_agda_fixed_height.md

---
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
tags: ["Agda", "Programming Languages"]
---

In the previous post, I introduced the class of finite-height lattices:
lattices where chains made from elements and the less-than operator `<`
can only be so long. As a first example,
[natural numbers form a lattice]({{< relref "01_spa_agda_lattices#natural-numbers" >}}),
but they __are not a finite-height lattice__; the following chain can be made
infinitely long:

{{< latex >}}
0 < 1 < 2 < ...
{{< /latex >}}

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 three elements) in
[the previous post]({{< relref "02_spa_agda_combining_lattices#sign-three-elements" >}}),
but here it is again:

{{< latex >}}
\bot < + < \top
{{< /latex >}}

It's also true that the [Cartesian product lattice \(L_1 \times L_2\)]({{< relref "02_spa_agda_combining_lattices#the-cartesian-product-lattice" >}})
has a finite height, as long as \(L_1\) and \(L_2\) are themselves finite-height
lattices. In the specific case where both \(L_1\) and \(L_2\) are the sign
lattice (\(L_1 = L_2 = \text{Sign} \)) we can observe that the longest
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) < ...
{{< /latex >}}

Another lattice that has a finite height under certain conditions is
[the map lattice]({{< relref "02_spa_agda_combining_lattices#the-map-lattice" >}}).
The "under certain conditions" part is important; we can easily construct
an infinite chain of map lattice elements in general:

{{< latex >}}
\{ a : 1 \} < \{ a : 1, b : 1 \} < \{ a: 1, b: 1, c: 1 \} < ...
{{< /latex >}}

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
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\}
{{< /latex >}}

The class of finite-height lattices is important for static program analysis,
because it ensures that out our analyses don't take infinite time. Though
there's an intuitive connection ("finite lattices mean finite execution"),
the details of why the former is needed for the latter are nuanced. We'll
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!

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