From 9d31764073984e1e30d7c042dfbda9a3caf1e425 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 19 May 2024 22:29:24 -0700 Subject: [PATCH] Tie up Lattices (1), and plan to write Lattices (2) Signed-off-by: Danila Fedorin --- content/blog/01_spa_agda_lattices.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/content/blog/01_spa_agda_lattices.md b/content/blog/01_spa_agda_lattices.md index bca1cab..5535d98 100644 --- a/content/blog/01_spa_agda_lattices.md +++ b/content/blog/01_spa_agda_lattices.md @@ -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.