Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Edit and publish part 2

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-08-08 16:45:13 -07:00
parent ecad4541f6
commit 21b2ff208e
1 changed files with 12 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
content/blog/02_spa_agda_combining_lattices.md
View File

@ -2,8 +2,7 @@
title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 2: Combining Lattices" title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 2: Combining Lattices"
series: "Static Program Analysis in Agda" series: "Static Program Analysis in Agda"
description: "In this post, I describe how lattices can be combined to create other, more complex lattices" description: "In this post, I describe how lattices can be combined to create other, more complex lattices"
date: 2024-07-06T17:37:44-07:00 date: 2024-08-08T16:40:00-07:00
draft: true
tags: ["Agda", "Programming Languages"] tags: ["Agda", "Programming Languages"]
--- ---
@ -30,8 +29,8 @@ 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. 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. 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: To start with, let's take a look at a very simple way of combining lattices
taking the [Cartesian product](https://mathworld.wolfram.com/CartesianProduct.html). into a new one: taking the [Cartesian product](https://mathworld.wolfram.com/CartesianProduct.html).
### The Cartesian Product Lattice ### The Cartesian Product Lattice
@ -50,11 +49,11 @@ module. Then, I'll define the lattice as another [parameterized module](https://
are lattices, this parameterized module will require `IsLattice` instances are lattices, this parameterized module will require `IsLattice` instances
for both types: for both types:
{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 1 7 >}} {{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 1 7 "hl_lines=7" >}}
Elements of \(L_1 \times L_2\) are in the form \((l_1, l_2)\), where 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 \(l_1 \in L_1\) and \(l_2 \in L_2\). Knowing that, let's define what it means
way is defining what it means for two such elements to be equal. Recall that for two such elements to be equal. Recall that
we opted for a [custom equivalence relation]({{< relref "01_spa_agda_lattices#definitional-equality" >}}) 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 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. equal; we'll have to define a similar relation for our new product lattice.
@ -122,7 +121,7 @@ two other lattices. If we have a type of analysis that can be expressed as
Perhaps the signs are the smallest and largest possible values of a variable. Perhaps the signs are the smallest and largest possible values of a variable.
{{< /sidenote >}} for example, we won't have to do all the work of {{< /sidenote >}} for example, we won't have to do all the work of
proving the (semi)lattice properties of those pairs. In fact, we can build up proving the (semi)lattice properties of those pairs. In fact, we can build up
even bigger data structures. By taking a product a product twice, like even bigger data structures. By taking a product twice, like
\(L_1 \times (L_2 \times L_3)\), we can construct a lattice of 3-tuples. Any \(L_1 \times (L_2 \times L_3)\), we can construct a lattice of 3-tuples. Any
of the lattices involved in that product can itself be a product; we can of the lattices involved in that product can itself be a product; we can
therefore create lattices out of arbitrary bundles of data, so long as therefore create lattices out of arbitrary bundles of data, so long as
@ -196,7 +195,7 @@ requires that each key in the smaller map be present in the larger one; as
a result, \(m_1 \sqcup m_2\) should contain all the keys in \(m_1\) __and__ a result, \(m_1 \sqcup m_2\) should contain all the keys in \(m_1\) __and__
all the keys in \(m_2\). So, we could just take the union of the two maps: all the keys in \(m_2\). So, we could just take the union of the two maps:
copy values from both into the result. Only, what happens if both \(m_1\) copy values from both into the result. Only, what happens if both \(m_1\)
and \(m_2\) have a value mapped to a particular key? The values in the two and \(m_2\) have a value mapped to a particular key \(k\)? The values in the two
maps could be distinct, and they might even be incomparable. This is where the maps could be distinct, and they might even be incomparable. This is where the
second part of the condition kicks in: the value in the combination of the second part of the condition kicks in: the value in the combination of the
maps needs to be bigger than the value in either sub-map. We already know how maps needs to be bigger than the value in either sub-map. We already know how
@ -248,7 +247,7 @@ on values.
{{< /latex >}} {{< /latex >}}
Turning once again to set theory, we can think of this operation like the Turning once again to set theory, we can think of this operation like the
extension of the intersection operator \((\cup)\) to maps. This can be extension of the intersection operator \((\cap)\) to maps. This can be
motivated in the same way as the union operation above; the \((\sqcap)\) motivated in the same way as the union operation above; the \((\sqcap)\)
operator combines lattice elements in such away that the result represents operator combines lattice elements in such away that the result represents
both of them, and intersections of sets contain elements that are in __both__ both of them, and intersections of sets contain elements that are in __both__
@ -269,6 +268,9 @@ transliteration:
{{< codelines "Agda" "agda-spa/Lattice/Map.agda" 530 531 >}} {{< codelines "Agda" "agda-spa/Lattice/Map.agda" 530 531 >}}
Defining equivalence more abstractly this way helps avoid concerns about the
precise implementation of our maps.
Okay, but we haven't actually defined what it means for one map to be a subset Okay, but we haven't actually defined what it means for one map to be a subset
of another. My definition is as follows: if \(m_1 \subseteq m_2\), that is, of another. My definition is as follows: if \(m_1 \subseteq m_2\), that is,
if \(m_1\) is a subset of \(m_2\), then every key in \(m_1\) is also present if \(m_1\) is a subset of \(m_2\), then every key in \(m_1\) is also present