dhil/phd-dissertation
1
0
Fork 0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 02:58:26 +00:00
Code Issues Releases Wiki Activity

another example

Browse Source
This commit is contained in:
Daniel Hillerström
2021-05-29 16:02:19 +01:00
parent d18a5e3058
commit 664956251c
3 changed files with 243 additions and 121 deletions
Download Patch File Download Diff File Expand all files Collapse all files

140
macros.tex
View File

@@ -705,4 +705,142 @@
edge from parent {} edge from parent {}
} }
; ;
\end{tikzpicture}} \end{tikzpicture}}
\newcommand{\smath}[1]{\ensuremath{{\scriptstyle #1}}}
\newcommand{\InfiniteModel}{%
\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 3.0cm/##1,
level distance = 1.0cm}]
\node (root) [draw=none] { }
child { node [opnode] {$\smath{\query 0}$}
child { node [opnode] {$\smath{\query 0}$}
child { node [draw=none,rotate=165] {$\vdots$}
edge from parent node { }
}
child { node[leaf] {$\smath{\ans\False}$}
edge from parent node { }
}
edge from parent node { }
}
child { node [leaf] {$\smath{\ans\False}$}
edge from parent node { }
}
edge from parent node { }
}
;
\end{tikzpicture}}
%
\newcommand{\ShortConjModel}{%
\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 3.5cm/##1,
level distance = 1.0cm}]
\node (root) [draw=none] { }
child { node [opnode] {$\smath{\query 0}$}
child { node [opnode] {$\smath{\query 0}$}
child { node [treenode] {$\smath{\ans\True}$}
edge from parent node { }
}
child { node[treenode] {$\smath{\ans\False}$}
edge from parent node { }
}
edge from parent node { }
}
child { node [treenode] {$\smath{\ans\False}$}
edge from parent node { }
}
edge from parent node { }
}
;
\end{tikzpicture}}
%
\newcommand{\TTTwoModel}{%
\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 8cm/##1,
level distance = 1.5cm}]
\node (root) [draw=none] { }
child { node [opnode] {$\smath{\query 0}$}
child { node [opnode] {$\smath{\query 1}$}
child { node [leaf] {$\smath{\ans\True}$}
edge from parent node { }
}
child { node[leaf] {$\smath{\ans\True}$}
edge from parent node { }
}
edge from parent node { }
}
child { node [opnode] {$\smath{\query 1}$}
child { node [leaf] {$\smath{\ans\True}$}
edge from parent node { }
}
child { node[leaf] {$\smath{\ans\True}$}
edge from parent node { }
}
edge from parent node { }
}
edge from parent node { }
}
;
\end{tikzpicture}}
%
\newcommand{\XORTwoModel}{%
\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 5.5cm/##1,
level distance = 1cm}]
\node (root) [draw=none] { }
child { node [opnode] {$\smath{\query 0}$}
child { node [opnode] {$\smath{\query 1}$}
child { node [treenode] {$\smath{\ans\False}$}
edge from parent node { }
}
child { node[treenode] {$\smath{\ans\True}$}
edge from parent node { }
}
edge from parent node { }
}
child { node [opnode] {$\smath{\query 1}$}
child { node [treenode] {$\smath{\ans\True}$}
edge from parent node { }
}
child { node[treenode] {$\smath{\ans\False}$}
edge from parent node { }
}
edge from parent node { }
}
edge from parent node { }
}
;
\end{tikzpicture}}
%
\newcommand{\SXORTwoModel}{%
\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 2.5cm/##1,
level distance = 1cm}]
\node (root) [opnode] {$\smath{\query 0}$}
child { node [opnode] {$\smath{\query 1}$}
child { node [treenode] {$\smath{\ans\False}$}
edge from parent node { }
}
child { node[treenode] {$\smath{\ans\True}$}
edge from parent node { }
}
edge from parent node { }
}
child { node [opnode] {$\smath{\query 1}$}
child { node [treenode] {$\smath{\ans\True}$}
edge from parent node { }
}
child { node[treenode] {$\smath{\ans\False}$}
edge from parent node { }
}
edge from parent node { }
}
;
\end{tikzpicture}}
%
\newcommand{\TTZeroModel}{%
\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 1cm/##1,
level distance = 1cm}]
\node (root) [draw=none] { }
child { node [treenode] {$\smath{\ans\True}$}
edge from parent node { }
}
;
\end{tikzpicture}}%

2
thesis.bib
View File

@@ -3749,4 +3749,4 @@
editor = {Andrew M. Pitts and Peter Dybjer}, editor = {Andrew M. Pitts and Peter Dybjer},
pages = {131--184}, pages = {131--184},
year = 1997 year = 1997
} }

222
thesis.tex
View File

@@ -4855,11 +4855,12 @@ designed by \citet{Longley09} in 2008~\cite{LongleyW08}. Its origin is
in game semantics, in which program evaluation is viewed as an in game semantics, in which program evaluation is viewed as an
interactive dialogue with the ambient environment~\cite{Hyland97} --- interactive dialogue with the ambient environment~\cite{Hyland97} ---
this view aligns neatly with the view of effect handler oriented this view aligns neatly with the view of effect handler oriented
programming. Curiously, \citeauthor{Longley09} and programming. Curiously, we can view catchcont and effect handlers as
\citeauthor{PlotkinP09} developed catchcont and effect handlers, ``siblings'' in the sense that \citeauthor{Longley09} and
respectively, during the same time, in the same country, in the same \citeauthor{PlotkinP09} them respectively, during the same time,
city, in the same building. Despite all of this the two operators have whilst working in the same department. However, the relationship is
not yet been related formally. presently just `spiritual' as no formal connections have been drawn
between the two operators.
The catchcont operator appears as a computation form in our calculus. The catchcont operator appears as a computation form in our calculus.
% %
@@ -4913,10 +4914,105 @@ the second component of the returned pair. Importantly, the second
$\lambda$-abstraction makes sure to bind any instances of $f$ in the $\lambda$-abstraction makes sure to bind any instances of $f$ in the
captured evaluation context once it has been reinstated by the captured evaluation context once it has been reinstated by the
\slab{Resume} rule. \slab{Resume} rule.
Let us consider an example use of catchcont to compute a tree
representing the interaction between a second-order function and its
first-order parameter.
%
\[
\bl
\dec{odd} : (\Int \to \Bool) \to \Bool \times \UnitType\\
\dec{odd}~f \defas \Record{\dec{xor}\,(f~0)\,(f~1); \Unit}
\el
\]
%
The function $\dec{odd}$ expects its environment to provide it with an
implementation of a single operation of type $\Int \to \Bool$. The
body of $\dec{odd}$ invokes, or queries, this operation twice with
arguments $0$ and $1$, respectively. The results are then tested using
exclusive-or.
Now, let us implement the environment for $\dec{odd}$.
%
\[
\bl
\dec{Dialogue} \defas [!:\Int;?:\Record{\Bool,\dec{Dialogue},\dec{Dialogue}}] \smallskip\\
\dec{env} : ((\Int \to \Bool) \to \Bool \times \UnitType) \to \dec{Dialogue}\\
\dec{env}~m \defas
\bl
\Case\;\Catchcont~f.m~f\;\{
\ba[t]{@{}l@{~}c@{~}l}
\Inl~\Record{ans;\Unit} &\mapsto& \dec{!}ans;\\
\Inr~\Record{q;k} &\mapsto& \dec{?}q\,(\dec{env}~k~\True)\,(\dec{env}~k~\False)\}
\ea
\el
\el
\]
%
We allow ourselves to use recursive data types to make the example
concise. Type $\dec{Dialogue}$ represents the dialogue between
$\dec{odd}$ and its parameter. The data structure is a standard binary
tree with two constructors: $!$ constructs a leaf holding a value of
type $\Int$ and $?$ constructs an interior node holding a value of
type $\Bool$ and two subtrees. The function $\dec{env}$ implements the
environment that $\dec{odd}$ will be run in. This function evaluates
its parameter $m$ under $\Catchcont$ which injects the operation
$f$. If $m$ returns, then the left component gets tagged with $!$,
otherwise the argument to the operation $q$ gets tagged with a $?$
along with the subtrees constructed by the two recursive applications
of $\dec{env}$.
%
% The primitive structure of catchcont makes it somewhat fiddly to
% program with it compared to other control operators as we have to
% manually unpack the data.
The following derivation gives the high-level details of how
evaluation proceeds.
% %
\begin{derivation} \begin{derivation}
1 + (\Catchcont~f. &\dec{env}~\dec{odd}\\
\reducesto^+ & \reason{$\beta$-reduction}\\
&\bl
\Case\;\Catchcont~f.\;\Record{\dec{xor}\,(f~0)\,(f~1);\Unit}\{\cdots\}
% \ba[t]{@{}l@{~}c@{~}l}
% \Inl~\Record{ans;\Unit} &\mapsto& \dec{!}ans;\\
% \Inr~\Record{q;k} &\mapsto& \dec{?}q\,(\dec{env}~k~\True)\,(\dec{env}~k~\False)\}
% \ea
\el\\
\reducesto& \reason{\slab{Capture} $\EC = \Record{\dec{xor}\,[\,]\,(f~1),\Unit}$}\\
&\bl
\Case\;\Inr\,\Record{0;\lambda x.\lambda f.\qq{\cont_{\EC}}\,x}\;\{\cdots\}
% \ba[t]{@{}l@{~}c@{~}l}
% \Inl~\Record{ans;\Unit} &\mapsto& \dec{!}ans;\\
% \Inr~\Record{q;k} &\mapsto& \dec{?}q\,\bl (\dec{env}~\qq{\cont_{\EC}}~\True)\\(\dec{env}~\qq{\cont_{\EC}}~\False)\}\el
% \ea
\el\\
\reducesto^+& \reason{\slab{Resume} $\EC$ with $\True$}\\
&\dec{?}0\,(\Case\;\Catchcont~f.\;\Record{\dec{xor}~\True\,(f~1);\Unit}\{\cdots\})\,(\dec{env}~\qq{\cont_{\EC}}~\False)\\
\reducesto^+& \reason{\slab{Capture} $\EC' = \Record{\dec{xor}~\True\,[\,], \Unit}$}\\
&\dec{?}0\,(\dec{?}1\,(\dec{env}~\qq{\cont_{\EC'}}~\True)\,(\dec{env}~\qq{\cont_{\EC'}}~\False))\,(\dec{env}~\qq{\cont_{\EC}}~\False)\\
\reducesto^+& \reason{\slab{Resume} $\EC'$ with $\True$}\\
&\dec{?}0\,\bl(\dec{?}1\,(\Case\;\Catchcont~f.\Record{\dec{xor}~\True~\True;\Unit}\;\{\cdots\})\,(\dec{env}~\qq{\cont_{\EC'}}~\False))\\(\dec{env}~\qq{\cont_{\EC}}~\False)\el\\
\reducesto^+& \reason{\slab{Value}}\\
&\dec{?}0\,\bl(\dec{?}1\,(\Case\;\Inl~\Record{\False;\Unit}\;\{\cdots\})\,(\dec{env}~\qq{\cont_{\EC'}}~\False))\\(\dec{env}~\qq{\cont_{\EC}}~\False)\el\\
\reducesto& \reason{$\beta$-reduction}\\
&\dec{?}0\,\bl(\dec{?}1\,\dec{!}\False\,(\dec{env}~\qq{\cont_{\EC'}}~\False))\,(\dec{env}~\qq{\cont_{\EC}}~\False)\el\\
\reducesto^+&\reason{Same reasoning}\\
&?0\,(?1\,!\False\,!\True)\,(?1\,!\True\,!\False)
\end{derivation} \end{derivation}
%
Figure~\ref{fig:decision-tree-cc} visualises this result as a binary
tree. The example here does not make use of the `continuation
component', the interested reader may consult \citet{LongleyW08} for
an example usage.
%
\begin{figure}
\begin{center}
\scalebox{1.3}{\SXORTwoModel}
\end{center}
\caption{Visualisation of the result obtained by
$\dec{env}~\dec{odd}$.}\label{fig:decision-tree-cc}
\end{figure}
% \subsection{Second-class control operators} % \subsection{Second-class control operators}
% Coroutines, async/await, generators/iterators, amb. % Coroutines, async/await, generators/iterators, amb.
@@ -17080,118 +17176,6 @@ applying it to $\dec{q}_1$ or $\dec{q}_2$ yields $\True$.
% %
\medskip \medskip
\newcommand{\smath}[1]{\ensuremath{{\scriptstyle #1}}}
\newcommand{\InfiniteModel}{%
\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 3.0cm/##1,
level distance = 1.0cm}]
\node (root) [draw=none] { }
child { node [opnode] {$\smath{\query 0}$}
child { node [opnode] {$\smath{\query 0}$}
child { node [draw=none,rotate=165] {$\vdots$}
edge from parent node { }
}
child { node[leaf] {$\smath{\ans\False}$}
edge from parent node { }
}
edge from parent node { }
}
child { node [leaf] {$\smath{\ans\False}$}
edge from parent node { }
}
edge from parent node { }
}
;
\end{tikzpicture}}
%
\newcommand{\ShortConjModel}{%
\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 3.5cm/##1,
level distance = 1.0cm}]
\node (root) [draw=none] { }
child { node [opnode] {$\smath{\query 0}$}
child { node [opnode] {$\smath{\query 0}$}
child { node [treenode] {$\smath{\ans\True}$}
edge from parent node { }
}
child { node[treenode] {$\smath{\ans\False}$}
edge from parent node { }
}
edge from parent node { }
}
child { node [treenode] {$\smath{\ans\False}$}
edge from parent node { }
}
edge from parent node { }
}
;
\end{tikzpicture}}
%
\newcommand{\TTTwoModel}{%
\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 8cm/##1,
level distance = 1.5cm}]
\node (root) [draw=none] { }
child { node [opnode] {$\smath{\query 0}$}
child { node [opnode] {$\smath{\query 1}$}
child { node [leaf] {$\smath{\ans\True}$}
edge from parent node { }
}
child { node[leaf] {$\smath{\ans\True}$}
edge from parent node { }
}
edge from parent node { }
}
child { node [opnode] {$\smath{\query 1}$}
child { node [leaf] {$\smath{\ans\True}$}
edge from parent node { }
}
child { node[leaf] {$\smath{\ans\True}$}
edge from parent node { }
}
edge from parent node { }
}
edge from parent node { }
}
;
\end{tikzpicture}}
%
\newcommand{\XORTwoModel}{%
\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 5.5cm/##1,
level distance = 1cm}]
\node (root) [draw=none] { }
child { node [opnode] {$\smath{\query 0}$}
child { node [opnode] {$\smath{\query 1}$}
child { node [treenode] {$\smath{\ans\False}$}
edge from parent node { }
}
child { node[treenode] {$\smath{\ans\True}$}
edge from parent node { }
}
edge from parent node { }
}
child { node [opnode] {$\smath{\query 1}$}
child { node [treenode] {$\smath{\ans\True}$}
edge from parent node { }
}
child { node[treenode] {$\smath{\ans\False}$}
edge from parent node { }
}
edge from parent node { }
}
edge from parent node { }
}
;
\end{tikzpicture}}
%
\newcommand{\TTZeroModel}{%
\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 1cm/##1,
level distance = 1cm}]
\node (root) [draw=none] { }
child { node [treenode] {$\smath{\ans\True}$}
edge from parent node { }
}
;
\end{tikzpicture}}%
% %
\begin{figure} \begin{figure}
\centering \centering
@@ -17279,7 +17263,7 @@ is precisely the number of $\ans \True$ leaves in the tree.
Of the examples we have given, the tree for $\dec{T}_0$ is 0-standard; Of the examples we have given, the tree for $\dec{T}_0$ is 0-standard;
those for $\dec{I}_0$ and $\dec{I}_1$ are 1-standard; that for those for $\dec{I}_0$ and $\dec{I}_1$ are 1-standard; that for
$\dec{Odd}_n$ is $n$-standard; and the rest are not $n$-standard for $\dec{odd}_n$ is $n$-standard; and the rest are not $n$-standard for
any $n$. any $n$.
\subsection{Formal definitions} \subsection{Formal definitions}