From d6b67950b2aeebed1996a63090d2f3bf828dfda3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Tue, 4 May 2021 23:00:40 +0100 Subject: [PATCH] WIP --- macros.tex | 95 +- thesis.bib | 162 +++ thesis.tex | 3360 +++++++++++++++++++++++++++++++++++++++++++++++++++- 3 files changed, 3568 insertions(+), 49 deletions(-) diff --git a/macros.tex b/macros.tex index 0e29279..c16ed17 100644 --- a/macros.tex +++ b/macros.tex @@ -235,6 +235,7 @@ \newcommand{\concat}{\mathbin{+\!\!+}} \newcommand{\revconcat}{\mathbin{\widehat{\concat}}} +\newcommand{\snoc}[2]{\ensuremath{#1 \concat [#2]}} %% %% CPS notation @@ -540,4 +541,96 @@ edge from parent node[above right] {$\res{\False}$} } ; -\end{tikzpicture}} \ No newline at end of file +\end{tikzpicture}} + +%% +%% Asymptotic improvement macros +%% +\newcommand{\naive}{naïve\xspace} +\newcommand{\naively}{naïvely\xspace} +\newcommand{\Naive}{Naïve\xspace} +\newcommand{\sem}[1]{\ensuremath{\pi_{#1}}} +\newcommand{\Iff}{\Leftrightarrow} +\newcommand{\Implies}{\Rightarrow} +\newcommand{\BCalcS}{\ensuremath{\lambda_{\textrm{\normalfont s}}\xspace}} +\newcommand{\BCalcE}{\ensuremath{\lambda_{\textrm{\normalfont e}}\xspace}} +\newcommand{\BCalcSE}{\ensuremath{\lambda_{\textrm{\normalfont se}}\xspace}} +\newcommand{\IfZero}{\keyw{ifzero}} +\newcommand{\Superpoint}{\lambda\_.\Do\;\Branch~\Unit} +\newcommand{\ECount}{\dec{effcount}} +\newcommand{\Countprog}{K} +\newcommand{\Plus}{\mathsf{Plus}} +\newcommand{\Minus}{\mathsf{Minus}} +\newcommand{\Eq}{\mathsf{Eq}} +\newcommand{\BList}{\mathbb{B}^\ast} + +\newcommand{\CtxCat}{\CatName{Ctx}} +\newcommand{\PureCont}{\mathsf{PureCont}} + +\newcommand{\Addr}{\mathsf{Addr}} +\newcommand{\Lab}{\mathsf{Lab}} +\newcommand{\Env}{\mathsf{Env}} + +\newcommand{\Time}{\dec{DTIME}} +\newcommand{\query}{\mathord{?}} +\newcommand{\ans}{\mathord{!}} +\newcommand{\labs}{\mathsf{labs}} +\newcommand{\steps}{\mathsf{steps}} + +\newcommand{\tree}{\tau} +\newcommand{\tl}{\labs(\tree)} +\newcommand{\ts}{\steps(\tree)} +\newcommand{\T}[1]{\ensuremath{\mathcal{T}_{#1}}} +\newcommand{\Config}{\dec{Config}} +\newcommand{\cekl}{\langle} +\newcommand{\cekr}{\rangle} + +\newcommand{\const}[1]{\ulcorner #1 \urcorner} +\newcommand{\HC}{\ensuremath{\mathcal{H}}} + +\newcommand{\tr}{\mathcal{T}} +\newcommand{\tru}{\mathcal{U}} +\newcommand{\Tree}{\dec{Tree}} +\newcommand{\TimedTree}{\dec{TimedTree}} +\newcommand{\denotep}[1]{\ensuremath{\mathbb{P}\llbracket #1 \rrbracket}} + +\newcommand\ttTwoTree{ +\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 4cm/##1, + level distance = 2.0cm}] +\node (root) [opnode] {Branch} + child { node [opnode] {Branch} + child { node [leaf] {$\True$} + edge from parent node[above left] {$\True$} + } + child { node [leaf] {$\True$} + edge from parent node[above right] {$\False$} + } + edge from parent node[above left] {$\True$} + } + child { node [opnode] {Branch} + child { node [leaf] {$\True$} + edge from parent node[above left] {$\True$} + } + child { node [leaf] {$\True$} + edge from parent node[above right] {$\False$} + } + edge from parent node[above right] {$\False$} + } +; +\end{tikzpicture}} + + +\newcommand{\tossTree}{ + \begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 2.5cm/##1, + level distance = 1.0cm}] +\node (root) [opnode] {$\dec{Branch}$} + child { node [leaf] {$\dec{Heads}$} + edge from parent node[above left] {$\True$} + } + child { node [leaf] {$\dec{Tails}$} + edge from parent node[above right] {$\False$} + } +; +\end{tikzpicture}} + +\newenvironment{twoeqs}{\ba[t]{@{}r@{~}c@{~}l@{~}c@{~}r@{~}c@{~}l@{}}}{\ea} \ No newline at end of file diff --git a/thesis.bib b/thesis.bib index 6f0da4b..afdb4cb 100644 --- a/thesis.bib +++ b/thesis.bib @@ -2901,4 +2901,166 @@ number = {3}, pages = {141--144}, year = {1986} +} + +# Exact real integration +@inproceedings{Simpson98, + author = {Alex K. Simpson}, + title = {Lazy Functional Algorithms for Exact Real Functionals}, + booktitle = {{MFCS}}, + series = {Lecture Notes in Computer Science}, + volume = {1450}, + pages = {456--464}, + publisher = {Springer}, + year = {1998} +} + +# Robbie Daniels' MSc dissertation +@MastersThesis{Daniels16, + author = {Robbie Daniels}, + title = {Efficient Generic Searches and Programming Language Expressivity}, + school = {School of Informatics, the University of Edinburgh}, + address = {Scotland}, + month = aug, + year = 2016, + OPTurl = {http://homepages.inf.ed.ac.uk/jrl/Research/Robbie_Daniels_MSc_dissertation.pdf} +} + +# Computability +@article{Plotkin77, + author = {Gordon Plotkin}, + title = {{LCF} considered as a programming language}, + journal = {Theor. Comput. Sci.}, + volume = {5}, + number = {3}, + pages = {223--255}, + year = {1977} +} + +@inproceedings{Pippenger96, + author = {Nicholas Pippenger}, + title = {Pure versus impure Lisp}, + booktitle = {{POPL}}, + pages = {104--109}, + publisher = {{ACM}}, + year = {1996} +} + +@inproceedings{Longley99, + author = {John Longley}, + title = {When is a functional program not a functional program?}, + booktitle = {{ICFP}}, + pages = {1--7}, + publisher = {{ACM}}, + year = {1999} +} + +@article{Longley18a, + author = {John Longley}, + title = {The recursion hierarchy for {PCF} is strict}, + journal = {Logical Methods in Comput. Sci.}, + volume = {14}, + number = {3:8}, + pages = {1--51}, + year = {2018} +} + +@article{Longley19, + author = {John Longley}, + title = {Bar recursion is not computable via iteration}, + journal = {Computability}, + volume = {8}, + number = {2}, + pages = {119--153}, + year = {2019} +} + +@article{BirdJdM97, + author = {Richard Bird and + Geraint Jones and + Oege de Moor}, + title = {More haste less speed: lazy versus eager evaluation}, + journal = {J. Funct. Program.}, + volume = {7}, + number = {5}, + pages = {541--547}, + year = {1997} +} + +@article{Jones01, + author = {Neil Jones}, + title = {The expressive power of higher-order types, or, life without {CONS}}, + journal = {J. Funct. Program.}, + volume = {11}, + pages = {5--94}, + year = {2001} +} + +# n-queens +@article{BellS09, + author = {Jordan Bell and + Brett Stevens}, + title = {A survey of known results and research areas for n-queens}, + journal = {Discret. Math.}, + volume = {309}, + number = {1}, + pages = {1--31}, + year = {2009} +} + +# Sudoko +@article{Bird06, + author = {Richard S. Bird}, + title = {Functional Pearl: {A} program to solve Sudoku}, + journal = {J. Funct. Program.}, + volume = {16}, + number = {6}, + pages = {671--679}, + year = {2006} +} + +# Environment-store model +@article{ScottS71, + author = {Dana Scott and Christopher Strachey}, + journal = {Proceedings of the Symposium on Computers and Automata}, + series = {Microwave Research Institute Symposia Series}, + volume = {21}, + year = {1971} +} + +# Backtracking +@article{KiselyovSFA05, + author = {Kiselyov, Oleg and Shan, Chung-chieh and Friedman, Daniel P. and Sabry, Amr}, + title = {Backtracking, Interleaving, and Terminating Monad Transformers: (Functional Pearl)}, + booktitle = {{ICFP}}, + pages = {192--203}, + publisher = {{ACM}}, + year = {2005}, +} + +# Ulrich Berger's PhD thesis +@phdthesis{Berger90, + author = {Ulrich Berger}, + title = {Totale Objekte und Mengen in der Bereichstheorie}, + school = {Ludwig Maximillians-Universtität}, + address = {Munich}, + year = {1990} +} + +# Exhaustive search on infinite sets +@inproceedings{Escardo07, + author = {Mart{\'{\i}}n H{\"{o}}tzel Escard{\'{o}}}, + title = {Infinite sets that admit fast exhaustive search}, + booktitle = {{LICS}}, + pages = {443--452}, + publisher = {{IEEE} Computer Society}, + year = {2007} +} + +@misc{Bauer11, + author = {Andrej Bauer}, + title = {How make the "impossible" functionals run even faster}, + howpublished = {{M}athematics, {A}lgorithms and {P}roofs, Leiden, the Netherlands}, + year = 2011, + url = {http://math.andrej.com/2011/12/06/how-to-make-the-impossible-functionals-run-even-faster/} } \ No newline at end of file diff --git a/thesis.tex b/thesis.tex index 3c82fc8..359bb34 100644 --- a/thesis.tex +++ b/thesis.tex @@ -10987,8 +10987,8 @@ Section~\ref{subsec:machine-correctness} easier to state. % Deep resumption application \mlab{Resume^\param} & \cek{ V\,\Record{W;W'} \mid \env \mid \shk} - &\stepsto& \cek{ \Return \; W \mid \env \mid (\sigma,(\env'[q \mapsto \val{W'}\env],q.\,H)) \cons \shk' \concat \shk}, - &\text{if }\val{V}{\env} = \shk' \concat [(\sigma,(\env',q.\,H))])^A \\ + &\stepsto& \cek{ \Return \; W \mid \env \mid \shk' \concat [(\sigma,(\env'[q \mapsto \val{W'}\env],q.\,H))] \concat \shk},&\\ + &&&\quad\text{if }\val{V}{\env} = \shk' \concat [(\sigma,(\env',q.\,H))])^A \\ % \mlab{Split} & \cek{ \Let \; \Record{\ell = x;y} = V \; \In \; N \mid \env \mid \shk} &\stepsto& \cek{ N \mid \env[x \mapsto v, y \mapsto w] \mid \shk}, @@ -11204,6 +11204,8 @@ configuration. \newcommand{\kappaid}{\ensuremath{\kappa_{\text{id}}}} \newcommand{\incr}{\dec{incr}} \newcommand{\Incr}{\dec{Incr}} +\newcommand{\prodf}{\dec{prod}} +\newcommand{\consf}{\dec{cons}} % To better understand how the abstract machine concretely transitions between configurations we will consider a small program consisting of @@ -11279,15 +11281,15 @@ a deep, parameterised, and shallow handler. % \[ \bl - \dec{prod} : \UnitType \to \alpha \eff \{\Incr : \UnitType \opto \Int; \Yield : \Int \opto \UnitType\}\\ - \dec{prod}\,\Unit \defas + \prodf : \UnitType \to \alpha \eff \{\Incr : \UnitType \opto \Int; \Yield : \Int \opto \UnitType\}\\ + \prodf\,\Unit \defas \bl \Let\;i \revto \Do\;\Incr\,\Unit\;\In\\ \Let\;x \revto \Do\;\Yield~i\\ \In\;\dec{prod}\,\Unit \el\smallskip\\ - \dec{cons} : \UnitType \to \Int \eff \{\Fork : \UnitType \opto \Bool; \Await : \UnitType \opto \Int\}\\ - \dec{cons}\,\Unit \defas + \consf : \UnitType \to \Int \eff \{\Fork : \UnitType \opto \Bool; \Await : \UnitType \opto \Int\}\\ + \consf\,\Unit \defas \bl \Let\;b \revto \Do\;\Fork\,\Unit\;\In\\ \Let\;x \revto \Do\;\Await\,\Unit\;\In\\ @@ -11298,18 +11300,18 @@ a deep, parameterised, and shallow handler. \] % \begin{derivation} - &\nondet\,(\lambda\Unit.\incr\,\Record{0;\lambda\Unit.\Pipe\,\Record{\dec{prod};\dec{cons}}})\\ + &\nondet\,(\lambda\Unit.\incr\,\Record{0;\lambda\Unit.\Pipe\,\Record{\prodf;\consf}})\\ \stepsto& \reason{\mlab{Init} with $\env_0$}\\ - &\cek{\nondet\,(\lambda\Unit.\incr\,\Record{0;\lambda\Unit.\Pipe\,\Record{\dec{prod};\dec{cons}}}) \mid \env_0 \mid \sks_0}\\ + &\cek{\nondet\,(\lambda\Unit.\incr\,\Record{0;\lambda\Unit.\Pipe\,\Record{\prodf;\consf}}) \mid \env_0 \mid \sks_0}\\ \stepsto^+& \reason{$3\times$(\mlab{App}, \mlab{Handle^\delta})}\\ &\bl \cek{c\,\Unit \mid \env_\Pipe \mid (\nil,\chi^\dagger_\Pipe) \cons (\nil, \chi^\param_\incr) \cons (\nil, \chi_\nondet) \cons \kappa_0}\\ \text{where } \bl - \env_\Pipe = \env_0[c \mapsto (\env_0, \dec{cons}), p \mapsto (\env_0, \dec{prod})]\\ + \env_\Pipe = \env_0[c \mapsto (\env_0, \consf), p \mapsto (\env_0, \prodf)]\\ \chi^\dagger_\Pipe = (\env_\Pipe, H^\dagger_\Pipe)\\ \env_\incr = \env_0[m \mapsto (\env_0, \lambda\Unit.\Pipe\cdots),i \mapsto 0]\\ - \chi^\param_\incr = (\env_\incr, H^\param_\Pipe)\\ + \chi^\param_\incr = (\env_\incr, H^\param_\incr)\\ \env_\nondet = \env_0[m \mapsto (\env_0, \lambda\Unit.\incr \cdots)]\\ \chi_\nondet = (\env_\nondet, H_\nondet) \el @@ -11356,7 +11358,7 @@ a deep, parameterised, and shallow handler. \cek{p\,\Unit \mid \env_\Copipe \mid (\nil, \chi^\dagger_\Copipe) \cons \kappa'}\\ \text{where } \ba[t]{@{~}r@{~}c@{~}l} - \env_\Copipe &=& \env_0[c \mapsto (\nil, [(\env_0',x,\If\;\cdots)]), p \mapsto (\env_0,\dec{prod})]\\ + \env_\Copipe &=& \env_0[c \mapsto (\nil, [(\env_0',x,\If\;\cdots)]), p \mapsto (\env_0,\prodf)]\\ \chi_\Copipe &=& (\env_\Copipe,H^\dagger_\Copipe)\\ \ea \el\\ @@ -11364,34 +11366,43 @@ a deep, parameterised, and shallow handler. &\cek{\Do\;\Incr\,\Unit \mid \env_0 \mid ([(\env_0,i,\Let\;x\revto\cdots)],\chi^\dagger_\Copipe) \cons \kappa'}\\ \stepsto^+& \reason{\mlab{Forward}, \mlab{Do^\param}, \mlab{Let}, \mlab{App}, \mlab{PureCont}}\\ &\bl - \cek{resume\,\Record{1;0} \mid \env_\incr' \mid \kappa'}\\ + \cek{resume\,\Record{1;0} \mid \env_\incr' \mid (\nil, \chi_\nondet) \cons \kappa_0'}\\ \text{where } \ba[t]{@{~}r@{~}c@{~}l} - \env_\incr' &=& \env_\incr[i' \mapsto 1, resume \mapsto [([(\env_0,i,\Let\;x\revto\cdots)],\chi^\dagger_\Copipe),(\nil,\chi^\param_\incr)]]\\ - \kappa' &=& (\nil, \chi_\nondet) \cons \kappa_0' + \env_\incr' &=& \env_\incr[i' \mapsto 1, resume \mapsto [([(\env_0,i,\Let\;x\revto\cdots)],\chi^\dagger_\Copipe),(\nil,\chi^\param_\incr)]] \ea \el - % &\bl - % \cek{\Do\;\Fork\,\Unit \mid \env_0 \mid ([(\env_0,x,\Record{x;\Pipe\,\Record{\dec{prod};\dec{cons}}})],\chi_\incr) \cons (\nil, \chi_\nondet) \cons \sks_0}\\ - % ~\text{where } \chi_\incr \defas (\env_0[i \mapsto i],H_\incr) - % \el\\ - % \stepsto^+& \reason{\mlab{Forward}, \mlab{Do^\param}}\\ - % &\bl - % \cek{resume~\True \concat resume~\False \mid \env_\nondet \mid \sks_0}\\ - % ~\text{where } \env_\nondet \defas \env_0[resume \mapsto [([(\env_0,x,\Record{x;\Pipe\,\Record{\dec{prod};\dec{cons}}})],\chi_\incr), (\nil, \chi_\nondet)] - % \el - % &\bl - % \cek{c\,\Unit \mid \env_{\Pipe} \mid (\nil,\chi_\Pipe) \cons (\nil,\chi_\incr) \cons (\nil, \chi_\nondet) \cons \sks_0}\\ - % \ba[t]{@{~}r@{~}c@{~}l} - % \text{where } \env_\Pipe &\defas& \env_0[pipe \mapsto (\env_0,\Pipe),p \mapsto (\env_0,\dec{prod}),c \mapsto (\env_0,\dec{cons})]\\ - % \text{and } \chi_\Pipe &\defas& (\env_{\Pipe},H_{\Pipe}) - % \ea - % \el\\ - % \stepsto^+& \reason{\mlab{App}, \mlab{Let}}\\ - % &\bl\cek{\Do\;\Await\,\Unit \mid \env_0 \mid ([(\env_0,x,x+\Do\;\Await\,\Unit)],\chi_\Pipe) \cons \sks_1}\\ - % ~\text{where } \sks_1 \defas (\nil,\chi_\incr) \cons (\nil, \chi_\nondet) \cons \sks_0 - % \el \end{derivation} +% +\begin{derivation} + \stepsto^+&\reason{\mlab{Resume^\param}, \mlab{PureCont}, \mlab{Let}}\\ + &\bl + \cek{\Do\;\Yield~i \mid \env_{\prodf}' \mid ([(\env_{\prodf}',x,\prodf\,\Unit)],\chi^\dagger_\Copipe) \cons \kappa_1}\\ + \text{where } + \ba[t]{@{~}r@{~}c@{~}l} + \env_\prodf' &=& \env_\prodf[i \mapsto 0]\\ + \kappa_1 &=& ([(\env_0,x,\If\;b\cdots)],\chi^\dagger_\Copipe) \cons (\nil,\chi^\param_\incr) \cons (\nil, \chi_\nondet) \cons \kappa_0' + \ea + \el\\ + \stepsto& \reason{\mlab{Do^\dagger}}\\ + &\bl + \cek{\Pipe\,\Record{resume;\lambda\Unit.c\,y} \mid \env_\Copipe' \mid \kappa_1}\\ + \text{where } + \ba[t]{@{~}r@{~}c@{~}l} + \env_\Copipe' &=& \env_\Copipe[y \mapsto 0, resume \mapsto (\nil,[(\env_{\prodf}',x,\prodf\,\Unit)])] + \ea + \el\\ + \stepsto^+& \reason{\mlab{App}, \mlab{Handle^\dagger}, \mlab{Resume^\dagger}, \mlab{PureCont}}\\ + &\bl + \cek{\If\;b\;\Then\;x + 2\;\Else\;x*2 \mid \env_\consf'' \mid \kappa_2}\\ + \text{where } + \ba[t]{@{~}r@{~}c@{~}l} + \env_\consf'' &=& \env_\consf[x \mapsto 0]\\ + \kappa_2 &=& ([(\env_0,i,\Let\;x\revto\cdots)],\chi^\dagger_\Pipe) \cons (\nil,\chi^\param_\incr) \cons (\nil, \chi_\nondet) \cons \kappa_0' + \ea + \el +\end{derivation} +% % \paragraph{Example} To make the transition rules in % Figure~\ref{fig:abstract-machine-semantics} concrete we give an @@ -12817,21 +12828,3274 @@ the captured context and continuation invocation context to coincide. \chapter{Asymptotic speedup with first-class control} \label{ch:handlers-efficiency} -Describe the methodology\dots -\section{Generic search} +\def\LLL{{\mathcal L}} +\def\N{{\mathbb N}} +% +In today's programming languages we find a wealth of powerful +constructs and features --- exceptions, higher-order store, dynamic +method dispatch, coroutines, explicit continuations, concurrency +features, Lisp-style `quote' and so on --- which may be present or +absent in various combinations in any given language. There are of +course many important pragmatic and stylistic differences between +languages, but here we are concerned with whether languages may differ +more essentially in their expressive power, according to the selection +of features they contain. + +One can interpret this question in various ways. For instance, +\citet{Felleisen91} considers the question of whether a language +$\LLL$ admits a translation into a sublanguage $\LLL'$ in a way which +respects not only the behaviour of programs but also aspects of their +(global or local) syntactic structure. If the translation of some +$\LLL$-program into $\LLL'$ requires a complete global restructuring, +we may say that $\LLL'$ is in some way less expressive than $\LLL$. +In the present paper, however, we have in mind even more fundamental +expressivity differences that would not be bridged even if +whole-program translations were admitted. These fall under two +headings. +% +\begin{enumerate} +\item \emph{Computability}: Are there operations of a given type + that are programmable in $\LLL$ but not expressible at all in $\LLL'$? +\item \emph{Complexity}: Are there operations programmable in $\LLL$ + with some asymptotic runtime bound (e.g.\ `$\BigO(n^2)$') that cannot be + achieved in $\LLL'$? +\end{enumerate} +% +We may also ask: are there examples of \emph{natural, practically + useful} operations that manifest such differences? If so, this +might be considered as a significant advantage of $\LLL$ over $\LLL'$. + +If the `operations' we are asking about are ordinary first-order +functions --- that is, both their inputs and outputs are of ground +type (strings, arbitrary-size integers etc.)\ --- then the situation +is easily summarised. At such types, all reasonable languages give +rise to the same class of programmable functions, namely the +Church-Turing computable ones. As for complexity, the runtime of a +program is typically analysed with respect to some cost model for +basic instructions (e.g.\ one unit of time per array access). +Although the realism of such cost models in the asymptotic limit can +be questioned (see, e.g., \citep[Section~2.6]{Knuth97}), it is broadly +taken as read that such models are equally applicable whatever +programming language we are working with, and moreover that all +respectable languages can represent all algorithms of interest; thus, +one does not expect the best achievable asymptotic run-time for a +typical algorithm (say in number theory or graph theory) to be +sensitive to the choice of programming language, except perhaps in +marginal cases. + +The situation changes radically, however, if we consider +\emph{higher-order} operations: programmable operations whose inputs +may themselves be programmable operations. Here it turns out that +both what is computable and the efficiency with which it can be +computed can be highly sensitive to the selection of language features +present. This is in fact true more widely for \emph{abstract data + types}, of which higher-order types can be seen as a special case: a +higher-order value will be represented within the machine as ground +data, but a program within the language typically has no access to +this internal representation, and can interact with the value only by +applying it to an argument. + +Most work in this area to date has focused on computability +differences. One of the best known examples is the \emph{parallel if} +operation which is computable in a language with parallel evaluation +but not in a typical `sequential' programming +language~\cite{Plotkin77}. It is also well known that the presence of +control features or local state enables observational distinctions +that cannot be made in a purely functional setting: for instance, +there are programs involving `call/cc' that detect the order in which +a (call-by-name) `+' operation evaluates its arguments +\citep{CartwrightF92}. Such operations are `non-functional' in the +sense that their output is not determined solely by the extension of +their input (seen as a mathematical function +$\N_\bot \times \N_\bot \rightarrow \N_\bot$); +%% +however, there are also programs with `functional' behaviour that can +be implemented with control or local state but not without them +\citep{Longley99}. More recent results have exhibited differences +lower down in the language expressivity spectrum: for instance, in a +purely functional setting \textit{\`a la} Haskell, the expressive +power of \emph{recursion} increases strictly with its type level +\citep{Longley18a}, and there are natural operations computable by +low-order recursion but not by high-order iteration +\citep{Longley19}. Much of this territory, including the mathematical +theory of some of the natural notions of higher-order computability +that arise in this way, is mapped out by \citet{LongleyN15}. + +Relatively few results of this character have so far been established +on the complexity side. \citet{Pippenger96} gives an example of an +`online' operation on infinite sequences of atomic symbols +(essentially a function from streams to streams) such that the first +$n$ output symbols can be produced within time $\BigO(n)$ if one is +working in an `impure' version of Lisp (in which mutation of `cons' +pairs is admitted), but with a worst-case runtime no better than +$\Omega(n \log n)$ for any implementation in pure Lisp (without such +mutation). This example was reconsidered by \citet{BirdJdM97} who +showed that the same speedup can be achieved in a pure language by +using lazy evaluation. Another candidate is the familiar $\log n$ +overhead involved in implementing maps (supporting lookup and +extension) in a pure functional language \cite{Okasaki99}, although to +our knowledge this situation has not yet been subjected to theoretical +scrutiny. \citet{Jones01} explores the approach of manifesting +expressivity and efficiency differences between certain languages by +artificially restricting attention to `cons-free' programs; in this +setting, the classes of representable first-order functions for the +various languages are found to coincide with some well-known +complexity classes. + +The purpose of the present paper is to give a clear example of such an +inherent complexity difference higher up in the expressivity spectrum. +Specifically, we consider the following \emph{generic count} problem, +parametric in $n$: given a boolean-valued predicate $P$ on the space +${\mathbb B}^n$ of boolean vectors of length $n$, return the number of +such vectors $q$ for which $P\,q = \True$. We shall consider boolean +vectors of any length to be represented by the type $\Nat \to \Bool$; +thus for each $n$, we are asking for an implementation of a certain +third-order operation +% +\[ \Count_n : ((\Nat \to \Bool) \to \Bool) \to \Nat \] +% +A \naive implementation strategy, supported by any reasonable +language, is simply to apply $P$ to each of the $2^n$ vectors in turn. +A much less obvious, but still purely `functional', approach due to +\citet{Berger90} achieves the effect of `pruned search' where the +predicate allows it (serving as a warning that counter-intuitive +phenomena can arise in this territory). Nonetheless, under a mild +condition on $P$ (namely that it must inspect all $n$ components of +the given vector before returning), both these approaches will have a +$\Omega(n 2^n)$ runtime. Moreover, we shall show that in a typical +call-by-value language without advanced control features, one cannot +improve on this: \emph{any} implementation of $\Count_n$ must +necessarily take time $\Omega(n2^n)$ on \emph{any} predicate $P$. On +the other hand, if we extend our language with a feature such as +\emph{effect handlers} (see Section~\ref{sec:handlers-primer} below), +it becomes possible to bring the runtime down to $\BigO(2^n)$: an +asymptotic gain of a factor of $n$. + +The \emph{generic search} problem is just like the generic count +problem, except rather than counting the vectors $q$ such that $P\,q = +\True$, it returns the list of all such vectors. +% +The $\Omega(n 2^n)$ runtime for purely functional implementations +transfers directly to generic search, as generic count reduces to +generic search composed with computing the length of the resulting +list. +% +In Section~\ref{sec:count-vs-search} we illustrate that the +$\BigO(2^n)$ runtime for generic count with effect handlers also +transfers to generic search. + +The idea behind the speedup is easily explained and will already be +familiar, at least informally, to programmers who have worked with +multi-shot continuations. +% +Suppose for example $n=3$, and suppose that the predicate $P$ always +inspects the components of its argument in the order $0,1,2$. +% +A \naive implementation of $\Count_3$ might start by applying the given +$P$ to $q_0 = (\True,\True,\True)$, and then to +$q_1 = (\True,\True,\False)$. Clearly there is some duplication here: +the computations of $P\,q_0$ and $P\,q_1$ will proceed identically up +to the point where the value of the final component is requested. What +we would like to do, then, is to record the state of the computation +of $P\,q_0$ at just this point, so that we can later resume this +computation with $\False$ supplied as the final component value in +order to obtain the value of $P\,q_1$. (Similarly for all other +internal nodes in the evident binary tree of boolean vectors.) Of +course, this `backup' approach would be standardly applied if one were +implementing a bespoke search operation for some \emph{particular} +choice of $P$ (corresponding, say, to the $n$-queens problem); but to +apply this idea of resuming previous subcomputations in the +\emph{generic} setting (that is, uniformly in $P$) requires some +special language feature such as effect handlers or multi-shot +continuations. +% +One could also obviate the need for such a feature by choosing to +present the predicate $P$ in some other way, but from our present +perspective this would be to move the goalposts: our intention is +precisely to show that our languages differ in an essential way +\emph{as regards their power to manipulate data of type} $(\Nat \to +\Bool) \to \Bool$. + +This idea of using first-class control to achieve `backtracking' has +been exploited before and is fairly widely known (see +e.g. \citep{KiselyovSFA05}), and there is a clear programming +intuition that this yields a speedup unattainable in languages without +such control features. Our main contribution in this paper is to +provide, for the first time, a precise mathematical theorem that pins +down this fundamental efficiency difference, thus giving formal +substance to this intuition. Since our goal is to give a realistic +analysis of the efficiency achievable in various settings without +getting bogged down in inessential implementation details, we shall +work concretely and operationally with the languages in question, +using a CEK-style abstract machine semantics as our basic model of +execution time, and with some specific programs in these languages. +In the first instance, we formulate our results as a comparison +between a purely functional base language (a version of call-by-value +PCF) and an extension with first-class control; we then indicate how +these results can be extended to base languages with other features +such as mutable state. + +In summary, our purpose is to exhibit an efficiency gap which, in our +view, manifests a fundamental feature of the programming language +landscape, challenging a common assumption that all real-world +programming languages are essentially `equivalent' from an asymptotic +point of view. We believe that such results are important not only +for a rounded understanding of the relative merits of existing +languages, but also for informing future language design. + +For their convenience as structured delimited control operators we +adopt effect handlers as our universal control abstraction of choice, +but our results adapt mutatis mutandis to other first-class control +abstractions such as `call/cc'~\cite{AbelsonHAKBOBPCRFRHSHW85}, `control' +($\mathcal{F}$) and 'prompt' ($\textbf{\#}$)~\citep{Felleisen88}, or +`shift' and `reset'~\citep{DanvyF90}. + +The rest of the paper is structured as follows. +\begin{itemize} + \item Section~\ref{sec:handlers-primer} provides an introduction to + effect handlers as a programming abstraction. + \item Section~\ref{sec:calculi} presents a PCF-like language + $\BCalc$ and its extension $\HCalc$ with effect handlers. + \item Section~\ref{sec:abstract-machine-semantics} defines abstract + machines for $\BCalc$ and $\HCalc$, yielding a runtime cost model. + \item Section~\ref{sec:generic-search} introduces generic count and + some associated machinery, and presents an implementation in + $\HCalc$ with runtime $\BigO(2^n)$. + \item Section~\ref{sec:pure-counting} establishes that any generic + count implementation in $\BCalc$ must have runtime $\Omega(n2^n)$. + \item Section~\ref{sec:robustness} shows that our results scale to + richer settings including support for a wider class of predicates, + the adaptation from generic count to generic search, and an + extension of the base language with state. + \item Section~\ref{sec:experiments} evaluates implementations of + generic search based on $\BCalc$ and $\HCalc$ in Standard ML. + \item Section \ref{sec:conclusions} concludes. +\end{itemize} +% +The languages $\BCalc$ and $\HCalc$ are rather minimal versions of +previously studied systems --- we only include the machinery needed +for illustrating the generic search efficiency phenomenon. +% +Auxiliary results are included in the appendices of the extended +version of the paper~\citep{HillerstromLL20}. + +%% +%% Effect handlers primer +%% +\section{Effect Handlers Primer} +\label{sec:handlers-primer} +Effect handlers were originally studied as a theoretical means to +provide a semantics for exception handling in the setting of algebraic +effects~\cite{PlotkinP01, PlotkinP13}. +% +Subsequently they have emerged as a practical programming abstraction +for modular effectful programming~\citep{BauerP15, ConventLMM20, + KammarLO13, KiselyovSS13, DolanWSYM15, Leijen17, HillerstromLA20}. +% +In this section we give a short introduction to effect handlers. For +a thorough introduction to programming with effect handlers, we +recommend the tutorial by \citet{Pretnar15}, and as an introduction to +the mathematical foundations of handlers, we refer the reader to the +founding paper by \citet{PlotkinP13} and the excellent tutorial paper +by \citet{Bauer18}. +% + +Viewed through the lens of universal algebra, an algebraic effect is +given by a signature $\Sigma$ of typed \emph{operation symbols} along +with an equational theory that describes the properties of the +operations~\cite{PlotkinP01}. +% +An example of an algebraic effect is \emph{nondeterminism}, whose +signature consists of a single nondeterministic choice operation: +$\Sigma \defas \{ \Branch : \One \to \Bool \}$. +% +The operation takes a single parameter of type unit and ultimately +produces a boolean value. +% +The pragmatic programmatic view of algebraic effects differs from the +original development as no implementation accounts for equations over +operations yet. + +As a simple example, let us use the operation $\Branch$ to model a +coin toss. +% +Suppose we have a data type $\dec{Toss} \defas \dec{Heads} \mid +\dec{Tails}$, then +% +we may implement a coin toss as follows. +% +{\small +\[ + \bl + \dec{toss} : \One \to \dec{Toss}\\ + \dec{toss}~\Unit = + \If \; \Do\; \Branch\; \Unit \; + \Then\; \dec{Heads} \; + \Else\; \dec{Tails} + \el +\]}% +% +From the type signature it is clear that the computation returns a +value of type $\dec{Toss}$. It is not clear from the signature of +$\dec{toss}$ whether it performs an effect. However, from the +definition, it evidently performs the operation $\Branch$ with +argument $\Unit$ using the $\Do$-invocation form. The result of the +operation determines whether the computation returns either +$\dec{Heads}$ or $\dec{Tails}$. +% +Systems such as Frank~\cite{LindleyMM17, ConventLMM20}, +Helium~\cite{BiernackiPPS19, BiernackiPPS20}, Koka~\cite{Leijen17}, +and Links~\cite{HillerstromL16, HillerstromLA20} include +type-and-effect systems which track the use of effectful operations, +whilst current iterations of systems such as Eff~\cite{BauerP15} and +Multicore OCaml~\cite{DolanWSYM15} elect not to track effects in the +type system. +% +Our language is closer to the latter two. + +% +We may view an effectful computation as a tree, where the interior +nodes correspond to operation invocations and the leaves correspond to +return values. +% +The computation tree for $\dec{toss}$ is as follows. +% +\begin{center} + {\small + \tossTree}% +\end{center} +% +It models interaction with the environment. The operation $\Branch$ +can be viewed as a \emph{query} for which the \emph{response} is +either $\True$ or $\False$. The response is provided by an effect +handler. As an example, consider the following handler which enumerates +the possible outcomes of a coin toss. +% +{\small +\[ + \bl + \Handle\; \dec{toss}~\Unit\;\With\\ + \quad\ba[t]{@{~}l@{~}c@{~}l} + \Val~x &\mapsto& [x]\\ + \Branch~\Unit~r &\mapsto& r~\True \concat r~\False + \ea + \el +\]}% +% +The $\Handle$-construct generalises the exceptional syntax +of~\citet{BentonK01}. +% +This handler has a \emph{success} clause and an \emph{operation} +clauses. +% +The success clause determines how to interpret the return value of +$\dec{toss}$, or equivalently how to interpret the leaves of its +computation tree. +% +It lifts the return value into a singleton list. +% +The operation clause determines how to interpret occurrences of +$\Branch$ in $\dec{toss}$. It provides access to the argument of +$\Branch$ (which is unit) and its resumption, $r$. The resumption is a +first-class delimited continuation which captures the remainder of the +$\dec{toss}$ computation from the invocation of $\Branch$ up to its +nearest enclosing handler. +% + +Applying $r$ to $\True$ resumes evaluation of $\dec{toss}$ via the +$\True$ branch, returning $\dec{Heads}$ and causing the success clause +of the handler to be invoked; thus the result of $r~\True$ is +$[\dec{Heads}]$. Evaluation continues in the operation clause, +meaning that $r$ is applied again, but this time to $\False$, which +causes evaluation to resume in $\dec{toss}$ via the $\False$ +branch. By the same reasoning, the value of $r~\False$ is +$[\dec{Tails}]$, which is concatenated with the result of the +$\True$ branch; hence the handler ultimately returns +$[\dec{Heads}, \dec{Tails}]$. + +%% +%% Base calculus +%% \section{Calculi} -\subsection{Base calculus} -\subsection{Handler calculus} -\section{A practical model of computation} -\subsection{Syntax} -\subsection{Semantics} -\subsection{Realisability} -\section{Points, predicates, and their models} -\section{Efficient generic search with effect handlers} -\subsection{Space complexity} -\section{Best-case complexity of generic search without control} -\subsection{No shortcuts} -\subsection{No sharing} +\label{sec:calculi} +In this section, we present our base language $\BCalc$ and its +extension with effect handlers $\HCalc$. + +\subsection{Base Calculus} +The base calculus $\BCalc$ is a fine-grain +call-by-value~\cite{LevyPT03} variation of PCF~\cite{Plotkin77}. +% +Fine-grain call-by-value is similar to A-normal +form~\cite{FlanaganSDF93} in that every intermediate computation is +named, but unlike A-normal form is closed under reduction. + +The syntax of $\BCalc$ is as follows. +{\small +\noindent + \begin{syntax} + \slab{Types} &A,B,C,D\in\TypeCat &::= & \Nat \mid \One \mid A \to B \mid A \times B \mid A + B \\ + \slab{Type Environments} &\Gamma\in\CtxCat &::= & \cdot \mid \Gamma, x:A \\ +\slab{Values} &V,W\in\ValCat &::= & x \mid k \mid c \mid \lambda x^A .\, M \mid \Rec \; f^{A \to B}\, x.M \\ + & &\mid& \Unit \mid \Record{V, W} \mid (\Inl\, V)^B \mid (\Inr\, W)^A\\ +% & & & +\slab{Computations} &M,N\in\CompCat + &::= & V\,W + \mid \Let\; \Record{x,y} = V \; \In \; N \\ + & &\mid&\Case \; V \;\{ \Inl \; x \mapsto M; \Inr \; y \mapsto N\}\\ + & &\mid& \Return\; V + \mid \Let \; x \revto M \; \In \; N \\ +\end{syntax}}% +% +The ground types are $\Nat$ and $\One$ which classify natural number +values and the unit value, respectively. The function type $A \to B$ +classifies functions that map values of type $A$ to values of type +$B$. The binary product type $A \times B$ classifies pairs of values +whose first and second components have types $A$ and $B$ +respectively. The sum type $A + B$ classifies tagged values of either +type $A$ or $B$. +% +Type environments $\Gamma$ map term variables to their types. + +We let $k$ range over natural numbers and $c$ range over primitive +operations on natural numbers ($+, -, =$). +% +We let $x, y, z$ range over term variables. +% +For convenience, we also use $f$, $g$, and $h$ for variables of +function type, $i$ and $j$ for variables of type $\Nat$, and $r$ to +denote resumptions. +% +The value terms are standard. +% Value terms comprise variables ($x$), the unit value ($\Unit$), +% natural number literals ($n$), primitive constants ($c$), lambda +% abstraction ($\lambda x^A . \, M$), recursion +% ($\Rec \; f^{A \to B}\, x.M$), pairs ($\Record{V, W}$), left +% ($(\Inl~V)^B$) and right $((\Inr~W)^A)$ injections. + +% +We will occasionally blur the distinction between object and meta +language by writing $A$ for the meta level type of closed value terms +of type $A$. +% +All elimination forms are computation terms. Abstraction is eliminated +using application ($V\,W$). +% +The product eliminator $(\Let \; \Record{x,y} = V \; \In \; N)$ splits +a pair $V$ into its constituents and binds them to $x$ and $y$, +respectively. Sums are eliminated by a case split ($\Case\; V\; +\{\Inl\; x \mapsto M; \Inr\; y \mapsto N\}$). +% +A trivial computation $(\Return\;V)$ returns value $V$. The sequencing +expression $(\Let \; x \revto M \; \In \; N)$ evaluates $M$ and binds +the result value to $x$ in $N$. + + +\begin{figure*} +\small +\raggedright\textbf{Values} +\begin{mathpar} +% Variable + \inferrule*[Lab=\tylab{Var}] + {x : A \in \Gamma} + {\typv{\Gamma}{x : A}} + +% Unit + \inferrule*[Lab=\tylab{Unit}] + { } + {\typv{\Gamma}{\Unit : \One}} + +% n : Nat + \inferrule*[Lab=\tylab{Nat}] + { k \in \mathbb{N} } + {\typv{\Gamma}{k : \Nat}} + +% c : A + \inferrule*[Lab=\tylab{Const}] + {c : A \to B} + {\typv{\Gamma}{c : A \to B}} +\\ +% Abstraction + \inferrule*[Lab=\tylab{Lam}] + {\typ{\Gamma, x : A}{M : B}} + {\typv{\Gamma}{\lambda x^A .\, M : A \to B}} + +% Recursion + \inferrule*[Lab=\tylab{Rec}] + {\typ{\Gamma, f : A \to B, x : A}{M : B}} + {\typv{\Gamma}{\Rec\; f^{A \to B}\,x .\, M : A \to B}} +\\ +% Products + \inferrule*[Lab=\tylab{Prod}] + { \typv{\Gamma}{V : A} \\ + \typv{\Gamma}{W : B} + } + {\typv{\Gamma}{\Record{V,W} : A \times B}} + +% Left injection + \inferrule*[Lab=\tylab{Inl}] + {\typv{\Gamma}{V : A}} + {\typv{\Gamma}{(\Inl\,V)^B : A + B}} + +% Right injection + \inferrule*[Lab=\tylab{Inr}] + {\typv{\Gamma}{W : B}} + {\typv{\Gamma}{(\Inr\,W)^A : A + B}} +\end{mathpar} + +\textbf{Computations} +\begin{mathpar} +% Application + \inferrule*[Lab=\tylab{App}] + {\typv{\Gamma}{V : A \to B} \\ + \typv{\Gamma}{W : A} + } + {\typ{\Gamma}{V\,W : B}} + +% Split + \inferrule*[Lab=\tylab{Split}] + {\typv{\Gamma}{V : A \times B} \\ + \typ{\Gamma, x : A, y : B}{N : C} + } + {\typ{\Gamma}{\Let \; \Record{x,y} = V\; \In \; N : C}} + +% Case + \inferrule*[Lab=\tylab{Case}] + { \typv{\Gamma}{V : A + B} \\ + \typ{\Gamma,x : A}{M : C} \\ + \typ{\Gamma,y : B}{N : C} + } + {\typ{\Gamma}{\Case \; V \;\{\Inl\; x \mapsto M; \Inr \; y \mapsto N \} : C}} +\\ +% Return + \inferrule*[Lab=\tylab{Return}] + {\typv{\Gamma}{V : A}} + {\typ{\Gamma}{\Return \; V : A}} + +% Let + \inferrule*[Lab=\tylab{Let}] + {\typ{\Gamma}{M : A} \\ + \typ{\Gamma, x : A}{N : C} + } + {\typ{\Gamma}{\Let \; x \revto M\; \In \; N : C}} +\end{mathpar} +\caption{Typing Rules for $\BCalc$} +\label{fig:typing} +\end{figure*} + +The typing rules are given in Figure~\ref{fig:typing}. +% +We require two typing judgements: one for values and the other for +computations. +% +The judgement $\typ{\Gamma}{\square : A}$ states that a $\square$-term +has type $A$ under type environment $\Gamma$, where $\square$ is +either a value term ($V$) or a computation term ($M$). +% +The constants have the following types. +% +{\small +\begin{mathpar} +\{(+), (-)\} : \Nat \times \Nat \to \Nat + +(=) : \Nat \times \Nat \to \One + \One +\end{mathpar}} +% +\begin{figure*} +\small +\begin{reductions} +\semlab{App} & (\lambda x^A . \, M) V &\reducesto& M[V/x] \\ +\semlab{App-Rec} & (\Rec\; f^A \,x.\, M) V &\reducesto& M[(\Rec\;f^A\,x .\,M)/f,V/x]\\ +\semlab{Const} & c~V &\reducesto& \Return\;(\const{c}\,(V)) \\ +\semlab{Split} & \Let \; \Record{x,y} = \Record{V,W} \; \In \; N &\reducesto& N[V/x,W/y] \\ +\semlab{Case-inl} & + \Case \; (\Inl\, V)^B \; \{\Inl \; x \mapsto M;\Inr \; y \mapsto N\} &\reducesto& M[V/x] \\ +\semlab{Case-inr} & + \Case \; (\Inr\, V)^A \; \{\Inl \; x \mapsto M; \Inr \; y \mapsto N\} &\reducesto& N[V/y]\\ +\semlab{Let} & + \Let \; x \revto \Return \; V \; \In \; N &\reducesto& N[V/x] \\ +\semlab{Lift} & + \EC[M] &\reducesto& \EC[N], \hfill \text{if }M \reducesto N \\ +\end{reductions} +\begin{syntax} +\slab{Evaluation contexts} & \mathcal{E} &::=& [\,] \mid \Let \; x \revto \mathcal{E} \; \In \; N +\end{syntax} +\caption{Contextual Small-Step Operational Semantics} +\label{fig:small-step} +\end{figure*} +% +We give a small-step operational semantics for \BCalc{} with +\emph{evaluation contexts} in the style of \citet{Felleisen87}. The +reduction rules are given in Figure~\ref{fig:small-step}. +% +We write $M[V/x]$ for $M$ with $V$ substituted for $x$ and $\const{c}$ +for the usual interpretation of constant $c$ as a meta-level function +on closed values. The reduction relation $\reducesto$ is defined on +computation terms. The statement $M \reducesto N$ reads: term $M$ +reduces to term $N$ in one step. +% +We write $R^+$ for the transitive closure of relation $R$ and $R^*$ +for the reflexive, transitive closure of relation $R$. + +\paragraph{Notation} +% +We elide type annotations when clear from context. +% +For convenience we 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: +% +{\small +\[ + \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. +% +{\small +\[ + 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 +% +{\small +\[ + \lambda\Unit.M \defas \lambda x^{\One}.M, \quad \text{where $x \notin FV(M)$} +\]}% +% +for suspended computations, and if the binder has a type other than +$\One$, we write: +% +{\small +\[ + \lambda\_^A.M \defas \lambda x^A.M, \quad \text{where $x \notin FV(M)$} +\]}% +% +We use the standard encoding of booleans as a sum: +{\small +\begin{mathpar} +\Bool \defas \One + \One + +\True \defas \Inl~\Unit + +\False \defas \Inr~\Unit + +\If\;V\;\Then\;M\;\Else\;N \defas \Case\;V\;\{\Inl~\Unit \mapsto M; \Inr~\Unit \mapsto N\} +\end{mathpar}}% + +% +% Handlers extension +% +\subsection{Handler Calculus} +\label{sec:handlers-calculus} + +We now define $\HCalc$ as an extension of $\BCalc$. +% +{\small +\begin{syntax} +\slab{Operation symbols} &\ell \in \mathcal{L} & & \\ +\slab{Signatures} &\Sigma&::=& \cdot \mid \{\ell : A \to B\} \cup \Sigma\\ +\slab{Handler types} &F &::=& C \Rightarrow D\\ +\slab{Computations} &M, N &::=& \dots \mid \Do \; \ell \; V + \mid \Handle \; M \; \With \; H \\ +\slab{Handlers} &H&::=& \{ \Val \; x \mapsto M \} + \mid \{ \ell \; p \; r \mapsto N \} \uplus H\\ +\end{syntax}}% +% +We assume a countably infinite set $\mathcal{L}$ of operation symbols +$\ell$. +% +An effect signature $\Sigma$ is a map from operation symbols to their +types, thus we assume that each operation symbol in a signature is +distinct. An operation type $A \to B$ classifies operations that take +an argument of type $A$ and return a result of type $B$. +% +We write $dom(\Sigma) \subseteq \mathcal{L}$ for the set of operation +symbols in a signature $\Sigma$. +% +A handler type $C \Rightarrow D$ classifies effect handlers that +transform computations of type $C$ into computations of type $D$. +% +Following \citet{Pretnar15}, we assume a global signature for every +program. +% +Computations are extended with operation invocation ($\Do\;\ell\;V$) +and effect handling ($\Handle\; M \;\With\; H$). +% +Handlers are constructed from one success clause $(\{\Val\; x \mapsto +M\})$ and one operation clause $(\{ \ell \; p \; r \mapsto N \})$ for +each operation $\ell$ in $\Sigma$. +% +Following \citet{PlotkinP13}, we adopt the convention that a handler +with missing operation clauses (with respect to $\Sigma$) is syntactic +sugar for one in which all missing clauses perform explicit +forwarding: +\[ + \{\ell \; p \; r \mapsto \Let\; x \revto \Do \; \ell \, p \;\In\; r \, x\} +\] + +\begin{figure*} +\small +\raggedright +\textbf{Computations} +\begin{mathpar} + \inferrule*[Lab=\tylab{Do}] + {(\ell : A \to B) \in \Sigma \\ \typ{\Gamma}{V : A} } + {\typ{\Gamma}{\Do \; \ell \; V : B}} + +\inferrule*[Lab=\tylab{Handle}] + {\typ{\Gamma}{M : C} \\ + \Gamma \vdash H : C \Rightarrow D} + {\typ{\Gamma}{\Handle \; M \; \With \; H : D}} +\end{mathpar} +\textbf{Handlers} +\begin{mathpar} +\inferrule*[Lab=\tylab{Handler}] + { \hret = \{\Val \; x \mapsto M\} \\ + [\hell = \{\ell \, p \; r \mapsto N_\ell\}]_{\ell \in dom(\Sigma)} \\\\ + \typ{\Gamma, x : C}{M : D} \\ + [\typ{\Gamma, p : A_\ell, r : B_\ell \to D}{N_\ell : D}]_{(\ell : A_\ell \to B_\ell) \in \Sigma} + } + {{\Gamma} \vdash {H : C \Rightarrow D}} +\end{mathpar} + +\caption{Additional Typing Rules for $\HCalc$} +\label{fig:typing-handlers} +\end{figure*} + +The typing rules for $\HCalc$ are those of $\BCalc$ +(Figure~\ref{fig:typing}) plus three additional rules for operations, +handling, and handlers given in Figure~\ref{fig:typing-handlers}. +% +The \tylab{Do} rule ensures that an operation invocation is only +well-typed if the operation $\ell$ appears in the effect signature +$\Sigma$ and the argument type $A$ matches the type of the provided +argument $V$. The result type $B$ determines the type of the +invocation. +% +The \tylab{Handle} rule types handler application. +% +The \tylab{Handler} rule ensures that the bodies of the success clause +and the operation clauses all have the output type $D$. The type of +$x$ in the success clause must match the input type $C$. The type of +the parameter $p$ ($A_\ell$) and resumption $r$ ($B_\ell \to D$) in +operation clause $\hell$ is determined by the type of $\ell$; the +return type of $r$ is $D$, as the body of the resumption will itself +be handled by $H$. +% +We write $\hell$ and $\hret$ for projecting success and operation +clauses. +{\small +\[ + \ba{@{~}r@{~}c@{~}l@{~}l} + \hret &\defas& \{\Val\, x \mapsto M \}, &\quad \text{where } \{\Val\, x \mapsto M \} \in H\\ + \hell &\defas& \{\ell\, p\,r \mapsto M \}, &\quad \text{where } \{\ell\, p\;r \mapsto M \} \in H + \ea +\]}% + +We extend the operational semantics to $\HCalc$. Specifically, we add +two new reduction rules: one for handling return values and another +for handling operation invocations. +% +{\small +\begin{reductions} +\semlab{Ret} & \Handle \; (\Return \; V) \; \With \; H &\reducesto& N[V/x], \qquad + \text{where } \hret = \{ \Val \; x \mapsto N \} \smallskip\\ + \semlab{Op} & \Handle \; \EC[\Do \; \ell \, V] \; \With \; H &\reducesto& N[V/p,\; (\lambda y.\Handle \; \EC[\Return \; y] \; \With \; H)/r],\\ + \multicolumn{4}{@{}r@{}}{ + \hfill\text{where } \hell = \{ \ell\, p \; r \mapsto N \} + } +\end{reductions}}% +% +The first rule invokes the success clause. +% +The second rule handles an operation via the corresponding operation +clause. +% +If we were \naively to extend evaluation contexts with the handle +construct then our semantics would become nondeterministic, as it may +pick an arbitrary handler in scope. +% +In order to ensure that the semantics is deterministic, we instead add +a distinct form of evaluation context for effectful computation, which +we call handler contexts. +% +{\small +\begin{syntax} +\slab{Handler contexts} & \HC &::= & [\,] \mid \Handle \; \HC \; \With \; H + \mid \Let\;x \revto \HC\; \In\; N\\ +\end{syntax}}% +% +We replace the $\semlab{Lift}$ rule with a corresponding rule for +handler contexts. +{\small +\[ + \HC[M] ~\reducesto~ \HC[N], \qquad\hfill\text{if } M \reducesto N +\]}% +% +The separation between pure evaluation contexts $\EC$ and handler +contexts $\HC$ ensures that the $\semlab{Op}$ rule always selects the +innermost handler. + +We now characterise normal forms and state the standard type soundness +property of $\HCalc$. +% +\begin{definition}[Computation normal forms] + A computation term $N$ is normal with respect to $\Sigma$, if $N = + \Return\;V$ for some $V$ or $N = \EC[\Do\;\ell\,W]$ for some $\ell + \in dom(\Sigma)$, $\EC$, and $W$. +\end{definition} +% + +\begin{theorem}[Type Soundness] + If $\typ{}{M : C}$, then either there exists $\typ{}{N : C}$ such + that $M \reducesto^* N$ and $N$ is normal with respect to $\Sigma$, + or $M$ diverges. +\end{theorem} + +%% +%% Abstract machine semantics +%% +\subsection{The Role of Types} + +Readers familiar with backtracking search algorithms may wonder where +types come into the expressiveness picture. +% +Types will not play a direct role in our proofs but rather in the +characterisation of which programs can be meaningfully compared. In +particular, types are used to rule out global approaches such as +continuation passing style (CPS): without types one could obtain an +efficient pure generic count program by CPS transforming the entire +program. + +Readers familiar with effect handlers may wonder why our handler +calculus does not include an effect type system. +% +As types frame the comparison of programs between languages, we +require that types be fixed across languages; hence $\HCalc$ does not +include effect types. +% +Future work includes reconciling effect typing with our approach to +expressiveness. + +\section{Abstract Machine Semantics} +\label{sec:abstract-machine-semantics} +Thus far we have introduced the base calculus $\BCalc$ and its +extension with effect handlers $\HCalc$. +% +For each calculus we have given a \emph{small-step operational + semantics} which uses a substitution model for evaluation. Whilst +this model is semantically pleasing, it falls short of providing a +realistic account of practical computation as substitution is an +expensive operation. We now develop a more practical model of +computation based on an \emph{abstract machine semantics}. + +\subsection{Base Machine} +\label{sec:base-abstract-machine} + +\newcommand{\Conf}{\dec{Conf}} +\newcommand{\EConf}{\dec{EConf}} +\newcommand{\MVal}{\dec{MVal}} + +We choose a \emph{CEK}-style abstract machine +semantics~\citep{FelleisenF86} for \BCalc{} based on that of +\citet{HillerstromLA20}. +% +The CEK machine operates on configurations which are triples of the +form $\cek{M \mid \gamma \mid \sigma}$. The first component contains +the computation currently being evaluated. The second component +contains the environment $\gamma$ which binds free variables. The +third component contains the continuation which instructs the machine +how to proceed once evaluation of the current computation is complete. +% +The syntax of abstract machine states is as follows. +{\small +\begin{syntax} +\slab{Configurations} & \conf \in \Conf &::=& \cek{M \mid \env \mid \sigma} \\ + % & &\mid& \cekop{M \mid \env \mid \kappa \mid \kappa'} \\ +\slab{Environments} &\env \in \Env &::=& \emptyset \mid \env[x \mapsto v] \\ +\slab{Machine values} &v, w \in \MVal &::= & x \mid n \mid c \mid \Unit \mid \Record{v, w} \\ + & &\mid& (\env, \lambda x^A .\, M) \mid (\env, \Rec\, f^{A \to B}\,x . \, M) + \mid (\Inl\, v)^B \mid (\Inr\,w)^A \\ +\slab{Pure continuations} &\sigma \in \PureCont &::=& \nil \mid (\env, x, N) \cons \sigma \\ +\end{syntax}}% +% +Values consist of function closures, constants, pairs, and left or +right tagged values. +% +We refer to continuations of the base machine as \emph{pure}. +% +A pure continuation is a stack of pure continuation frames. A pure +continuation frame $(\env, x, N)$ closes a let-binding $\Let \;x +\revto [~] \;\In\;N$ over environment $\env$. +% +We write $\nil$ for an empty pure continuation and $\phi \cons \sigma$ +for the result of pushing the frame $\phi$ onto $\sigma$. We use +pattern matching to deconstruct pure continuations. +% + +\begin{figure*} +\small +\raggedright +\textbf{Transition relation} +\begin{reductions} +% App +\mlab{App} & \cek{ V\;W \mid \env \mid \sigma} + &\stepsto& \cek{ M \mid \env'[x \mapsto \val{W}{\env}] \mid \sigma},\\ + &&& \quad\text{ if }\val{V}{\env} = (\env', \lambda x^A . \, M)\\ + +% App rec +\mlab{Rec} & \cek{ V\;W \mid \env \mid \sigma} + &\stepsto& \cek{ M \mid \env'[\bl + f \mapsto (\env', \Rec\,f^{A \to B}\,x. M), \\ + x \mapsto \val{W}{\env}] \mid \sigma},\\ + \el \\ + &&& \quad\text{ if }\val{V}{\env} = (\env', \Rec\, f^{A \to B}\, x. M)\\ + +% Constant +\mlab{Const} & \cek{ V~W \mid \env \mid \sigma} + &\stepsto& \cek{ \Return\; (\const{c}\,(\val{W}\env)) \mid \env \mid \sigma},\\ + &&& \quad\text{ if }\val{V}{\env} = c \\ +\mlab{Split} & \cek{ \Let \; \Record{x,y} = V \; \In \; N \mid \env \mid \sigma} + &\stepsto& \cek{ N \mid \env[x \mapsto v, y \mapsto w] \mid \sigma}, \\ + &&& \quad\text{ if }\val{V}{\env} = \Record{v; w} \\ + +% Case left +\mlab{CaseL} & \ba{@{}l@{}l@{}} + \cekl \Case\; V\, \{&\Inl\, x \mapsto M; \\ + &\Inr\, y \mapsto N\} \mid \env \mid \sigma \cekr \\ + \ea + &\stepsto& \cek{ M \mid \env[x \mapsto v] \mid \sigma},\\ + &&& \quad\text{ if }\val{V}{\env} = \Inl\, v \\ + +% Case right +\mlab{CaseR} & \ba{@{}l@{}l@{}} + \cekl \Case\; V\, \{&\Inl\, x \mapsto M; \\ + &\Inr\, y \mapsto N\} \mid \env \mid \sigma \cekr \\ + \ea + &\stepsto& \cek{ N \mid \env[y \mapsto v] \mid \sigma},\\ + &&& \quad\text{ if }\val{V}{\env} = \Inr\, v \\ + +% Let - eval M +\mlab{Let} & \cek{ \Let \; x \revto M \; \In \; N \mid \env \mid \sigma} + &\stepsto& \cek{ M \mid \env \mid (\env,x,N) \cons \sigma} \\ + +% Return - let binding +\mlab{RetCont} &\cek{ \Return \; V \mid \env \mid (\env',x,N) \cons \sigma} + &\stepsto& \cek{ N \mid \env'[x \mapsto \val{V}{\env}] \mid \sigma} \\ + +\end{reductions} + +\textbf{Value interpretation} +\[ +\bl +\begin{eqs} +\val{x}{\env} &=& \env(x) \\ +\val{\Unit{}}{\env} &=& \Unit{} \\ +\end{eqs} +\qquad\qquad\qquad +\begin{eqs} +\val{n}{\env} &=& n \\ +\val{c}\env &=& c \\ +\end{eqs} +\qquad\qquad\qquad +\begin{eqs} +\val{\lambda x^A.M}{\env} &=& (\env, \lambda x^A.M) \\ +\val{\Rec\, f^{A \to B}\, x.M}{\env} &=& (\env, \Rec\,f^{A \to B}\, x.M) \\ +\end{eqs} +\medskip \\ +\begin{eqs} +\val{\Record{V, W}}{\env} &=& \Record{\val{V}{\env}, \val{W}{\env}} \\ +\end{eqs} +\qquad\qquad\qquad +\ba{@{}r@{~}c@{~}l@{}} +\val{(\Inl\, V)^B}{\env} &=& (\Inl\; \val{V}{\env})^B \\ +\val{(\Inr\, V)^A}{\env} &=& (\Inr\; \val{V}{\env})^A \\ +\ea +\el +\] + +\caption{Abstract Machine Semantics for $\BCalc$} +\label{fig:abstract-machine-semantics} +\end{figure*} + +The abstract machine semantics is given in +Figure~\ref{fig:abstract-machine-semantics}. +% +The transition relation ($\stepsto$) makes use of the value +interpretation ($\val{-}$) from value terms to machine values. +% +The machine is initialised by placing a term in a configuration +alongside the empty environment ($\emptyset$) and identity +pure continuation ($\nil$). +% +The rules (\mlab{App}), (\mlab{Rec}), (\mlab{Const}), (\mlab{Split}), +(\mlab{CaseL}), and (\mlab{CaseR}) eliminate values. +% +The (\mlab{Let}) rule extends the current pure continuation with let +bindings. +% +The (\mlab{RetCont}) rule extends the environment in the top frame of +the pure continuation with a returned value. +% +Given an input of a well-typed closed computation term $\typ{}{M : + A}$, the machine will either diverge or return a value of type $A$. +% +A final state is given by a configuration of the form $\cek{\Return\;V + \mid \env \mid \nil}$ in which case the final return value is given +by the denotation $\val{V}{\env}$ of $V$ under environment $\gamma$. +% + +\paragraph{Correctness} +% +The base machine faithfully simulates the operational semantics for +$\BCalc$; most transitions correspond directly to $\beta$-reductions, +but $\mlab{Let}$ performs an administrative step to bring the +computation $M$ into evaluation position. +% +We formally state and prove the correspondence in +Appendix~\ref{sec:base-machine-correctness}, relying on an +inverse map $\inv{-}$ from configurations to +terms~\citep{HillerstromLA20}. +% +\newcommand{\contapp}[2]{#1 #2} +\newcommand{\contappp}[2]{#1(#2)} + +\subsection{Handler Machine} +\newcommand{\HClosure}{\dec{HClo}} +We now enrich the $\BCalc$ machine to a $\HCalc$ machine. +% +We extend the syntax as follows. +% +{\small +\begin{syntax} + \slab{Configurations} &\conf \in \Conf &::=& \cek{M \mid \env \mid \kappa}\\ + \slab{Resumptions} &\rho \in \dec{Res} &::=& (\sigma, \chi)\\ + \slab{Continuations} &\kappa \in \Cont &::=& \nil \mid \rho \cons \kappa\\ + \slab{Handler closures} &\chi \in \HClosure &::=& (\env, H) \\ + \slab{Machine values} &v, w \in \MVal &::=& \cdots \mid \rho \\ +\end{syntax}}% +% +The notion of configurations changes slightly in that the continuation +component is replaced by a generalised continuation +$\kappa \in \Cont$~\cite{HillerstromLA20}; a continuation is now a +list of resumptions. A resumption is a pair of a pure continuation (as +in the base machine) and a handler closure ($\chi$). +% +A handler closure consists of an environment and a handler definition, +where the former binds the free variables that occur in the latter. +% +The identity continuation is a singleton list containing the identity +resumption, which is an empty pure continuation paired with the +identity handler closure: +% +{\small +\[ +\kappa_0 \defas [(\nil, (\emptyset, \{\Val\;x \mapsto x\}))] +\]}% +% +Machine values are augmented to include resumptions as an operation +invocation causes the topmost frame of the machine continuation to be +reified (and bound to the resumption parameter in the operation +clause). +% + +The handler machine adds transition rules for handlers, and modifies +$(\mlab{Let})$ and $(\mlab{RetCont})$ from the base machine to account +for the richer continuation +structure. Figure~\ref{fig:abstract-machine-semantics-handlers} +depicts the new and modified rules. +% +The $(\mlab{Handle})$ rule pushes a handler closure along with an +empty pure continuation onto the continuation stack. +% +The $(\mlab{RetHandler})$ rule transfers control to the success clause +of the current handler once the pure continuation is empty. +% +The $(\mlab{Handle-Op})$ rule transfers control to the matching +operation clause on the topmost handler, and during the process it +reifies the handler closure. Finally, the $(\mlab{Resume})$ rule +applies a reified handler closure, by pushing it onto the continuation +stack. +% +The handler machine has two possible final states: either it yields a +value or it gets stuck on an unhandled operation. + +\begin{figure*} +\small +\raggedright + +\textbf{Transition relation} +\begin{reductions} +% Resume resumption +\mlab{Resume} & \cek{ V\;W \mid \env \mid \kappa} + &\stepsto& \cek{ \Return \; W \mid \env \mid (\sigma, \chi) \cons \kappa},\\ + &&&\quad\text{ if }\val{V}{\env} = (\sigma, \chi) \\ + +% Let - eval M +\mlab{Let} & \cek{ \Let \; x \revto M \; \In \; N \mid \env \mid (\sigma, \chi) \cons \kappa} + &\stepsto& \cek{ M \mid \env \mid ((\env,x,N) \cons \sigma, \chi) \cons \kappa} \\ + +% Apply (machine) continuation - let binding +\mlab{RetCont} &\cek{ \Return \; V \mid \env \mid ((\env',x,N) \cons \sigma, \chi) \cons \kappa} + &\stepsto& \cek{ N \mid \env'[x \mapsto \val{V}{\env}] \mid (\sigma, \chi) \cons \kappa} \\ + +% Handle +\mlab{Handle} & \cek{ \Handle \; M \; \With \; H \mid \env \mid \kappa} + &\stepsto& \cek{ M \mid \env \mid (\nil, (\env, H)) \cons \kappa} \\ + +% Return - handler +\mlab{RetHandler} & \cek{ \Return \; V \mid \env \mid (\nil, (\env',H)) \cons \kappa} + &\stepsto& \cek{ M \mid \env'[x \mapsto \val{V}{\env}] \mid \kappa},\\ + &&&\quad\text{ if } \hret = \{\Val\; x \mapsto M\} \\ + +% Handle op +\mlab{Handle-Op} & \cek{ \Do \; \ell~V \mid \env \mid (\sigma, (\env', H)) \cons \kappa } + &\stepsto& \cek{ M \mid \env'[\bl + p \mapsto \val{V}\env, \\ + r \mapsto (\sigma, (\env', H))] \mid \kappa }, \\ + \el \\ + &&&\quad\bl + \text{ if } \ell : A \to B \in \Sigma\\ + \text{ and } \hell = \{\ell\; p \; r \mapsto M\} + \el\\ +\end{reductions} +\caption{Abstract Machine Semantics for $\HCalc$} +\label{fig:abstract-machine-semantics-handlers} +\end{figure*} + +\paragraph{Correctness} +% +The handler machine faithfully simulates the operational semantics of +$\HCalc$. +% +Extending the result for the base machine, we formally state and prove +the correspondence in +Appendix~\ref{sec:handler-machine-correctness}. + +\subsection{Realisability and Asymptotic Complexity} +\label{sec:realisability} +As witnessed by the work of \citet{HillerstromL18} the machine +structures are readily realisable using standard persistent functional +data structures. +% +Pure continuations on the base machine and generalised continuations +on the handler machine can be implemented using linked lists with a +time complexity of $\BigO(1)$ for the extension operation +$(\_\cons\_)$. +% +The topmost pure continuation on the handler machine may also be +extended in time $\BigO(1)$, as extending it only requires reaching +under the topmost handler closure. +% +Environments, $\env$, can be realised using a map, with a time +complexity of $\BigO(\log|\env|)$ for extension and +lookup~\citep{Okasaki99}. + +The worst-case time complexity of a single machine transition is +exhibited by rules which involve operations on the environment, since +any other operation is constant time, hence the worst-time complexity +of a transition is $\BigO(\log|\env|)$. +% +The value interpretation function $\val{-}\env$ is defined +structurally on values. Its worst-time complexity is exhibited by a +nesting of pairs of variables $\val{\Record{x_1,\dots,x_n}}\env$ which +has complexity $\BigO(n\log|\env|)$. + +\paragraph{Continuation copying} On the handler machine the topmost +continuation frame can be copied in constant time due to the +persistent runtime and the layout of machine continuations. An +alternative design would be to make the runtime non-persistent +% +in which case copying a continuation frame $((\sigma, \_) \cons +\_)$ would be a $\BigO(|\sigma|)$ time operation. + +\paragraph{Primitive operations on naturals} +% +Our model assumes that arithmetic operations on arbitrary natural +numbers take $\BigO(1)$ time. This is common practice in the study of +algorithms when the main interest lies +elsewhere~\citep[Section~2.2]{CormenLRS09}. If desired, one could +adopt a more refined cost model that accounted for the bit-level +complexity of arithmetic operations; however, doing so would have the +same impact on both of the situations we are wishing to compare, and +thus would add nothing but noise to the overall analysis. + + +%% +%% Generic search +%% +\section{Predicates, Decision Trees and Generic Count} +\label{sec:generic-search} + +We now come to the crux of the paper. In this section and the next, we +prove that $\HCalc$ supports implementations of certain operations +with an asymptotic runtime bound that cannot be achieved in $\BCalc$ +(Section~\ref{sec:pure-counting}). +% +While the positive half of this claim essentially consolidates a +known piece of folklore, the negative half appears to be new. +% +To establish our result, it will suffice to exhibit a single +`efficient' program in $\HCalc$, then show that no equivalent program +in $\BCalc$ can achieve the same asymptotic efficiency. We take +\emph{generic search} as our example. + +Generic search is a modular search procedure that takes as input +a predicate $P$ on some multi-dimensional search space, +and finds all points of the space satisfying $P$. +Generic search is agnostic to the specific instantiation of $P$, +and as a result is applicable across a wide spectrum of domains. +Classic examples such as Sudoku solving~\citep{Bird06}, the +$n$-queens problem~\citep{BellS09} and graph colouring +can be cast as instances of generic search, and similar ideas have +been explored in connection with Nash equilibria and +exact real integration~\citep{Simpson98, Daniels16}. +% Taken out Nash equilibria. + +For simplicity, we will restrict attention to search spaces of the form $\B^n$, +the set of bit vectors of length $n$. +To exhibit our phenomenon in the simplest +possible setting, we shall actually focus on the \emph{generic count} problem: +given a predicate $P$ on some $\B^n$, return the \emph{number of} points +of $\B^n$ satisfying $P$. However, we shall explain why our results +are also applicable to generic search proper. + +We shall view $\B^n$ as the set of functions $\N_n \to \B$, +where $\N_n \defas \{0,\dots,n-1\}$. +In both $\BCalc$ and $\HCalc$ we may represent such functions by terms of type $\Nat \to \Bool$. +We will often informally write $\Nat_n$ in place of $\Nat$ to indicate that +only the values $0,\dots,n-1$ are relevant, but this convention has no +formal status since our setup does not support dependent types. + +To summarise, in both $\BCalc$ and $\HCalc$ we will be working with the types +% +{\small +\[ +\begin{twoeqs} + \Point & \defas & \Nat \to \Bool & \hspace*{2.0em} & + \Point_n & \defas & \Nat_n \to \Bool \\ + \Predicate & \defas & \Point \to \Bool & & + \Predicate_n & \defas & \Point_n \to \Bool +\end{twoeqs} +\] +} +% +and will be looking for programs +% +{\small +\[ + \Count_n : \Predicate_n \to \Nat +\]}% +% +such that for suitable terms $P$ representing semantic predicates $\Pi: \B^n \to \B$, +$\Count_n~P$ finds the number of points of $\B^n$ satisfying $\Pi$. + +Before formalising these ideas more closely, let us look at some examples, +which will also illustrate the machinery of \emph{decision trees} that we will be using. + + +\subsection{Examples of Points, Predicates and Trees} +\label{sec:predicates-points} +Consider first the following terms of type $\Point$: +{\small +\begin{mathpar} +\dec{q}_0 \defas \lambda \_. \True + +\dec{q}_1 \defas \lambda i. i=0 + +\dec{q}_2 \defas \lambda i.\, + \If\;i = 0\;\Then\;\True\; + \Else\;\If\;i = 1\;\Then\;\False\; + \Else\;\bot +\end{mathpar}}% +(Here $\bot$ is the diverging term $(\Rec\; f\,i.f\,i)\,\Unit$.) +Then $\dec{q}_0$ represents $\langle{\True,\dots,\True}\rangle \in \B^n$ for any $n$; +$\dec{q}_1$ represents $\langle{\True,\False,\dots,\False}\rangle \in \B^n$ for any $n \geq 1$; +and $\dec{q}_2$ represents $\langle{\True,\False}\rangle \in \B^2$. + +Next some predicates. +First, the following terms all represent the constant true predicate $\B^2 \to \B$: +{\small +\begin{mathpar} +\dec{T}_0 \defas \lambda q. \True + +\dec{T}_1 \defas \lambda q.(q\,1; q\,0; \True) + +\dec{T}_2 \defas \lambda q.(q\,0; q\,0; \True) +\end{mathpar}}% +These illustrate that in the course of evaluating a predicate term $P$ at a point $\dec{q}$, +for each $i,>=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 + \begin{subfigure}{0.1\textwidth} + \begin{center} + \vspace*{6.5ex} + \scalebox{1.0}{\TTZeroModel} + \vspace*{6.5ex} + \end{center} + \caption{$\dec{T}_0$} + \label{fig:tt0-tree} + \end{subfigure} + % + \begin{subfigure}{0.3\textwidth} + \begin{center} + \scalebox{1.0}{\ShortConjModel} + \end{center} + \caption{$\dec{I}_2$} + \label{fig:div1-tree} + \end{subfigure} + % + \begin{subfigure}{0.4\textwidth} + \begin{center} + \scalebox{1.0}{\XORTwoModel} + \end{center} + \caption{$\dec{Odd}_2$} + \label{fig:xor2-tree} + \end{subfigure} + \caption{Examples of Decision Trees} + \label{fig:example-models} +\end{figure} + +We can think of a predicate term $P$ as participating in a `dialogue' +with a given point $Q : \Point_n$. +The predicate may \emph{query} $Q$ at some coordinate $k$; +$Q$ may \emph{respond} with $\True$ or $\False$ and this returned value +may influence the future course of the dialogue. +After zero or more such query/response pairs, the predicate may return a +final \emph{answer} ($\True$ or $\False$). + +The set of possible dialogues with a given term $P$ may be organised +in an obvious way into an unrooted binary \emph{decision tree}, in +which each internal node is labelled with a query $\query k$ (with +$k0$ where + both claims hold for all $m'