my forest
first chunk of dt done
+185
-2
+1
trees/dt-0005.tree
+1
trees/dt-0005.tree
+1
trees/dt-001E.tree
+1
trees/dt-001E.tree
+5
-1
trees/dt-001I.tree
+5
-1
trees/dt-001I.tree
+24
trees/dt-001P.tree
+24
trees/dt-001P.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Theorem}
3
+
\title{The Kleene fixed point theorem}
4
+
\p{Let #{(S, \sqsubseteq)} be a [cpo](dt-001D) and #{f : S \rightarrow S} be a [continuous](dt-001J) function. Then the [lub](dt-0017) of the [Kleene chain](dt-000X) #{\bigsqcup_{n\in \mathbb{N}}f^{n}(\bot)} is the least [fixed point](dt-000S) of #{f}.}
5
+
\scope{
6
+
\put\transclude/toc{false}
7
+
\put\transclude/numbered{false}
8
+
\subtree{\taxon{Proof}
9
+
\p{We apply [continuity](dt-001J) to show that it is a [fixed point](dt-000S):
10
+
11
+
##{\begin{array}{lclr}
12
+
f(\bigsqcup_{n \in \mathbb{N}} f^n(\bot) ) & = &
13
+
\bigsqcup_{n \in \mathbb{N}} f(f^n(\bot)) &
14
+
\text{(continuity)} \acr{0.5em}
15
+
&=& \bigsqcup_{n \in \mathbb{N}} f^{n+1}(\bot)\acr{0.5em}
16
+
&=& \bigsqcup_{n=1,2\dots}f^{n}(\bot)
17
+
&\qquad\text{(reindexing)}\acr{0.5em}
18
+
&=& \bot \sqcup \bigsqcup_{n=1,2\dots}f^{n}(\bot)\acr{0.5em}
19
+
&=&\bigsqcup_{n\in \mathbb{N}}f^{n}(\bot)\acr{0.5em}
20
+
\end{array}
21
+
}
22
+
To see that it is the \em{least} [fixed point](dt-000S): Let #{y} be a [fixed point](dt-000S) of #{f}. We know that #{\bot \sqsubseteq y} by [definition of #{\bot}](dt-000A). Taking #{f} of both sides, we get #{f(\bot) \sqsubseteq y}. We can continue this inductively and thus we know that, for all #{n \in \mathbb{N}}, #{f^n(\bot) \sqsubseteq y}. Because #{y} is, therefore, an [upper bound](dm-000C) of the [ascending Kleene chain](dt-000X), it must also be at least as large as the [lub](dt-0017) of that [chain](dt-000V).
23
+
}
24
+
}}
+5
trees/dt-001Q.tree
+5
trees/dt-001Q.tree
+6
trees/dt-001R.tree
+6
trees/dt-001R.tree
+31
trees/dt-001S.tree
+31
trees/dt-001S.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Exercise}
4
+
\ol{
5
+
\li{What is #{\fixop(\mathsf{id})} where #{\mathsf{id}} is the identity function on #{\mathbb{B}_\bot}?
6
+
\scope{
7
+
\put\transclude/toc{false}
8
+
\put\transclude/numbered{false}
9
+
\put\transclude/expanded{false}
10
+
\subtree{\taxon{Solution} ##{\bigsqcup \Set{ \bot, \mathsf{id}(\bot), \mathsf{id}(\mathsf{id}(\bot)), \dots } = \bot}}}
11
+
}
12
+
\li{What is #{\fixop(\kappa_\False)} where #{\kappa_\False} is the constant function that always returns #{\False}?
13
+
\scope{
14
+
\put\transclude/toc{false}
15
+
\put\transclude/numbered{false}
16
+
\put\transclude/expanded{false}
17
+
\subtree{\taxon{Solution} ##{\bigsqcup \{ \bot, \kappa_F(\bot), \kappa_F(\kappa_F(\bot)), \dots \} = \False}}}}
18
+
\li{What is #{\fixop(f)} where
19
+
##{\begin{array}{l}
20
+
f : [\mathbb{N}_\bot] \rightarrow [\mathbb{N}_\bot]\\
21
+
f(x) = 1::x
22
+
\end{array}}
23
+
(where #{[\mathbb{N}_\bot]} denotes Haskell-style lazy lists of #{\mathbb{N}_\bot})?
24
+
\scope{
25
+
\put\transclude/toc{false}
26
+
\put\transclude/numbered{false}
27
+
\put\transclude/expanded{false}
28
+
\subtree{\taxon{Solution}
29
+
\p{##{\bigsqcup \{ \bot, 1::\bot, 1::1::\bot, \dots \} = 1::1::1::\cdots}
30
+
Here #{\fixop(f)} would be the semantics of the recursive definition #{\mathsf{ones} = 1 :: \mathsf{ones}}.}}}}
31
+
}
+25
trees/dt-001T.tree
+25
trees/dt-001T.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Exercise}
3
+
\author{liamoc}
4
+
\ol{
5
+
\li{Write down the first few approximations #{\Phi^m(\bot)} to #{\fixop(\Phi)}, where the higher order function #{\Phi : (\mathbb{Z}_\bot \rightarrow [\mathbb{Z}_\bot]) \rightarrow (\mathbb{Z}_\bot \rightarrow [\mathbb{Z}_\bot])} is given by:
6
+
##{\Phi(f) = \lambda n.\ n :: f (n+1)}
7
+
What is #{\Phi^m(\bot)}? What is #{\fixop(\Phi)}?}
8
+
\scope{
9
+
\put\transclude/toc{false}
10
+
\put\transclude/numbered{false}
11
+
\put\transclude/expanded{false}
12
+
\subtree{\taxon{Solution}
13
+
\p{The approximations are #{\Set{ \lambda n.\ \bot, \lambda n.\ n :: \bot, \lambda n.\ n :: (n + 1) :: \bot, \dots }}. The limit is a function that, given a natural number #{n}, produces the infinite list of natural numbers starting from #{n}.}
14
+
}}
15
+
\li{Repeat the same process, but this time for a new higher order function #{\Phi : (\mathbb{Z}_\bot \rightarrow \mathbb{Z}_\bot) \rightarrow (\mathbb{Z}_\bot \rightarrow \mathbb{Z}_\bot)} given by:
16
+
##{\Phi(f) = \lambda n.\ \text{if}\ n = 0\ \text{then}\ 0\ \text{else}\ f(n-2)}}
17
+
\scope{
18
+
\put\transclude/toc{false}
19
+
\put\transclude/numbered{false}
20
+
\put\transclude/expanded{false}
21
+
\subtree{\taxon{Solution}
22
+
\p{The #{n}th approximation returns #{0} if the input number
23
+
is non-negative, even and less than #{2n}, otherwise it diverges (returns #{\bot}). The limit returns #{0} for any non-negative even number, and diverges otherwise. }
24
+
}}
25
+
}
+16
trees/dt-001U.tree
+16
trees/dt-001U.tree
···
1
+
\import{dt-macros}
2
+
\title{Semantics of recursive functions}
3
+
\author{liamoc}
4
+
\p{Consider the function #{\Phi \in (\mathbb{N}_\bot \rightarrow \mathbb{N}_\bot) \rightarrow (\mathbb{N}_\bot \rightarrow \mathbb{N}_\bot)}, given by:
5
+
##{\Phi(f) = \lambda n.\ \text{if}\ n = 0\ \text{then}\ 1\ \text{else}\ n\cdot f(n-1)}
6
+
Looking at the first few elements of our [Kleene chain](dt-000X), we get:
7
+
##{
8
+
\begin{array}{lcl}
9
+
\Phi^0(\bot) & = & \lambda n.\ \bot \quad \text{(i.e. $\bot_{\mathbb{N}_\bot \rightarrow \mathbb{N}_\bot}$)}\\
10
+
\Phi^1(\bot) & = & \lambda n.\ \text{if}\ n = 0\ \text{then}\ 1\ \text{else}\ \bot\\
11
+
\Phi^2(\bot) & = & \lambda n.\ \text{if}\ n = 0\ \text{then}\ 1\ \text{else}\ n\cdot(\text{if}\ n - 1 = 0\ \text{then}\ 1\ \text{else}\ \bot)\\
12
+
\cdots
13
+
\end{array}
14
+
}
15
+
Continuing on, we see that the #{m}th approximation #{\Phi^m(\bot)} to #{\fixop(\Phi)} is the function that gives #{x!} for all #{x} up to #{m}, and diverges (#{\bot}) for all other arguments. Hence the limit #{\fixop(\Phi)} is the \em{factorial} function on #{\mathbb{N}_\bot}!
16
+
}
+13
trees/dt-001V.tree
+13
trees/dt-001V.tree
···
1
+
\import{dt-macros}
2
+
\title{Semantics of loops}
3
+
\author{liamoc}
4
+
\p{Armed with [the \fixop operator](dt-001Q), we can return to our semantics of #{\mathsf{while}} loops from \ref{dt-0006} and \ref{dt-000R}, and at last define their semantics without relying on dubious recursive definitions:
5
+
##{
6
+
\begin{array}{l}
7
+
\llbracket \mathsf{while}\ b\ \mathsf{do}\ c\ \mathsf{od} \rrbracket_\mathcal{C} = \fixop(f)\acr{0.5em}
8
+
\qquad \text{where}\; f(X)\ \sigma\; \triangleq \; \begin{cases} X\ (\llbracket c \rrbracket_\mathcal{C}\ \sigma) & \text{if}\ \llbracket b \rrbracket_\mathcal{B}\ \sigma = \True \\
9
+
\sigma & \text{otherwise}
10
+
\end{cases}
11
+
\end{array}
12
+
}}
13
+
\p{Proof that #{f} is [continuous](dt-001J) is technically required but is omitted here.}
+15
trees/dt-001W.tree
+15
trees/dt-001W.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Exercise}
3
+
\author{liamoc}
4
+
\p{Show that if a function #{f : A \rightarrow B} on [cpos](dt-001D) #{A} and #{B} is [monotonic](dt-000J) and #{A} is finite, then #{f} is [continuous](dt-001J). }
5
+
\p{\em{Hint}: Finite [directed](dt-0010) sets contain their [lub](dt-0017)}
6
+
\scope{
7
+
\put\transclude/toc{false}
8
+
\put\transclude/numbered{false}
9
+
\put\transclude/expanded{false}
10
+
\subtree{\taxon{Solution}
11
+
\p{Because of \ref{dt-001O}, it suffices to show the second condition of [continuity](dt-001J), as #{f} is [monotonic](dt-000J). }
12
+
\p{Because #{A} is finite, any directed subset #{X \subseteq A} is also finite, and therefore #{\bigsqcup X \in X}. Because #{f} is [monotone](dt-000J), #{f(x) \sqsubseteq f (\bigsqcup X)} for all #{x \in X}. }
13
+
\p{The solution to \ref{dt-001N} shows that #{\Set{f(x) \mid x \in X}} is [directed](dt-0010) and therefore contains its upper bound #{c}. Because #{f} is monotone, #{f(\bigsqcup X)} must be #{c} (else it would contradict the above).}
14
+
\p{Therefore #{\bigsqcup \Set{f(x) \mid x \in X} = f (\bigsqcup X)}, as required. }
15
+
}}
+40
trees/dt-001X.tree
+40
trees/dt-001X.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Exercise}
3
+
\author{liamoc}
4
+
\ol{
5
+
\li{Show that if #{A} and #{B} are [posets](dm-0004) and #{X \subseteq A \times B} is [directed](dt-0010) (by the ordering in \ref{dt-000E}), then the subsets #{\pi_0(X) \subseteq A} and #{\pi_1(X) \subseteq B} (defined below) are also [directed](dt-0010).
6
+
##{ \begin{array}{lcl}
7
+
\pi_0(X) & = & \{ a \in A \mid \exists b \in B.\ (a,b) \in X \}\\
8
+
\pi_1(X) & = & \{ b \in B \mid \exists a \in A.\ (a,b) \in X \}\\
9
+
\end{array}
10
+
}
11
+
\scope{
12
+
\put\transclude/toc{false}
13
+
\put\transclude/numbered{false}
14
+
\put\transclude/expanded{false}
15
+
\subtree{\taxon{Solution}
16
+
\p{Given two elements #{x,y \in \pi_0(X)}, we know that there exists #{b_x, b_y \in B} such that #{(x,b_x) \in X} and #{(y,b_y) \in X}. Because #{X} is [directed](dt-0010), we can conclude that there exists an [upper bound](dm-000C) #{(z, b_z) \in X} where #{x \sqsubseteq z} and #{y \sqsubseteq z}. As #{z \in \pi_0(X)}, #{z} is an [upper bound](dm-000C) in #{\pi_0(X)} for both #{x} and #{y} and thus #{\pi_0(X)} is [directed](dt-0010). The proof for #{\pi_1} is analogous.
17
+
}
18
+
}}
19
+
}
20
+
\li{ Give an example of a set #{X \subseteq \{\top,\bot\}\times\{\top,\bot\}} such that #{\pi_0(X)} and #{\pi_1(X)} are [directed](dt-0010), but #{X} is not.
21
+
\scope{
22
+
\put\transclude/toc{false}
23
+
\put\transclude/numbered{false}
24
+
\put\transclude/expanded{false}
25
+
\subtree{\taxon{Solution}
26
+
\p{#{X = \Set{(\top,\bot), (\bot,\top)}} is not directed as the two elements are not comparable, but #{\pi_0(X) = \pi_1(X) = \Set{\top,\bot}} which is directed as #{\bot \sqsubseteq \top}.}
27
+
}}
28
+
}
29
+
\li{ Show that if #{A} and #{B} are [cpos](dt-001D) and #{X \subseteq A \times B} is [directed](dt-0010), then ##{\bigsqcup X = \left(\bigsqcup \pi_0(X), \bigsqcup\pi_1(X)\right)}
30
+
\strong{Note}: Together with #{\bot_{A\times B} = (\bot_A, \bot_B)} this shows that the [Cartesian product](dm-0005) of two [cpos](dt-001D) is itself a [cpo](dt-001D).}
31
+
\scope{
32
+
\put\transclude/toc{false}
33
+
\put\transclude/numbered{false}
34
+
\put\transclude/expanded{false}
35
+
\subtree{\taxon{Solution}
36
+
\p{
37
+
Let #{(x,y) = \left(\bigsqcup \pi_0(X), \bigsqcup\pi_1(X)\right)}. Because of the ordering in \ref{dt-000E}, #{(x,y)} is certainly \em{a} [upper bound](dm-000C) of the directed set #{X}. To show it is the \em{least} [upper bound](dm-000C), assume for the sake of contradiction that #{(x,y)} is \em{not} the [least upper bound](dt-0017) of #{X}. Then, there must be a #{(v,w)\sqsubset (x,y)} such that #{\forall x \in X.\ x \sqsubseteq (v,w)}. But then, #{v} would be a lesser [upper bound](dm-000C) for #{\pi_0(X)} than #{x}, which is supposed to be the [lub](dt-0017). Thus there is a contradiction, and #{(x,y)} must be the [lub](dt-0017) of #{X}.
38
+
}
39
+
}}
40
+
}