content/blog/02_spa_agda_combining_lattices.md

@@ -151,10 +151,9 @@ Let's start thinking about what sorts of lattices our maps will be.
 The thing that [motivated our introduction]({{< relref "01_spa_agda_lattices#specificity" >}})
 of lattices was comparing them by "specificity", so let's try figure out how
 to compare maps. For that, we can begin small, by looking at singleton maps.
-If we have `{"x": +}` and `{"x": ⊤}`, which one of them is smaller? Well, we have
+If we have `{"x": +}` and `{"x": ⊤}`, which one of them is smaller? Well, wehave previously established that `+` is more specific (and thus less than) `⊤`. Thus, it shouldn't be too much of a stretch
-previously established that `+` is more specific (and thus less than) `⊤`. Thus,
+to say that for singleton maps of the same key, the one with the smaller
-it shouldn't be too much of a stretch to say that for singleton maps of the same
+value is smaller.
-key, the one with the smaller value is smaller.
 
 Now, what about a pair of singleton maps like `{"x": +}` and `{"y": ⊤}`? Among
 these two, each contains some information that the other does not. Although the
@@ -164,56 +163,4 @@ these maps incompatible, then. More generally, if we have two maps and each one
 has a key that the other doesn't, we can't compare them.
 
 If only one map has a unique key, though, things are different. Take for
-instance `{"x": +}` and `{"x": +, "y": +}`. Are they really incomparable?
+instance `{"x": +}` and `{"x": +, "y": +}`.
-The keys that the two maps do share can be compared (`+ <= +`, because they're
-equal).
-
-
-All of the above leads to the following conventional definition, which I find
-easier to further motivate using \((\sqcup)\) and \((\sqcap)\)
-(and [do so below]({{< relref "#union-as-or" >}})).
-
-> A map `m1` is less than or equal to another map `m2` (`m1 <= m2`) if for
-> every key `k` that has a value in `m1`, the key also has a value in `m2`, and
-> `m1[k] <= m2[k]`.
-
-That definitions matches our intuitions so far. The only key in `{"x": +}` is `x`;
-this key is also in `{"x": ⊤}` (check) and `+ < ⊤` (check). On the other hand,
-both `{"x": +}` and `{"y": ⊤}` have a key that the other doesn't, so the
-definition above is not satisfied. Finally, for `{"x": +}` and
-`{"x": +, "y": +}`, the only key in the former is also present in the latter,
-and `+ <= +`; the definition is satisfied.
-
-Next, we need to define the \((\sqcup)\) and \((\sqcap)\) operators that match
-our definition of "less than or equal". Let's start with \((\sqcup)\). For two
-maps \(m_1\) and \(m_2\), the join of those two maps, \(m_1 \sqcup m_2\) should
-be greater than or equal to both; in other words, both sub-maps should be less
-than or equal to the join. Our newly-introduced condition for "less than or equal"
-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__
-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\)
-and \(m_2\) have a value mapped to a particular key? The values in the two
-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
-maps needs to be bigger than the value in either sub-map. We already know how
-to get a value that's bigger than two other values: we use a join on the
-values! Thus, define \(m_1 \sqcup m_2\) as a map that has all the keys
-from \(m_1\) and \(m_2\), where the value at a particular key is given
-as follows:
-
-{{< latex >}}
-(m_1 \sqcup m_2)[k] =
-\begin{cases}
-m_1[k] \sqcup m_2[k] & k \in m_1, k \in m_2 \\
-m_1[k] & k \in m_1, k \notin m_2 \\
-m_2[k] & k \notin m_1, k \in m_2
-\end{cases}
-{{< /latex >}}
-
-{{< todo >}}
-I started using 'join' but haven't introduced it before.
-{{< /todo >}}
-
-something something lub glub
-{#union-as-or}

data/hosts.json

@@ -1,5 +0,0 @@
-{
-    "https://dev.danilafe.com" : {
-        "linesSuffix": "#L%d-L%d"
-    }
-}

themes/vanilla

@@ -1 +1 @@
-Subproject commit df22cb2b87cf9bc1a9da372e17d4c4eedfc3efff
+Subproject commit 97e965feece9fd3d3a5328156c043bd2a0cca80f