82 lines
3.4 KiB
Markdown
82 lines
3.4 KiB
Markdown
|
---
|
||
|
|
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-05-30T19:37:01-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 length three) in
|
||
|
|
[the previous post]({{< relref "02_spa_agda_combining_lattices#sign-length-three" >}}),
|
||
|
|
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 >}}
|
||
|
|
|
||
|
|
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:
|
||
|
|
|
||
|
|
{{< 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.
|
||
|
|
|
||
|
|
{{< 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.
|
||
|
|
|
||
|
|
{{< todo >}}
|
||
|
|
The rest of this.
|
||
|
|
{{< /todo >}}
|