diff --git a/trees/dm/dm-000R.tree b/trees/dm/dm-000R.tree new file mode 100644 index 0000000..1a041ff --- /dev/null +++ b/trees/dm/dm-000R.tree @@ -0,0 +1,6 @@ +\taxon{Definition} +\author{liamoc} +\title{Submonoid} +\p{ +A \em{submonoid} of a [monoid](dm-000O) #{(X, \iota, \bullet)} is a subset #{Y \subseteq X} such that #{Y} is closed under #{\bullet} and #{\iota \in Y} +} \ No newline at end of file diff --git a/trees/dt/dt-001Y.tree b/trees/dt/dt-001Y.tree index 84d17d8..d04c6bd 100644 --- a/trees/dt/dt-001Y.tree +++ b/trees/dt/dt-001Y.tree @@ -6,12 +6,13 @@ \transclude{dt-001Z} \subtree{ \taxon{Lecture} -\title{Scott Domains} +\title{Recursively Defined Domains} \p{todo} } \subtree{ \taxon{Lecture} -\title{Recursively Defined Domains} +\title{Scott Domains} +\transclude{dt-0040} \p{todo} } \subtree{ diff --git a/trees/dt/dt-003U.tree b/trees/dt/dt-003U.tree new file mode 100644 index 0000000..94b8267 --- /dev/null +++ b/trees/dt/dt-003U.tree @@ -0,0 +1,12 @@ +\import{dt-macros} +\title{Compactness} +\taxon{Definition} +\author{liamoc} +\p{ +Let #{A} be a [cpo](dt-001D). Then #{x \in A} is \em{compact} (a.k.a. \em{finite}) iff for all [directed](dt-0010) #{X \subseteq A}: +##{ +x \sqsubseteq \bigsqcup X \implies \exists y \in X.\ x \sqsubseteq y +} +In English: A compact element will approximate some element of a [directed](dt-0010) set if it approximates the [lub](dt-0017). We write #{\compact{A}} for the set of compact elements of #{A}, i.e.: +##{\compact{A} = \Set{x \in A \mid x\ \text{is compact} }} +} \ No newline at end of file diff --git a/trees/dt/dt-003V.tree b/trees/dt/dt-003V.tree new file mode 100644 index 0000000..28fce42 --- /dev/null +++ b/trees/dt/dt-003V.tree @@ -0,0 +1,10 @@ +\import{dt-macros} +\author{liamoc} +\taxon{Example} +\title{Compact elements} +\ul{ +\li{Every element in a finite [cpo](dt-001D) is [compact](dt-003U). More generally, every element of a [cpo](dt-001D) of finite \em{height} (e.g. #{\mathbb{Z}_\bot}) is [compact](dt-003U). This is because finite [directed sets](dt-0010) are always [boring](dt-003W).} +\li{ Take the [cpo](dt-001D) #{\mathcal{P}(X)} of subsets of #{X} ordered by inclusion #{\subseteq}, as seen in \ref{dt-001G}. The [compact](dt-003U) elements of #{\mathcal{P}(X)} are those of finite cardinality. } +\li{ Take the [cpo](dt-001D) #{\mathbb{N} \nrightarrow \mathbb{N}} of partial functions on the natural numbers, ordered by inclusion of graphs. The [compact](dt-003U) elements of #{\mathbb{N} \nrightarrow \mathbb{N}} are the functions which are defined only for finite domains. } +} + diff --git a/trees/dt/dt-003W.tree b/trees/dt/dt-003W.tree new file mode 100644 index 0000000..250fe6b --- /dev/null +++ b/trees/dt/dt-003W.tree @@ -0,0 +1,12 @@ +\import{dt-macros} +\import{table-macros} +\author{liamoc} +\taxon{Definition} +\title{Boring and interesting sets} +\p{ +There are two kinds of [directed sets](dt-0010): +\ol{ + \li{ \em{Boring} sets contain their [lub](dt-0017). \br \strong{Example}: Finite directed sets are boring (but boring sets aren't all finite!). } + \li{ \em{Interesting} sets don't contain their [lub](dt-0017). \br \strong{Example}: #{\mathbb{N}} in the chain #{\mathbb{N} \cup \Set{ \infty }} is interesting.} +} +} \ No newline at end of file diff --git a/trees/dt/dt-003X.tree b/trees/dt/dt-003X.tree new file mode 100644 index 0000000..092c3c3 --- /dev/null +++ b/trees/dt/dt-003X.tree @@ -0,0 +1,17 @@ +\import{dt-macros} +\import{table-macros} +\title{Compact elements with infinitely many approximations } +\taxon{Example} +\author{liamoc} +\[class]{sidefigure}{ +\tex{\usepackage{tikz-cd}\usetikzlibrary{decorations.pathreplacing}\usepackage{amsmath}}{\begin{tikzcd} + \infty + 1& \ar[l,thick]\text{\scriptsize compact}\\ + \infty\ar[u,-,thick] & \ar[l,thick]\text{\scriptsize non-compact}\\ + 2\ar[u,-,thick, dotted] & \quad\arrow[dd, start anchor=north, end anchor=south, no head, xshift=-1em, decorate, decoration={brace,amplitude=10pt,raise=-15pt}, thick,"\text{compact}" right=0pt]\\ + 1\ar[u,-,thick]\\ + 0\ar[u,-,thick] & \quad +\end{tikzcd}} +} +\p{[Compact](dt-003U) elements may still have an infinite number of approximations. Consider the [cpo](dt-001D) #{\mathbb{N} \cup \Set{ \infty, \infty + 1 }}, where we have tacked on an additional top element #{\infty + 1} to our normal [cpo](dt-001D) of natural numbers extended with infinity. Then, while #{\infty} is not [compact](dt-003U), #{\infty + 1} \em{is} [compact](dt-003U) — it is not the [lub](dt-0017) of an [interesting](dt-003W) [directed set](dt-0010). If #{\infty + 1} is the [lub](dt-0017) of a set #{X} then #{\infty + 1} must be in the set #{X}. Nonetheless, there are an infinite number of \em{approximations} to #{\infty + 1}, i.e., elements #{x} such that #{x \sqsubseteq \infty + 1}.} +\p{As an aside, requiring that our [compact](dt-003U) elements have a \em{truly} finite number of approximations is the basis for the theory of \em{Berry domains and stable functions}.} + diff --git a/trees/dt/dt-003Y.tree b/trees/dt/dt-003Y.tree new file mode 100644 index 0000000..9513cc6 --- /dev/null +++ b/trees/dt/dt-003Y.tree @@ -0,0 +1,4 @@ +\taxon{Theorem} +\author{liamoc} +\title{Submonoids as a cpo} +\p{The [submonoids](dm-000R) of a [monoid](dm-000O) #{(X, \iota, \bullet)} form a [cpo](dt-001D) under #{\subseteq}, where union gives the [lub](dt-0017).} diff --git a/trees/dt/dt-003Z.tree b/trees/dt/dt-003Z.tree new file mode 100644 index 0000000..a956a3e --- /dev/null +++ b/trees/dt/dt-003Z.tree @@ -0,0 +1,11 @@ +\import{dt-macros} +\author{liamoc} +\title{Both infinite and compact} +\taxon{Exercise} +\p{Find a set in the [cpo of submonoids](dt-003Y) of #{(\mathbb{N},0,+)} that is \em{both} infinite and [compact](dt-003U)} + +\solnblock{ +\p{Take #{E \triangleq \Set{ n \in \mathbb{N} \mid n\ \text{is even}}}. Let #{Y \subseteq \pow{\mathbb{N}}} be directed and #{E \subseteq \bigcup Y}. Since #{2 \in E} there must exist #{y \in Y} such that #{2 \in Y}. Since #{(y,0,+)} is a [monoid](dm-000O), every positive multiple of #{2} is also in #{y}, thus #{E \subseteq y} and therefore #{E} is [compact](dt-003U).} +\p{Seeing as [compact](dt-003U) elements are also sometimes called \em{finite}, this is surprising as #{E} is an infinite set. The reason it is nonetheless [compact](dt-003U) is that #{E} is \em{finitely generated} — it is the smallest [submonoid](dm-000R) of #{(\mathbb{N},0,+)} such that the \em{finite} set #{\Set{ 2 } \subseteq E}. In fact, the [compact](dt-003U) [submonoids](dm-000R) of #{(\mathbb{N},0,+)} are precisely the finitely generated ones. +} +} diff --git a/trees/dt/dt-0040.tree b/trees/dt/dt-0040.tree new file mode 100644 index 0000000..1d95208 --- /dev/null +++ b/trees/dt/dt-0040.tree @@ -0,0 +1,33 @@ +\title{Compactness and Finiteness} +\author{liamoc} +\p{We begin by formalising the notion of an element in a [cpo](dt-001D) representing a \em{finite} amount of information. } +\transclude{dt-003W} +\p{ +Following the above intuition, we might be tempted to say that the \em{"infinite"} elements of a [cpo](dt-001D) are those which are the [lub](dt-0017) of an [interesting](dt-003W) set, but this notion is too weak. Consider this [cpo](dt-001D) #{X}: +\figure{ +\tex{\usepackage{tikz-cd,amsmath,amssymb}}{ +\begin{tikzcd} +\infty\\ +2\ar[u,thick,-,dotted]\\ +1\ar[u,thick,-] & & x\ar[uull,thick,-]\\ +0\ar[u,thick,-] \\ +& \bot \ar[ul,thick,-]\ar[uur,thick,-] +\end{tikzcd} +}} +By the above definition, the only infinite element would be #{\infty}, but if we consider the following isomorphic [cpo](dt-001D), ordered by subset inclusion: +\figure{ +\tex{\usepackage{tikz-cd,amsmath,amssymb}}{ +\begin{tikzcd} +\mathbb{N}\\ +\{0,1,2\}\ar[u,thick,-,dotted]\\ +\{0,1\}\ar[u,thick,-] & & x\ar[uull,thick,-]\\ +\{0\}\ar[u,thick,-] \\ +& \emptyset \ar[ul,thick,-]\ar[uur,thick,-] +\end{tikzcd} +}} +Then the set #{x} cannot be a finite set, as any finite set would be a subset of one of the finite sets in the chain #{\emptyset \sqsubseteq \Set{ 0 } \sqsubseteq \Set{0,1} \sqsubseteq \cdots}. Thus, it makes more sense for us to call #{x} an \em{"infinite"} element as well.} +\transclude{dt-003U} +\p{In the example cpo #{X} above, all the elements except #{\infty} and #{x} would be [compact](dt-003U). Thus, compactness better captures our notion of an element representing a finite amount of information. This understanding of [compact](dt-003U) elements is a generalisation of the notion of a finite element from the theory of algebraic lattices.} +\transclude{dt-003V} +\transclude{dt-003X} +\transclude{dt-003Z} diff --git a/trees/dt/dt-macros.tree b/trees/dt/dt-macros.tree index c89ff34..fe2c17f 100644 --- a/trees/dt/dt-macros.tree +++ b/trees/dt/dt-macros.tree @@ -1,5 +1,6 @@ \def\cal[body]{#{\mathcal{\body}}} \def\syn[body]{#{\mathsf{\body}}} +\def\compact[body]{#{\mathsf{K}(\body)}} \def\inferrule[top][bottom]{\dfrac{\top}{\bottom}} \def\proofblock[body]{\scope{ \put\transclude/toc{false}