my forest
more dt
+110
-1
+1
trees/dt-000U.tree
+1
trees/dt-000U.tree
+3
-1
trees/dt-001E.tree
+3
-1
trees/dt-001E.tree
+9
trees/dt-001H.tree
+9
trees/dt-001H.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Remark}
3
+
\title{[Lubs](dt-0017) of chains}
4
+
\p{The \em{limit} of the [ascending Kleene chain](dt-000X) of a [monotonic](dt-000J) function #{f : X \rightarrow X} is the same as the [least upper bound](dt-0017) of the set #{\Set{ f^n(\bot) \mid n \in \nat}} (where #{f^n} is the #{n}-fold self-composition of the function #{f}). If we require that our semantic domain #{X} is a [cpo](dt-001D), we know that this limit exists.
5
+
\scope{
6
+
\put\transclude/toc{false}
7
+
\put\transclude/numbered{false}
8
+
\subtree{\taxon{Thesis}
9
+
\p{Our semantic domains are [cpos](dt-001D), ensuring the presence of these limits.}}}}
+17
trees/dt-001I.tree
+17
trees/dt-001I.tree
···
1
+
\import{dt-macros}
2
+
\title{Continuity and Fixed Points}
3
+
\p{By choosing a [cpo](dt-001D) for our semantic domain, we can ensure that the [Kleene chain](dt-000X) has a limit. However, it is not guaranteed that the limit we find will be a [fixed point](dt-000S) to our [monotonic](dt-000J) function #{f}.}
4
+
\transclude{dt-001K}
5
+
\p{
6
+
To address this problem, we shall strengthen our requirement on functions from mere [monotonicity](dt-000J) to \em{continuity}.}
7
+
\transclude{dt-001J}
8
+
\transclude{dt-001L}
9
+
\transclude{dt-001M}
10
+
\transclude{dt-001N}
11
+
\transclude{dt-001O}
12
+
\scope{
13
+
\put\transclude/toc{false}
14
+
\put\transclude/numbered{false}
15
+
\subtree{\taxon{Thesis}
16
+
\p{Computable functions are [continuous](dt-001J) functions on [cpos](dt-001D).}
17
+
}}
+11
trees/dt-001J.tree
+11
trees/dt-001J.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Definition}
3
+
\author{liamoc}
4
+
\title{Continuity}
5
+
\p{A function #{f : A \rightarrow B} on [cpos](dt-001D) #{A} and #{B} is \em{continuous} iff for all [directed](dt-0010) #{X \subseteq A},
6
+
\ol{
7
+
\li{#{\bigsqcup \{ f(x) \mid x \in X \}} exists, and}
8
+
\li{#{f(\bigsqcup X) = \bigsqcup \{ f(x) \mid x \in X \}}, i.e., #{f} preserves [lubs](dt-0017).}
9
+
}
10
+
The intuition behind continuity is that "nothing is suddenly invented at infinity": our function will behave analogously at the limit as it does for each element in our [chain](dt-000V).
11
+
}
+20
trees/dt-001K.tree
+20
trees/dt-001K.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Problem}
4
+
\title{Monotonicity is insufficient}
5
+
\p{Consider this [monotonic](dt-000J) function #{g} defined over a [cpo](dt-001D) #{(\mathbb{R} \cup \{\infty,-\infty\}, \leq)}:
6
+
##{g(x) = \begin{cases}
7
+
\tan^{-1} x & \text{if}\ x < 0\\
8
+
1 & \text{otherwise}
9
+
\end{cases}
10
+
}
11
+
Note this function is not continuous at 0. Starting from our [#{\bot} element](dt-000A) #{-\infty}, we can see that the limit of the [ascending Kleene chain](dt-000X) is #{0}:
12
+
##{
13
+
\begin{array}{lcl}
14
+
g(-\infty) & = & -\frac{\pi}{2}\\
15
+
g(-\frac{\pi}{2}) & = & -1\\
16
+
g(-1) & \approx & -0.78\\
17
+
\end{array}
18
+
}
19
+
But #{g(0) = 1}! — the [lub](dt-0017) of the [Kleene chain](dt-000X) is \em{not} a [fixed point](dt-000S)!
20
+
}
+11
trees/dt-001L.tree
+11
trees/dt-001L.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Theorem}
4
+
\title{Continuity implies monotonicity}
5
+
\p{All [continuous](dt-001J) functions are [monotonic](dt-000J).
6
+
\scope{
7
+
\put\transclude/toc{false}
8
+
\put\transclude/numbered{false}
9
+
\subtree{\taxon{Proof}
10
+
\p{Consider two elements #{x, y} of a [cpo](dt-001D) where #{x \sqsubseteq y}. Then #{\Set{x,y}} is [directed](dt-0010) with a [lub](dt-0017) of #{y}. By the second condition in \ref{dt-001J}, we get #{f(y) = f(x) \sqcup f(y)} which is equivalent to #{f(x) \sqsubseteq f(y)}.}
11
+
}}}
+12
trees/dt-001M.tree
+12
trees/dt-001M.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Example}
4
+
\title{[Monotonic](dt-000J) but not [continuous](dt-001J)}
5
+
\p{Consider this function from #{\mathbb{N} \cup \Set{\infty} \rightarrow \Set{\top,\bot}}, defined by:
6
+
##{f(x) = \begin{cases}
7
+
\bot & \text{if}\ x \in \mathbb{N}\\
8
+
\top & \text{otherwise}
9
+
\end{cases}
10
+
}
11
+
This function is [monotonic](dt-000J), but, taking #{X = \mathbb{N}} (which is a [directed](dt-0010) subset of the [cpo](dt-001D) #{\mathbb{N} \cup \{\infty\}}), then #{f(\bigsqcup \mathbb{N}) = f(\infty) = \top}, but #{\bigsqcup \{ f(n) \mid n \in \mathbb{N} \} = \bigsqcup \{ \bot \} = \bot}. Thus, this function is not [continuous](dt-001J).
12
+
}
+11
trees/dt-001N.tree
+11
trees/dt-001N.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Exercise}
4
+
\p{Show that if a function on [cpos](dt-001D) #{f : A \rightarrow B} is [monotonic](dt-000J), then #{\bigsqcup \Set{ f(x) \mid x \in X }} exists for any [directed](dt-0010) #{X \subseteq A} (i.e.the first condition for [continuity](dt-001J) in \ref{dt-001J}).}
5
+
\p{\strong{Hint}: It suffices to show that #{\Set{ f(x) \mid x \in X } \subseteq B} is [directed](dt-0010).}
6
+
\scope{
7
+
\put\transclude/toc{false}
8
+
\put\transclude/numbered{false}
9
+
\put\transclude/expanded{false}
10
+
\subtree{\taxon{Solution}
11
+
\p{Because #{B} is a [cpo](dt-001D), it suffices to show that #{\Set{ f(x) \mid x \in X } \subseteq B} is [directed](dt-0010). Let #{a,b \in \Set{ f(x) \mid x \in X }}. Let #{x_a, x_b \in X} be the values that #{f} maps to #{a} and #{b} respectively, i.e. #{f(x_a) = a} and #{f(x_b) = b}. Because #{X} is [directed](dt-0010), an [upper bound](dm-000C) of #{x_a} and #{x_b} exists in #{X}. Call this [upper bound](dm-000C) #{x_c}. Because #{x_a \sqsubseteq x_c} and #{x_b \sqsubseteq x_c}, we know that #{f(x_a) = a \sqsubseteq f(x_c)} and #{f(x_b) = b \sqsubseteq f(x_c)} by [monotonicity](dt-000J) of #{f}. Also, #{f(x_c) \in \Set{ f(x) \mid x \in X }} because #{x_c \in X}. Therefore, because two arbitrary elements in #{\Set{ f(x) \mid x \in X }} have an [upper bound](dm-000C) within the set, the set #{\Set{ f(x) \mid x \in X }} is [directed](dt-0010). }}}
+15
trees/dt-001O.tree
+15
trees/dt-001O.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Theorem}
3
+
\author{liamoc}
4
+
\title{Alternative definition of continuity}
5
+
\p{A function #{f : A \rightarrow B} on [cpos](dt-001D) #{A} and #{B} is [continuous](dt-001J) iff:
6
+
\ol{
7
+
\li{#{f} is [monotonic](dt-000J), and}
8
+
\li{#{f(\bigsqcup X) = \bigsqcup \{ f(x) \mid x \in X \}}, for all [directed](dt-0010) #{X \subseteq A}}
9
+
}
10
+
\scope{
11
+
\put\transclude/toc{false}
12
+
\put\transclude/numbered{false}
13
+
\subtree{\taxon{Proof}
14
+
\p{The second condition here is identical to that of \ref{dt-001J}. The [monotonicity](dt-000J) requirement is equivalent to the first condition of \ref{dt-001J}, with one direction shown by \ref{dt-001L}, and the other shown by the solution of \ref{dt-001N}. }}}
15
+
}