From 58e7a1f2dc89c6d85dd40b2e0f525be47f158ea7 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 20 May 2024 21:39:03 -0700 Subject: [PATCH] Start on a draft of 'combining lattices' Signed-off-by: Danila Fedorin --- .../blog/02_spa_agda_combining_lattices.md | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 content/blog/02_spa_agda_combining_lattices.md diff --git a/content/blog/02_spa_agda_combining_lattices.md b/content/blog/02_spa_agda_combining_lattices.md new file mode 100644 index 0000000..44292ea --- /dev/null +++ b/content/blog/02_spa_agda_combining_lattices.md @@ -0,0 +1,30 @@ +--- +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 +--- + +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.