1.4 KiB
title, series, date, draft
| title | series | date | draft |
|---|---|---|---|
| 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 |
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.