diff --git a/content/blog/01_spa_agda_lattices.md b/content/blog/01_spa_agda_lattices.md index b11e9f6..16fe024 100644 --- a/content/blog/01_spa_agda_lattices.md +++ b/content/blog/01_spa_agda_lattices.md @@ -283,6 +283,7 @@ to in the main body of the text). The same is true for the set union and intersection operations, \((\cup)\) and \((\cap)\). {{< /sidenote >}}". For example, \((+\ \sqcap\ ?)\ =\ +\), because a variable that's both "any sign" and "positive" must be positive. +{#lub-glub-or-and} There's just one hiccup: what's the greatest lower bound of `+` and `-`? it needs to be a value that's less than both of them, but so far, we don't have diff --git a/content/blog/02_spa_agda_combining_lattices.md b/content/blog/02_spa_agda_combining_lattices.md index 1097a71..ba6193c 100644 --- a/content/blog/02_spa_agda_combining_lattices.md +++ b/content/blog/02_spa_agda_combining_lattices.md @@ -188,7 +188,9 @@ 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" +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: @@ -198,7 +200,9 @@ 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 +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: @@ -211,9 +215,25 @@ m_2[k] & k \notin m_1, k \in m_2 \end{cases} {{< /latex >}} +If you're familiar with set theory, this operation is like +{{< sidenote "right" "map-union-note" "an extension of the union operator \((\cup)\)" >}} +There are, of course, other ways to extend the "union" operation to maps. +Haskell, for instance, defines it in a "left-biased" way (preferring the +elements from the left operand of the operation when duplicates are encountered).
+
+However, with a "join" operation \((\sqcup)\) that's defined on the values +stored in the map gives us an extra tool to work with. As a result, I would +argue that our extension, given such an operator, is the most natural. +{{< /sidenote >}} to maps. In fact, this begins to motivate +the choice to use \((\sqcup)\) to denote this operation. A further bit of +motivation is this: +[we've already seen]({{< relref "01_spa_agda_lattices#lub-glub-or-and" >}}) +that the \((\sqcup)\) and \((\sqcap)\) operators correspond to "or" +and "and". The elements in the union of two sets are precisely +those that are in one set __or__ the other. Thus, using union here fits our +notion of how the \((\sqcup)\) operator behaves. +{#union-as-or} + {{< todo >}} I started using 'join' but haven't introduced it before. {{< /todo >}} - -something something lub glub -{#union-as-or}