finished recursive domains

trees/dt/dt-004O.tree

···
 \transclude{dt-004W}
 \transclude{dt-004X}
 \transclude{dt-004Y}
-\transclude{dt-0050}
+\transclude{dt-005M}
+\transclude{dt-0050}
+\transclude{dt-005N}

trees/dt/dt-004Z.tree

···
 \transclude{dt-004J}
 \transclude{dt-004O}
 \transclude{dt-0052}
-\strong{TODO: Colimit construction}
-\strong{TODO: Producing Endofunctors}
-\strong{TODO: Untyped Lambda Calculus}
+\transclude{dt-005L}

trees/dt/dt-0052.tree

···
 \author{liamoc}
 \title{From #{\textbf{Cpo}} to #{\textbf{Cpo}^{\textbf{R}}}}
 \transclude{dt-0053}
+\transclude{dt-005O}
 \transclude{dt-0054}
 \transclude{dt-0055}
 \transclude{dt-0056}
···
 \transclude{dt-0058}
 \transclude{dt-0059}
 \transclude{dt-005A}
+\transclude{dt-005I}
 \transclude{dt-005B}
 \transclude{dt-005H}

trees/dt/dt-005I.tree

···
+\import{dt-macros}
+\title{Extending cpo Mappings to endofunctors on #{\textbf{Cpo}^\mathbf{R}}}
+\author{liamoc}
+\p{If #{\mathcal{F}} is a mapping on [cpos](dt-001D) built up from basic cpos using the constructions #{\times}, #{\otimes}, #{+}, #{\oplus}, #{(\cdot)_\bot}, \em{as well as} #{\contto} and #{\strictto}, then #{\mathcal{F}} extends to a (\em{covariant}!) [cocontinuous functor](dt-005E) on #{\textbf{Cpo}^\mathbf{R}}. 
+We shall detail the construction for products and functions here, but the other constructions are all similar.}
+\transclude{dt-005J}
+\transclude{dt-005K}

trees/dt/dt-005J.tree

···
+\import{dt-macros}
+\taxon{Definition}
+\author{liamoc}
+\title{#{\times} operation for retraction pairs}
+\p{
+Given two [retraction pairs](dt-0054) #{(f,g)} and #{(h,i)}, our [retraction pair](dt-0054) for their [product](dt-0021) is just the product of their \em{embedding} and \em{projection}, i.e. #{(f \times h, g \times i)}, using our [product operation on continuous functions](dt-0026):
+##{
+\inferrule{A \rpair{f}{g} B\quad C \rpair{h}{i} D}{A\times C \rpair{f \times h}{g \times i} B \times D}
+}
+}

trees/dt/dt-005K.tree

···
+\import{dt-macros}
+\taxon{Definition}
+\author{liamoc}
+\title{#{\contto} operation for retraction pairs}
+\p{
+We are given two [retraction pairs](dt-0054) #{A \rpair{f}{g} B} and
+ #{C \rpair{h}{i} D}. To define a suitable \em{covariant} [functor](dt-005E), we define our morphism mapping in terms of our #{\contto} [operation on continuous functions](dt-002X): ##{ (f,g) \contto (h,i) \; \triangleq \; (g\contto h, f \contto i)}
+Note that the positions of #{f} and #{g} are swapped in the above definition.
+##{
+\inferrule{A \rpair{f}{g} B \quad C \rpair{h}{i} D}{A \contto C \rpair{g \contto h}{f \contto i} B \contto D}
+}
+Unlike [with the category #{\textbf{Cpo}}](dt-0053), this functor is not [contravariant](dm-000S) but \em{covariant}: Note the positions of #{A} and #{B} are not swapped!
+}

trees/dt/dt-005L.tree

···
+\import{dt-macros}
+\title{Semantics of untyped #{\lambda}-calculus}
+\author{liamoc}
+\p{
+Recall the untyped #{\lambda} calculus:
+\transclude{dt-004K}
+We mentioned before that the semantic domain of this language must be a cpo #{D} such that ##{D \simeq D\contto D} In other words, solutions  to this equation are fixed points of #{\mathcal{F}(X) = X\contto X}. The least such fixed point can expressed, by \ref{dt-005B}, as the [colimit](dt-005H) of the [#{\omega}-chain](dt-005C):
+\figure{
+\tex{\usepackage{tikz-cd}}{
+\begin{tikzcd}
+	\mathbf{1} \ar[r,"f_0",->,yshift=0.2em]\ar[r,"g_0"', <-,yshift=-0.2em]  &
+	\mathcal{F}(\mathbf{1}) \ar[r,"f_1",->,yshift=0.2em]\ar[r,"g_1"', <-,yshift=-0.2em]  &
+	\mathcal{F}(\mathcal{F}(\mathbf{1})) \ar[r,"f_2",->,yshift=0.2em]\ar[r,"g_2"', <-,yshift=-0.2em]  &
+	\mathcal{F}(\mathcal{F}(\mathcal{F}(\mathbf{1}))) \ar[r,-,dashed,yshift=0.2em]\ar[r,dashed,-,yshift=-0.2em]  &
+	\cdots
+\end{tikzcd}
+}}
+But, the least solution to this equation is \em{trivial}: #{D_\infty \simeq \mathbf{1}}, because #{\mathbf{1} \simeq \mathbf{1}\contto \mathbf{1}}. A non-trivial solution is obtained by starting the chain at #{\mathbf{2}}, the [cpo](dt-001D) containing just #{\Set{\top,\bot}}, rather than #{\mathbf{1}}.
+\figure{\tex{\usepackage{tikz-cd}}{
+\begin{tikzcd}
+	\mathbf{2} \ar[r,"f_0",->,yshift=0.2em]\ar[r,"g_0"', <-,yshift=-0.2em]  &
+	\mathcal{F}(\mathbf{2}) \ar[r,"f_1",->,yshift=0.2em]\ar[r,"g_1"', <-,yshift=-0.2em]  &
+	\mathcal{F}(\mathcal{F}(\mathbf{2})) \ar[r,"f_2",->,yshift=0.2em]\ar[r,"g_2"', <-,yshift=-0.2em]  &
+	\mathcal{F}(\mathcal{F}(\mathcal{F}(\mathbf{2}))) \ar[r,-,dashed,yshift=0.2em]\ar[r,dashed,-,yshift=-0.2em]  &
+	\cdots
+\end{tikzcd}
+}}}
+\p{
+We will now sketch a proof of the [retraction pair](dt-0054) between #{D_\infty} and #{D_\infty \contto D_\infty}, by providing two functions, #{\textbf{\textsf{up}} : D_\infty \rightarrow (D_\infty\contto D_\infty)} and its inverse #{\textbf{\textsf{down}} : (D_\infty\contto D_\infty) \rightarrow D_\infty}. }
+\p{
+Observe that each element of #{D_i} (for #{i > 0}) is a \em{function} #{D_{i-1} \contto D_{i-1}}. Therefore, an element of [the colimit #{D_\infty}](dt-005H) is an #{\omega}-tuple of such functions. To define #{\textbf{\textsf{up}}(d)(x)}, we must essentially "apply" each function in the element #{d \in D_\infty} (viewed as an #{\omega}-tuple of functions) to the element #{x \in D_\infty} (viewed as an #{\omega}-tuple of values). More specifically, we say that #{\textbf{\textsf{up}}(d)(x)} is an #{\omega}-tuple #{(y_m \mid y \in \mathbb{N})}, as follows:
+##{
+y_m = \bigsqcup_{k \in \mathbb{N}} \theta_{m+k,m}(d_{m+k+1}(x_{m+k}))
+}
+To define #{\textbf{\textsf{down}}(f)}, we are given a ([continuous](dt-001J)) function #{f : D_\infty\contto D_\infty} and must construct the #{\omega}-tuple of approximations at every #{D_n}. We do this by projecting the action of #{f} down to #{D_n}. We say that #{\textbf{\textsf{down}}(f)} is an #{\omega}-tuple #{(v_n \mid n \in \mathbb{N})} where:
+##{
+\begin{array}{lcl}
+	v_0 & \triangleq & \theta_{\infty,0}(f(\theta_{0,\infty}(\bot_{D_0})))\\
+	v_{n+1} & \triangleq & \theta_{\infty,n} \circ f \circ \theta_{n,\infty}
+\end{array}
+}}
+\subtree{
+\taxon{Definition}
+\title{Denotations for untyped #{\lambda}-calculus}
+\p{
+Using the new functions #{\textbf{\textsf{up}}} and #{\textbf{\textsf{down}}}, it is now straightforward to define a semantics for untyped #{\lambda}-calculus, where #{\sigma} is an environment #{\mathsf{Var} \rightarrow D_\infty}:
+##{\llbracket \cdot \rrbracket : (\mathsf{Var} \rightarrow D_\infty)\contto D_\infty}
+##{
+\begin{array}{lcl}
+\llbracket x \rrbracket \sigma 	& = & \sigma (x) \\
+\llbracket e_0\ e_1 \rrbracket \sigma & = & \textbf{\textsf{up}}(\llbracket e_0 \rrbracket \sigma) (\llbracket e_1 \rrbracket \sigma)\\
+\llbracket \lambda x.\ e \rrbracket \sigma & = & \textbf{\textsf{down}}(\boldsymbol{\lambda} v \in D_{\infty}.\ \llbracket e \rrbracket\ \sigma(x \mapsto v) )
+\end{array}
+}
+This semantics does not distinguish non-terminating computations from terminating ones. To model call-by-value more faithfully, we could use the equation #{D \simeq D\contto D_\bot} instead, and for call-by-name we could use #{D \simeq D_\bot\contto D_\bot}. The constructions are very similar.
+}
+}

trees/dt/dt-005M.tree

···
+\import{dt-macros}
+\taxon{Exercise}
+\author{liamoc}
+\p{
+Show that #{\mathcal{F}(X) \triangleq \mathbf{1} + X} and #{\mathcal{F}(f) \triangleq \mathsf{id}_\mathbf{1} + f} (using our [#{+} operator for functions](dt-0037)) define an [endofunctor](dt-004T) #{\mathbf{Cpo} \rightarrow \mathbf{Cpo}}, i.e. that they satisfy the functor laws.}
+\solnblock{
+\ol{
+	\li{
+		We must show #{\mathcal{F}(\mathsf{id}_A : A \contto A) = \mathsf{id}_{\mathcal{F}(A)} : \mathcal{F}(A) \contto \mathcal{F}(A)}. 
+		##{\begin{array}{lcl}
+		\mathcal{F}(\mathsf{id}_A)& =& \mathsf{id}_\mathbf{1} + \mathsf{id}_A\\
+		                           &=& \mathsf{id}_{\mathbf{1} + A}\\
+								   &=& \mathsf{id}_{\mathcal{F}(A)}
+								  \end{array}}
+		
+	}
+	\li{
+		We must show #{\mathcal{F}(f \circ g) = \mathcal{F}(f) \circ \mathcal{F}(g)}.
+		##{\begin{array}{lcl}
+	\mathcal{F}(f \circ g) &=& \mathsf{id}_\mathbf{1} + (f \circ g) \\
+	                        &=& (\mathsf{id}_\mathbf{1} + f) \circ (\mathsf{id}_\mathbf{1} + g) \\
+							& = & \mathcal{F}(f) \circ \mathcal{F}(g)
+								  \end{array}}
+	}
+}
+}

trees/dt/dt-005N.tree

···
+\import{dt-macros}
+\taxon{Exercise}
+\author{liamoc}
+\p{
+The lazy natural numbers, also called conats, are defined as the least solution to the equation #{X \simeq \mathbf{1} + X}. 
+\ol{
+\li{Sketch the first four approximations to the least fixed point. Call the two sum injections #{\mathsf{zero}} and #{\mathsf{succ}}.
+\solnblock{
+##{
+\begin{array}{lcl}
+A_0 & = & \Set{\bot} \\
+A_1 & = & \Set{\mathsf{zero}\ \bot, \mathsf{succ}\ \bot, \bot} \\
+A_2 & = & \Set{\mathsf{zero}\ \bot, \mathsf{succ}\ \bot, \mathsf{succ}\ (\mathsf{zero}\ \bot), \mathsf{succ}\ (\mathsf{succ}\ \bot), \bot} \\
+A_3 & = & \Set{\mathsf{zero}\ \bot, \mathsf{succ}\ \bot, \mathsf{succ}\ (\mathsf{zero}\ \bot), \mathsf{succ}\ (\mathsf{succ}\ \bot), \mathsf{succ}\ (\mathsf{succ}\ (\mathsf{zero}\ \bot)), \mathsf{succ}\ (\mathsf{succ}\ (\mathsf{succ}\ \bot)), \bot} \\
+\end{array}
+}
+}}
+\li{Repeat this exercise assuming:
+\ol{
+	\li{ #{\mathsf{zero}} is strict (i.e. #{\mathsf{zero}\ \bot = \bot})
+\solnblock{
+	##{
+	\begin{array}{lcl}
+	A_0 & = & \Set{\bot} \\
+	A_1 & = & \Set{\mathsf{succ}\ \bot, \bot} \\
+	A_2 & = & \Set{\mathsf{succ}\ \bot, \mathsf{succ}\ (\mathsf{succ}\ \bot), \bot} \\
+	A_3 & = & \Set{\mathsf{succ}\ \bot, \mathsf{succ}\ (\mathsf{succ}\ \bot), \mathsf{succ}\ (\mathsf{succ}\ (\mathsf{succ}\ \bot)), \bot} \\
+	\end{array}
+	}
+	}
+}
+	\li{ #{\mathsf{succ}} is strict (i.e. #{\mathsf{succ}\ \bot = \bot})
+\solnblock{
+	##{
+	\begin{array}{lcl}
+	A_0 & = & \Set{\bot} \\
+	A_1 & = & \Set{\mathsf{zero}\ \bot, \bot} \\
+	A_2 & = & \Set{\mathsf{zero}\ \bot, \mathsf{succ}\ (\mathsf{zero}\ \bot), \bot} \\
+	A_3 & = & \Set{\mathsf{zero}\ \bot, \mathsf{succ}\ (\mathsf{zero}\ \bot),  \mathsf{succ}\ (\mathsf{succ}\ (\mathsf{zero}\ \bot)), \bot} \\
+	\end{array}
+	}
+	}
+}
+}
+}
+}}

trees/dt/dt-005O.tree

···
+\import{dt-macros}
+\taxon{Exercise}
+\author{liamoc}
+\p{
+Show that, in contrast to #{\mathcal{F}(X) = X\contto \mathbb{Z}_\bot} from \ref{dt-0053}, the mapping #{\mathcal{G}(X) = \mathbb{Z}_\bot\contto X} \em{can} be extended to [continuous](dt-001J) functions giving a \em{covariant} [endofunctor](dt-004T) on #{\textbf{Cpo}}.
+\solnblock{
+\p{Given a continuous function #{f : A \contto B}, we must produce a continuous function #{\mathcal{F}(f) : (\mathbb{Z}_\bot \contto A) \contto (\mathbb{Z}_\bot \contto B)}, defined as follows:
+##{\mathcal{F}(f)(g)(x) = f \circ g(x)}
+Composition of continuous functions preserves continuity. The [functor laws](dt-004T) can be shown straightforwardly.
+}
+}}