diff --git a/macros.tex b/macros.tex index efee607..28d3f6c 100644 --- a/macros.tex +++ b/macros.tex @@ -705,4 +705,142 @@ edge from parent {} } ; -\end{tikzpicture}} \ No newline at end of file +\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}}% \ No newline at end of file diff --git a/thesis.bib b/thesis.bib index eb8692d..3f2a5a4 100644 --- a/thesis.bib +++ b/thesis.bib @@ -3749,4 +3749,4 @@ editor = {Andrew M. Pitts and Peter Dybjer}, pages = {131--184}, year = 1997 -} +} \ No newline at end of file diff --git a/thesis.tex b/thesis.tex index 150bba6..960a5dc 100644 --- a/thesis.tex +++ b/thesis.tex @@ -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 interactive dialogue with the ambient environment~\cite{Hyland97} --- this view aligns neatly with the view of effect handler oriented -programming. Curiously, \citeauthor{Longley09} and -\citeauthor{PlotkinP09} developed catchcont and effect handlers, -respectively, during the same time, in the same country, in the same -city, in the same building. Despite all of this the two operators have -not yet been related formally. +programming. Curiously, we can view catchcont and effect handlers as +``siblings'' in the sense that \citeauthor{Longley09} and +\citeauthor{PlotkinP09} them respectively, during the same time, +whilst working in the same department. However, the relationship is +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. % @@ -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 captured evaluation context once it has been reinstated by the \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} - 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} +% +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} % Coroutines, async/await, generators/iterators, amb. @@ -17080,118 +17176,6 @@ applying it to $\dec{q}_1$ or $\dec{q}_2$ yields $\True$. % \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} \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; 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$. \subsection{Formal definitions}