my forest
more dt
+164
-3
+5
trees/dm-0007.tree
+5
trees/dm-0007.tree
+5
trees/dm-0008.tree
+5
trees/dm-0008.tree
+6
trees/dm-0009.tree
+6
trees/dm-0009.tree
+6
trees/dm-000A.tree
+6
trees/dm-000A.tree
···
1
+
\taxon{Definition}
2
+
\title{Set bijection}
3
+
\author{liamoc}
4
+
\p{
5
+
A \em{bijection} between sets #{A} and #{B} is a one to one correspondence between their elements. That is, #{R \subseteq A \times B} is a \em{bijection} between #{A} and #{B} if, for each #{x \in A}, there is exactly one #{y \in B} such that #{x\ R\ y}, and vice versa.
6
+
}
+6
trees/dm-000B.tree
+6
trees/dm-000B.tree
+2
-2
trees/dt-0007.tree
+2
-2
trees/dt-0007.tree
···
30
30
\transclude{dt-000P}
31
31
Unfolding the definition of #{\Sigma}, we end up with a recursive equation for the definition of #{\mathbf{C}}:
32
32
##{\mathbf{C} \; = \; (\mathcal{V} \rightarrow (\mathbb{Z} \uplus \mathbf{C})) \rightarrow (\mathcal{V} \rightarrow (\mathbb{Z} \uplus \mathbf{C}))}
33
-
Such equations have \em{no} set-theoretic solution, even if we weaken equality to mere \em{set isomorphism} (here notated #{\simeq}).
33
+
Such equations have \em{no} set-theoretic solution, even if we weaken equality to mere [set isomorphism](dm-000B) (here notated #{\simeq}).
34
34
}
35
35
\subtree{\taxon{Example}\title{A simpler equation with no solution}
36
-
\p{Consider the recursive equation #{X = X \rightarrow \mathbb{B}}. Cantor's theorem says that there is no set #{X} such that #{X \simeq \pow{X}} (where #{\pow{X}} is the [[dm-0006]] of #{X}), and seeing as #{\pow{X} \simeq (X \rightarrow \mathbb{B})} it follows that #{X = X \rightarrow \mathbb{B}} has no solution.}
36
+
\p{Consider the recursive equation #{X = X \rightarrow \mathbb{B}}. Cantor's theorem says that there is no set #{X} such that #{X \simeq \pow{X}} (where #{\pow{X}} is the [power set](dm-0006) of #{X}), and seeing as #{\pow{X} \simeq (X \rightarrow \mathbb{B})} it follows that #{X = X \rightarrow \mathbb{B}} has no solution.}
37
37
}
38
38
\p{Any kind of \em{higher-order} construct leads to such recursive domain equations.}
39
39
\scope{
-1
trees/dt-000T.tree
-1
trees/dt-000T.tree
···
8
8
\p{Not all [monotonic](dt-000J) functions on [posets](dm-0004) have [fixed points](dt-000S), and some have \em{multiple} [fixed point](dt-000S)s!}
9
9
}}
10
10
\p{So, requiring our functions to be monotonic is insufficient to guarantee that a single "best" solution exists. }
11
-
\p{Intuitively, recursive programs are executed by "unfolding" as much as necessary to get a result. We would like to characterise our domains to ensure that solutions always exist, and to allow us to pick the solutions that are "minimal" in the sense that they rely on a minimal amount of unfolding.}
+2
trees/dt-000U.tree
+2
trees/dt-000U.tree
+7
trees/dt-000V.tree
+7
trees/dt-000V.tree
+7
trees/dt-000W.tree
+7
trees/dt-000W.tree
···
1
+
\taxon{Definition}
2
+
\title{#{\omega}-chain}
3
+
\author{liamoc}
4
+
\p{
5
+
An \em{#{\omega}-chain} is a [chain](dt-000V) that is [countable](dm-0009). In other words, it is a sequence of elements #{x_{i \in \mathbb{N}}} such that:
6
+
##{x_0 \sqsubseteq x_1 \sqsubseteq x_2 \sqsubseteq x_3 \dots}
7
+
}
+7
trees/dt-000X.tree
+7
trees/dt-000X.tree
···
1
+
\title{Ascending Kleene chain}
2
+
\taxon{Example}
3
+
\p{
4
+
Given a [pointed poset](dt-000G) #{(X,\subseteq)} and a [monotonic](dt-000J) function #{f : X \rightarrow X}, the \em{ascending Kleene chain} is the [#{\omega}-chain](dt-000W):
5
+
##{ \bot \sqsubseteq f(\bot) \sqsubseteq f(f(\bot)) \sqsubseteq f(f(f(\bot))) \sqsubseteq \cdots}
6
+
Because #{\bot} is the [bottom element](dt-000A), we know that #{\bot \sqsubseteq f(\bot)}. Each subsequent step in the chain exists because of [monotonicity](dt-000J).
7
+
}
+7
trees/dt-000Y.tree
+7
trees/dt-000Y.tree
···
1
+
\title{Chains and Unfolding}
2
+
\p{Intuitively, recursive programs are executed by "unfolding" as much as necessary to get a result. We would like to characterise our domains to ensure that solutions always exist, and to allow us to pick the solutions that are "minimal" in the sense that they rely on a minimal amount of unfolding.}
3
+
\p{After converting a recursive program into a non-recursive [monotonic](dt-000J) higher order function #{f}, the [fixed point](dt-000S) we desire would intuitively be the [limit](todo) of the [ascending Kleene chain](dt-000X) of #{f}: }
4
+
\transclude{dt-000X}
5
+
\p{Each element of [this chain](dt-000X) is another "unfolding" of the recursion.}
6
+
\transclude{dt-000V}
7
+
\transclude{dt-000W}
+6
trees/dt-000Z.tree
+6
trees/dt-000Z.tree
···
1
+
\title{From chains to directed sets}
2
+
\p{While [#{\omega}-chains](dt-000W) are technically sufficient for [denotational semantics](dt-0001), for our purposes it is a little more convenient to think in terms of [directed sets](dt-0010) rather than [chains](dt-000V).}
3
+
\transclude{dt-0010}
4
+
\transclude{dt-0011}
5
+
\transclude{dt-0012}
6
+
\transclude{dt-0013}
+29
trees/dt-0010.tree
+29
trees/dt-0010.tree
···
1
+
\taxon{Definition}
2
+
\title{Directed set}
3
+
\author{liamoc}
4
+
\p{
5
+
Formally, A non-empty subset #{Y \subseteq X} of a [poset](dm-0004) #{(X,\sqsubseteq)} is \em{directed} iff: ##{\forall x, y \in Y.\ \exists z \in Y.\ x \sqsubseteq z \land y \sqsubseteq z}
6
+
\figure{\tex{\usepackage{tikz}}{
7
+
\begin{tikzpicture}
8
+
\draw[dotted, thick] (0,0) circle (1.5 cm);
9
+
\draw[dotted, thick] (5,0) circle (1.5 cm);
10
+
\node at (2.5,0) {\Huge $\Rightarrow$ };
11
+
\node at (2.5,0.6) {$\exists z$ };
12
+
\node at (-0.7,-0.5) { \Large $\bullet$ };
13
+
\node at (-0.7,-0.8) { $x$ };
14
+
\node at (0.7,-0.5) { \Large $\bullet$ };
15
+
\node at (0.7,-0.8) { $y$ };
16
+
\node (x) at (4.3,-0.5) { \Large $\bullet$ };
17
+
\node at (4.3,-0.8) { $x$ };
18
+
\node (y) at (5.7,-0.5) { \Large $\bullet$ };
19
+
\node at (5.7,-0.8) { $y$ };
20
+
\node (z)at (5,0.5) { \Large $\bullet$ };
21
+
\node at (5,0.8) { $z$ };
22
+
\draw[thick] (x) -- (z)
23
+
(y) -- (z);
24
+
\end{tikzpicture}
25
+
}
26
+
}
27
+
The #{z} above is an [upper bound] of #{x} and #{y}. Hence, a non-empty set is \em{directed} iff every pair of values has an [upperbound] \em{in the set}.}
28
+
\p{Intuitively, directed sets are "going somewhere" — given two elements we can always find a "greater" one in the set.}
29
+
+32
trees/dt-0011.tree
+32
trees/dt-0011.tree
···
1
+
\taxon{Example}
2
+
\p{The [power set](dm-0006) of any set #{X} is directed under #{\subseteq}.}
3
+
\p{ \strong{Below}: #{\cal{P}(\{1,2,3\})}: }
4
+
\figure{\tex{\usepackage{tikz}}{
5
+
\begin{tikzpicture}
6
+
\node (abc) at (1,3) {$\{1,2,3\}$};
7
+
\node (ab) at (0,2) {$\{1,2\}$};
8
+
\node (ac) at (1,2) {$\{1,3\}$};
9
+
\node (bc) at (2,2) {$\{2,3\}$};
10
+
\node (a) at (0,1) {$\{1\}$};
11
+
\node (b) at (1,1) {$\{2\}$};
12
+
\node (c) at (2,1) {$\{3\}$};
13
+
\node (em) at (1,0) {$\emptyset$};
14
+
\draw[thick]
15
+
(em) -- (a)
16
+
(em) -- (b)
17
+
(em) -- (c);
18
+
\draw[thick]
19
+
(ab) -- (abc)
20
+
(bc) -- (abc)
21
+
(ac) -- (abc);
22
+
\draw[thick]
23
+
(a) -- (ab)
24
+
(a) -- (ac);
25
+
\draw[thick]
26
+
(c) -- (bc)
27
+
(c) -- (ac);
28
+
\draw[thick]
29
+
(b) -- (bc)
30
+
(b) -- (ab);
31
+
\end{tikzpicture}
32
+
}}
+7
trees/dt-0012.tree
+7
trees/dt-0012.tree
···
1
+
\taxon{Theorem}
2
+
\author{liamoc}
3
+
\p{All non-empty [chains](dt-000V) are [directed](dt-0010).}
4
+
\subtree{
5
+
\taxon{Proof}
6
+
\p{Let #{C} be a chain. Then, given two elements #{x,y \in C} we know from [totality](dm-0008) that either #{x \sqsubseteq y} or #{y \subseteq x}. If #{x \sqsubseteq y}, then #{y} is the [upperbound], otherwise #{x} is the [upperbound]. }
7
+
}
+30
trees/dt-0013.tree
+30
trees/dt-0013.tree
···
1
+
\taxon{Definition}
2
+
\title{Consistent subsets}
3
+
\p{
4
+
A subset #{Y \subseteq X} of a [poset](dm-0004) #{X} is \em{consistent} iff
5
+
##{\exists x \in X.\ \forall y \in Y.\ y \sqsubseteq x}
6
+
Such an #{x} is called an [upper bound] of #{Y}.
7
+
\figure{\tex{\usepackage{tikz}}{
8
+
\begin{tikzpicture}
9
+
\node (a) at (-0.8,0) {$\bullet$};
10
+
\node (b) at (0.8,0) {$\bullet$};
11
+
\node (c) at (0,-1) {$\bullet$};
12
+
\draw[thick] (c) -- (a) (c) -- (b);
13
+
\draw[dashed, rounded corners=0.4cm] (-1.2,-0.4) rectangle (1.2,0.4);
14
+
\node (foo) at (2,-1.5) {a non-\emph{consistent} set};
15
+
\draw[->,thick] (foo) edge[bend right] (1.2,0);
16
+
\node (a) at (4.2,0) {$\bullet$};
17
+
\node (b) at (5.8,0) {$\bullet$};
18
+
\node (x) at (4.2,1) {$\bullet$};
19
+
\node (y) at (5.8,1) {$\bullet$};
20
+
\node (c) at (5,-1) {$\bullet$};
21
+
\draw[thick] (c) -- (a) (c) -- (b) (a) -- (x) (a) -- (y) (b) -- (x) (b) -- (y);
22
+
\draw[dashed, rounded corners=0.4cm] (3.8,-0.4) rectangle (6.2,0.4);
23
+
\node (foo) at (7,-1.2) {a \emph{consistent} set};
24
+
\draw[->,thick] (foo) edge[bend right] (6.2,0);
25
+
\node (foo) at (2,1) {upper bound};
26
+
\draw[->,thick] (foo) edge[bend left] (x);
27
+
\draw[->,thick] (foo) edge[bend left] (y);
28
+
\end{tikzpicture}
29
+
}}
30
+
}