blog-static/content/blog/02_spa_agda_combining_lattices.md
Danila Fedorin 04f12b545d Minor edits to 'lattices 2'
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-25 20:45:19 -07:00

5.2 KiB

title series date draft tags
Implementing and Verifying "Static Program Analysis" in Agda, Part 2: Combining Lattices Static Program Analysis in Agda 2024-04-13T14:23:03-07:01 true
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 lattice-based descriptions. 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, and so on.

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 module. Then, I'll define the lattice as another parameterized module. 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 defining what it means for two such elements to be equal. Recall that we opted for a [custom equivalence relation]({{< relref "01_spa_agda_lattices#definitional-equality" >}}) instead of definitional equality to allow similar elements to be considered equal; we'll have to define a similar relation for our new product lattice. 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 reasonable 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 >}}

Verifying that this relation has the properties of an equivalence relation boils down to the fact that _≈₁_ and _≈₂_ are themselves equivalence relations.

{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 42 48 >}}

Defining (\sqcup) and (\sqcap) by simply applying the corresponding operators from L_1 and L_2 seems quite natural as well.

{{< latex >}} (l_1, l_2) \sqcup (j_1, j_2) \triangleq (l_1 \sqcup_1 j_1, l_2 \sqcup_2 j_2) \ (l_1, l_2) \sqcap (j_1, j_2) \triangleq (l_1 \sqcap_1 j_1, l_2 \sqcap_2 j_2) {{< /latex >}}

In Agda:

{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 50 54 >}}

All that's left is to prove the various (semi)lattice properties. Intuitively, we can see that since the "combined" operator _⊔_ just independently applies the element operators _⊔₁_ and _⊔₂_, as long as they are idempotent, commutative, and associative, so is the "combined" operator itself. Moreover, the proofs that _⊔_ and _⊓_ form semilattices are identical up to replacing (\sqcup) with (\sqcap). Thus, in Agda, we can write the code once, parameterizing it by the binary operators involved (and proofs that these operators obey the semilattice laws).

{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 56 82 >}}

Above, I used f₁ to stand for "either _⊔₁_ or _⊓₁_", and similarly f₂ for "either _⊔₂_ or _⊓₂_". Much like the semilattice properties, proving lattice properties boils down to applying the lattice properties of L_1 and L_2 to individual components.

{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 84 96 >}}