From 826a16eb660bdc3e97ed0e76d6a2ae88bca40033 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Thu, 27 Jun 2024 22:26:01 -0700
Subject: [PATCH] Start working on part 3

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 content/blog/01_spa_agda_lattices.md          |  2 +
 .../blog/02_spa_agda_combining_lattices.md    |  1 +
 content/blog/03_spa_agda_fixed_height.md      | 81 +++++++++++++++++++
 3 files changed, 84 insertions(+)
 create mode 100644 content/blog/03_spa_agda_fixed_height.md

diff --git a/content/blog/01_spa_agda_lattices.md b/content/blog/01_spa_agda_lattices.md
index 2a0079c..68bee16 100644
--- a/content/blog/01_spa_agda_lattices.md
+++ b/content/blog/01_spa_agda_lattices.md
@@ -323,6 +323,8 @@ following are the updated Cayley tables for our operations.
  \bot & \bot & \bot & \bot & \bot & \bot \\
 \end{array}
 {{< /latex >}}
+{#sign-lattice}
+
 
 So, it turns out that our set of possible signs is a semilattice in two
 ways. And if "semi" means "half", does two "semi"s make a whole? Indeed it does!
diff --git a/content/blog/02_spa_agda_combining_lattices.md b/content/blog/02_spa_agda_combining_lattices.md
index bdc82ec..c324f5f 100644
--- a/content/blog/02_spa_agda_combining_lattices.md
+++ b/content/blog/02_spa_agda_combining_lattices.md
@@ -425,6 +425,7 @@ we can create the infinite chain:
 
 On the other hand, our sign lattice _is_ of finite height; the longest chains
 we can make have three elements and two `<` signs. Here's one:
+{#sign-length-three}
 
 {{< latex >}}
 \bot < + < \top
diff --git a/content/blog/03_spa_agda_fixed_height.md b/content/blog/03_spa_agda_fixed_height.md
new file mode 100644
index 0000000..ba11c1b
--- /dev/null
+++ b/content/blog/03_spa_agda_fixed_height.md
@@ -0,0 +1,81 @@
+---
+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 >}}