---
title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 2: Combining Lattices"
series: "Static Program Analysis in Agda"
date: 2024-04-13T14:23:03-07:01
draft: true
tags: ["Agda", "Programming Languages"]
---

In the previous post, I wrote about how lattices arise when tracking, comparing
and combining static information about programs. I then showed two simple lattices:
the natural numbers, and the (parameterized) "above-below" lattice, which
modified an arbitrary set with "bottom" and "top" elements (\(\bot\) and \(\top\)
respectively). One instance of the "above-below" lattice was the sign lattice,
which could be used to reason about the signs (positive, negative, or zero)
of variables in a program.

At the end of that post, I introduced a source of complexity: the "full"
lattices that we want to use for the program analysis aren't signs or numbers,
but maps of states and variables to lattices-based states. The full lattice
for sign analysis might something in the form:

{{< latex >}}
\text{Info} \triangleq \text{ProgramStates} \to (\text{Variables} \to \text{Sign})
{{< /latex >}}

Thus, we have to compare and find least upper bounds (e.g.) of not just
signs, but maps! Proving the various lattice laws for signs was not too
challenging, but for for a two-level map like \(\text{info}\) above, we'd
need to do a lot more work. We need tools to build up such complicated lattices!

The way to do this, it turns out, is by using simpler lattices as building blocks.
To start with, let's take a look at a very simple way of combining lattices:
taking the Cartesian product.

### The Cartesian Product Lattice

Suppose you have two lattices \(L_1\) and \(L_2\). As I covered in the previous
post, each lattice comes equipped with a "least upper bound" operator \((\sqcup)\)
and a "greatest lower bound" operator \((\sqcap)\). Since we now have two lattices,
let's use numerical suffixes to disambiguate between the operators
of the first and second lattice: \((\sqcup_1)\) will be the LUB operator of
the first lattice \(L_1\), and \((\sqcup_2)\) of the second lattice \(L_2\).

Then, let's take the Cartesian product of the elements of \(L_1\) and \(L_2\);
mathematically, we'll write this as \(L_1 \times L_2\), and in Agda, we can
just use the standard [`Data.Product`](https://agda.github.io/agda-stdlib/master/Data.Product.html)
module. In Agda, I'll define the lattice as another [parameterized module](https://agda.readthedocs.io/en/latest/language/module-system.html#parameterised-modules). Since both \(L_1\) and \(L_2\)
are lattices, this parameterized module will require `IsLattice` instances
for both types:

{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 1 7 >}}

Elements of \(L_1 \times L_2\) are in the form \((l_1, l_2)\), where
\(l_1 \in L_1\) and \(l_2 \in L_2\). The first thing we can get out of the
way is define what it means for two such elements to be equal. That's easy
enough: we have an equality predicate `_≈₁_` that checks if an element
of \(L_1\) is equal to another, and we have `_≈₂_` that does the same for \(L_2\).
It's reasonably to say that _pairs_ of elements are equal if their respective
first and second elements are equal:

{{< latex >}}
  (l_1, l_2) \approx (j_1, j_2) \iff l_1 \approx_1 j_1 \land l_2 \approx_2 j_2
{{< /latex >}}

In Agda:

{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 39 40 >}}