my forest
more dt
+35
-7
+3
trees/dm-000C.tree
+3
trees/dm-000C.tree
+2
-2
trees/dt-000Y.tree
+2
-2
trees/dt-000Y.tree
···
1
1
\title{Chains and Unfolding}
2
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}: }
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 \em{limit} of the [ascending Kleene chain](dt-000X) of #{f}, i.e. #{f(f(f(f(\dots))))}: }
4
4
\transclude{dt-000X}
5
-
\p{Each element of [this chain](dt-000X) is another "unfolding" of the recursion.}
5
+
\p{Each successive element of [this chain](dt-000X) is another "unfolding" of the recursion.}
6
6
\transclude{dt-000V}
7
7
\transclude{dt-000W}
+2
-1
trees/dt-000Z.tree
+2
-1
trees/dt-000Z.tree
+2
-2
trees/dt-0010.tree
+2
-2
trees/dt-0010.tree
···
2
2
\title{Directed set}
3
3
\author{liamoc}
4
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}
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
6
\figure{\tex{\usepackage{tikz}}{
7
7
\begin{tikzpicture}
8
8
\draw[dotted, thick] (0,0) circle (1.5 cm);
···
24
24
\end{tikzpicture}
25
25
}
26
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}.}
27
+
The #{z} above is an [upper bound](dm-000C) of #{x} and #{y}. Hence, a non-empty set is \em{directed} iff every pair of values has an [upper bound](dm-000C) \em{in the set}.}
28
28
\p{Intuitively, directed sets are "going somewhere" — given two elements we can always find a "greater" one in the set.}
29
29
+1
trees/dt-0011.tree
+1
trees/dt-0011.tree
+6
-1
trees/dt-0012.tree
+6
-1
trees/dt-0012.tree
···
1
1
\taxon{Theorem}
2
+
\title{Chain → Directed}
2
3
\author{liamoc}
3
4
\p{All non-empty [chains](dt-000V) are [directed](dt-0010).}
5
+
\scope{
6
+
\put\transclude/toc{false}
7
+
\put\transclude/numbered{false}
4
8
\subtree{
5
9
\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]. }
10
+
\p{Let #{C} be a [chain](dt-000V). Then, given two elements #{x,y \in C} we know from [totality](dm-0008) that either #{x \sqsubseteq y} or #{y \sqsubseteq x}. If #{x \sqsubseteq y}, then #{y} is the [upper bound](dm-000C), otherwise #{x} is the [upper bound](dm-000C). }
11
+
}
7
12
}
+1
-1
trees/dt-0013.tree
+1
-1
trees/dt-0013.tree
···
3
3
\p{
4
4
A subset #{Y \subseteq X} of a [poset](dm-0004) #{X} is \em{consistent} iff
5
5
##{\exists x \in X.\ \forall y \in Y.\ y \sqsubseteq x}
6
-
Such an #{x} is called an [upper bound] of #{Y}.
6
+
Such an #{x} is called an [upper bound](dm-000C) of #{Y}.
7
7
\figure{\tex{\usepackage{tikz}}{
8
8
\begin{tikzpicture}
9
9
\node (a) at (-0.8,0) {$\bullet$};
+17
trees/dt-0014.tree
+17
trees/dt-0014.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Theorem}
3
+
\title{Alternative characterisation of directedness}
4
+
\author{liamoc}
5
+
\p{A subset #{Y \subseteq X} of a [poset](dm-0004) #{X} is [directed](dt-0010) iff every \em{finite} subset of #{Y' \subseteq Y} has an [upper bound](dm-000C) in #{Y}.}
6
+
\scope{
7
+
\put\transclude/toc{false}
8
+
\put\transclude/numbered{false}
9
+
\subtree{
10
+
\taxon{Proof}
11
+
\ul{
12
+
\li{\strong{⇐}: Every pair of elements #{x,y \in Y} has an [upper bound](dm-000C) simply by taking the [upper bound](dm-000C) of the set #{ \Set{x,y}. }
13
+
\li{\strong{⇒}: Given a finite set #{ X = \Set{x_1,x_2,\dots, x_n} }, we can show it has an [upper bound](dm-000C) by an inductive process, first taking the [upper bound](dm-000C) of #{x_1} and #{x_2}, and then taking the [upper bound](dm-000C) of that an #{x_3} and so on until we have an [upper bound](dm-000C) for the whole set. This induction works because the set #{X} is finite.}
14
+
}
15
+
}
16
+
}
17
+
}