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, but they are not a finite-height lattice; the following chain can be made infinitely long:

$0 < 1 < 2 < ...$

There isn’t a “biggest natural number”! On the other hand, we’ve seen that our 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, but here it is again:

$\bot < + < \top$

It’s also true that the Cartesian product lattice $L_1 \times L_2$ 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:

$(\bot, \bot) < (\bot, +) < (\bot, \top) < (+, \top) < (\top, \top)$

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:

$(\bot, 0) < (\bot, 1) < (\bot, 2) < ...$

Another lattice that has a finite height under certain conditions is the map lattice. The “under certain conditions” part is important; we can easily construct an infinite chain of map lattice elements in general:

$\{ a : 1 \} < \{ a : 1, b : 1 \} < \{ a: 1, b: 1, c: 1 \} < ...$

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.

$\{a: \bot, a: \bot\} < \{a: \bot, b: +\} < \{a: \bot, b: \top\} < \{a: +, b: \top\} < \{a: \top, b: \top\}$

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 the ordering relation 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).

From Chain.agda, lines 3 through 7
 3 4 5 6 7  module Chain {a} {A : Set a} (_≈_ : A → A → Set a) (≈-equiv : IsEquivalence A _≈_) (_R_ : A → A → Set a) (R-≈-cong : ∀ {a₁ a₁' a₂ a₂'} → a₁ ≈ a₁' → a₂ ≈ a₂' → a₁ R a₂ → a₁' R a₂') where

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.

From Chain.agda, lines 19 through 21
 19 20 21   data Chain : A → A → ℕ → Set a where done : ∀ {a a' : A} → a ≈ a' → Chain a a' 0 step : ∀ {a₁ a₂ a₂' a₃ : A} {n : ℕ} → a₁ R a₂ → a₂ ≈ a₂' → Chain a₂' a₃ n → Chain a₁ a₃ (suc n)

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 be bounded by a certain height; simply put, all chains must have length less than or equal to the bound.

From Chain.agda, lines 38 through 39
 38 39   Bounded : ℕ → Set a Bounded bound = ∀ {a₁ a₂ : A} {n : ℕ} → Chain a₁ a₂ n → n ≤ bound

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 (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). 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.

From Chain.agda, lines 47 through 53
 47 48 49 50 51 52 53   record Height (height : ℕ) : Set a where field ⊥ : A ⊤ : A longestChain : Chain ⊥ ⊤ height bounded : Bounded height

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.

From Lattice.agda, lines 183 through 210
 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210  record IsLattice {a} (A : Set a) (_≈_ : A → A → Set a) (_⊔_ : A → A → A) (_⊓_ : A → A → A) : Set a where field joinSemilattice : IsSemilattice A _≈_ _⊔_ meetSemilattice : IsSemilattice A _≈_ _⊓_ absorb-⊔-⊓ : (x y : A) → (x ⊔ (x ⊓ y)) ≈ x absorb-⊓-⊔ : (x y : A) → (x ⊓ (x ⊔ y)) ≈ x open IsSemilattice joinSemilattice public open IsSemilattice meetSemilattice public using () renaming ( ⊔-assoc to ⊓-assoc ; ⊔-comm to ⊓-comm ; ⊔-idemp to ⊓-idemp ; ⊔-Monotonicˡ to ⊓-Monotonicˡ ; ⊔-Monotonicʳ to ⊓-Monotonicʳ ; ≈-⊔-cong to ≈-⊓-cong ; _≼_ to _≽_ ; _≺_ to _≻_ ; ≼-refl to ≽-refl ; ≼-trans to ≽-trans ) FixedHeight : ∀ (h : ℕ) → Set a FixedHeight h = Chain.Height (_≈_) ≈-equiv _≺_ ≺-cong h

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 — 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.
From AboveBelow.agda, lines 315 through 335
 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335   ⊥≺[x] : ∀ (x : A) → ⊥ ≺ [ x ] ⊥≺[x] x = (≈-refl , λ ()) x≺[y]⇒x≡⊥ : ∀ (x : AboveBelow) (y : A) → x ≺ [ y ] → x ≡ ⊥ x≺[y]⇒x≡⊥ x y ((x⊔[y]≈[y]) , x̷≈[y]) with x ... | ⊥ = refl ... | ⊤ with () ← x⊔[y]≈[y] ... | [ b ] with ≈₁-dec b y ... | yes b≈y = ⊥-elim (x̷≈[y] (≈-lift b≈y)) ... | no _ with () ← x⊔[y]≈[y] [x]≺⊤ : ∀ (x : A) → [ x ] ≺ ⊤ [x]≺⊤ x rewrite x⊔⊤≡⊤ [ x ] = (≈-⊤-⊤ , λ ()) [x]≺y⇒y≡⊤ : ∀ (x : A) (y : AboveBelow) → [ x ] ≺ y → y ≡ ⊤ [x]≺y⇒y≡⊤ x y ([x]⊔y≈y , [x]̷≈y) with y ... | ⊥ with () ← [x]⊔y≈y ... | ⊤ = refl ... | [ a ] with ≈₁-dec x a ... | yes x≈a = ⊥-elim ([x]̷≈y (≈-lift x≈a)) ... | no _ with () ← [x]⊔y≈y

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

From AboveBelow.agda, line 85
 85  module Plain (x : A) where

I use this witness to construct the two-< chain.

From AboveBelow.agda, lines 339 through 340
 339 340   longestChain : Chain ⊥ ⊤ 2 longestChain = step (⊥≺[x] x) ≈-refl (step ([x]≺⊤ x) ≈-⊤-⊤ (done ≈-⊤-⊤))

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).
From AboveBelow.agda, lines 342 through 355
 342 343 344 345 346 347 348 349 350 351 352 353 354 355   ¬-Chain-⊤ : ∀ {ab : AboveBelow} {n : ℕ} → ¬ Chain ⊤ ab (suc n) ¬-Chain-⊤ {x} (step (⊤⊔x≈x , ⊤̷≈x) _ _) rewrite ⊤⊔x≡⊤ x = ⊥-elim (⊤̷≈x ⊤⊔x≈x) isLongest : ∀ {ab₁ ab₂ : AboveBelow} {n : ℕ} → Chain ab₁ ab₂ n → n ≤ 2 isLongest (done _) = z≤n isLongest (step _ _ (done _)) = s≤s z≤n isLongest (step _ _ (step _ _ (done _))) = s≤s (s≤s z≤n) isLongest {⊤} c@(step _ _ _) = ⊥-elim (¬-Chain-⊤ c) isLongest {[ x ]} (step {_} {y} [x]≺y y≈y' c@(step _ _ _)) rewrite [x]≺y⇒y≡⊤ x y [x]≺y with ≈-⊤-⊤ ← y≈y' = ⊥-elim (¬-Chain-⊤ c) isLongest {⊥} (step {_} {⊥} (_ , ⊥̷≈⊥) _ _) = ⊥-elim (⊥̷≈⊥ ≈-⊥-⊥) isLongest {⊥} (step {_} {⊤} _ ≈-⊤-⊤ c@(step _ _ _)) = ⊥-elim (¬-Chain-⊤ c) isLongest {⊥} (step {_} {[ x ]} _ (≈-lift _) (step [x]≺y y≈z c@(step _ _ _))) rewrite [x]≺y⇒y≡⊤ _ _ [x]≺y with ≈-⊤-⊤ ← y≈z = ⊥-elim (¬-Chain-⊤ c)

Thus, the above-below lattice has a length of two comparisons (or alternatively, three elements).

From AboveBelow.agda, lines 357 through 363
 357 358 359 360 361 362 363   fixedHeight : IsLattice.FixedHeight isLattice 2 fixedHeight = record { ⊥ = ⊥ ; ⊤ = ⊤ ; longestChain = longestChain ; bounded = isLongest }

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

From Prod.agda, lines 115 through 117
 115 116 117  module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) (h₁ h₂ : ℕ) (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where

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’re building 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:

$(a_1, b_1) < (a_2, b_2)$

That works, but we can construct an even longer chain by increasing only one element at a time:

$(a_1, b_1) < (a_1, b_2) < (a_2, b_2)$

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

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.

From Chain.agda, lines 31 through 33
 31 32 33   concat : ∀ {a₁ a₂ a₃ : A} {n₁ n₂ : ℕ} → Chain a₁ a₂ n₁ → Chain a₂ a₃ n₂ → Chain a₁ a₃ (n₁ + n₂) concat (done a₁≈a₂) a₂a₃ = Chain-≈-cong₁ (≈-sym a₁≈a₂) a₂a₃ concat (step a₁Ra a≈a' a'a₂) a₂a₃ = step a₁Ra a≈a' (concat a'a₂ a₂a₃)

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:

From Lattice.agda, lines 226 through 247
 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247  module ChainMapping {a b} {A : Set a} {B : Set b} {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b} {_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B} (slA : IsSemilattice A _≈₁_ _⊔₁_) (slB : IsSemilattice B _≈₂_ _⊔₂_) where open IsSemilattice slA renaming (_≼_ to _≼₁_; _≺_ to _≺₁_; ≈-equiv to ≈₁-equiv; ≺-cong to ≺₁-cong) open IsSemilattice slB renaming (_≼_ to _≼₂_; _≺_ to _≺₂_; ≈-equiv to ≈₂-equiv; ≺-cong to ≺₂-cong) open Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong using () renaming (Chain to Chain₁; step to step₁; done to done₁) open Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong using () renaming (Chain to Chain₂; step to step₂; done to done₂) Chain-map : ∀ (f : A → B) → Monotonic _≼₁_ _≼₂_ f → Injective _≈₁_ _≈₂_ f → f Preserves _≈₁_ ⟶ _≈₂_ → ∀ {a₁ a₂ : A} {n : ℕ} → Chain₁ a₁ a₂ n → Chain₂ (f a₁) (f a₂) n Chain-map f Monotonicᶠ Injectiveᶠ Preservesᶠ (done₁ a₁≈a₂) = done₂ (Preservesᶠ a₁≈a₂) Chain-map f Monotonicᶠ Injectiveᶠ Preservesᶠ (step₁ (a₁≼₁a , a₁̷≈₁a) a≈₁a' a'a₂) = let fa₁≺₂fa = (Monotonicᶠ a₁≼₁a , λ fa₁≈₂fa → a₁̷≈₁a (Injectiveᶠ fa₁≈₂fa)) fa≈fa' = Preservesᶠ a≈₁a' in step₂ fa₁≺₂fa fa≈fa' (Chain-map f Monotonicᶠ Injectiveᶠ Preservesᶠ a'a₂)

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_2)$, 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 $(\top_1, \bot_2)$, and the second starts with it.

From Prod.agda, lines 169 through 171
 169 170 171   ; longestChain = concat (ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁) (ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂)

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 combined lengths 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.

From Prod.agda, line 149
 149   unzip : ∀ {a₁ a₂ : A} {b₁ b₂ : B} {n : ℕ} → Chain (a₁ , b₁) (a₂ , b₂) n → Σ (ℕ × ℕ) (λ (n₁ , n₂) → ((Chain₁ a₁ a₂ n₁ × Chain₂ b₁ b₂ n₂) × (n ≤ n₁ + n₂)))
(Click here for the implementation of unzip)
From Prod.agda, lines 149 through 163
 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163   unzip : ∀ {a₁ a₂ : A} {b₁ b₂ : B} {n : ℕ} → Chain (a₁ , b₁) (a₂ , b₂) n → Σ (ℕ × ℕ) (λ (n₁ , n₂) → ((Chain₁ a₁ a₂ n₁ × Chain₂ b₁ b₂ n₂) × (n ≤ n₁ + n₂))) unzip (done (a₁≈a₂ , b₁≈b₂)) = ((0 , 0) , ((done₁ a₁≈a₂ , done₂ b₁≈b₂) , ≤-refl)) unzip {a₁} {a₂} {b₁} {b₂} {n} (step {(a₁ , b₁)} {(a , b)} ((a₁≼a , b₁≼b) , a₁b₁̷≈ab) (a≈a' , b≈b') a'b'a₂b₂) with ≈₁-dec a₁ a | ≈₂-dec b₁ b | unzip a'b'a₂b₂ ... | yes a₁≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = ⊥-elim (a₁b₁̷≈ab (a₁≈a , b₁≈b)) ... | no a₁̷≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = ((suc n₁ , n₂) , ((step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , Chain₂-≈-cong₁ (≈₂-sym (≈₂-trans b₁≈b b≈b')) c₂), +-monoʳ-≤ 1 (n≤n₁+n₂))) ... | yes a₁≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = ((n₁ , suc n₂) , ( (Chain₁-≈-cong₁ (≈₁-sym (≈₁-trans a₁≈a a≈a')) c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂) , subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂) )) ... | no a₁̷≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = ((suc n₁ , suc n₂) , ( (step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂) , m≤n⇒m≤o+n 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂)) ))

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.

From Prod.agda, lines 165 through 175
 165 166 167 168 169 170 171 172 173 174 175   fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂) fixedHeight = record { ⊥ = (⊥₁ , ⊥₂) ; ⊤ = (⊤₁ , ⊤₂) ; longestChain = concat (ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁) (ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂) ; bounded = λ a₁b₁a₂b₂ → let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂ in ≤-trans n≤n₁+n₂ (+-mono-≤ (bounded₁ a₁a₂) (bounded₂ b₁b₂)) }

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 created 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:

$\overbrace{L_1 \times ... \times L_1}^{n\ \text{times}} \times L_2.$

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.

From IterProd.agda, lines 7 through 11
  7 8 9 10 11  module Lattice.IterProd {a} {A B : Set a} (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a) (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B) (_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B) (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
From IterProd.agda, lines 23 through 24
 23 24  IterProd : ℕ → Set a IterProd k = iterate k (λ t → A × t) B

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 being either finite or infinite. I supported this by defining a helper type:

From IterProd.agda, lines 40 through 55
 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55   record RequiredForFixedHeight : Set (lsuc a) where field ≈₁-dec : IsDecidable _≈₁_ ≈₂-dec : IsDecidable _≈₂_ h₁ h₂ : ℕ fhA : FixedHeight₁ h₁ fhB : FixedHeight₂ h₂ ⊥₁ : A ⊥₁ = Height.⊥ fhA ⊥₂ : B ⊥₂ = Height.⊥ fhB ⊥k : ∀ (k : ℕ) → IterProd k ⊥k = build ⊥₁ ⊥₂

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.

From IterProd.agda, lines 57 through 76
 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76   record IsFiniteHeightWithBotAndDecEq {A : Set a} {_≈_ : A → A → Set a} {_⊔_ : A → A → A} {_⊓_ : A → A → A} (isLattice : IsLattice A _≈_ _⊔_ _⊓_) (⊥ : A) : Set (lsuc a) where field height : ℕ fixedHeight : IsLattice.FixedHeight isLattice height ≈-dec : IsDecidable _≈_ ⊥-correct : Height.⊥ fixedHeight ≡ ⊥ record Everything (k : ℕ) : Set (lsuc a) where T = IterProd k field _≈_ : T → T → Set a _⊔_ : T → T → T _⊓_ : T → T → T isLattice : IsLattice T _≈_ _⊔_ _⊓_ isFiniteHeightIfSupported : ∀ (req : RequiredForFixedHeight) → IsFiniteHeightWithBotAndDecEq isLattice (RequiredForFixedHeight.⊥k req k)

Finally, the proof by induction. It’s actually relatively long, so I’ll include it as a collapsible block.

From IterProd.agda, lines 78 through 120
  78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120   everything : ∀ (k : ℕ) → Everything k everything 0 = record { _≈_ = _≈₂_ ; _⊔_ = _⊔₂_ ; _⊓_ = _⊓₂_ ; isLattice = lB ; isFiniteHeightIfSupported = λ req → record { height = RequiredForFixedHeight.h₂ req ; fixedHeight = RequiredForFixedHeight.fhB req ; ≈-dec = RequiredForFixedHeight.≈₂-dec req ; ⊥-correct = refl } } everything (suc k') = record { _≈_ = P._≈_ ; _⊔_ = P._⊔_ ; _⊓_ = P._⊓_ ; isLattice = P.isLattice ; isFiniteHeightIfSupported = λ req → let fhlRest = Everything.isFiniteHeightIfSupported everythingRest req in record { height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightWithBotAndDecEq.height fhlRest ; fixedHeight = P.fixedHeight (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest) (RequiredForFixedHeight.h₁ req) (IsFiniteHeightWithBotAndDecEq.height fhlRest) (RequiredForFixedHeight.fhA req) (IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest) ; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest) ; ⊥-correct = cong ((Height.⊥ (RequiredForFixedHeight.fhA req)) ,_) (IsFiniteHeightWithBotAndDecEq.⊥-correct fhlRest) } } where everythingRest = everything k' import Lattice.Prod _≈₁_ (Everything._≈_ everythingRest) _⊔₁_ (Everything._⊔_ everythingRest) _⊓₁_ (Everything._⊓_ everythingRest) lA (Everything.isLattice everythingRest) as P

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

$\begin{array}{cccccc} \{ & a: 1, & b: 2, & c: 3, & \} \\ & & \iff & & \\ ( & 1, & 2, & 3 & ) \end{array}$

This is why I introduced 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. Using this padding helps reduce the number of special cases; without the adding, the tuple definition might be something like the following:

$\text{tup}(A, k) = \begin{cases} \top & k = 0 \\ A & k = 1 \\ A \times \text{tup}(A, k - 1) & k > 1 \end{cases}$

On the other hand, if we were to allow the extra padding, we could drop the definition down to:

$\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}$

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 and maps). 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: a pair of functions that convert between the two representations, and preserve the properties and relationships (such as $(\sqcup)$) of lattice elements. In fact, the list of the conversion functions’ properties is quite extensive:

From Isomorphism.agda, lines 22 through 33
 22 23 24 25 26 27 28 29 30 31 32 33  module TransportFiniteHeight {a b : Level} {A : Set a} {B : Set b} {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b} {_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B} {_⊓₁_ : A → A → A} {_⊓₂_ : B → B → B} {height : ℕ} (fhlA : IsFiniteHeightLattice A height _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) {f : A → B} {g : B → A} (f-preserves-≈₁ : f Preserves _≈₁_ ⟶ _≈₂_) (g-preserves-≈₂ : g Preserves _≈₂_ ⟶ _≈₁_) (f-⊔-distr : ∀ (a₁ a₂ : A) → f (a₁ ⊔₁ a₂) ≈₂ ((f a₁) ⊔₂ (f a₂))) (g-⊔-distr : ∀ (b₁ b₂ : B) → g (b₁ ⊔₂ b₂) ≈₁ ((g b₁) ⊔₁ (g b₂))) (inverseˡ : IsInverseˡ _≈₁_ _≈₂_ f g) (inverseʳ : IsInverseʳ _≈₁_ _≈₂_ f g) where
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. Specifically, if $f$ is a conversion function, then the following should hold:

$f(a \sqcup b) \approx f(a) \sqcup f(b)$

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 a 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)$ given by Lars Hupel, which in brief is $a \leq b \triangleq a \sqcup b = b$):

$\begin{array}{rcr} a \leq b & \iff & (\text{definition of less than})\\ a \sqcup b \approx b & \implies & (\text{conversions preserve equivalence}) \\ 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) \leq f(b) \end{array}$
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:

From Isomorphism.agda, lines 52 through 64
 52 53 54 55 56 57 58 59 60 61 62 63 64   f-preserves-̷≈ : f Preserves (λ x y → ¬ x ≈₁ y) ⟶ (λ x y → ¬ x ≈₂ y) f-preserves-̷≈ x̷≈y = λ fx≈fy → x̷≈y (f-Injective fx≈fy) g-preserves-̷≈ : g Preserves (λ x y → ¬ x ≈₂ y) ⟶ (λ x y → ¬ x ≈₁ y) g-preserves-̷≈ x̷≈y = λ gx≈gy → x̷≈y (g-Injective gx≈gy) portChain₁ : ∀ {a₁ a₂ : A} {h : ℕ} → Chain₁ a₁ a₂ h → Chain₂ (f a₁) (f a₂) h portChain₁ (done₁ a₁≈a₂) = done₂ (f-preserves-≈₁ a₁≈a₂) portChain₁ (step₁ {a₁} {a₂} (a₁≼a₂ , a₁̷≈a₂) a₂≈a₂' c) = step₂ (≈₂-trans (≈₂-sym (f-⊔-distr a₁ a₂)) (f-preserves-≈₁ a₁≼a₂) , f-preserves-̷≈ a₁̷≈a₂) (f-preserves-≈₁ a₂≈a₂') (portChain₁ c) portChain₂ : ∀ {b₁ b₂ : B} {h : ℕ} → Chain₂ b₁ b₂ h → Chain₁ (g b₁) (g b₂) h portChain₂ (done₂ a₂≈a₁) = done₁ (g-preserves-≈₂ a₂≈a₁) portChain₂ (step₂ {b₁} {b₂} (b₁≼b₂ , b₁̷≈b₂) b₂≈b₂' c) = step₁ (≈₁-trans (≈₁-sym (g-⊔-distr b₁ b₂)) (g-preserves-≈₂ b₁≼b₂) , g-preserves-̷≈ b₁̷≈b₂) (g-preserves-≈₂ b₂≈b₂') (portChain₂ c)

With that, we can prove the second lattice’s finite height:

From Isomorphism.agda, lines 66 through 80
 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80   isFiniteHeightLattice : IsFiniteHeightLattice B height _≈₂_ _⊔₂_ _⊓₂_ isFiniteHeightLattice = let open Chain.Height (IsFiniteHeightLattice.fixedHeight fhlA) using () renaming (⊥ to ⊥₁; ⊤ to ⊤₁; bounded to bounded₁; longestChain to c) in record { isLattice = lB ; fixedHeight = record { ⊥ = f ⊥₁ ; ⊤ = f ⊤₁ ; longestChain = portChain₁ c ; bounded = λ c' → bounded₁ (portChain₂ c') } }

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.

From FiniteValueMap.agda, lines 68 through 85
 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85   from : ∀ {ks : List A} → FiniteMap ks → IterProd (length ks) from {[]} (([] , _) , _) = tt from {k ∷ ks'} (((k' , v) ∷ fm' , push _ uks') , refl) = (v , from ((fm' , uks'), refl)) to : ∀ {ks : List A} → Unique ks → IterProd (length ks) → FiniteMap ks to {[]} _ ⊤ = (([] , empty) , refl) to {k ∷ ks'} (push k≢ks' uks') (v , rest) = let ((fm' , ufm') , fm'≡ks') = to uks' rest -- This would be easier if we pattern matched on the equiality proof -- to get refl, but that makes it harder to reason about 'to' when -- the arguments are not known to be refl. k≢fm' = subst (λ ks → All (λ k' → ¬ k ≡ k') ks) (sym fm'≡ks') k≢ks' kvs≡ks = cong (k ∷_) fm'≡ks' in (((k , v) ∷ fm' , push k≢fm' ufm') , kvs≡ks)

Above, FiniteValueMap ks is the type of maps whose keys are fixed to ks; defined as follows:

From FiniteMap.agda, lines 58 through 60
 58 59 60  module WithKeys (ks : List A) where FiniteMap : Set (a ⊔ℓ b) FiniteMap = Σ Map (λ m → Map.keys m ≡ ks)

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

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

From Unit.agda, lines 6 through 7
 6 7  open import Data.Unit using (⊤; tt) public open import Data.Unit.Properties using (_≟_; ≡-setoid)

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).

From Unit.agda, lines 17 through 25
 17 18 19 20 21 22 23 24 25  _≈_ : ⊤ → ⊤ → Set _≈_ = _≡_ ≈-equiv : IsEquivalence ⊤ _≈_ ≈-equiv = record { ≈-refl = refl ; ≈-sym = sym ; ≈-trans = trans }

Both the join $(\sqcup)$ and meet $(\sqcap)$ operations are trivially defined; in both cases, they simply take two tts and produce a new tt. Mathematically, one might write this as $(\text{tt}, \text{tt}) \mapsto \text{tt}$. In Agda:

From Unit.agda, lines 30 through 34
 30 31 32 33 34  _⊔_ : ⊤ → ⊤ → ⊤ tt ⊔ tt = tt _⊓_ : ⊤ → ⊤ → ⊤ tt ⊓ tt = tt

These operations are trivially associative, commutative, and idempotent.

From Unit.agda, lines 39 through 46
 39 40 41 42 43 44 45 46  ⊔-assoc : (x y z : ⊤) → ((x ⊔ y) ⊔ z) ≈ (x ⊔ (y ⊔ z)) ⊔-assoc tt tt tt = Eq.refl ⊔-comm : (x y : ⊤) → (x ⊔ y) ≈ (y ⊔ x) ⊔-comm tt tt = Eq.refl ⊔-idemp : (x : ⊤) → (x ⊔ x) ≈ x ⊔-idemp tt = Eq.refl

That’s sufficient for them to be semilattices:

From Unit.agda, lines 48 through 54
 48 49 50 51 52 53 54  isJoinSemilattice : IsSemilattice ⊤ _≈_ _⊔_ isJoinSemilattice = record { ≈-equiv = ≈-equiv ; ≈-⊔-cong = ≈-⊔-cong ; ⊔-assoc = ⊔-assoc ; ⊔-comm = ⊔-comm ; ⊔-idemp = ⊔-idemp

The absorption laws are also trivially satisfied, which means that the unit type forms a lattice.

From Unit.agda, lines 78 through 90
 78 79 80 81 82 83 84 85 86 87 88 89 90  absorb-⊔-⊓ : (x y : ⊤) → (x ⊔ (x ⊓ y)) ≈ x absorb-⊔-⊓ tt tt = Eq.refl absorb-⊓-⊔ : (x y : ⊤) → (x ⊓ (x ⊔ y)) ≈ x absorb-⊓-⊔ tt tt = Eq.refl isLattice : IsLattice ⊤ _≈_ _⊔_ _⊓_ isLattice = record { joinSemilattice = isJoinSemilattice ; meetSemilattice = isMeetSemilattice ; absorb-⊔-⊓ = absorb-⊔-⊓ ; absorb-⊓-⊔ = absorb-⊓-⊔ }

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.

From Unit.agda, lines 102 through 117
 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116  private longestChain : Chain tt tt 0 longestChain = done refl isLongest : ∀ {t₁ t₂ : ⊤} {n : ℕ} → Chain t₁ t₂ n → n ≤ 0 isLongest {tt} {tt} (step (tt⊔tt≈tt , tt̷≈tt) _ _) = ⊥-elim (tt̷≈tt refl) isLongest (done _) = z≤n fixedHeight : IsLattice.FixedHeight isLattice 0 fixedHeight = record { ⊥ = tt ; ⊤ = tt ; longestChain = longestChain ; bounded = isLongest }