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

Compare commits

base: Web-Projects:7c65afbc934c1b46239bd25e0c8989f0012d9499
Branches Tags
Web-Projects:master
Web-Projects:donations
Web-Projects:search
Web-Projects:localization
Web-Projects:colors
Web-Projects:table-of-contents
Web-Projects:margin-rework
Web-Projects:sidenotes
..
compare: Web-Projects:292cf009e66e96107f5e2eccb24f04c0ac9a6481
Branches Tags
Web-Projects:master
Web-Projects:donations
Web-Projects:search
Web-Projects:localization
Web-Projects:colors
Web-Projects:table-of-contents
Web-Projects:margin-rework
Web-Projects:sidenotes

No commits in common. "7c65afbc934c1b46239bd25e0c8989f0012d9499" and "292cf009e66e96107f5e2eccb24f04c0ac9a6481" have entirely different histories.
7c65afbc93 ... 292cf009e6

4 changed files with 20 additions and 20 deletions
Show Stats Expand all files Collapse all files

2
content/blog/01_spa_agda_lattices.md
View File

@ -138,7 +138,7 @@ Moreover, the value we'll get out of the fixed point algorithm will be
the _least fixed point_. For us, this means that the result will be the _least fixed point_. For us, this means that the result will be
"the most specific result possible". "the most specific result possible".
{{< codelines "Agda" "agda-spa/Fixedpoint.agda" 86 86 >}} {{< codelines "Agda" "agda-spa/Fixedpoint.agda" 80 80 >}}
The above explanation omits a lot of details, but it's a start. To get more The above explanation omits a lot of details, but it's a start. To get more
precise, we must drill down into several aspects of what I've said so far. precise, we must drill down into several aspects of what I've said so far.

34
content/blog/03_spa_agda_fixed_height.md
View File

@ -125,7 +125,7 @@ we could take the previous natural number, and it would be a bound as well).
Thus, I define the `Height` predicate to require that a chain of the desired Thus, I define the `Height` predicate to require that a chain of the desired
height exists, and that this height bounds the length of all other chains. height exists, and that this height bounds the length of all other chains.
{{< codelines "agda" "agda-spa/Chain.agda" 47 53 >}} {{< codelines "agda" "agda-spa/Chain.agda" 47 48 >}}
Finally, for a lattice to have a finite height, the type of chains formed by using Finally, for a lattice to have a finite height, the type of chains formed by using
its less-than operator needs to have that height (satisfy the `Height h` predicate). its less-than operator needs to have that height (satisfy the `Height h` predicate).
@ -133,7 +133,7 @@ To avoid having to thread through the equivalence relation, congruence proof,
and more, I define a specialized predicate for lattices specifically. and more, I define a specialized predicate for lattices specifically.
I do so as a "method" in my `IsLattice` record. I do so as a "method" in my `IsLattice` record.
{{< codelines "agda" "agda-spa/Lattice.agda" 183 210 "hl_lines = 27 28">}} {{< codelines "agda" "agda-spa/Lattice.agda" 153 180 "hl_lines = 27 28">}}
Thus, bringing the operators and other definitions of `IsLattice` into scope Thus, bringing the operators and other definitions of `IsLattice` into scope
will also bring in the `FixedHeight` predicate. will also bring in the `FixedHeight` predicate.
@ -192,7 +192,7 @@ three or more comparisons.
Thus, the above-below lattice has a length of two comparisons (or alternatively, Thus, the above-below lattice has a length of two comparisons (or alternatively,
three elements). three elements).
{{< codelines "agda" "agda-spa/Lattice/AboveBelow.agda" 357 363 >}} {{< codelines "agda" "agda-spa/Lattice/AboveBelow.agda" 357 358 >}}
And that's it. And that's it.
@ -262,7 +262,7 @@ be collapsed into \(f(a) \not< f(a)\), changing its length. Finally,
the function needs to produce equivalent outputs when giving equivalent inputs. the function needs to produce equivalent outputs when giving equivalent inputs.
The result is the following lemma: The result is the following lemma:
{{< codelines "agda" "agda-spa/Lattice.agda" 226 247 >}} {{< codelines "agda" "agda-spa/Lattice.agda" 196 217 >}}
Given this, and two lattices of finite height, we construct the full product Given this, and two lattices of finite height, we construct the full product
chain by lifting the `A` chain into the product via \(a \mapsto (a, \bot_2)\), chain by lifting the `A` chain into the product via \(a \mapsto (a, \bot_2)\),
@ -270,7 +270,7 @@ lifting the `B` chain into the product via \(b \mapsto (\top_1, b)\), and
concatenating the results. This works because the first chain ends with concatenating the results. This works because the first chain ends with
\((\top_1, \bot_2)\), and the second starts with it. \((\top_1, \bot_2)\), and the second starts with it.
{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 169 171 >}} {{< codelines "agda" "agda-spa/Lattice/Prod.agda" 177 179 >}}
This gets us the longest chain; what remains is to prove that this chain's This gets us the longest chain; what remains is to prove that this chain's
length is the bound of all other changes. To do so, we need to work in length is the bound of all other changes. To do so, we need to work in
@ -292,15 +292,15 @@ and will put the implementation in a collapsible detail block. One last
detail is that the need to decide which chain to grow --- and thus which element detail is that the need to decide which chain to grow --- and thus which element
has increased --- is what introduces the need for decidable equality. has increased --- is what introduces the need for decidable equality.
{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 149 149 >}} {{< codelines "agda" "agda-spa/Lattice/Prod.agda" 158 158 >}}
{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 149 163 "" "**(Click here for the implementation of `unzip`)**" >}} {{< codelines "agda" "agda-spa/Lattice/Prod.agda" 158 172 "" "**(Click here for the implementation of `unzip`)**" >}}
Having decomposed the product chain into constituent chains, we simply combine Having decomposed the product chain into constituent chains, we simply combine
the facts that they have to be bounded by the height of the `A` and `B` lattices, the facts that they have to be bounded by the height of the `A` and `B` lattices,
as well as the fact that they bound the combined chain. as well as the fact that they bound the combined chain.
{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 165 175 "hl_lines = 8-10" >}} {{< codelines "agda" "agda-spa/Lattice/Prod.agda" 174 183 "hl_lines = 8-9" >}}
This completes the proof! This completes the proof!
@ -326,7 +326,7 @@ lattices as input.
{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 7 11 >}} {{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 7 11 >}}
{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 23 24 >}} {{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 21 22 >}}
At a high level, the proof goes by induction on the number of applications At a high level, the proof goes by induction on the number of applications
of the product. There's just one trick. I'd like to build up an `isLattice` of the product. There's just one trick. I'd like to build up an `isLattice`
@ -347,18 +347,18 @@ To build up with the lattice instance and --- if possible --- the finite height
instance, I needed to allow for the constituent lattices being either finite instance, I needed to allow for the constituent lattices being either finite
or infinite. I supported this by defining a helper type: or infinite. I supported this by defining a helper type:
{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 40 55 >}} {{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 34 40 >}}
Then, I defined the "everything at once" type, in which, instead of Then, I defined the "everything at once" type, in which, instead of
a field for the proof of finite height, has a field that constructs a field for the proof of finite height, has a field that constructs
this proof _if the necessary additional information is present_. this proof _if the necessary additional information is present_.
{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 57 76 >}} {{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 42 55 >}}
Finally, the proof by induction. It's actually relatively long, so I'll Finally, the proof by induction. It's actually relatively long, so I'll
include it as a collapsible block. include it as a collapsible block.
{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 78 120 "" "**(Click here to expand the inductive proof)**" >}} {{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 57 95 "" "**(Click here to expand the inductive proof)**" >}}
### Fixed Height of the Map Lattice ### Fixed Height of the Map Lattice
@ -472,11 +472,11 @@ As you can tell, the chain porting mechanism is doing the heavy lifting here.
It's relatively easy to implement given the conditions we've set on It's relatively easy to implement given the conditions we've set on
conversion functions, in both directions: conversion functions, in both directions:
{{< codelines "agda" "agda-spa/Isomorphism.agda" 52 64 >}} {{< codelines "agda" "agda-spa/Isomorphism.agda" 51 63 >}}
With that, we can prove the second lattice's finite height: With that, we can prove the second lattice's finite height:
{{< codelines "agda" "agda-spa/Isomorphism.agda" 66 80 >}} {{< codelines "agda" "agda-spa/Isomorphism.agda" 65 72 >}}
The conversion functions are also not too difficult to define. I give The conversion functions are also not too difficult to define. I give
@ -485,12 +485,12 @@ properties (such as the fact that `from` and `to` are inverses, preserve
equivalence, and distribute over join) here. You can view them by clicking equivalence, and distribute over join) here. You can view them by clicking
the link at the top of the code block below. the link at the top of the code block below.
{{< codelines "agda" "agda-spa/Lattice/FiniteValueMap.agda" 68 85 >}} {{< codelines "agda" "agda-spa/Lattice/FiniteValueMap.agda" 67 84 >}}
Above, `FiniteValueMap ks` is the type of maps whose keys are fixed to Above, `FiniteValueMap ks` is the type of maps whose keys are fixed to
`ks`; defined as follows: `ks`; defined as follows:
{{< codelines "agda" "agda-spa/Lattice/FiniteMap.agda" 58 60 >}} {{< codelines "agda" "agda-spa/Lattice/FiniteMap.agda" 50 52 >}}
Proving the remaining properties (which as I mentioned, I omit from Proving the remaining properties (which as I mentioned, I omit from
the main body of the post) is sufficient to apply the isomorphism, the main body of the post) is sufficient to apply the isomorphism,
@ -500,7 +500,7 @@ proving that maps with finite keys are of a finite height.
### Using the Finite Height Property ### Using the Finite Height Property
Lattices having a finite height is a crucial property for the sorts of Lattices having a finite height is a crucial property for the sorts of
static program analyses I've been working to implement. static program analyses I've been working to implement.
We can create functions that traverse "up" through the lattice, We can create functions that traverse "up" through the lattice,
creating larger values each time. If these lattices are of a finite height, creating larger values each time. If these lattices are of a finite height,
then the static analyses functions can only traverse "so high". then the static analyses functions can only traverse "so high".

2
content/blog/agda_hugo.md
View File

@ -92,7 +92,7 @@ as well as a surrounding "context" that says what file the code is from,
which lines are listed, and where to find the full code (e.g., on my Git server). which lines are listed, and where to find the full code (e.g., on my Git server).
It looks something like this: It looks something like this:
{{< codelines "Agda" "agda-spa/Language/Base.agda" 12 20 >}} {{< codelines "Agda" "agda-spa/Language.agda" 20 27 >}}
In summary: In summary:

2
data/submodules.json
View File

@ -1,5 +1,5 @@
{ {
"agda-spa": "https://dev.danilafe.com/DanilaFe/agda-spa/src/commit/828b652d3b9266e27ef7cf5a8a7fb82e3fd3133f", "agda-spa": "https://dev.danilafe.com/DanilaFe/agda-spa/src/commit/f0da9a902005b24db4e03a89c2862493735467c4",
"aoc-2020": "https://dev.danilafe.com/Advent-of-Code/AdventOfCode-2020/src/commit/7a8503c3fe1aa7e624e4d8672aa9b56d24b4ba82", "aoc-2020": "https://dev.danilafe.com/Advent-of-Code/AdventOfCode-2020/src/commit/7a8503c3fe1aa7e624e4d8672aa9b56d24b4ba82",
"blog-static-flake": "https://dev.danilafe.com/Nix-Configs/blog-static-flake/src/commit/67b47d9c298e7476c2ca211aac5c5fd961637b7b", "blog-static-flake": "https://dev.danilafe.com/Nix-Configs/blog-static-flake/src/commit/67b47d9c298e7476c2ca211aac5c5fd961637b7b",
"compiler": "https://dev.danilafe.com/DanilaFe/bloglang/src/commit/137455b0f4365ba3fd11c45ce49781cdbe829ec3", "compiler": "https://dev.danilafe.com/DanilaFe/bloglang/src/commit/137455b0f4365ba3fd11c45ce49781cdbe829ec3",