Consistency

macros.tex

@@ -705,4 +705,142 @@
     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}}%

thesis.bib

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

thesis.tex

@@ -262,9 +262,10 @@
   with the world.
   %
   Programs use words from this vocabulary with a preconceived idea of
-  their meaning, however, importantly words are just mere syntax. The
+  their meaning, however, importantly, words are just mere syntax. The
-  semantics of each word is determined by the operating system
+  semantics of each word is determined by the operating
-  (typically such that it aligns with the intent of the program).
+  system (typically such that it aligns with the intent of the
+  program).
 
   This separation of syntax and semantics makes it possible for
   programs and operating systems to evolve independently, because any
@@ -272,7 +273,20 @@
   to the expectations of the program. It has proven to be a remarkably
   successful model for building and maintaining computer programs.
 
-  \emph{Effect handlers} localise are tiny programmable operating systems 
+  Conventionally, an operating system has been a complex and
+  monolithic single global entity in a computer system.
+  %
+  However, \emph{effect handlers} are a novel programming abstraction,
+  which enables programs to be decomposed into syntax and semantics
+  internally, by localising the notion of operating systems. In
+  essence, an effect handler is a tiny programmable operating system,
+  that a program may use internally to determine the meaning of its
+  subprograms. The key property of effect handlers is that they
+  compose seamlessly, and as a result the semantics of a program can
+  be compartmentalised into several fine-grained and comprehensible
+  components. The ability to seamlessly swap out one component for
+  another component provides a promising basis for modular
+  construction and reconfiguration of computer programs.
 
   In this dissertation I develop the foundations for programming with
   effect handlers. Specifically, I present a practical design for
@@ -280,16 +294,6 @@
   two universal implementation strategies for effect handlers, and I
   give a precise mathematical characterisation of the inherent
   computational efficiency of effect handlers.
-
-  % The meaning of words This separation of
-
- % modular reconfiguration of programs
-
-  % Computer programs interact with the real world by way of \emph{system calls}\dots this interaction
-  % is facilitated by the operating system, which is responsible for
-  % %
-  % Effect handlers provide a modular means for structuring the internal
-  % code of computer programs.
 \end{laysummary}
 
 %% Acknowledgements
@@ -3073,7 +3077,7 @@ language.
     \hline
   \end{tabular}
   \caption{Classification of first-class sequential control operators.}\label{tbl:classify-ctrl}
-  \dhil{TODO: Possibly split into two tables: undelimited and delimited. Change the table to display the behaviour of control reifiers.}
+  % \dhil{TODO: Possibly split into two tables: undelimited and delimited. Change the table to display the behaviour of control reifiers.}
 \end{table}
 %
 
@@ -3094,11 +3098,11 @@ depicts the syntax of types and terms in the calculus.
 \begin{figure}
   \centering
 \begin{syntax}
-  \slab{Types}        & A,B &::=& \UnitType \mid A \to B \mid A \times B \mid \Cont\,\Record{A;B} \mid A + B \smallskip\\
+  \slab{Types}        & A,B \in \TypeCat &::=& \UnitType \mid A \to B \mid A \times B \mid \Cont\,\Record{A;B} \mid A + B \smallskip\\
-  \slab{Values}       & V,W &::=& \Unit \mid \lambda x^A.M \mid \Record{V;W} \mid \cont_\EC \mid \Inl~V \mid \Inr~W \mid x\\
+  \slab{Values}       & V,W \in \ValCat &::=& \Unit \mid \lambda x^A.M \mid \Record{V;W} \mid \cont_\EC \mid \Inl~V \mid \Inr~W \mid x\\
-  \slab{Computations} & M,N &::=& \Return\;V \mid \Let\;x \revto M \;\In\;N \mid \Let\;\Record{x;y} = V \;\In\; N \\
+  \slab{Computations} & M,N \in \CompCat &::=& \Return\;V \mid \Let\;x \revto M \;\In\;N \mid \Let\;\Record{x;y} = V \;\In\; N \\
                        &     &\mid& V\,W \mid \Continue~V~W \smallskip\\
-  \slab{Evaluation\textrm{ }contexts} & \EC &::=& [\,] \mid \Let\;x \revto \EC \;\In\;N
+  \slab{Evaluation\textrm{ }contexts} & \EC \in \CatName{Ctx} &::=& [\,] \mid \Let\;x \revto \EC \;\In\;N
 \end{syntax}
 \caption{Types and term syntax}\label{fig:pcf-lang-control}
 \end{figure}
@@ -3125,6 +3129,9 @@ save some ink, we will use the following notation.
 \[
   \qq{\cont_{\EC}} \defas \lambda x. \Continue~\cont_{\EC}~x
 \]
+%
+We will permit ourselves various syntactic sugar to keep the examples
+relative concise, e.g. we write the examples in ordinary call-by-value.
 
 \subsection{Undelimited control operators}
 %
@@ -3243,7 +3250,7 @@ identical to \citeauthor{Reynolds98a}' escape operator, save for the
 syntax.
 %
 \[
-  M,N ::= \cdots \mid \Catch~k.M
+  M,N \in \CompCat ::= \cdots \mid \Catch~k.M
 \]
 %
 Although, their syntax differ, their dynamic semantics are the same.
@@ -3435,9 +3442,9 @@ The other way around also appears to be impossible, because neither
 the base calculus nor $\Callcomc$ has the ability to discard an
 evaluation context.
 %
-\dhil{Remark that $\Callcomc$ was originally obtained by decomposing
+% \dhil{Remark that $\Callcomc$ was originally obtained by decomposing
-  $\fcontrol$ a continuation composing primitive and an abortive
+%   $\fcontrol$ a continuation composing primitive and an abortive
-  primitive. Source: Matthew Flatt, comp.lang.scheme, May 2007}
+%   primitive. Source: Matthew Flatt, comp.lang.scheme, May 2007}
 
 \paragraph{\FelleisenC{} and \FelleisenF{}}
 %
@@ -3995,7 +4002,7 @@ In our setting both shift and reset appear as computation forms.
 %
 \begin{syntax}
  % & V, W &::=& \cdots \mid \shift\\
- & M, N &::=& \cdots \mid \shift\; k.M \mid \reset{M}
+ & M, N \in \CompCat &::=& \cdots \mid \shift\; k.M \mid \reset{M}
 \end{syntax}
 %
 The $\shift$ construct captures the continuation delimited by an
@@ -4177,7 +4184,7 @@ continuation'').
 Splitter and the two operations abort and calldc are value forms.
 %
 \[
-  V,W ::= \cdots \mid \splitter \mid \abort \mid \calldc
+  V,W \in \ValCat ::= \cdots \mid \splitter \mid \abort \mid \calldc
 \]
 %
 In their treatment of splitter, \citeauthor{QueinnecS91} gave three
@@ -4188,9 +4195,9 @@ a pleasant static semantics too. Thus, we further extend the syntactic
 categories with the machinery for first-class prompts.
 %
 \begin{syntax}
-  & A,B &::=& \cdots \mid \prompttype~A \smallskip\\
+  & A,B \in \TypeCat &::=& \cdots \mid \prompttype~A \smallskip\\
-  & V,W &::=& \cdots \mid p\\
+  & V,W \in \ValCat &::=& \cdots \mid p\\
-  & M,N &::=& \cdots \mid \Prompt_V~M
+  & M,N \in \CompCat &::=& \cdots \mid \Prompt_V~M
 \end{syntax}
 %
 The type $\prompttype~A$ classifies prompts whose answer type is
@@ -4356,8 +4363,8 @@ The operator fcontrol is a value and prompt with handler is a
 computation.
 %
 \begin{syntax}
-  & V, W &::=& \cdots \mid \fcontrol\\
+  & V, W \in \ValCat &::=& \cdots \mid \fcontrol\\
-  & M, N &::=& \cdots \mid \fprompt~V.M
+  & M, N \in \CompCat &::=& \cdots \mid \fprompt~V.M
 \end{syntax}
 %
 As with $\Callcc$, the value $\fcontrol$ may be regarded as a special
@@ -4416,9 +4423,9 @@ thus, augments the syntactic categories of types, values, and
 computations.
 %
 \begin{syntax}
-  & A,B  &::=& \cdots \mid \prompttype~A \smallskip\\
+  & A,B \in \TypeCat &::=& \cdots \mid \prompttype~A \smallskip\\
-  & V,W  &::=& \cdots \mid p \mid \newPrompt\\
+  & V,W \in \ValCat &::=& \cdots \mid p \mid \newPrompt\\
-  & M,N  &::=& \cdots \mid \Set\;V\;\In\;N \mid \Cupto~V~k.M
+  & M,N \in \CompCat &::=& \cdots \mid \Set\;V\;\In\;N \mid \Cupto~V~k.M
 \end{syntax}
 %
 The type $\prompttype~A$ is the type of prompts. It is parameterised
@@ -4851,11 +4858,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
+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.
 %
@@ -4876,7 +4884,7 @@ The typing rule for $\Catchcont$ is as follows.
 \begin{mathpar}
   \inferrule*
     {\typ{\Gamma, f : A \to B}{M : C \times D} \\ \Ground\;C}
-    {\typ{\Gamma}{\Catchcont\;f.M : C \times ((A \to B) \to D) + (A \times (B \to (A \to B) \to C \times D))}}
+    {\typ{\Gamma}{\Catchcont~f.M : C \times ((A \to B) \to D) + (A \times (B \to (A \to B) \to C \times D))}}
 \end{mathpar}
 %
 The computation handled by $\Catchcont$ must return a pair, where the
@@ -4895,9 +4903,9 @@ The operational rules for $\Catchcont$ are as follows.
 %
 \begin{reductions}
   \slab{Value} &
-     \Catchcont \; f . \Record{V;W} &\reducesto& \Inl\; \Record{V;\lambda\,f. W}\\
+     \Catchcont~f . \Record{V;W} &\reducesto& \Inl\; \Record{V;\lambda\,f. W}\\
   \slab{Capture} &
-     \Catchcont \; f .\EC[\,f\,V]   &\reducesto& \Inr\; \Record{V; \lambda x. \lambda f. \Continue~\cont_{\EC}~x}\\
+     \Catchcont~f .\EC[\,f\,V]   &\reducesto& \Inr\; \Record{V; \lambda x. \lambda f. \Continue~\cont_{\EC}~x}\\
   \slab{Resume} & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]
 \end{reductions}
 %
@@ -4909,6 +4917,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}
+  &\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.
 
@@ -5065,11 +5172,11 @@ implementation strategies.
     \hline
     Eff      & Effect handlers & Virtual machine, interpreter \\
     \hline
-    Effekt   & Lexical effect handlers & ??\\
+    Effekt   & Lexical effect handlers & CPS\\
     \hline
     Frank    & N-ary effect handlers & CEK machine \\
-    \hline
+    % \hline
-    Gauche   & callcc, shift/reset & Virtual machine \\
+    % Gauche   & callcc, shift/reset & Virtual machine \\
     \hline
     Helium   & Effect handlers & CEK machine \\
     \hline
@@ -5095,7 +5202,6 @@ implementation strategies.
     \hline
   \end{tabular}
   \caption{Some languages and their implementation strategies for continuations.}\label{tbl:ctrl-operators-impls}
-  \dhil{TODO: Figure out which implementation strategy Effekt uses}
 \end{table}
 %
 The control stack provides a adequate runtime representation of
@@ -5939,15 +6045,14 @@ calls due to \citet{Clinger98}. First, we define what it means for a
 computation to syntactically \emph{appear in tail position}.
 %
 \begin{definition}[Tail position]\label{def:tail-comp}
-  Tail position is a transitive notion for computation terms, which is
+  Tail position is defined for computation terms as follows.
-  defined inductively as follows.
   %
   \begin{itemize}
     \item The body $M$ of a $\lambda$-abstraction ($\lambda x. M$) appears in
       tail position.
     \item The body $M$ of a $\Lambda$-abstraction $(\Lambda \alpha.M)$
       appears in tail position.
-    \item If $\Case\;V\;\{\ell\,x \mapsto M; y \mapsto N\}$ appears in tail
+    \item If $\Case\;V\;\{\ell~x \mapsto M; y \mapsto N\}$ appears in tail
       position, then both $M$ and $N$ appear in tail positions.
     \item If $\Let\;\Record{\ell = x; y} = V \;\In\;N$ appears in tail
       position, then $N$ is in tail position.
@@ -6347,6 +6452,54 @@ combination of fine-grain call-by-value and evaluation contexts
 provide the basis for a convenient, simple semantic framework for
 working with continuations.
 
+\paragraph{Syntactic sugar}
+We will adopt a few conventions to make the notation more convenient
+for writing out examples. First, we elide type annotations when they
+are clear from the context.
+%
+We will often write code in direct-style assuming the standard
+left-to-right call-by-value elaboration into fine-grain
+call-by-value~\citep{Moggi91, FlanaganSDF93}.
+%
+For example, the expression $f\,(h\,w) + g\,\Unit$ is syntactic sugar
+for:
+%
+{
+\[
+      \ba[t]{@{~}l}
+      \Let\; x \revto h\,w \;\In\;
+      \Let\; y \revto f\,x \;\In\;
+      \Let\; z \revto g\,\Unit \;\In\;
+      y + z
+      \ea
+\]}%
+%
+We define sequencing of computations in the standard way.
+%
+{
+\[
+  M;N \defas \Let\;x \revto M \;\In\;N, \quad \text{where $x \notin FV(N)$}
+\]}%
+%
+We make use of standard syntactic sugar for pattern matching. For
+instance, we write
+%
+{
+\[
+  \lambda\Unit.M \defas \lambda x^{\One}.M, \quad \text{where $x \notin FV(M)$}
+\]}%
+%
+for suspended computations.  We encode booleans using variants:
+\begin{mathpar}
+\Bool \defas [\dec{True}:\UnitType;\dec{False}:\UnitType]
+
+\True \defas \dec{True}\,\Unit
+
+\False \defas \dec{False}\,\Unit
+
+\If\;V\;\Then\;M\;\Else\;N \defas \Case\;V\;\{\dec{True}~\Unit \mapsto M; \dec{False}~\Unit \mapsto N\}
+\end{mathpar}%
+
 \section{Metatheoretic properties of \BCalc{}}
 \label{sec:base-language-metatheory}
 
@@ -16254,7 +16407,7 @@ The constants have the following types.
   \EC[M] &\reducesto& \EC[N], \hfill \text{if }M \reducesto N \\
 \end{reductions}
 \begin{syntax}
-\slab{Evaluation\textrm{ }contexts} &  \mathcal{E} &::=& [\,] \mid \Let \; x \revto \mathcal{E} \; \In \; N
+\slab{Evaluation\textrm{ }contexts} &  \mathcal{E} \in \EvalCat &::=& [\,] \mid \Let \; x \revto \mathcal{E} \; \In \; N
 \end{syntax}
 \caption{Contextual small-step operational semantics.}
 \label{fig:small-step}
@@ -16340,9 +16493,9 @@ We now define $\HPCF$ as an extension of $\BPCF$.
 {
 \begin{syntax}
 \slab{Operation\textrm{ }symbols} &\ell \in \mathcal{L} & & \\
-\slab{Signatures}        &\Sigma&::=& \cdot \mid \{\ell : A \to B\} \cup \Sigma\\
+\slab{Signatures}        &\Sigma \CatName{Sig} &::=& \cdot \mid \{\ell : A \to B\} \cup \Sigma\\
-\slab{Handler\textrm{ }types}     &F     &::=& C \Rightarrow D\\
+\slab{Handler\textrm{ }types}     &F \in \HandlerTypeCat    &::=& C \Rightarrow D\\
-\slab{Computations} &M, N &::=& \dots \mid \Do \; \ell \; V
+\slab{Computations} &M, N \in \CompCat &::=& \dots \mid \Do \; \ell \; V
                           \mid  \Handle \; M \; \With \; H \\
 \slab{Handlers}     &H&::=& \{ \Return \; x \mapsto M \}
                       \mid  \{ \OpCase{\ell}{p}{r} \mapsto N \} \uplus H\\
@@ -16479,7 +16632,7 @@ we call handler contexts.
 %
 {
 \begin{syntax}
-\slab{Handler\textrm{ }contexts} &  \HC &::= & [\,] \mid \Handle \; \HC \; \With \; H
+\slab{Handler\textrm{ }contexts} &  \HC \CatName{Ctx} &::= & [\,] \mid \Handle \; \HC \; \With \; H
                                 \mid  \Let\;x \revto \HC\; \In\; N\\
 \end{syntax}}%
 %
@@ -17025,118 +17178,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
@@ -17224,7 +17265,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}