Tie up Lattices (1), and plan to write Lattices (2)

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-19 22:29:24 -07:00
parent d787548915
commit 9d31764073

View File

@ -463,7 +463,7 @@ and instantiate the `AboveBelow` module:
{{< codelines "Agda" "agda-spa/Analysis/Sign.agda" 34 47 >}}
### Making Lattices out of Lattices
### From Simple Lattices to Complex Ones
Natural numbers and signs alone are cool enough, but they will not be sufficient
to write program analyzers. That's because when we're writing an analyzer,
@ -490,3 +490,4 @@ maps, and how do we define the \((\sqcup)\) and \((\sqcap)\) operations?
The solution turns out to be to define ways in which simpler lattices
(like our sign) can be combined and transformed to define more complex lattices.
We'll move on to that in the next post of this series.