gray!40 gray!40

# Effects for Efficiency

Asymptotic Speedup with First-Class Control

Daniel Hillerström  The University of EdinburghUK<EMAIL_ADDRESS>,  Sam Lindley  The University of Edinburgh and Imperial College London and
Heriot-Watt UniversityUK<EMAIL_ADDRESS>and  John Longley  The
University of EdinburghUK<EMAIL_ADDRESS>
###### Abstract.

We study the fundamental efficiency of delimited control. Specifically, we
show that effect handlers enable an asymptotic improvement in runtime
complexity for a certain class of functions. We consider the _generic count_
problem using a pure PCF-like base language $\lambda_{\textrm{b}}$ and its
extension with effect handlers $\lambda_{\textrm{h}}$. We show that
$\lambda_{\textrm{h}}$ admits an asymptotically more efficient implementation
of generic count than any $\lambda_{\textrm{b}}$ implementation. We also show
that this efficiency gap remains when $\lambda_{\textrm{b}}$ is extended with
mutable state.

To our knowledge this result is the first of its kind for control operators.

##  1\. Introduction

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, Felleisen
(1991) considers the question of whether a language ${\mathcal{L}}$ admits a
translation into a sublanguage ${\mathcal{L}}^{\prime}$ 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
${\mathcal{L}}$-program into ${\mathcal{L}}^{\prime}$ requires a complete
global restructuring, we may say that ${\mathcal{L}}^{\prime}$ is in some way
less expressive than ${\mathcal{L}}$. 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.

  1. (1)

_Computability_ : Are there operations of a given type that are programmable
in ${\mathcal{L}}$ but not expressible at all in ${\mathcal{L}}^{\prime}$?

  2. (2)

_Complexity_ : Are there operations programmable in ${\mathcal{L}}$ with some
asymptotic runtime bound (e.g. ‘$\mathcal{O}(n^{2})$’) that cannot be achieved
in ${\mathcal{L}}^{\prime}$?

We may also ask: are there examples of _natural, practically useful_
operations that manifest such differences? If so, this might be considered as
a significant advantage of ${\mathcal{L}}$ over ${\mathcal{L}}^{\prime}$.

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., (Knuth, 1997, Section 2.6)), 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 _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
_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 _parallel if_ operation which is computable
in a language with parallel evaluation but not in a typical ‘sequential’
programming language (Plotkin, 1977). 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 (Cartwright and Felleisen, 1992). 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
${\mathbb{N}}_{\bot}\times{\mathbb{N}}_{\bot}\rightarrow{\mathbb{N}}_{\bot}$);
however, there are also programs with ‘functional’ behaviour that can be
implemented with control or local state but not without them (Longley, 1999).
More recent results have exhibited differences lower down in the language
expressivity spectrum: for instance, in a purely functional setting à la
Haskell, the expressive power of _recursion_ increases strictly with its type
level (Longley, 2018), and there are natural operations computable by low-
order recursion but not by high-order iteration (Longley, 2019). 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 Longley
and Normann (2015).

Relatively few results of this character have so far been established on the
complexity side. Pippenger (1996) 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
$\mathcal{O}(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 Bird et al. (1997) 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 (Okasaki,
1999), although to our knowledge this situation has not yet been subjected to
theoretical scrutiny. Jones (2001) 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 _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=\mathsf{true}$. We shall consider boolean vectors of any length to be
represented by the type $\mathsf{Nat}\to\mathsf{Bool}$; thus for each $n$, we
are asking for an implementation of a certain third-order operation

$\mathsf{count}_{n}:((\mathsf{Nat}\to\mathsf{Bool})\to\mathsf{Bool})\to\mathsf{Nat}$

A naïve 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 Berger (1990) 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(n2^{n})$ runtime. Moreover, we shall show that in a
typical call-by-value language without advanced control features, one cannot
improve on this: _any_ implementation of $\mathsf{count}_{n}$ must necessarily
take time $\Omega(n2^{n})$ on _any_ predicate $P$. On the other hand, if we
extend our language with a feature such as _effect handlers_ (see Section 2
below), it becomes possible to bring the runtime down to $\mathcal{O}(2^{n})$:
an asymptotic gain of a factor of $n$.

The _generic search_ problem is just like the generic count problem, except
rather than counting the vectors $q$ such that $P\,q=\mathsf{true}$, it
returns the list of all such vectors. The $\Omega(n2^{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 7.2 we illustrate that the $\mathcal{O}(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 naïve
implementation of $\mathsf{count}_{3}$ might start by applying the given $P$
to $q_{0}=(\mathsf{true},\mathsf{true},\mathsf{true})$, and then to
$q_{1}=(\mathsf{true},\mathsf{true},\mathsf{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 $\mathsf{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 _particular_ choice of $P$ (corresponding, say, to the
$n$-queens problem); but to apply this idea of resuming previous
subcomputations in the _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 _as regards their power to
manipulate data of type_ $(\mathsf{Nat}\to\mathsf{Bool})\to\mathsf{Bool}$.

This idea of using first-class control to achieve ‘backtracking’ has been
exploited before and is fairly widely known (see e.g. (Kiselyov et al.,
2005)), 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’ (Sperber et al., 2009), ‘control’ ($\mathcal{F}$) and ’prompt’
(#) (Felleisen, 1988), or ‘shift’ and ‘reset’ (Danvy and Filinski, 1990).

The rest of the paper is structured as follows.

  * •

Section 2 provides an introduction to effect handlers as a programming
abstraction.

  * •

Section 3 presents a PCF-like language $\lambda_{\textrm{b}}$ and its
extension $\lambda_{\textrm{h}}$ with effect handlers.

  * •

Section 4 defines abstract machines for $\lambda_{\textrm{b}}$ and
$\lambda_{\textrm{h}}$, yielding a runtime cost model.

  * •

Section 5 introduces generic count and some associated machinery, and presents
an implementation in $\lambda_{\textrm{h}}$ with runtime $\mathcal{O}(2^{n})$.

  * •

Section 6 establishes that any generic count implementation in
$\lambda_{\textrm{b}}$ must have runtime $\Omega(n2^{n})$.

  * •

Section 7 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.

  * •

Section 8 evaluates implementations of generic search based on
$\lambda_{\textrm{b}}$ and $\lambda_{\textrm{h}}$ in Standard ML.

  * •

Section 9 concludes.

The languages $\lambda_{\textrm{b}}$ and $\lambda_{\textrm{h}}$ 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
(Hillerström et al., 2020b).

##  2\. Effect Handlers Primer

Effect handlers were originally studied as a theoretical means to provide a
semantics for exception handling in the setting of algebraic effects (Plotkin
and Power, 2001; Plotkin and Pretnar, 2013). Subsequently they have emerged as
a practical programming abstraction for modular effectful programming (Bauer
and Pretnar, 2015; Convent et al., 2020; Kammar et al., 2013; Kiselyov et al.,
2013; Dolan et al., 2015; Leijen, 2017; Hillerström et al., 2020a). 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
Pretnar (2015), and as an introduction to the mathematical foundations of
handlers, we refer the reader to the founding paper by Plotkin and Pretnar
(2013) and the excellent tutorial paper by Bauer (2018).

Viewed through the lens of universal algebra, an algebraic effect is given by
a signature $\Sigma$ of typed _operation symbols_ along with an equational
theory that describes the properties of the operations (Plotkin and Power,
2001). An example of an algebraic effect is _nondeterminism_ , whose signature
consists of a single nondeterministic choice operation:
$\Sigma\mathrel{:=}\\{\mathsf{Branch}:\mathsf{Unit}\to\mathsf{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 $\mathsf{Branch}$ to model a
coin toss. Suppose we have a data type
$\mathsf{Toss}\mathrel{:=}\mathsf{Heads}\mid\mathsf{Tails}$, then we may
implement a coin toss as follows.

$\begin{array}[t]{@{}l@{}}\mathsf{toss}:\mathsf{Unit}\to\mathsf{Toss}\\\
\mathsf{toss}~{}\langle\rangle=\mathbf{if}\;\mathbf{do}\;\mathsf{Branch}\;\langle\rangle\;\mathbf{then}\;\mathsf{Heads}\;\mathbf{else}\;\mathsf{Tails}\end{array}$

From the type signature it is clear that the computation returns a value of
type $\mathsf{Toss}$. It is not clear from the signature of $\mathsf{toss}$
whether it performs an effect. However, from the definition, it evidently
performs the operation $\mathsf{Branch}$ with argument $\langle\rangle$ using
the $\mathbf{do}$-invocation form. The result of the operation determines
whether the computation returns either $\mathsf{Heads}$ or $\mathsf{Tails}$.
Systems such as Frank (Lindley et al., 2017; Convent et al., 2020), Helium
(Biernacki et al., 2019, 2020), Koka (Leijen, 2017), and Links (Hillerström
and Lindley, 2016; Hillerström et al., 2020a) include type-and-effect systems
which track the use of effectful operations, whilst current iterations of
systems such as Eff (Bauer and Pretnar, 2015) and Multicore OCaml (Dolan et
al., 2015) 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 $\mathsf{toss}$ is as follows.

$\mathsf{Branch}$$\mathsf{Heads}$$\mathsf{true}$$\mathsf{Tails}$$\mathsf{false}$

It models interaction with the environment. The operation $\mathsf{Branch}$
can be viewed as a _query_ for which the _response_ is either $\mathsf{true}$
or $\mathsf{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.

$\begin{array}[t]{@{}l@{}}\mathbf{handle}\;\mathsf{toss}~{}\langle\rangle\;\mathbf{with}\\\
\quad\begin{array}[t]{@{~}l@{~}c@{~}l}{}\lx@intercol\mathbf{val}~{}x\hfil~{}&\mapsto\hfil~{}&[x]\\\
{}\lx@intercol\mathsf{Branch}~{}\langle\rangle~{}r\hfil~{}&\mapsto\hfil~{}&r~{}\mathsf{true}\mathbin{+\\!\\!+}r~{}\mathsf{false}\end{array}\end{array}$

The $\mathbf{handle}$-construct generalises the exceptional syntax of Benton
and Kennedy (2001). This handler has a _success_ clause and an _operation_
clauses. The success clause determines how to interpret the return value of
$\mathsf{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 $\mathsf{Branch}$
in $\mathsf{toss}$. It provides access to the argument of $\mathsf{Branch}$
(which is unit) and its resumption, $r$. The resumption is a first-class
delimited continuation which captures the remainder of the $\mathsf{toss}$
computation from the invocation of $\mathsf{Branch}$ up to its nearest
enclosing handler.

Applying $r$ to $\mathsf{true}$ resumes evaluation of $\mathsf{toss}$ via the
$\mathsf{true}$ branch, returning $\mathsf{Heads}$ and causing the success
clause of the handler to be invoked; thus the result of $r~{}\mathsf{true}$ is
$[\mathsf{Heads}]$. Evaluation continues in the operation clause, meaning that
$r$ is applied again, but this time to $\mathsf{false}$, which causes
evaluation to resume in $\mathsf{toss}$ via the $\mathsf{false}$ branch. By
the same reasoning, the value of $r~{}\mathsf{false}$ is $[\mathsf{Tails}]$,
which is concatenated with the result of the $\mathsf{true}$ branch; hence the
handler ultimately returns $[\mathsf{Heads},\mathsf{Tails}]$.

##  3\. Calculi

In this section, we present our base language $\lambda_{\textrm{b}}$ and its
extension with effect handlers $\lambda_{\textrm{h}}$.

###  3.1. Base Calculus

The base calculus $\lambda_{\textrm{b}}$ is a fine-grain call-by-value (Levy
et al., 2003) variation of PCF (Plotkin, 1977). Fine-grain call-by-value is
similar to A-normal form (Flanagan et al., 1993) in that every intermediate
computation is named, but unlike A-normal form is closed under reduction.

The syntax of $\lambda_{\textrm{b}}$ is as follows.

$\begin{array}[]{@{}l@{\quad}r@{~}c@{~}l@{}}\textrm{Types}&A,B,C,D\in\mathrm{Type}~{}&::=\hfil~{}&\mathsf{Nat}\mid\mathsf{Unit}\mid
A\to B\mid A\times B\mid A+B\\\ \textrm{Type
Environments}&\Gamma\in\mathrm{Ctx}~{}&::=\hfil~{}&\cdot\mid\Gamma,x:A\\\
\textrm{Values}&V,W\in\mathrm{Val}~{}&::=\hfil~{}&x\mid k\mid c\mid\lambda
x^{A}.\,M\mid\mathbf{rec}\;f^{A\to B}\,x.M\\\
&~{}&\mid\hfil~{}&\langle\rangle\mid\langle
V,W\rangle\mid(\mathbf{inl}\,V)^{B}\mid(\mathbf{inr}\,W)^{A}\\\
\textrm{Computations}&M,N\in\mathrm{Comp}~{}&::=\hfil~{}&V\,W\mid\mathbf{let}\;\langle
x,y\rangle=V\;\mathbf{in}\;N\\\
&~{}&\mid\hfil~{}&\mathbf{case}\;V\;\\{\mathbf{inl}\;x\mapsto
M;\mathbf{inr}\;y\mapsto N\\}\\\
&~{}&\mid\hfil~{}&\mathbf{return}\;V\mid\mathbf{let}\;x\leftarrow
M\;\mathbf{in}\;N\\\ \end{array}$

The ground types are $\mathsf{Nat}$ and $\mathsf{Unit}$ 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 $\mathsf{Nat}$, and $r$ to denote resumptions.
The value terms are standard.

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 $(\mathbf{let}\;\langle
x,y\rangle=V\;\mathbf{in}\;N)$ splits a pair $V$ into its constituents and
binds them to $x$ and $y$, respectively. Sums are eliminated by a case split
($\mathbf{case}\;V\;\\{\mathbf{inl}\;x\mapsto M;\mathbf{inr}\;y\mapsto N\\}$).
A trivial computation $(\mathbf{return}\;V)$ returns value $V$. The sequencing
expression $(\mathbf{let}\;x\leftarrow M\;\mathbf{in}\;N)$ evaluates $M$ and
binds the result value to $x$ in $N$.

Values

T-Var $\displaystyle\displaystyle{\hbox{\hskip
18.0094pt\vbox{\hbox{\hskip-18.0094pt\hbox{\hbox{$\displaystyle\displaystyle
x:A\in\Gamma$}}}\vbox{}}}\over\hbox{\hskip
17.7594pt\vbox{\vbox{}\hbox{\hskip-17.75938pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
x:A$}}}}}}$ T-Unit $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
20.82643pt\vbox{\vbox{}\hbox{\hskip-20.82642pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\langle\rangle:\mathsf{Unit}$}}}}}}$
T-Nat $\displaystyle\displaystyle{\hbox{\hskip
10.10939pt\vbox{\hbox{\hskip-10.10939pt\hbox{\hbox{$\displaystyle\displaystyle
k\in\mathbb{N}$}}}\vbox{}}}\over\hbox{\hskip
20.4219pt\vbox{\vbox{}\hbox{\hskip-20.42189pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
k:\mathsf{Nat}$}}}}}}$ T-Const $\displaystyle\displaystyle{\hbox{\hskip
17.46149pt\vbox{\hbox{\hskip-17.46149pt\hbox{\hbox{$\displaystyle\displaystyle
c:A\to B$}}}\vbox{}}}\over\hbox{\hskip
25.524pt\vbox{\vbox{}\hbox{\hskip-25.52399pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
c:A\to B$}}}}}}$ T-Lam $\displaystyle\displaystyle{\hbox{\hskip
31.50471pt\vbox{\hbox{\hskip-31.5047pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A\vdash
M:B$}}}\vbox{}}}\over\hbox{\hskip
38.26973pt\vbox{\vbox{}\hbox{\hskip-38.26971pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\lambda
x^{A}.\,M:A\to B$}}}}}}$ T-Rec $\displaystyle\displaystyle{\hbox{\hskip
51.7063pt\vbox{\hbox{\hskip-51.7063pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,f:A\to
B,x:A\vdash M:B$}}}\vbox{}}}\over\hbox{\hskip
48.14261pt\vbox{\vbox{}\hbox{\hskip-48.14261pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\mathbf{rec}\;f^{A\to
B}\,x.\,M:A\to B$}}}}}}$ T-Prod $\displaystyle\displaystyle{\hbox{\hskip
48.13911pt\vbox{\hbox{\hskip-48.1391pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
V:A$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
W:B$}}}}\vbox{}}}\over\hbox{\hskip
35.4655pt\vbox{\vbox{}\hbox{\hskip-35.46548pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\langle
V,W\rangle:A\times B$}}}}}}$ T-Inl $\displaystyle\displaystyle{\hbox{\hskip
17.56252pt\vbox{\hbox{\hskip-17.56252pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
V:A$}}}\vbox{}}}\over\hbox{\hskip
37.98949pt\vbox{\vbox{}\hbox{\hskip-37.98947pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash(\mathbf{inl}\,V)^{B}:A+B$}}}}}}$
T-Inr $\displaystyle\displaystyle{\hbox{\hskip
20.32658pt\vbox{\hbox{\hskip-20.32657pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
W:B$}}}\vbox{}}}\over\hbox{\hskip
39.60411pt\vbox{\vbox{}\hbox{\hskip-39.6041pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash(\mathbf{inr}\,W)^{A}:A+B$}}}}}}$

Computations

T-App $\displaystyle\displaystyle{\hbox{\hskip
56.26413pt\vbox{\hbox{\hskip-56.26411pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
V:A\to B$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
W:A$}}}}\vbox{}}}\over\hbox{\hskip
24.70158pt\vbox{\vbox{}\hbox{\hskip-24.70157pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
V\,W:B$}}}}}}$ T-Split $\displaystyle\displaystyle{\hbox{\hskip
79.36215pt\vbox{\hbox{\hskip-79.36214pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
V:A\times B$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A,y:B\vdash
N:C$}}}}\vbox{}}}\over\hbox{\hskip
49.91039pt\vbox{\vbox{}\hbox{\hskip-49.91037pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\mathbf{let}\;\langle
x,y\rangle=V\;\mathbf{in}\;N:C$}}}}}}$ T-Case
$\displaystyle\displaystyle{\hbox{\hskip
108.06903pt\vbox{\hbox{\hskip-108.06903pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
V:A+B$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A\vdash M:C$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,y:B\vdash
N:C$}}}}}\vbox{}}}\over\hbox{\hskip
65.16527pt\vbox{\vbox{}\hbox{\hskip-65.16527pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\mathbf{case}\;V\;\\{\mathbf{inl}\;x\mapsto
M;\mathbf{inr}\;y\mapsto N\\}:C$}}}}}}$ T-Return
$\displaystyle\displaystyle{\hbox{\hskip
18.81252pt\vbox{\hbox{\hskip-18.81252pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
V:A$}}}\vbox{}}}\over\hbox{\hskip
31.08754pt\vbox{\vbox{}\hbox{\hskip-31.08754pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\mathbf{return}\;V:A$}}}}}}$
T-Let $\displaystyle\displaystyle{\hbox{\hskip
59.69753pt\vbox{\hbox{\hskip-59.69753pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
M:A$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A\vdash
N:C$}}}}\vbox{}}}\over\hbox{\hskip
45.13501pt\vbox{\vbox{}\hbox{\hskip-45.135pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\mathbf{let}\;x\leftarrow
M\;\mathbf{in}\;N:C$}}}}}}$

Figure 1. Typing Rules for $\lambda_{\textrm{b}}$

The typing rules are given in Figure 1. We require two typing judgements: one
for values and the other for computations. The judgement
$\Gamma\vdash\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.

$\displaystyle\\{(+),(-)\\}:\mathsf{Nat}\times\mathsf{Nat}\to\mathsf{Nat}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt(=):\mathsf{Nat}\times\mathsf{Nat}\to\mathsf{Unit}+\mathsf{Unit}$

$\begin{array}[]{@{}l@{\quad}@{}r@{~}c@{~}l@{}}\text{{S-App}}&(\lambda
x^{A}.\,M)V~{}&\leadsto\hfil~{}&M[V/x]\\\ \text{{S-App-
Rec}}&(\mathbf{rec}\;f^{A}\,x.\,M)V~{}&\leadsto\hfil~{}&M[(\mathbf{rec}\;f^{A}\,x.\,M)/f,V/x]\\\
\text{{S-Const}}&c~{}V~{}&\leadsto\hfil~{}&\mathbf{return}\;(\ulcorner
c\urcorner\,(V))\\\ \text{{S-Split}}&\mathbf{let}\;\langle x,y\rangle=\langle
V,W\rangle\;\mathbf{in}\;N~{}&\leadsto\hfil~{}&N[V/x,W/y]\\\ \text{{S-Case-
inl}}&\mathbf{case}\;(\mathbf{inl}\,V)^{B}\;\\{\mathbf{inl}\;x\mapsto
M;\mathbf{inr}\;y\mapsto N\\}~{}&\leadsto\hfil~{}&M[V/x]\\\ \text{{S-Case-
inr}}&\mathbf{case}\;(\mathbf{inr}\,V)^{A}\;\\{\mathbf{inl}\;x\mapsto
M;\mathbf{inr}\;y\mapsto N\\}~{}&\leadsto\hfil~{}&N[V/y]\\\
\text{{S-Let}}&\mathbf{let}\;x\leftarrow\mathbf{return}\;V\;\mathbf{in}\;N~{}&\leadsto\hfil~{}&N[V/x]\\\
\text{{S-Lift}}&\mathcal{E}[M]~{}&\leadsto\hfil~{}&\mathcal{E}[N],\hfill\text{if
}M\leadsto N\\\ \end{array}$

$\begin{array}[]{@{}l@{\quad}r@{~}c@{~}l@{}}\textrm{Evaluation
contexts}&\mathcal{E}~{}&::=\hfil~{}&[\,]\mid\mathbf{let}\;x\leftarrow\mathcal{E}\;\mathbf{in}\;N\end{array}$

Figure 2. Contextual Small-Step Operational Semantics

We give a small-step operational semantics for $\lambda_{\textrm{b}}$ with
_evaluation contexts_ in the style of Felleisen (1987). The reduction rules
are given in Figure 2. We write $M[V/x]$ for $M$ with $V$ substituted for $x$
and $\ulcorner c\urcorner$ for the usual interpretation of constant $c$ as a
meta-level function on closed values. The reduction relation $\leadsto$ is
defined on computation terms. The statement $M\leadsto 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$.

#### 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 (Moggi, 1991; Flanagan et al.,
1993). For example, the expression $f\,(h\,w)+g\,\langle\rangle$ is syntactic
sugar for:

$\begin{array}[t]{@{~}l}{}\lx@intercol\mathbf{let}\;x\leftarrow
h\,w\;\mathbf{in}\;\mathbf{let}\;y\leftarrow
f\,x\;\mathbf{in}\;\mathbf{let}\;z\leftarrow
g\,\langle\rangle\;\mathbf{in}\;y+z\end{array}$

We define sequencing of computations in the standard way.

$M;N\mathrel{:=}\mathbf{let}\;x\leftarrow M\;\mathbf{in}\;N,\quad\text{where
$x\notin FV(N)$}$

We make use of standard syntactic sugar for pattern matching. For instance, we
write

$\lambda\langle\rangle.M\mathrel{:=}\lambda
x^{\mathsf{Unit}}.M,\quad\text{where $x\notin FV(M)$}$

for suspended computations, and if the binder has a type other than
$\mathsf{Unit}$, we write:

$\lambda\\_^{A}.M\mathrel{:=}\lambda x^{A}.M,\quad\text{where $x\notin
FV(M)$}$

We use the standard encoding of booleans as a sum:

$\displaystyle\mathsf{Bool}\mathrel{:=}\mathsf{Unit}+\mathsf{Unit}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\mathsf{true}\mathrel{:=}\mathbf{inl}~{}\langle\rangle\penalty 50\hskip
20.00003pt plus 0.5fil minus
5.0pt\mathsf{false}\mathrel{:=}\mathbf{inr}~{}\langle\rangle\penalty 50\hskip
20.00003pt plus 0.5fil minus
5.0pt\mathbf{if}\;V\;\mathbf{then}\;M\;\mathbf{else}\;N\mathrel{:=}\mathbf{case}\;V\;\\{\mathbf{inl}~{}\langle\rangle\mapsto
M;\mathbf{inr}~{}\langle\rangle\mapsto N\\}$

###  3.2. Handler Calculus

We now define $\lambda_{\textrm{h}}$ as an extension of
$\lambda_{\textrm{b}}$.

$\begin{array}[]{@{}l@{\quad}r@{~}c@{~}l@{}}\textrm{Operation
symbols}&\ell\in\mathcal{L}~{}&\hfil~{}&\\\
\textrm{Signatures}&\Sigma~{}&::=\hfil~{}&\cdot\mid\\{\ell:A\to
B\\}\cup\Sigma\\\ \textrm{Handler types}&F~{}&::=\hfil~{}&C\Rightarrow D\\\
\textrm{Computations}&M,N~{}&::=\hfil~{}&\dots\mid\mathbf{do}\;\ell\;V\mid\mathbf{handle}\;M\;\mathbf{with}\;H\\\
\textrm{Handlers}&H~{}&::=\hfil~{}&\\{\mathbf{val}\;x\mapsto
M\\}\mid\\{\ell\;p\;r\mapsto N\\}\uplus H\\\ \end{array}$

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 Pretnar (2015), we assume a global signature for every program.
Computations are extended with operation invocation ($\mathbf{do}\;\ell\;V$)
and effect handling ($\mathbf{handle}\;M\;\mathbf{with}\;H$). Handlers are
constructed from one success clause $(\\{\mathbf{val}\;x\mapsto M\\})$ and one
operation clause $(\\{\ell\;p\;r\mapsto N\\})$ for each operation $\ell$ in
$\Sigma$. Following Plotkin and Pretnar (2013), 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\mathbf{let}\;x\leftarrow\mathbf{do}\;\ell\,p\;\mathbf{in}\;r\,x\\}$

Computations

T-Do $\displaystyle\displaystyle{\hbox{\hskip
57.45164pt\vbox{\hbox{\hskip-57.45163pt\hbox{\hbox{$\displaystyle\displaystyle(\ell:A\to
B)\in\Sigma$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
V:A$}}}}\vbox{}}}\over\hbox{\hskip
26.9516pt\vbox{\vbox{}\hbox{\hskip-26.9516pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\mathbf{do}\;\ell\;V:B$}}}}}}$
T-Handle $\displaystyle\displaystyle{\hbox{\hskip
59.51439pt\vbox{\hbox{\hskip-59.51437pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
M:C$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
H:C\Rightarrow D$}}}}\vbox{}}}\over\hbox{\hskip
48.87567pt\vbox{\vbox{}\hbox{\hskip-48.87566pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\mathbf{handle}\;M\;\mathbf{with}\;H:D$}}}}}}$

Handlers

T-Handler $\displaystyle\displaystyle{\hbox{\hskip
148.1373pt\vbox{\hbox{\hskip-148.13728pt\hbox{\hbox{$\displaystyle\displaystyle
H^{\mathrm{val}}=\\{\mathbf{val}\;x\mapsto M\\}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle[H^{\ell}=\\{\ell\,p\;r\mapsto
N_{\ell}\\}]_{\ell\in dom(\Sigma)}$}\hskip
18.00003pt\hbox{\hskip-108.43063pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:C\vdash
M:D$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle[\Gamma,p:A_{\ell},r:B_{\ell}\to
D\vdash N_{\ell}:D]_{(\ell:A_{\ell}\to
B_{\ell})\in\Sigma}$}}}}}}}\vbox{\hbox{\hskip-108.43063pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:C\vdash
M:D$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle[\Gamma,p:A_{\ell},r:B_{\ell}\to
D\vdash N_{\ell}:D]_{(\ell:A_{\ell}\to
B_{\ell})\in\Sigma}$}}}}\vbox{}}}}\over\hbox{\hskip
27.8075pt\vbox{\vbox{}\hbox{\hskip-27.8075pt\hbox{\hbox{$\displaystyle\displaystyle{\Gamma}\vdash{H:C\Rightarrow
D}$}}}}}}$

Figure 3. Additional Typing Rules for $\lambda_{\textrm{h}}$

The typing rules for $\lambda_{\textrm{h}}$ are those of
$\lambda_{\textrm{b}}$ (Figure 1) plus three additional rules for operations,
handling, and handlers given in Figure 3. The T-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 T-Handle rule types handler application. The T-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 $H^{\ell}$ 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 $H^{\ell}$ and $H^{\mathrm{val}}$ for
projecting success and operation clauses.

$\begin{array}[]{@{~}r@{~}c@{~}l@{~}l}{}\lx@intercol\hfil
H^{\mathrm{val}}~{}&\mathrel{:=}\hfil~{}&\\{\mathbf{val}\,x\mapsto
M\\},\hfil~{}&\quad\text{where }\\{\mathbf{val}\,x\mapsto M\\}\in H\\\
{}\lx@intercol\hfil H^{\ell}~{}&\mathrel{:=}\hfil~{}&\\{\ell\,p\,r\mapsto
M\\},\hfil~{}&\quad\text{where }\\{\ell\,p\;r\mapsto M\\}\in H\end{array}$

We extend the operational semantics to $\lambda_{\textrm{h}}$. Specifically,
we add two new reduction rules: one for handling return values and another for
handling operation invocations.

$\begin{array}[]{@{}l@{\quad}@{}r@{~}c@{~}l@{}}\text{{S-Ret}}&\mathbf{handle}\;(\mathbf{return}\;V)\;\mathbf{with}\;H~{}&\leadsto\hfil~{}&N[V/x],\qquad\text{where
}H^{\mathrm{val}}=\\{\mathbf{val}\;x\mapsto N\\}\vskip 3.0pt plus 1.0pt minus
1.0pt\\\
\text{{S-Op}}&\mathbf{handle}\;\mathcal{E}[\mathbf{do}\;\ell\,V]\;\mathbf{with}\;H~{}&\leadsto\hfil~{}&N[V/p,\;(\lambda
y.\mathbf{handle}\;\mathcal{E}[\mathbf{return}\;y]\;\mathbf{with}\;H)/r],\\\
\lx@intercol\hfil\hfill\text{where }H^{\ell}=\\{\ell\,p\;r\mapsto
N\\}\end{array}$

The first rule invokes the success clause. The second rule handles an
operation via the corresponding operation clause. If we were naïvely 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.

$\begin{array}[]{@{}l@{\quad}r@{~}c@{~}l@{}}\textrm{Handler
contexts}&\mathcal{H}~{}&::=\hfil~{}&[\,]\mid\mathbf{handle}\;\mathcal{H}\;\mathbf{with}\;H\mid\mathbf{let}\;x\leftarrow\mathcal{H}\;\mathbf{in}\;N\\\
\end{array}$

We replace the S-Lift rule with a corresponding rule for handler contexts.

$\mathcal{H}[M]~{}\leadsto~{}\mathcal{H}[N],\qquad\hfill\text{if }M\leadsto N$

The separation between pure evaluation contexts $\mathcal{E}$ and handler
contexts $\mathcal{H}$ ensures that the S-Op rule always selects the innermost
handler.

We now characterise normal forms and state the standard type soundness
property of $\lambda_{\textrm{h}}$.

###### Definition 3.1 (Computation normal forms).

A computation term $N$ is normal with respect to $\Sigma$, if
$N=\mathbf{return}\;V$ for some $V$ or $N=\mathcal{E}[\mathbf{do}\;\ell\,W]$
for some $\ell\in dom(\Sigma)$, $\mathcal{E}$, and $W$.

###### Theorem 3.2 (Type Soundness).

If $\vdash M:C$, then either there exists $\vdash N:C$ such that
$M\leadsto^{*}N$ and $N$ is normal with respect to $\Sigma$, or $M$ diverges.

###  3.3. 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
$\lambda_{\textrm{h}}$ does not include effect types. Future work includes
reconciling effect typing with our approach to expressiveness.

##  4\. Abstract Machine Semantics

Thus far we have introduced the base calculus $\lambda_{\textrm{b}}$ and its
extension with effect handlers $\lambda_{\textrm{h}}$. For each calculus we
have given a _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 _abstract machine semantics_.

###  4.1. Base Machine

We choose a _CEK_ -style abstract machine semantics (Felleisen and Friedman,
1987) for $\lambda_{\textrm{b}}$ based on that of Hillerström et al. (2020a).
The CEK machine operates on configurations which are triples of the form
$\langle M\mid\gamma\mid\sigma\rangle$. 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.

$\begin{array}[]{@{}l@{\quad}r@{~}c@{~}l@{}}\textrm{Configurations}&\mathcal{C}\in\mathsf{Conf}~{}&::=\hfil~{}&\langle
M\mid\gamma\mid\sigma\rangle\\\
\textrm{Environments}&\gamma\in\mathsf{Env}~{}&::=\hfil~{}&\emptyset\mid\gamma[x\mapsto
v]\\\ \textrm{Machine values}&v,w\in\mathsf{MVal}~{}&::=\hfil~{}&x\mid n\mid
c\mid\langle\rangle\mid\langle v,w\rangle\\\ &~{}&\mid\hfil~{}&(\gamma,\lambda
x^{A}.\,M)\mid(\gamma,\mathbf{rec}\,f^{A\to
B}\,x.\,M)\mid(\mathbf{inl}\,v)^{B}\mid(\mathbf{inr}\,w)^{A}\\\ \textrm{Pure
continuations}&\sigma\in\mathsf{PureCont}~{}&::=\hfil~{}&[]\mid(\gamma,x,N)::\sigma\\\
\end{array}$

Values consist of function closures, constants, pairs, and left or right
tagged values. We refer to continuations of the base machine as _pure_. A pure
continuation is a stack of pure continuation frames. A pure continuation frame
$(\gamma,x,N)$ closes a let-binding
$\mathbf{let}\;x\leftarrow[~{}]\;\mathbf{in}\;N$ over environment $\gamma$. We
write $[]$ for an empty pure continuation and $\phi::\sigma$ for the result of
pushing the frame $\phi$ onto $\sigma$. We use pattern matching to deconstruct
pure continuations.

Transition relation

$\begin{array}[]{@{}l@{\quad}@{}r@{~}c@{~}l@{}}\text{{M-App}}&\langle
V\;W\mid\gamma\mid\sigma\rangle~{}&\longrightarrow\hfil~{}&\langle
M\mid\gamma^{\prime}[x\mapsto\llbracket
W\rrbracket\gamma]\mid\sigma\rangle,\\\ &~{}&\hfil~{}&\quad\text{ if
}\llbracket V\rrbracket\gamma=(\gamma^{\prime},\lambda x^{A}.\,M)\\\
\text{{M-Rec}}&\langle
V\;W\mid\gamma\mid\sigma\rangle~{}&\longrightarrow\hfil~{}&\langle
M\mid\gamma^{\prime}[\begin{array}[t]{@{}l@{}}f\mapsto(\gamma^{\prime},\mathbf{rec}\,f^{A\to
B}\,x.M),\\\ x\mapsto\llbracket W\rrbracket\gamma]\mid\sigma\rangle,\\\
\end{array}\\\ &~{}&\hfil~{}&\quad\text{ if }\llbracket
V\rrbracket\gamma=(\gamma^{\prime},\mathbf{rec}\,f^{A\to B}\,x.M)\\\
\text{{M-Const}}&\langle
V~{}W\mid\gamma\mid\sigma\rangle~{}&\longrightarrow\hfil~{}&\langle\mathbf{return}\;(\ulcorner
c\urcorner\,(\llbracket W\rrbracket\gamma))\mid\gamma\mid\sigma\rangle,\\\
&~{}&\hfil~{}&\quad\text{ if }\llbracket V\rrbracket\gamma=c\\\
\text{{M-Split}}&\langle\mathbf{let}\;\langle
x,y\rangle=V\;\mathbf{in}\;N\mid\gamma\mid\sigma\rangle~{}&\longrightarrow\hfil~{}&\langle
N\mid\gamma[x\mapsto v,y\mapsto w]\mid\sigma\rangle,\\\
&~{}&\hfil~{}&\quad\text{ if }\llbracket V\rrbracket\gamma=\langle
v;w\rangle\\\
\text{{M-CaseL}}&\begin{array}[]{@{}l@{}l@{}}\langle\mathbf{case}\;V\,\\{&\mathbf{inl}\,x\mapsto
M;\\\ &\mathbf{inr}\,y\mapsto N\\}\mid\gamma\mid\sigma\rangle\\\
\end{array}~{}&\longrightarrow\hfil~{}&\langle M\mid\gamma[x\mapsto
v]\mid\sigma\rangle,\\\ &~{}&\hfil~{}&\quad\text{ if }\llbracket
V\rrbracket\gamma=\mathbf{inl}\,v\\\
\text{{M-CaseR}}&\begin{array}[]{@{}l@{}l@{}}\langle\mathbf{case}\;V\,\\{&\mathbf{inl}\,x\mapsto
M;\\\ &\mathbf{inr}\,y\mapsto N\\}\mid\gamma\mid\sigma\rangle\\\
\end{array}~{}&\longrightarrow\hfil~{}&\langle N\mid\gamma[y\mapsto
v]\mid\sigma\rangle,\\\ &~{}&\hfil~{}&\quad\text{ if }\llbracket
V\rrbracket\gamma=\mathbf{inr}\,v\\\
\text{{M-Let}}&\langle\mathbf{let}\;x\leftarrow
M\;\mathbf{in}\;N\mid\gamma\mid\sigma\rangle~{}&\longrightarrow\hfil~{}&\langle
M\mid\gamma\mid(\gamma,x,N)::\sigma\rangle\\\
\text{{M-RetCont}}&\langle\mathbf{return}\;V\mid\gamma\mid(\gamma^{\prime},x,N)::\sigma\rangle~{}&\longrightarrow\hfil~{}&\langle
N\mid\gamma^{\prime}[x\mapsto\llbracket V\rrbracket\gamma]\mid\sigma\rangle\\\
\end{array}$

Value interpretation

$\begin{array}[t]{@{}l@{}}\begin{array}[t]{@{}r@{~}c@{~}l@{}}\llbracket
x\rrbracket\gamma~{}&=\hfil~{}&\gamma(x)\\\
\llbracket\langle\rangle{}\rrbracket\gamma~{}&=\hfil~{}&\langle\rangle{}\\\
\end{array}\qquad\qquad\qquad\begin{array}[t]{@{}r@{~}c@{~}l@{}}\llbracket
n\rrbracket\gamma~{}&=\hfil~{}&n\\\ \llbracket
c\rrbracket\gamma~{}&=\hfil~{}&c\\\
\end{array}\qquad\qquad\qquad\begin{array}[t]{@{}r@{~}c@{~}l@{}}\llbracket\lambda
x^{A}.M\rrbracket\gamma~{}&=\hfil~{}&(\gamma,\lambda x^{A}.M)\\\
\llbracket\mathbf{rec}\,f^{A\to
B}\,x.M\rrbracket\gamma~{}&=\hfil~{}&(\gamma,\mathbf{rec}\,f^{A\to B}\,x.M)\\\
\end{array}\vskip 6.0pt plus 2.0pt minus 2.0pt\\\
\begin{array}[t]{@{}r@{~}c@{~}l@{}}\llbracket\langle
V,W\rangle\rrbracket\gamma~{}&=\hfil~{}&\langle\llbracket
V\rrbracket\gamma,\llbracket W\rrbracket\gamma\rangle\\\
\end{array}\qquad\qquad\qquad\begin{array}[]{@{}r@{~}c@{~}l@{}}\llbracket(\mathbf{inl}\,V)^{B}\rrbracket\gamma~{}&=\hfil~{}&(\mathbf{inl}\;\llbracket
V\rrbracket\gamma)^{B}\\\
\llbracket(\mathbf{inr}\,V)^{A}\rrbracket\gamma~{}&=\hfil~{}&(\mathbf{inr}\;\llbracket
V\rrbracket\gamma)^{A}\\\ \end{array}\end{array}$

Figure 4. Abstract Machine Semantics for $\lambda_{\textrm{b}}$

The abstract machine semantics is given in Figure 4. The transition relation
($\longrightarrow$) makes use of the value interpretation
($\llbracket-\rrbracket$) 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 ($[]$). The rules
(M-App), (M-Rec), (M-Const), (M-Split), (M-CaseL), and (M-CaseR) eliminate
values. The (M-Let) rule extends the current pure continuation with let
bindings. The (M-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 $\vdash 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
$\langle\mathbf{return}\;V\mid\gamma\mid[]\rangle$ in which case the final
return value is given by the denotation $\llbracket V\rrbracket\gamma$ of $V$
under environment $\gamma$.

#### Correctness

The base machine faithfully simulates the operational semantics for
$\lambda_{\textrm{b}}$; most transitions correspond directly to
$\beta$-reductions, but M-Let performs an administrative step to bring the
computation $M$ into evaluation position. We formally state and prove the
correspondence in Appendix A, relying on an inverse map
$\llparenthesis-\rrparenthesis$ from configurations to terms (Hillerström et
al., 2020a).

###  4.2. Handler Machine

We now enrich the $\lambda_{\textrm{b}}$ machine to a $\lambda_{\textrm{h}}$
machine. We extend the syntax as follows.

$\begin{array}[]{@{}l@{\quad}r@{~}c@{~}l@{}}\textrm{Configurations}&\mathcal{C}\in\mathsf{Conf}~{}&::=\hfil~{}&\langle
M\mid\gamma\mid\kappa\rangle\\\
\textrm{Resumptions}&\rho\in\mathsf{Res}~{}&::=\hfil~{}&(\sigma,\chi)\\\
\textrm{Continuations}&\kappa\in\mathsf{Cont}~{}&::=\hfil~{}&[]\mid\rho::\kappa\\\
\textrm{Handler closures}&\chi\in\mathsf{HClo}~{}&::=\hfil~{}&(\gamma,H)\\\
\textrm{Machine values}&v,w\in\mathsf{MVal}~{}&::=\hfil~{}&\cdots\mid\rho\\\
\end{array}$

The notion of configurations changes slightly in that the continuation
component is replaced by a generalised continuation $\kappa\in\mathsf{Cont}$
(Hillerström et al., 2020a); 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:

$\kappa_{0}\mathrel{:=}[([],(\emptyset,\\{\mathbf{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
$(\text{{M-Let}})$ and $(\text{{M-RetCont}})$ from the base machine to account
for the richer continuation structure. Figure 5 depicts the new and modified
rules. The $(\text{{M-Handle}})$ rule pushes a handler closure along with an
empty pure continuation onto the continuation stack. The
$(\text{{M-RetHandler}})$ rule transfers control to the success clause of the
current handler once the pure continuation is empty. The $(\text{{M-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
$(\text{{M-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.

Transition relation

$\begin{array}[]{@{}l@{\quad}@{}r@{~}c@{~}l@{}}\text{{M-Resume}}&\langle
V\;W\mid\gamma\mid\kappa\rangle~{}&\longrightarrow\hfil~{}&\langle\mathbf{return}\;W\mid\gamma\mid(\sigma,\chi)::\kappa\rangle,\\\
&~{}&\hfil~{}&\quad\text{ if }\llbracket V\rrbracket\gamma=(\sigma,\chi)\\\
\text{{M-Let}}&\langle\mathbf{let}\;x\leftarrow
M\;\mathbf{in}\;N\mid\gamma\mid(\sigma,\chi)::\kappa\rangle~{}&\longrightarrow\hfil~{}&\langle
M\mid\gamma\mid((\gamma,x,N)::\sigma,\chi)::\kappa\rangle\\\
\text{{M-RetCont}}&\langle\mathbf{return}\;V\mid\gamma\mid((\gamma^{\prime},x,N)::\sigma,\chi)::\kappa\rangle~{}&\longrightarrow\hfil~{}&\langle
N\mid\gamma^{\prime}[x\mapsto\llbracket
V\rrbracket\gamma]\mid(\sigma,\chi)::\kappa\rangle\\\
\text{{M-Handle}}&\langle\mathbf{handle}\;M\;\mathbf{with}\;H\mid\gamma\mid\kappa\rangle~{}&\longrightarrow\hfil~{}&\langle
M\mid\gamma\mid([],(\gamma,H))::\kappa\rangle\\\
\text{{M-RetHandler}}&\langle\mathbf{return}\;V\mid\gamma\mid([],(\gamma^{\prime},H))::\kappa\rangle~{}&\longrightarrow\hfil~{}&\langle
M\mid\gamma^{\prime}[x\mapsto\llbracket
V\rrbracket\gamma]\mid\kappa\rangle,\\\ &~{}&\hfil~{}&\quad\text{ if
}H^{\mathrm{val}}=\\{\mathbf{val}\;x\mapsto M\\}\\\ \text{{M-Handle-
Op}}&\langle\mathbf{do}\;\ell~{}V\mid\gamma\mid(\sigma,(\gamma^{\prime},H))::\kappa\rangle~{}&\longrightarrow\hfil~{}&\langle
M\mid\gamma^{\prime}[\begin{array}[t]{@{}l@{}}p\mapsto\llbracket
V\rrbracket\gamma,\\\
r\mapsto(\sigma,(\gamma^{\prime},H))]\mid\kappa\rangle,\\\ \end{array}\\\
&~{}&\hfil~{}&\quad\begin{array}[t]{@{}l@{}}\text{ if }\ell:A\to B\in\Sigma\\\
\text{ and }H^{\ell}=\\{\ell\;p\;r\mapsto M\\}\end{array}\\\ \end{array}$

Figure 5. Abstract Machine Semantics for $\lambda_{\textrm{h}}$

#### Correctness

The handler machine faithfully simulates the operational semantics of
$\lambda_{\textrm{h}}$. Extending the result for the base machine, we formally
state and prove the correspondence in Appendix B.

###  4.3. Realisability and Asymptotic Complexity

As witnessed by the work of Hillerström and Lindley (2018) 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 $\mathcal{O}(1)$ for the extension operation
$(\\_::\\_)$. The topmost pure continuation on the handler machine may also be
extended in time $\mathcal{O}(1)$, as extending it only requires reaching
under the topmost handler closure. Environments, $\gamma$, can be realised
using a map, with a time complexity of $\mathcal{O}(\log|\gamma|)$ for
extension and lookup (Okasaki, 1999).

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
$\mathcal{O}(\log|\gamma|)$. The value interpretation function
$\llbracket-\rrbracket\gamma$ is defined structurally on values. Its worst-
time complexity is exhibited by a nesting of pairs of variables
$\llbracket\langle x_{1},\dots,x_{n}\rangle\rrbracket\gamma$ which has
complexity $\mathcal{O}(n\log|\gamma|)$.

#### 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,\\_)::\\_)$
would be a $\mathcal{O}(|\sigma|)$ time operation.

#### Primitive operations on naturals

Our model assumes that arithmetic operations on arbitrary natural numbers take
$\mathcal{O}(1)$ time. This is common practice in the study of algorithms when
the main interest lies elsewhere (Cormen et al., 2009, Section 2.2). 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.

##  5\. Predicates, Decision Trees and Generic Count

We now come to the crux of the paper. In this section and the next, we prove
that $\lambda_{\textrm{h}}$ supports implementations of certain operations
with an asymptotic runtime bound that cannot be achieved in
$\lambda_{\textrm{b}}$ (Section 6). 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 $\lambda_{\textrm{h}}$, then show that no equivalent
program in $\lambda_{\textrm{b}}$ can achieve the same asymptotic efficiency.
We take _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 (Bird, 2006), the $n$-queens problem (Bell and
Stevens, 2009) 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 (Simpson, 1998; Daniels, 2016).

For simplicity, we will restrict attention to search spaces of the form
$\mathbb{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
_generic count_ problem: given a predicate $P$ on some $\mathbb{B}^{n}$,
return the _number of_ points of $\mathbb{B}^{n}$ satisfying $P$. However, we
shall explain why our results are also applicable to generic search proper.

We shall view $\mathbb{B}^{n}$ as the set of functions
${\mathbb{N}}_{n}\to\mathbb{B}$, where
${\mathbb{N}}_{n}\mathrel{:=}\\{0,\dots,n-1\\}$. In both
$\lambda_{\textrm{b}}$ and $\lambda_{\textrm{h}}$ we may represent such
functions by terms of type $\mathsf{Nat}\to\mathsf{Bool}$. We will often
informally write $\mathsf{Nat}_{n}$ in place of $\mathsf{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 $\lambda_{\textrm{b}}$ and $\lambda_{\textrm{h}}$ we
will be working with the types

$\begin{array}[t]{@{}r@{~}c@{~}l@{~}c@{~}r@{~}c@{~}l@{}}\mathsf{Point}~{}&\mathrel{:=}\hfil~{}&\mathsf{Nat}\to\mathsf{Bool}\hfil~{}&\hfil~{}&\mathsf{Point}_{n}~{}&\mathrel{:=}\hfil~{}&\mathsf{Nat}_{n}\to\mathsf{Bool}\\\
\mathsf{Predicate}~{}&\mathrel{:=}\hfil~{}&\mathsf{Point}\to\mathsf{Bool}\hfil~{}&\hfil~{}&\mathsf{Predicate}_{n}~{}&\mathrel{:=}\hfil~{}&\mathsf{Point}_{n}\to\mathsf{Bool}\end{array}$

and will be looking for programs

$\mathsf{count}_{n}:\mathsf{Predicate}_{n}\to\mathsf{Nat}$

such that for suitable terms $P$ representing semantic predicates
$\Pi:\mathbb{B}^{n}\to\mathbb{B}$, $\mathsf{count}_{n}~{}P$ finds the number
of points of $\mathbb{B}^{n}$ satisfying $\Pi$.

Before formalising these ideas more closely, let us look at some examples,
which will also illustrate the machinery of _decision trees_ that we will be
using.

###  5.1. Examples of Points, Predicates and Trees

Consider first the following terms of type $\mathsf{Point}$:

$\displaystyle\mathsf{q}_{0}\mathrel{:=}\lambda\\_.\mathsf{true}\penalty
50\hskip 20.00003pt plus 0.5fil minus 5.0pt\mathsf{q}_{1}\mathrel{:=}\lambda
i.i=0\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt\mathsf{q}_{2}\mathrel{:=}\lambda
i.\,\mathbf{if}\;i=0\;\mathbf{then}\;\mathsf{true}\;\mathbf{else}\;\mathbf{if}\;i=1\;\mathbf{then}\;\mathsf{false}\;\mathbf{else}\;\bot$

(Here $\bot$ is the diverging term
$(\mathbf{rec}\;f\,i.f\,i)\,\langle\rangle$.) Then $\mathsf{q}_{0}$ represents
$\langle{\mathsf{true},\dots,\mathsf{true}}\rangle\in\mathbb{B}^{n}$ for any
$n$; $\mathsf{q}_{1}$ represents
$\langle{\mathsf{true},\mathsf{false},\dots,\mathsf{false}}\rangle\in\mathbb{B}^{n}$
for any $n\geq 1$; and $\mathsf{q}_{2}$ represents
$\langle{\mathsf{true},\mathsf{false}}\rangle\in\mathbb{B}^{2}$.

Next some predicates. First, the following terms all represent the constant
true predicate $\mathbb{B}^{2}\to\mathbb{B}$:

$\displaystyle\mathsf{T}_{0}\mathrel{:=}\lambda q.\mathsf{true}\penalty
50\hskip 20.00003pt plus 0.5fil minus 5.0pt\mathsf{T}_{1}\mathrel{:=}\lambda
q.(q\,1;q\,0;\mathsf{true})\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt\mathsf{T}_{2}\mathrel{:=}\lambda q.(q\,0;q\,0;\mathsf{true})$

These illustrate that in the course of evaluating a predicate term $P$ at a
point $\mathsf{q}$, for each $i<n$ the value of $\mathsf{q}$ at $i$ may be
inspected zero, one or many times.

Likewise, the following all represent the ‘identity’ predicate
$\mathbb{B}^{1}\to\mathbb{B}$ (here $\&\&$ is shortcut ‘and’):

$\displaystyle\mathsf{I}_{0}\mathrel{:=}\lambda q.q\,0\penalty 50\hskip
20.00003pt plus 0.5fil minus 5.0pt\mathsf{I}_{1}\mathrel{:=}\lambda
q.\,\mathbf{if}\;q\,0\;\mathbf{then}\;\mathsf{true}\;\mathbf{else}\;\mathsf{false}\penalty
50\hskip 20.00003pt plus 0.5fil minus 5.0pt\mathsf{I}_{2}\mathrel{:=}\lambda
q.(q\,0)\,\&\&\,(q\,0)$

Slightly more interestingly, for each $n$ we have the following program which
determines whether a point contains an odd number of $\mathsf{true}$
components:

$\mathsf{Odd}_{n}\mathrel{:=}\lambda
q.\,\mathsf{fold}\otimes\mathsf{false}~{}(\mathsf{map}~{}q~{}[0,\dots,n-1])$

Here $\mathsf{fold}$ and $\mathsf{map}$ are the standard combinators on lists,
and $\otimes$ is exclusive-or. Applying $\mathsf{Odd}_{2}$ to $\mathsf{q}_{0}$
yields $\mathsf{false}$; applying it to $\mathsf{q}_{1}$ or $\mathsf{q}_{2}$
yields $\mathsf{true}$.

${\scriptstyle\mathord{!}\mathsf{true}}$

(a) $\mathsf{T}_{0}$

${\scriptstyle\mathord{?}0}$${\scriptstyle\mathord{?}0}$${\scriptstyle\mathord{!}\mathsf{true}}$${\scriptstyle\mathord{!}\mathsf{false}}$${\scriptstyle\mathord{!}\mathsf{false}}$

(b) $\mathsf{I}_{2}$

${\scriptstyle\mathord{?}0}$${\scriptstyle\mathord{?}1}$${\scriptstyle\mathord{!}\mathsf{false}}$${\scriptstyle\mathord{!}\mathsf{true}}$${\scriptstyle\mathord{?}1}$${\scriptstyle\mathord{!}\mathsf{true}}$${\scriptstyle\mathord{!}\mathsf{false}}$

(c) $\mathsf{Odd}_{2}$

Figure 6. Examples of Decision Trees

We can think of a predicate term $P$ as participating in a ‘dialogue’ with a
given point $Q:\mathsf{Point}_{n}$. The predicate may _query_ $Q$ at some
coordinate $k$; $Q$ may _respond_ with $\mathsf{true}$ or $\mathsf{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
_answer_ ($\mathsf{true}$ or $\mathsf{false}$).

The set of possible dialogues with a given term $P$ may be organised in an
obvious way into an unrooted binary _decision tree_ , in which each internal
node is labelled with a query $\mathord{?}k$ (with $k<n$), and with left and
right branches corresponding to the responses $\mathsf{true}$,
$\mathsf{false}$ respectively. Any point will thus determine a path through
the tree, and each leaf is labelled with an answer $\mathord{!}\mathsf{true}$
or $\mathord{!}\mathsf{false}$ according to whether the corresponding point or
points satisfy the predicate.

Decision trees for a sample of the above predicate terms are depicted in
Figure 6; the relevant formal definitions are given in the next subsection. In
the case of $\mathsf{I}_{2}$, one of the $\mathord{!}\mathsf{false}$ leaves
will be ‘unreachable’ if we are working in $\lambda_{\textrm{b}}$ (but
reachable in a language supporting mutable state).

We think of the edges in the tree as corresponding to portions of computation
undertaken by $P$ between queries, or before delivering the final answer. The
tree is unrooted (i.e. starts with an edge rather than a node) because in the
evaluation of $P\,Q$ there is potentially some ‘thinking’ done by $P$ even
before the first query or answer is reached. For the purpose of our runtime
analysis, we will also consider _timed_ variants of these decision trees, in
which each edge is labelled with the number of computation steps involved.

It is possible that for a given $P$ the construction of a decision tree may
hit trouble, because at some stage $P$ either goes undefined or gets stuck at
an unhandled operation. It is also possible that the decision tree is infinite
because $P$ can keep asking queries forever. However, we shall be restricting
our attention to terms representing _total_ predicates: those with finite
decision trees in which every path leads to a leaf.

In order to present our complexity results in a simple and clear form, we will
give special prominence to certain well-behaved decision trees. For
$n\in{\mathbb{N}}$, we shall say a tree is _$n$ -standard_ if it is total
(i.e. every maximal path leads to a leaf labelled with an answer) and along
any path to a leaf, each coordinate $k<n$ is queried once and only once. Thus,
an $n$-standard decision tree is a complete binary tree of depth $n+1$, with
$2^{n}-1$ internal nodes and $2^{n}$ leaves. However, there is no constraint
on the order of the queries, which indeed may vary from one path to another.
One pleasing property of this notion is that for a predicate term with an
$n$-standard decision tree, the number of points in $\mathbb{B}^{n}$
satisfying the predicate is precisely the number of $\mathord{!}\mathsf{true}$
leaves in the tree.

Of the examples we have given, the tree for $\mathsf{T}_{0}$ is 0-standard;
those for $\mathsf{I}_{0}$ and $\mathsf{I}_{1}$ are 1-standard; that for
$\mathsf{Odd}_{n}$ is $n$-standard; and the rest are not $n$-standard for any
$n$.

###  5.2. Formal Definitions

We now formalise the above notions. We will present our definitions in the
setting of $\lambda_{\textrm{h}}$, but everything can clearly be relativised
to $\lambda_{\textrm{b}}$ with no change to the meaning in the case of
$\lambda_{\textrm{b}}$ terms. For the purpose of this subsection we fix
$n\in{\mathbb{N}}$, set ${\mathbb{N}}_{n}\mathrel{:=}\\{0,\ldots,n-1\\}$, and
use $k$ to range over ${\mathbb{N}}_{n}$. We write $\mathbb{B}$ for the set of
booleans, which we shall identify with the (encoded) boolean values of
$\lambda_{\textrm{h}}$, and use $b$ to range over $\mathbb{B}$.

As suggested by the foregoing discussion, we will need to work with both
syntax and semantics. For points, the relevant definitions are as follows.

###### Definition 5.1 ($n$-points).

A closed value $Q:\mathsf{Point}$ is said to be a _syntactic $n$-point_ if:

$\forall k\in{\mathbb{N}}_{n}.\,\exists
b\in\mathbb{B}.~{}Q~{}k\leadsto^{\ast}\mathbf{return}\;b$

A _semantic $n$-point_ $\pi$ is simply a mathematical function
$\pi:{\mathbb{N}}_{n}\to\mathbb{B}$. (We shall also write
$\pi\in\mathbb{B}^{n}$.) Any syntactic $n$-point $Q$ is said to _denote_ the
semantic $n$-point $\llbracket Q\rrbracket$ given by:

$\forall k\in{\mathbb{N}}_{n},\,b\in\mathbb{B}.~{}\llbracket
Q\rrbracket(k)=b\,\Leftrightarrow\,Q~{}k\leadsto^{\ast}\mathbf{return}\;b$

Any two syntactic $n$-points $Q$ and $Q^{\prime}$ are said to be _distinct_ if
$\llbracket Q\rrbracket\neq\llbracket Q^{\prime}\rrbracket$.

By default, the unqualified term _$n$ -point_ will from now on refer to
syntactic $n$-points.

Likewise, we wish to work with predicates both syntactically and semantically.
By a _semantic $n$-predicate_ we shall mean simply a mathematical function
$\Pi:\mathbb{B}^{n}\to\mathbb{B}$. One slick way to define syntactic
$n$-predicates would be as closed terms $P:\mathsf{Predicate}$ such that for
every $n$-point $Q$, $P\,Q$ evaluates to either
$\mathbf{return}\;\mathsf{true}$ or $\mathbf{return}\;\mathsf{false}$. For our
purposes, however, we shall favour an approach to $n$-predicates via _decision
trees_ , which will yield more information on their behaviour.

We will model decision trees as certain partial functions from _addresses_ to
_labels_. An address will specify the position of a node in the tree via the
path that leads to it, while a label will represent the information present at
a node. Formally:

###### Definition 5.2 (untimed decision tree).

(i) The address set $\mathsf{Addr}$ is simply the set $\mathbb{B}^{\ast}$ of
finite lists of booleans. If $bs,bs^{\prime}\in\mathsf{Addr}$, we write
$bs\sqsubseteq bs^{\prime}$ (resp. $bs\sqsubset bs^{\prime}$) to mean that
$bs$ is a prefix (resp. proper prefix) of $bs^{\prime}$.

(ii) The label set $\mathsf{Lab}$ consists of _queries_ parameterised by a
natural number and _answers_ parameterised by a boolean:

$\mathsf{Lab}\mathrel{:=}\\{\mathord{?}k\mid
k\in{\mathbb{N}}\\}\cup\\{\mathord{!}b\mid b\in\mathbb{B}\\}$

(iii) An (untimed) decision tree is a partial function
$\tau:\mathsf{Addr}\rightharpoonup\mathsf{Lab}$ such that:

  * •

The domain of $\tau$ (written $dom(\tau)$) is prefix closed.

  * •

Answer nodes are always leaves: if $\tau(bs)=\mathord{!}b$ then
$\tau(bs^{\prime})$ is undefined whenever $bs\sqsubset bs^{\prime}$.

As our goal is to reason about the time complexity of generic count programs
and their predicates, it is also helpful to decorate decision trees with
timing data that records the number of machine steps taken for each piece of
computation performed by a predicate:

###### Definition 5.3 (timed decision tree).

A timed decision tree is a partial function
$\tau:\mathsf{Addr}\rightharpoonup\mathsf{Lab}\times{\mathbb{N}}$ such that
its first projection $bs\mapsto\tau(bs).1$ is a decision tree. We write
$\mathsf{labs}(\tau)$ for the first projection ($bs\mapsto\tau(bs).1$) and
$\mathsf{steps}(\tau)$ for the second projection ($bs\mapsto\tau(bs).2$) of a
timed decision tree.

Here we think of $\mathsf{steps}(\tau)(bs)$ as the computation time associated
with the edge whose _target_ is the node addressed by $bs$.

We now come to the method for associating a specific tree with a given term
$P$. One may think of this as a kind of denotational semantics, but here we
shall extract a tree from a term by purely operational means using our
abstract machine model. The key idea is to try applying $P$ to a distinguished
free variable $q:\mathsf{Point}$, which we think of as an ‘abstract point’.
Whenever $P$ wants to interrogate its argument at some index $i$, the
computation will get stuck at some term $q\,i$: this both flags up the
presence of a query node in the decision tree, and allows us to explore the
subsequent behaviour under both possible responses to this query.

The core of our definition is couched in terms of abstract machine
configurations. We write $\mathsf{Conf}_{q}$ for the set of $\lambda_{h}$
configurations possibly involving $q$ (but no other free variables). We write
$a\simeq b$ for Kleene equality: either both $a$ and $b$ are undefined or both
are defined and $a=b$.

It is convenient to define the timed tree and then extract the untimed one
from it:

###### Definition 5.4.

(i) Define
$\mathcal{T}:\mathsf{Conf}_{q}\to\mathsf{Addr}\rightharpoonup(\mathsf{Lab}\times{\mathbb{N}})$
to be the minimal family of partial functions satisfying the following
equations:

$\displaystyle\begin{array}[]{@{}r@{~}c@{~}l@{\qquad}l@{}}\mathcal{T}(\langle\mathbf{return}\;W\mid\gamma\mid[]\rangle)\,[]~{}&~{}={}\hfil~{}&(!b,0),&\text{if
}\llbracket W\rrbracket\gamma=b\vskip 3.0pt plus 1.0pt minus 1.0pt\\\
\mathcal{T}(\langle
z\,V\mid\gamma\mid\kappa\rangle)\,[]~{}&~{}={}\hfil~{}&(?\llbracket
V\rrbracket\gamma,0),&\text{if }\gamma(z)=q\vskip 3.0pt plus 1.0pt minus
1.0pt\\\ \mathcal{T}(\langle
z\,V\mid\gamma\mid\kappa\rangle)\,(b::bs)~{}&~{}\simeq{}\hfil~{}&\mathcal{T}(\langle\mathbf{return}\;b\mid\gamma\mid\kappa\rangle)\,bs,&\text{if
}\gamma(z)=q\vskip 3.0pt plus 1.0pt minus 1.0pt\\\ \mathcal{T}(\langle
M\mid\gamma\mid\kappa\rangle)\,bs~{}&~{}\simeq{}\hfil~{}&\mathsf{inc}\,(\mathcal{T}(\langle
M^{\prime}\mid\gamma^{\prime}\mid\kappa^{\prime}\rangle)\,bs),&\text{if
}\langle M\mid\gamma\mid\kappa\rangle\longrightarrow\langle
M^{\prime}\mid\gamma^{\prime}\mid\kappa^{\prime}\rangle\end{array}$

Here $\mathsf{inc}(\ell,s)=(\ell,s+1)$, and in all of the above equations
$\gamma(q)=\gamma^{\prime}(q)=q$. Clearly $\mathcal{T}(\mathcal{C})$ is a
timed decision tree for any $\mathcal{C}\in\mathsf{Conf}_{q}$.

(ii) The timed decision tree of a computation term is obtained by placing it
in the initial configuration: $\mathcal{T}(M)\mathrel{:=}\mathcal{T}(\langle
M,\emptyset[q\mapsto q],\kappa_{0}\rangle)$.

(iii) The timed decision tree of a closed value $P:\mathsf{Predicate}$ is
$\mathcal{T}(P\,q)$. Since $q$ plays the role of a dummy argument, we will
usually omit it and write $\mathcal{T}(P)$ for $\mathcal{T}(P\,q)$.

(iv) The untimed decision tree $\mathcal{U}(P)$ is obtained from
$\mathcal{T}(P)$ via first projection:
$\mathcal{U}(P)=\mathsf{labs}(\mathcal{T}(P))$.

If the execution of a configuration $\mathcal{C}$ runs forever or gets stuck
at an unhandled operation, then $\mathcal{T}(\mathcal{C})(bs)$ will be
undefined for all $bs$. Although this is admitted by our definition of
decision tree, we wish to exclude such behaviours for the terms we accept as
valid predicates. Specifically, we frame the following definition:

###### Definition 5.5.

A decision tree $\tau$ is an _$n$ -predicate tree_ if it satisfies the
following:

  * •

For every query $\mathord{?}k$ appearing in $\tau$, we have
$k\in{\mathbb{N}}_{n}$.

  * •

Every query node has both children present:

$\forall
bs\in\mathsf{Addr},\,k\in{\mathbb{N}}_{n},\,b\in\mathbb{B}.~{}\tau(bs)=\mathord{?}k\Rightarrow
bs\mathbin{+\\!\\!+}[b]\in dom(\tau)$

  * •

All paths in $\tau$ are finite (so every maximal path terminates in an answer
node).

A closed term $P:\mathsf{Predicate}$ is a _(syntactic) $n$-predicate_ if
$\mathcal{U}(P)$ is an $n$-predicate tree.

If $\tau$ is an $n$-predicate tree, clearly any semantic $n$-point $\pi$ gives
rise to a path $b_{0}b_{1}\dots$ through $\tau$, given inductively by:

$\forall j.~{}\mbox{if~{}}\tau(b_{0}\dots
b_{j-1})=\mathord{?}k_{j}\mbox{~{}then~{}}b_{j}=\pi(k_{j})$

This path will terminate at some answer node $b_{0}b_{1}\dots b_{r-1}$ of
$\tau$, and we may write $\tau\bullet\pi\in\mathbb{B}$ for the answer at this
leaf.

###### Proposition 5.6.

If $P$ is an $n$-predicate and $Q$ is an $n$-point, then
$P\,Q\leadsto^{\ast}\mathbf{return}\;b$ where
$b=\mathcal{U}(P)\bullet\llbracket Q\rrbracket$.

###### Proof.

By interleaving the computation for the relevant path through $\mathcal{U}(P)$
with computations for queries to $Q$, and appealing to the correspondence
between the small-step reduction and abstract machine semantics. We omit the
routine details. ∎

It is thus natural to define the _denotation_ of an $n$-predicate $P$ to be
the semantic $n$-predicate $\llbracket P\rrbracket$ given by $\llbracket
P\rrbracket(\pi)=\mathcal{U}(P)\bullet\pi$.

As mentioned earlier, we shall also be interested in a more constrained class
of trees and predicates:

###### Definition 5.7 ($n$-standard trees and predicates).

An $n$-predicate tree $\tau$ is said to be $n$-standard if the following hold:

  * •

The domain of $\tau$ is precisely $\mathsf{Addr}_{n}$, the set of bit vectors
of length $\leq n$.

  * •

There are no repeated queries along any path in $\tau$:

$\forall bs,bs^{\prime}\in dom(\tau),\,k\in{\mathbb{N}}_{n}.~{}bs\sqsubseteq
bs^{\prime}\wedge\tau(bs)=\tau(bs^{\prime})=\mathord{?}k\Rightarrow
bs=bs^{\prime}$

A timed decision tree $\tau$ is $n$-standard if its underlying untimed
decision tree ($bs\mapsto\tau(bs).1$) is so. An $n$-predicate $P$ is
$n$-standard if $\mathcal{T}(P)$ is $n$-standard.

Clearly, in an $n$-standard tree, each of the $n$ queries
$\mathord{?}0,\dots,\mathord{?}(n-1)$ appears exactly once on the path to any
leaf, and there are $2^{n}$ leaves, all of them answer nodes.

###  5.3. Specification of Counting Programs

We can now specify what it means for a program
$K:\mathsf{Predicate}\to\mathsf{Nat}$ to implement counting.

###### Definition 5.8.

(i) The _count_ of a semantic $n$-predicate $\Pi$, written $\sharp\Pi$, is
simply the number of semantic $n$-points $\pi\in\mathbb{B}^{n}$ for which
$\Pi(\pi)=\mathsf{true}$.

(ii) If $P$ is any $n$-predicate, we say that $K$ _correctly counts_ $P$ if
$K\,P\leadsto^{\ast}\mathbf{return}\;m$, where $m=\sharp\llbracket
P\rrbracket$.

This definition gives us the flexibility to talk about counting programs that
operate on various classes of predicates, allowing us to state our results in
their strongest natural form. On the positive side, we shall shortly see that
there is a single ‘efficient’ program in $\lambda_{\textrm{h}}$ that correctly
counts all $n$-standard $\lambda_{h}$ predicates for every $n$; in Section 7.1
we improve this to one that correctly counts _all_ $n$-predicates of
$\lambda_{h}$. On the negative side, we shall show that an $n$-indexed family
of counting programs written in $\lambda_{\textrm{b}}$, even if only required
to work correctly on $n$-standard $\lambda_{b}$ predicates, can never compete
with our $\lambda_{\textrm{h}}$ program for asymptotic efficiency even in the
most favourable cases.

###  5.4. Efficient Generic Count with Effects

We now present the simplest version of our effectful implementation of
counting: one that works on $n$-standard predicates.

Our program uses a variation of the handler for nondeterministic computation
that we gave in Section 2. The main idea is to implement points as
‘nondeterministic computations’ using the $\mathsf{Branch}$ operation such
that the handler may respond to every query twice, by invoking the provided
resumption with $\mathsf{true}$ and subsequently $\mathsf{false}$. The key
insight is that the resumption restarts computation at the invocation site of
$\mathsf{Branch}$, which means that prior computation need not be repeated. In
other words, the resumption ensures that common portions of computations prior
to any query are shared between both branches.

We assert that $\mathsf{Branch}:\mathsf{Unit}\to\mathsf{Bool}\in\Sigma$ is a
distinguished operation that may not be handled in the definition of any input
predicate (it has to be forwarded according to the default convention). The
algorithm is then as follows.

$\begin{array}[t]{@{}l@{}}\mathsf{effcount}:((\mathsf{Nat}\to\mathsf{Bool})\to\mathsf{Bool})\to\mathsf{Nat}\\\
\mathsf{effcount}\,pred\mathrel{:=}\begin{array}[t]{@{}l@{}}\mathbf{handle}\;pred\,(\lambda\\_.\mathbf{do}\;\mathsf{Branch}\;\langle\rangle)\;\mathbf{with}\\\
\quad\begin{array}[t]{@{}l@{\hspace{1.5ex}}c@{\hspace{1.5ex}}l@{}}\mathbf{val}\,x\hfil\hskip
5.81247pt&\mapsto\hfil\hskip
5.81247pt&\mathbf{if}\;x\;\mathbf{then}\;\mathbf{return}\;1\;\mathbf{else}\;\mathbf{return}\;0\\\
\mathsf{Branch}\,\langle\rangle\,\,r\hfil\hskip 5.81247pt&\mapsto\hfil\hskip
5.81247pt&\begin{array}[t]{@{}l}\mathbf{let}\;x_{\mathsf{true}}\leftarrow
r\,\mathsf{true}\;\mathbf{in}\\\ \mathbf{let}\;x_{\mathsf{false}}\leftarrow
r\,\mathsf{false}\;\mathbf{in}\;x_{\mathsf{true}}+x_{\mathsf{false}}\\\
\end{array}\end{array}\\\ \end{array}\end{array}$

The handler applies predicate $pred$ to a single ‘generic point’ defined using
$\mathsf{Branch}$. The boolean return value is interpreted as a single
solution, whilst $\mathsf{Branch}$ is interpreted by alternately supplying
$\mathsf{true}$ and $\mathsf{false}$ to the resumption and summing the
results. The sharing enabled by the use of the resumption is exactly the
‘magic’ we need to make it possible to implement generic count more
efficiently in $\lambda_{\textrm{h}}$ than in $\lambda_{\textrm{b}}$. A
curious feature of $\mathsf{effcount}$ is that it works for all $n$-standard
predicates without having to know the value of $n$. This is because the
generic point $(\lambda\\_.\mathbf{do}\;\mathsf{Branch}~{}\langle\rangle)$
informally serves as a ‘superposition’ of all possible points.

We may now articulate the crucial correctness and efficiency properties of
$\mathsf{effcount}$.

###### Theorem 5.9.

The following hold for any $n\in{\mathbb{N}}$ and any $n$-standard predicate
$P$ of $\lambda_{\textrm{h}}$:

  1. (1)

$\mathsf{effcount}$ correctly counts $P$.

  2. (2)

The number of machine steps required to evaluate $\mathsf{effcount}~{}P$ is

$\left(\displaystyle\sum_{bs\in\mathsf{Addr}_{n}}\mathsf{steps}(\mathcal{T}(P))(bs)\right)~{}+~{}\mathcal{O}(2^{n})$

###### Proof Outline.

Suppose $bs\in\mathsf{Addr}_{n}$, with $|bs|=j$. From the construction of
$\mathcal{T}(P)$, one may easily read off a configuration $\mathcal{C}_{bs}$
whose execution is expected to compute the count for the subtree below node
$bs$, and we can explicitly describe the form $\mathcal{C}_{bs}$ will have. We
write $\mathsf{Hyp}(bs)$ for the claim that $\mathcal{C}_{bs}$ correctly
counts this subtree, and does so within the following number of steps:

$\left(\displaystyle\sum_{bs^{\prime}\in\mathsf{Addr}_{n},\;bs^{\prime}\sqsupset
bs}\mathsf{steps}(\mathcal{T}(P))(bs^{\prime})\right)~{}+~{}9*(2^{n-j}-1)+2*2^{n-j}$

The $9*(2^{n-j}-1)$ expression is the number of machine steps contributed by
the $\mathsf{Branch}$-case inside the handler, whilst the $2*2^{n-j}$
expression is the number of machine steps contributed by the
$\mathbf{val}$-case. We prove $\mathsf{Hyp}(bs)$ by a laborious but routine
downwards induction on the length of $bs$. The proof combines counting of
explicit machine steps with ‘oracular’ appeals to the assumed behaviour of $P$
as modelled by $\mathcal{T}(P)$. Once $\mathsf{Hyp}([])$ is established, both
halves of the theorem follow easily. Full details are given in Appendix C. ∎

The above formula can clearly be simplified for certain reasonable classes of
predicates. For instance, suppose we fix some constant $c\in{\mathbb{N}}$, and
let $\mathcal{P}_{n,c}$ be the class of all $n$-standard predicates $P$ for
which all the edge times $\mathsf{steps}(\mathcal{T}(P))(bs)$ are bounded by
$c$. (Clearly, many reasonable predicates will belong to $\mathcal{P}_{n,c}$
for some modest value of $c$.) Since the number of sequences $bs$ in question
is less than $2^{n+1}$, we may read off from the above formula that for
predicates in $\mathcal{P}_{n,c}$, the runtime of $\mathsf{effcount}$ is
$\mathcal{O}(c2^{n})$.

Alternatively, should we wish to use the finer-grained cost model that assigns
an $O(\log|\gamma|)$ runtime to each abstract machine step (see Section 4.3),
we may note that any environment $\gamma$ arising in the computation contains
at most $n$ entries introduced by the let-bindings in $\mathsf{effcount}$, and
(if $P\in\mathcal{P}_{n,c}$) at most $\mathcal{O}(cn)$ entries introduced by
$P$. Thus, the time for each step in the computation remains $\mathcal{O}(\log
c+\log n)$, and the total runtime for $\mathsf{effcount}$ is
$\mathcal{O}(c2^{n}(\log c+\log n))$.

One might also ask about the execution time for an implementation of
$\lambda_{\textrm{h}}$ that performs genuine copying of continuations, as in
systems such as MLton (2020). As MLton copies the entire continuation (stack),
whose size is $\mathcal{O}(n)$, at each of the $2^{n}$ branches, continuation
copying alone takes time $\mathcal{O}(n2^{n})$ and the effectful
implementation offers no performance benefit (Table 2). More refined
implementations (Farvardin and Reppy, 2020; Flatt and Dybvig, 2020) that are
able to take advantage of delimited control operators or sharing in copies of
the stack can bring the complexity of continuation copying back down to
$\mathcal{O}(2^{n})$.

Finally, one might consider another dimension of cost, namely the space used
by $\mathsf{effcount}$. Consider a class $\mathcal{Q}_{n,c,d}$ of $n$-standard
predicates $P$ for which the edge times in $\mathcal{T}(P)$ never exceed $c$
and the sizes of pure continuations never exceed $d$. If we consider any
$P\in\mathcal{Q}_{n,c,d}$ then the total number of environment entries is
bounded by $cn$, taking up space $\mathcal{O}(cn(\log cn))$. We must also
account for the pure continuations. There are $n$ of these, each taking at
most $d$ space. Thus the total space is $\mathcal{O}(n(d+c(\log c+\log n)))$.

##  6\. Pure Generic Count: A Lower Bound

We have shown that there is an implementation of generic count in
$\lambda_{\textrm{h}}$ with a runtime bound of $\mathcal{O}(2^{n})$ for
certain well-behaved predicates. We now prove that no implementation in
$\lambda_{\textrm{b}}$ can match this: in fact, we establish a lower bound of
$\Omega(n2^{n})$ for the runtime of any counting program on _any_ $n$-standard
predicate. This mathematically rigorous characterisation of the efficiency gap
between languages with and without first-class control constructs is the
central contribution of the paper.

One might ask at this point whether the claimed lower bound could not be
obviated by means of some known continuation passing style (CPS) or monadic
transform of effect handlers (Hillerström et al., 2017; Leijen, 2017). This
can indeed be done, but only by dint of changing the type of our predicates
$P$ — which, as noted in the introduction, would defeat the purpose of our
enquiry. Our intention is precisely to investigate the relative power of
various languages for manipulating predicates that are given to us in a
certain way which we do not have the luxury of choosing.

To get a feel for the issues that our proof must address, let us consider how
one might construct a counting program in $\lambda_{\textrm{b}}$. The naïve
approach, of course, would be simply to apply the given predicate $P$ to all
$2^{n}$ possible $n$-points in turn, keeping a count of those on which $P$
yields true. It is a routine exercise to implement this approach in
$\lambda_{\textrm{b}}$, yielding (parametrically in $n$) a program

$\mathsf{naivecount}_{n}~{}:((\mathsf{Nat}_{n}\to\mathsf{Bool})\to\mathsf{Bool})\to\mathsf{Nat}$

Since the evaluation of an $n$-standard predicate on an individual $n$-point
must clearly take time $\Omega(n)$, we have that the evaluation of
$\mathsf{naivecount}_{n}$ on any $n$-standard predicate $P$ must take time
$\Omega(n2^{n})$. If $P$ is not $n$-standard, the $\Omega(n)$ lower bound need
not apply, but we may still say that the evaluation of
$\mathsf{naivecount}_{n}$ on _any_ predicate $P$ (at level $n$) must take time
$\Omega(2^{n})$.

One might at first suppose that these properties are inevitable for any
implementation of generic count within $\lambda_{\textrm{b}}$, or indeed any
purely functional language: surely, the only way to learn something about the
behaviour of $P$ on every possible $n$-point is to apply $P$ to each of these
points in turn? It turns out, however, that the $\Omega(2^{n})$ lower bound
can sometimes be circumvented by implementations that cleverly exploit
_nesting_ of calls to $P$. The germ of the idea may be illustrated within
$\lambda_{\textrm{b}}$ itself. Suppose that we first construct some program

$\mathsf{bestshot}_{n}~{}:((\mathsf{Nat}_{n}\to\mathsf{Bool})\to\mathsf{Bool})\to(\mathsf{Nat}_{n}\to\mathsf{Bool})$

which, given a predicate $P$, returns some $n$-point $Q$ such that $P~{}Q$
evaluates to true, if such a point exists, and any point at all if no such
point exists. (In other words, $\mathsf{bestshot}_{n}$ embodies Hilbert’s
choice operator $\varepsilon$ on predicates.) It is once again routine to
construct such a program by naïve means; and we may moreover assume that for
any $P$, the evaluation of $\mathsf{bestshot}_{n}\;P$ takes only constant
time, all the real work being deferred until the argument of type
$\mathsf{Nat}_{n}$ is supplied.

Now consider the following program:

$\mathsf{lazycount}_{n}\mathrel{:=}\lambda
pred.\;\mathbf{if}\;pred~{}(\mathsf{bestshot}_{n}\;pred)\;\mathbf{then}\;\mathsf{naivecount}_{n}\;pred\;\mathbf{else}\;\mathbf{return}\;0$

Here the term $pred~{}(\mathsf{bestshot}_{n}~{}pred)$ serves to test whether
there exists an $n$-point satisfying $pred$: if there is not, our count
program may return $0$ straightaway. It is thus clear that
$\mathsf{lazycount}_{n}$ is a correct implementation of generic count, and
also that if $pred$ is the predicate $\lambda q.\mathsf{false}$ then
$\mathsf{lazycount}_{n}\;pred$ returns $0$ within $O(1)$ time, thus violating
the $\Omega(2^{n})$ lower bound suggested above.

This might seem like a footling point, as $\mathsf{lazycount}_{n}$ offers this
efficiency gain _only_ on (certain implementations of) the constantly false
predicate. However, it turns out that by a recursive application of this
nesting trick, we may arrive at a generic count program that spectacularly
defies the $\Omega(2^{n})$ lower bound for an interesting class of
(non-$n$-standard) predicates, and indeed proves quite viable for counting
solutions to ‘$n$-queens’ and similar problems. We shall refer to this program
as $\mathsf{BergerCount}$, as it is modelled largely on Berger’s PCF
implementation of the so-called _fan functional_ (Berger, 1990; Longley and
Normann, 2015). This program is of interest in its own right and is briefly
presented in Appendix D. It actually requires a mild extension of
$\lambda_{\textrm{b}}$ with a ‘memoisation’ primitive to achieve the effect of
call-by-need evaluation; but such a language can still be seen as purely
‘functional’ in the same sense as Haskell.

In the meantime, however, the moral is that the use of _nesting_ can lead to
surprising phenomena which sometimes defy intuition (Escardó (2007) gives some
striking further examples). What we now wish to show is that for _$n$
-standard_ predicates, the naïve lower bound of $\Omega(n2^{n})$ cannot in
fact be circumvented. The example of $\mathsf{BergerCount}$ both highlights
the need for a rigorous proof of this and tells us that such a proof will need
to pay particular attention to the possibility of nesting.

We now proceed to the proof itself. We here present the argument in the basic
setting of $\lambda_{\textrm{b}}$; later we will see how a more delicate
argument applies to languages with mutable state (Section 7.3).

As a first step, we note that where lower bounds are concerned, it will
suffice to work with the small-step operational semantics of
$\lambda_{\textrm{b}}$ rather than the more elaborate abstract machine model
employed in Section 4.1. This is because, as observed in Section 4.1, there is
a tight correspondence between these two execution models such that for the
evaluation of any closed term, the number of abstract machine steps is always
at least the number of small-step reductions. Thus, if we are able to show
that the number of small-step reductions for any generic program program in
$\lambda_{\textrm{b}}$ on any $n$-standard predicate is $\Omega(n2^{n})$, this
will establish the desired lower bound on the runtime.

Let us suppose, then, that $K$ is a program of $\lambda_{\textrm{b}}$ that
correctly counts all $n$-standard predicates of $\lambda_{\textrm{b}}$ for
some specific $n$. We now establish a key lemma, which vindicates the naïve
intuition that if $P$ is $n$-standard, the only way for $K$ to discover the
correct value for $\sharp\llbracket P\rrbracket$ is to perform $2^{n}$
separate applications $P\;Q$ (allowing for the possibility that these
applications need not be performed ‘in turn’ but might be nested in some
complex way).

###### Lemma 6.1 (No shortcuts).

Suppose $K$ correctly counts all $n$-standard predicates of
$\lambda_{\textrm{b}}$. If $P$ is an $n$-standard predicate, then $K$ applies
$P$ to at least $2^{n}$ distinct $n$-points. More formally, for any of the
$2^{n}$ possible semantic $n$-points $\pi:{\mathbb{N}}_{n}\to\mathbb{B}$,
there is a term $\mathcal{E}[P~{}Q]$ appearing in the small-step reduction of
$K~{}P$ such that $Q$ is an $n$-point and $\llbracket Q\rrbracket=\pi$.

###### Proof.

Suppose for a contradiction that $\pi$ is some semantic $n$-point such that no
application $P~{}Q$ with $\llbracket Q\rrbracket=\pi$ ever arises in the
course of computing $K~{}P$. Let $\tau$ be the untimed decision tree for $P$.
Let $l$ be the maximal path through $\tau$ associated with $\pi$: that is, the
one we construct by responding to each query $\mathord{?}k$ with $\pi(k)$.
Then $l$ is a leaf node such that $\tau(l)=\mathord{!}(\tau\bullet\pi)$. We
now let $\tau^{\prime}$ be the tree obtained from $\tau$ by simply negating
this answer value at $l$.

It is a simple matter to construct a $\lambda_{\textrm{b}}$ $n$-standard
predicate $P^{\prime}$ whose decision tree is $\tau^{\prime}$. This may be
done just by mirroring the structure of $\tau^{\prime}$ by nested
$\mathbf{if}$ statements; we omit the easy details.

Since the numbers of true-leaves in $\tau$ and $\tau^{\prime}$ differ by 1, it
is clear that if $K$ indeed correctly counts all $n$-standard predicates, then
the values returned by $K~{}P$ and $K~{}P^{\prime}$ will have an absolute
difference of 1. On the other hand, we shall argue that if the computation of
$K~{}P$ never actually ‘visits’ the leaf $l$ in question, then $K$ will be
unable to detect any difference between $P$ and $P^{\prime}$.

The situation is reminiscent of Milner’s _context lemma_ (Milner, 1977), which
(loosely) says that essentially the only way to observe a difference between
two programs is to apply them to some argument on which they differ.
Traditional proofs of the context lemma reason by induction on length of
reduction sequences, and our present proof is closely modelled on these.

We shall make frequent use of term contexts $M[-]$ with a hole of type
$\mathsf{Predicate}$ (which may appear zero, one or more times in $M$) in
order to highlight particular occurrences of $P$ within a term. The following
definition enables us to talk about computations that avoid the critical point
$\pi$:

###### Definition 6.2 (Safe terms).

If $M[-]$ is such a context of ground type, let us say $M[-]$ is _safe_ if

  * •

$M[P]$ is closed, and $M[P]\leadsto^{\ast}\mathbf{return}\;W$ for some closed
ground type value $W$;

  * •

For any term $\mathcal{E}[P~{}Q]$ appearing in the reduction of $M[P]$, where
the applicand $P$ in $P~{}Q$ is a residual of one of the abstracted
occurrences in $M[P]$, we have that $\llbracket Q\rrbracket\neq\pi$.

We may express this as ‘$M[P]$ is safe’ when it is clear which occurrences of
$P$ we intend to abstract.

For example, our current hypotheses imply that $K~{}P$ is safe (formally,
$K^{\prime}[-]\mathrel{:=}K\;-$ is safe).

We may now prove the following:

###### Lemma 6.3.

(i) Suppose $Q[-]:\mathsf{Point}$ and $k:\mathsf{Nat}$ are values such that
$Q[P]~{}k$ is safe, and suppose $Q[P]~{}k\leadsto^{m}\mathbf{return}\;b$ where
$m\in{\mathbb{N}}$. Then also
$Q[P^{\prime}]~{}k\leadsto^{\ast}\mathbf{return}\;b$.

(ii) Suppose $P~{}Q[P]$ is safe and $P~{}Q[P]\leadsto^{m}\mathbf{return}\;b$.
Then also $P^{\prime}~{}Q[P^{\prime}]\leadsto^{\ast}\mathbf{return}\;b$.

We prove these claims by simultaneous induction on the computation length $m$.
Both claims are vacuous when $m=0$ as neither $Q[P]~{}k$ nor $P~{}Q[P]$ is a
$\mathbf{return}$ term. We therefore assume $m>0$ where both claims hold for
all $m^{\prime}<m$.

(i) Let $p:\mathsf{Predicate}$ be a distinguished free variable, and consider
the behaviour of $Q[p]~{}k$. If this reduces to a value $\mathbf{return}\,W$,
then also $Q[P]~{}k\leadsto^{\ast}\mathbf{return}\,W$, whence $W=b$ and also
$Q[P^{\prime}]~{}k\leadsto\mathbf{return}\;b$ as required. Otherwise, the
reduction of $Q[p]~{}k$ will get stuck at some term
$M_{0}=\mathcal{E}_{0}[p~{}Q_{0}[p],p]$. Here the first hole in
$\mathcal{E}_{0}[-,-]$ is in the evaluation position, and the second hole
abstracts all remaining occurrences of $p$ within $M_{0}$. We may also assume
that $Q_{0}[-]$ abstracts all occurrences of $p$ in $Q_{0}[p]$.

Correspondingly, the reduction of $Q[P]~{}k$ will reach
$\mathcal{E}_{0}[P~{}Q_{0}[P],P]$ and then proceed with the embedded reduction
of $P~{}Q_{0}[P]$. Note that $P~{}Q_{0}[P]$ will be safe because $Q[P]~{}k$
is. So let us suppose that
$P~{}Q_{0}[P]\leadsto^{\ast}\mathbf{return}\;b_{0}$, whence
$Q[P]~{}k\leadsto^{\ast}\mathcal{E}_{0}[\mathbf{return}\;b_{0},P]$.

We may now investigate the subsequent reduction behaviour of $Q[P]~{}k$ by
considering the reduction of $\mathcal{E}_{0}[\mathbf{return}\;b_{0},p]$. Once
again, this may reduce to a value $\mathbf{return}\;W$, in which case $W=b$
and our computation is complete. Otherwise, the reduction of
$\mathcal{E}_{0}[\mathbf{return}\;b_{0},p]$ will get stuck at some
$M_{1}=\mathcal{E}_{1}[p~{}Q_{1}[p],p]$, and we may again proceed as above.

By continuing in this way, we may analyse the reduction of $Q[P]~{}k$ as
follows.

$\displaystyle\begin{array}[t]{@{}r@{~}c@{~}l@{}}Q[P]~{}k~{}&\leadsto^{\ast}\hfil~{}&\mathcal{E}_{0}[P~{}Q_{0}[P],P]~{}\leadsto^{\ast}~{}\mathcal{E}_{0}[\mathbf{return}\;b_{0},P]~{}\leadsto^{\ast}~{}\mathcal{E}_{1}[P~{}Q_{1}[P],P]~{}\leadsto^{\ast}~{}\mathcal{E}_{1}[\mathbf{return}\;b_{1},P]\\\
~{}&\leadsto^{\ast}\hfil~{}&\dots~{}\leadsto^{\ast}~{}\mathcal{E}_{r-1}[P~{}Q_{r-1}[P],P]~{}\leadsto^{\ast}~{}\mathcal{E}_{r-1}[\mathbf{return}\;b_{r-1},P]~{}\leadsto~{}\mathbf{return}\;b\end{array}$

Here the terms $P~{}Q_{j}[P]$ will be safe, and the reductions
$P~{}Q_{j}[P]\leadsto^{\ast}\mathbf{return}\;b_{j}$ each have length $<m$. We
may therefore apply part (ii) of the induction hypothesis and conclude that
also $P^{\prime}~{}Q_{j}[P^{\prime}]\leadsto^{\ast}\mathbf{return}\;b_{j}$.
Furthermore, the remaining segments of the above computation are all obtained
as instantiations of ‘generic’ reduction sequences involving $p$, so these
segments will remain valid if $p$ is instantiated to $P^{\prime}$.
Reassembling everything, we have a valid reduction sequence:

$\displaystyle\begin{array}[t]{@{}r@{~}c@{~}l@{}}Q[P^{\prime}]~{}k~{}&\leadsto^{\ast}\hfil~{}&\mathcal{E}_{0}[P^{\prime}~{}Q_{0}[P^{\prime}],P^{\prime}]~{}\leadsto^{\ast}~{}\mathcal{E}_{0}[\mathbf{return}\;b_{0},P^{\prime}]~{}\leadsto^{\ast}~{}\mathcal{E}_{1}[P^{\prime}~{}Q_{1}[P^{\prime}],P^{\prime}]~{}\leadsto^{\ast}~{}\mathcal{E}_{1}[\mathbf{return}\;b_{1},P^{\prime}]\\\
~{}&\leadsto^{\ast}\hfil~{}&\dots~{}\leadsto^{\ast}~{}\mathcal{E}_{r-1}[P^{\prime}~{}Q_{r-1}[P^{\prime}],P^{\prime}]~{}\leadsto^{\ast}~{}\mathcal{E}_{r-1}[\mathbf{return}\;b_{r-1},P^{\prime}]~{}\leadsto~{}\mathbf{return}\;b\end{array}$

This establishes the induction step for part (i).

(ii) We may apply a similar analysis to the computation of $P~{}Q[P]$ to
detect the places where $Q[P]$ is applied to an argument. We do this by
considering the reduction behaviour of $P~{}q$, where $q:\mathsf{Point}$ is
the distinguished variable that featured in Definition 5.4. In this way we may
analyse the computation of $P~{}Q[P]$ as:

$\displaystyle\begin{array}[t]{@{}r@{~}c@{~}l@{}}P~{}Q[P]~{}&~{}\leadsto^{\ast}{}\hfil~{}&\mathcal{E}_{0}[Q[P]~{}k_{0},Q[P]]~{}\leadsto^{\ast}~{}\mathcal{E}_{0}[\mathbf{return}\;b_{0},Q[P]]~{}\leadsto^{\ast}~{}\mathcal{E}_{1}[Q[P]~{}k_{1},Q[P]]~{}\leadsto^{\ast}{}\dots\\\
~{}&~{}\leadsto^{\ast}{}\hfil~{}&\mathcal{E}_{r-1}[Q[P]~{}k_{r-1},Q[P]]~{}\leadsto^{\ast}~{}\mathcal{E}_{r-1}[\mathbf{return}\;b_{r-1},Q[P]]~{}\leadsto~{}\mathbf{return}\;b\end{array}$

where for each $j$, the first hole in $\mathcal{E}_{j}[-,-]$ is in evaluation
position, the term $Q[P]~{}k_{j}$ is safe, the reduction
$Q[P]~{}k_{j}\leadsto^{\ast}\mathbf{return}\;b_{j}$ has length $<m$, and the
remaining portions of computation are instantiations of generic reductions
involving $q$. By part (i) of the induction hypothesis we may conclude that
also $Q[P^{\prime}]~{}k_{j}\leadsto^{\ast}\mathbf{return}\;b_{j}$ for each
$j$, and for the remaining segments of computation we may instantiate $q$ to
$Q[P^{\prime}]$. We thus obtain a computation exhibiting that
$P~{}Q[P^{\prime}]\leadsto^{\ast}\mathbf{return}\;b$.

It remains to show that the applicand $P$ may be replaced by $P^{\prime}$ here
without affecting the result. The idea here is that the booleans
$b_{0},\dots,b_{r-1}$ trace out a path through the decision tree for $P$; but
since $P~{}Q[P]$ is safe, we have that $\llbracket Q[P]\rrbracket\neq\pi$, and
so this path does _not_ lead to the critical leaf $l$. We now have everything
we need to establish that
$P^{\prime}~{}Q[P^{\prime}]\leadsto^{\ast}\mathbf{return}\;b$ as required.

More formally, in view of the correspondence between small-step reduction and
abstract machine semantics, we may readily correlate the above computation of
$P~{}Q[P]$ with an exploration of the path $bs=b_{0}\dots b_{r-1}$ in
$\tau=\mathcal{U}(P)$, leading to a leaf with label $\mathord{!}b$. Since $P$
is $n$-standard, this correlation shows that $r=n$, that for each $j$ we have
$\tau(b_{0}\ldots b_{j-1})=\mathord{?}k_{j}$, and that
$\\{k_{0},\ldots,k_{r-1}\\}=\\{0,\dots,n-1\\}$. Furthermore, we have already
ascertained that the values of $Q[P]$ and $Q[P^{\prime}]$ at $k_{j}$ are both
$b_{j}$, whence $\llbracket Q[P]\rrbracket=\llbracket
Q[P^{\prime}]\rrbracket=\pi^{\prime}$ where $\pi^{\prime}(k_{j})=b_{j}$ for
all $j$. But $P~{}Q[P]$ is safe, so in particular $\pi^{\prime}=\llbracket
Q[P]\rrbracket\neq\pi$. We therefore also have $\tau^{\prime}(b_{0}\dots
b_{j-1})=\mathord{?}k_{j}$ for each $j\leq r$ and $\tau^{\prime}(b_{0}\dots
b_{r-1})=b$. Since $\tau^{\prime}=\mathcal{U}(P^{\prime})$ and $\llbracket
Q[P^{\prime}]\rrbracket=\pi^{\prime}$, we may conclude by Proposition 5.6 that
$P^{\prime}~{}Q[P^{\prime}]\leadsto^{\ast}\mathbf{return}\;b$. This completes
the proof of Lemma 6.3.

To finish off the proof of Lemma 6.1, we apply the same analysis one last time
to the reduction of $K~{}P$ itself. This will have the form

$\displaystyle\begin{array}[t]{@{}r@{~}c@{~}l@{}}K~{}P~{}&~{}\leadsto^{\ast}{}\hfil~{}&\mathcal{E}_{0}[P~{}Q_{0}[P],P]~{}\leadsto^{\ast}\mathcal{E}_{0}[\mathbf{return}\;b_{0},P]~{}\leadsto^{\ast}{}\dots\\\
~{}&~{}\leadsto^{\ast}{}\hfil~{}&\mathcal{E}_{r-1}[P~{}Q_{r-1}[P],P]~{}\leadsto^{\ast}\mathcal{E}_{r-1}[\mathbf{return}\;b_{r-1},P]~{}\leadsto^{\ast}~{}\mathbf{return}\;c\end{array}$

where, by hypothesis, each $P~{}Q_{j}[P]$ is safe. Using Lemma 6.3 we may
replace each subcomputation
$P~{}Q_{j}[P]\leadsto^{\ast}\mathbf{return}\;b_{j}$ with
$P^{\prime}~{}Q_{j}[P^{\prime}]\leadsto^{\ast}\mathbf{return}\;b_{j}$, and so
construct a computation exhibiting that
$K~{}P^{\prime}\leadsto^{\ast}\mathbf{return}\;c$.

This gives our contradiction, as the values of $K~{}P$ and $K~{}P^{\prime}$
are supposed to differ by 1. ∎

###### Corollary 6.4.

Suppose $K$ and $P$ are as in Lemma 6.1. For any semantic $n$-point $\pi$ and
any natural number $k<n$, the reduction sequence for $K~{}P$ contains a term
$\mathcal{F}[Q~{}k]$, where $\mathcal{F}$ is an evaluation context and
$\llbracket Q\rrbracket=\pi$.

###### Proof.

Suppose $\pi\in\mathbb{B}^{n}$. By Lemma 6.1, the computation of $K~{}P$
contains some $\mathcal{E}[P~{}Q]$ where $\llbracket Q\rrbracket=\pi$, and the
above analysis of the computation of $P~{}Q$ shows that it contains a term
$\mathcal{E}^{\prime}[Q~{}k]$ for each $k<n$. The corollary follows, taking
$\mathcal{F}[-]\mathrel{:=}\mathcal{E}[\mathcal{E}^{\prime}[-]]$. ∎

This gives our desired lower bound. Since our $n$-points $Q$ are values, it is
clearly impossible that
$\mathcal{F}[Q~{}k]=\mathcal{F}^{\prime}[Q^{\prime}~{}k^{\prime}]$ (where
$\mathcal{F},\mathcal{F}^{\prime}$ are evaluation contexts) unless
$Q=Q^{\prime}$ and $k=k^{\prime}$. We may therefore read off $\pi$ from
$\mathcal{F}[Q~{}k]$ as $\llbracket Q\rrbracket$. There are thus at least
$n2^{n}$ distinct terms in the reduction sequence for $K~{}P$, so the
reduction has length $\geq n2^{n}$. We have thus proved:

###### Theorem 6.5.

If $K$ is a $\lambda_{\textrm{b}}$ program that correctly counts all
$n$-standard $\lambda_{\textrm{b}}$ predicates, and $P$ is any $n$-standard
$\lambda_{\textrm{b}}$ predicate, then the evaluation of $K~{}P$ must take
time $\Omega(n2^{n})$. ∎

Although we shall not go into details, it is not too hard to apply our proof
strategy with minor adjustments to certain richer languages: for instance, an
extension of $\lambda_{\textrm{b}}$ with exceptions, or one containing the
memoisation primitive required for $\mathsf{BergerCount}$ (Appendix D). A
deeper adaptation is required for languages with state: we will return to this
in Section 7.

It is worth noting where the above argument breaks down if applied to
$\lambda_{\textrm{h}}$. In $\lambda_{\textrm{b}}$, in the course of computing
$K~{}P$, every $Q$ to which $P$ is applied will be a self-contained closed
term denoting some specific point $\pi$. This is intuitively why we may only
learn about one point at a time. In $\lambda_{\textrm{h}}$, this is not the
case, because of the presence of operation symbols. For instance, our
$\mathsf{effcount}$ program from Section 5.4 will apply $P$ to the ‘generic
point’ $\lambda\\_.\mathbf{do}\;\mathsf{Branch}~{}\langle\rangle$. Thus, for
example, in our treatment of Lemma 6.3(i), it need no longer be the case that
the reduction of $Q[p]~{}k$ either yields a value or gets stuck at some
$\mathcal{E}_{0}[p~{}Q_{0}[p],p]$: a third possibility is that it gets stuck
at some invocation of $\ell$, so that control will then pass to the effect
handler.

##  7\. Extensions and Variations

Our complexity result is robust in that it continues to hold in more general
settings. We outline here how it generalises: beyond $n$-standard predicates,
from generic count to generic search, and from pure $\lambda_{\textrm{b}}$ to
stateful $\lambda_{\textrm{s}}$.

###  7.1. Beyond $n$-Standard Predicates

The $n$-standard restriction on predicates serves to make the efficiency
phenomenon stand out as clearly as possible. However, we can relax the
restriction by tweaking $\mathsf{effcount}$ to handle repeated queries and
missing queries. The trade off is that the analysis of $\mathsf{effcount}$
becomes more involved. The key to relaxing the $n$-standard restriction is the
use of state to keep track of which queries have been computed. We can give
stateful implementations of $\mathsf{effcount}$ without changing its type
signature by using _parameter-passing_ (Kammar et al., 2013; Pretnar, 2015) to
internalise state within a handler. Parameter-passing abstracts every handler
clause such that the current state is supplied before the evaluation of a
clause continues and the state is threaded through resumptions: a resumption
becomes a two-argument curried function $r:B\to S\to D$, where the first
argument of type $B$ is the return type of the operation and the second
argument is the updated state of type $S$.

#### Repeated queries

We can generalise $\mathsf{effcount}$ to handle repeated queries by memoising
previous answers. First, we generalise the type of $\mathsf{Branch}$ such that
it carries an index of a query.

$\mathsf{Branch}:\mathsf{Nat}\to\mathsf{Bool}$

We assume a family of natural number to boolean maps, $\mathsf{Map}_{n}$ with
the following interface.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\mathsf{empty}_{n}~{}&:\hfil~{}&\mathsf{Map}_{n}\\\
\mathsf{add}_{n}~{}&:\hfil~{}&(\mathsf{Nat}_{n}\times\mathsf{Bool})\to\mathsf{Map}_{n}\to\mathsf{Map}_{n}\\\
\mathsf{lookup}_{n}~{}&:\hfil~{}&\mathsf{Nat}_{n}\to\mathsf{Map}_{n}\to(\mathsf{Unit}+\mathsf{Bool})\\\
\end{array}$

Invoking $\mathsf{lookup}~{}i~{}map$ returns $\mathbf{inl}~{}\langle\rangle$
if $i$ is not present in $map$, and $\mathbf{inr}~{}ans$ if $i$ is associated
by $map$ with the value $ans:\mathsf{Bool}$. Allowing ourselves a few extra
constant-time arithmetic operations, we can realise suitable maps in
$\lambda_{\textrm{b}}$ such that the time complexity of $\mathsf{add}_{n}$ and
$\mathsf{lookup}_{n}$ is $\mathcal{O}(\log n)$ (Okasaki, 1999). We can then
use parameter-passing to support repeated queries as follows.

$\begin{array}[t]{@{}l@{}}\mathsf{effcount}^{\prime}_{n}:((\mathsf{Nat}_{n}\to\mathsf{Bool})\to\mathsf{Bool})\to\mathsf{Nat}\\\
\mathsf{effcount}^{\prime}_{n}\,pred\mathrel{:=}\begin{array}[t]{@{}l@{}}\mathbf{let}\;h\leftarrow\mathbf{handle}\;pred\,(\lambda
i.\mathbf{do}\;\mathsf{Branch}~{}i)\;\mathbf{with}\\\
\quad\begin{array}[t]{@{}l@{\hspace{1.5ex}}c@{\hspace{1.5ex}}l@{}}\mathbf{val}\,x\hfil\hskip
5.81247pt&\mapsto\hfil\hskip 5.81247pt&\lambda
s.\mathbf{if}\;x\;\mathbf{then}\;1\;\mathbf{else}\;0\\\
\mathsf{Branch}\,i\,\,r\hfil\hskip 5.81247pt&\mapsto\hfil\hskip
5.81247pt&\begin{array}[t]{@{}l}\lambda
s.\begin{array}[t]{@{}l}\mathbf{case}\;\mathsf{lookup}_{n}~{}i~{}s\;\\{\\\
\quad\begin{array}[t]{@{~}l@{~}c@{~}l}{}\lx@intercol\mathbf{inl}\,\langle\rangle\hfil~{}&\mapsto\hfil~{}&\begin{array}[t]{@{}l}\mathbf{let}\;x_{\mathsf{true}}\leftarrow
r~{}\mathsf{true}~{}(\mathsf{add}_{n}~{}\langle
i,\mathsf{true}\rangle~{}s)\;\mathbf{in}\\\
\mathbf{let}\;x_{\mathsf{false}}\leftarrow
r~{}\mathsf{false}~{}(\mathsf{add}_{n}~{}\langle
i,\mathsf{false}\rangle~{}s)\;\mathbf{in}\\\
(x_{\mathsf{true}}+x_{\mathsf{false}});\\\ \end{array}\\\
{}\lx@intercol\mathbf{inr}\,x\hfil~{}&\mapsto\hfil~{}&r~{}x~{}s\;\\}\\\
\end{array}\\\ \end{array}\\\ \end{array}\\\ \end{array}\\\
\mathbf{in}\;h~{}\mathsf{empty}_{n}\\\ \end{array}\\\ \end{array}$

The state parameter $s$ memoises query results, thus avoiding double-counting
and enabling $\mathsf{effcount}^{\prime}_{n}$ to work correctly for predicates
performing the same query multiple times.

#### Missing queries

Similarly, we can use parameter-passing to support missing queries.

$\begin{array}[t]{@{}l@{}}\mathsf{effcount}^{\prime\prime}_{n}:((\mathsf{Nat}_{n}\to\mathsf{Bool})\to\mathsf{Bool})\to\mathsf{Nat}\\\
\mathsf{effcount}^{\prime\prime}_{n}\,pred\mathrel{:=}\begin{array}[t]{@{}l@{}}\mathbf{let}\;h\leftarrow\begin{array}[t]{@{}l@{}}\mathbf{handle}\;pred\,(\lambda
i.\mathbf{do}\;\mathsf{Branch}~{}\langle\rangle)\;\mathbf{with}\\\
\quad\begin{array}[t]{@{}l@{\hspace{1.5ex}}c@{\hspace{1.5ex}}l@{}}\mathbf{val}~{}x\hfil\hskip
5.81247pt&\mapsto\hfil\hskip 5.81247pt&\lambda
d.\begin{array}[t]{@{}l}\mathbf{let}\;result\leftarrow\mathbf{if}\;x\;\mathbf{then}\;1\;\mathbf{else}\;0\;\mathbf{in}\;result\times
2^{n-d}\\\ \end{array}\\\ \mathsf{Branch}~{}\langle\rangle~{}r\hfil\hskip
5.81247pt&\mapsto\hfil\hskip 5.81247pt&\lambda
d.\begin{array}[t]{@{}l}\mathbf{let}\;x_{\mathsf{true}}\leftarrow
r~{}\mathsf{true}~{}(d+1)\;\mathbf{in}\\\
\mathbf{let}\;x_{\mathsf{false}}\leftarrow
r~{}\mathsf{false}~{}(d+1)\;\mathbf{in}\\\
(x_{\mathsf{true}}+x_{\mathsf{false}})\end{array}\end{array}\\\ \end{array}\\\
\mathbf{in}\;h~{}0\\\ \end{array}\\\ \end{array}$

The parameter $d$ tracks the depth and the returned result is scaled by
$2^{n-d}$ accounting for the unexplored part of the current subtree. This
enables $\mathsf{effcount}^{\prime\prime}_{n}$ to operate correctly on
predicates that inspect $n$ points at most once. We leave it as an exercise
for the reader to combine $\mathsf{effcount}^{\prime}_{n}$ and
$\mathsf{effcount}^{\prime\prime}_{n}$ in order to handle both repeated
queries and missing queries.

###  7.2. From Generic Count to Generic Search

We can generalise the problem of generic counting to generic searching. The
main operational difference is that a generic search procedure must
materialise a list of solutions, thus its type is

$\mathsf{search}_{n}:((\mathsf{Nat}_{n}\to\mathsf{Bool})\to\mathsf{Bool})\to\mathsf{List}_{\mathsf{Nat}_{n}\to\mathsf{Bool}}$

where $\mathsf{List}_{A}$ is the type of cons-lists whose elements have type
$A$. We modify $\mathsf{effcount}$ to return a list of solutions rather than
the number of solutions by lifting each result into a singleton list and using
list concatenation instead of addition to combine partial results
$xs_{\mathsf{true}}$ and $xs_{\mathsf{false}}$ as follows.

$\begin{array}[t]{@{}l@{}}\mathsf{effsearch}_{n}:((\mathsf{Nat}_{n}\to\mathsf{Bool})\to\mathsf{Bool})\to\mathsf{List}_{\mathsf{Nat}_{n}\to\mathsf{Bool}}\\\
\mathsf{effsearch}_{n}\,pred\mathrel{:=}\begin{array}[t]{@{}l@{}}\mathbf{let}\;f\leftarrow\begin{array}[t]{@{}l@{}}\mathbf{handle}\;pred\,(\lambda
i.\mathbf{do}\;\mathsf{Branch}~{}i)\;\mathbf{with}\\\
\begin{array}[t]{@{}l@{\hspace{1.5ex}}c@{\hspace{1.5ex}}l@{}}\mathbf{val}\,x\hfil\hskip
5.81247pt&\mapsto\hfil\hskip 5.81247pt&\lambda
q.\mathbf{if}\,x\;\mathbf{then}\;\mathsf{singleton}~{}q\;\mathbf{else}\;\mathsf{nil}\\\
\mathsf{Branch}\,i\,\,r\hfil\hskip 5.81247pt&\mapsto\hfil\hskip
5.81247pt&\begin{array}[t]{@{}l}\lambda
q.\begin{array}[t]{@{}l}\mathbf{let}\;xs_{\mathsf{true}}\leftarrow
r~{}\mathsf{true}~{}(\lambda
j.\mathbf{if}\;i=j\;\mathbf{then}\;\mathsf{true}\;\mathbf{else}\;q~{}j)\;\mathbf{in}\\\
\mathbf{let}\;xs_{\mathsf{false}}\leftarrow r~{}\mathsf{false}~{}(\lambda
j.\mathbf{if}\;i=j\;\mathbf{then}\;\mathsf{false}\;\mathbf{else}\;q~{}j)\;\mathbf{in}\\\
\mathsf{concat}~{}\langle xs_{\mathsf{true}},xs_{\mathsf{false}}\rangle\\\
\end{array}\\\ \end{array}\\\ \end{array}\\\ \end{array}\\\
\mathbf{in}\;\mathsf{toConsList}~{}(f~{}(\lambda j.\bot))\end{array}\\\
\end{array}$

The $\mathsf{Branch}$ operation is now parameterised by an index $i$. The
handler is now parameterised by the current path as a point $q$, which is
output at a leaf iff it is in the predicate. A little care is required to
ensure that $\mathsf{effsearch}_{n}$ has runtime $\mathcal{O}(2^{n})$; naïve
use of cons-list concatenation would result in $\mathcal{O}(n2^{n})$ runtime,
as cons-list concatenation is linear in its first operand. In place of cons-
lists we use Hughes lists (Hughes, 1986), which admit constant time
concatenation:
$\mathsf{HList}_{A}\mathrel{:=}\mathsf{List}_{A}\to\mathsf{List}_{A}$. The
empty Hughes list $\mathsf{nil}:\mathsf{HList}_{A}$ is defined as the identity
function: $\mathsf{nil}\mathrel{:=}\lambda xs.xs$.

$\begin{array}[]{@{}l@{\qquad}l@{\qquad}l}\mathsf{singleton}_{A}:A\to\mathsf{HList}_{A}&\mathsf{concat}_{A}:\mathsf{HList}_{A}\times\mathsf{HList}_{A}\to\mathsf{HList}_{A}&\mathsf{toConsList}_{A}:\mathsf{HList}\to\mathsf{List}_{A}\\\
\mathsf{singleton}_{A}~{}x\mathrel{:=}\lambda
xs.x::xs&\mathsf{concat}_{A}~{}f\,g\mathrel{:=}\lambda
xs.g~{}(f~{}xs)&\mathsf{toConsList}_{A}~{}f\mathrel{:=}f~{}[]\end{array}$

We use the function $\mathsf{toConsList}$ to convert the final Hughes list to
a standard cons-list at the end; this conversion has linear time complexity
(it just conses all of the elements of the list together).

###  7.3. From Pure $\lambda_{\textrm{b}}$ to Stateful $\lambda_{\textrm{s}}$

Mutable state is a staple ingredient of many practical programming languages.
We now outline how our main lower bound result can be extended to a language
with state. We will not give full details, but merely point out the respects
in which our earlier treatment needs to be modified.

We have in mind an extension $\lambda_{\textrm{s}}$ of $\lambda_{\textrm{b}}$
with ML-style reference cells: we extend our grammar for types with a
reference type ($\ref{~}A$), and that for computation terms with forms for
creating references ($\mathbf{letref}\;x=V\;\mathbf{in}\;N$), dereferencing
($!x$), and destructive update ($x:=V$), with the familiar typing rules. We
also add a new kind of value, namely _locations_ $l^{A}$, of type $\ref{~}A$.
We adopt a basic Scott-Strachey (1971) model of store: a location is a natural
number decorated with a type, and the execution of a stateful program
allocates locations in the order $0,1,2,\ldots$, assigning types to them as it
does so. A _store_ $s$ is a type-respecting mapping from some set of locations
$\\{0,\ldots,l-1\\}$ to values. For the purposes of small-step operational
semantics, a _configuration_ will be a triple $(M,l,s)$, where $M$ is a
computation, $l$ is a ‘location counter’, and $s$ is a store with domain
$\\{0,\ldots,l-1\\}$. A reduction relation $\leadsto$ on configurations is
defined in a familiar way (again we omit the details).

Certain aspects of our setup require care in the presence of state. For
instance, there is in general no unique way to assign an (untimed) decision
tree to a closed value $P:\mathsf{Predicate}_{n}$, since the behaviour of $P$
on a value $q:\mathsf{Point}_{n}$ may depend both on the initial state when
$P$ is invoked, and on the ways in which the associated computations
$q~{}V\leadsto^{\ast}\mathbf{return}\;W$ modify the state. In this situation,
there is not even a clear specification for what an $n$-count program ought to
do.

The simplest way to circumvent this difficulty is to restrict attention to
predicates $P$ _within the sublanguage $\lambda_{\textrm{b}}$_. For such
predicates, the notions of decision tree, counting and $n$-standardness are
unproblematic. Our result will establish a runtime lower bound of
$\Omega(n2^{n})$ for programs $K\in\lambda_{\textrm{s}}$ that correctly count
predicates $P$ of this kind. On the other hand, since $K$ itself may be
stateful, we cannot exclude the possibility that $K~{}P$ will apply $P$ to a
term $Q$ that is itself stateful. Such a $Q$ will no longer unambiguously
denote a semantic point $\pi$, hence the proof of Section 6 must be adapted.

To adapt our proof to the setting of $\lambda_{\textrm{s}}$, some more
machinery is needed. If $K$ is an $n$-count program and $P$ an $n$-standard
predicate, we expect that the evaluation of $K~{}P$ will feature terms
$\mathcal{E}[P~{}Q]$ which are then reduced to some
$\mathcal{E}[\mathbf{return}\;b]$, via a reduction sequence which, modulo
$\mathcal{E}[-]$, has the following form:

$P\,Q\leadsto^{\ast}\mathcal{E}_{0}[Q~{}k_{0}]\leadsto^{\ast}\mathcal{E}_{0}[\mathbf{return}\,b_{0}]\leadsto^{\ast}\cdots\leadsto^{\ast}\mathcal{E}_{n-1}[Q~{}k_{n-1}]\leadsto^{\ast}\mathcal{E}_{n-1}[\mathbf{return}\,b_{n-1}]\leadsto^{\ast}\mathbf{return}\;b$

(For notational clarity, we suppress mention of the location and store
components here.) Informally we think of this as a dialogue in which control
passes back and forth between $P$ and $Q$. We shall refer to the portions
$\mathcal{E}_{j}[Q~{}k_{j}]\leadsto^{\ast}\mathcal{E}_{j}[\mathbf{return}\;b_{j}]$
of the above reduction as _$Q$ -sections_, and to the remaining portions
(including the first and the last) as _$P$ -sections_. We refer to the
totality of these $P$-sections and $Q$-sections as the _thread_ arising from
the given occurrence of the application $P\,Q$. An important point to note is
that since $Q$ may contain other occurrences of $P$, it is quite possible for
the $Q$-sections above to contain further threads corresponding to other
applications $P~{}Q^{\prime}$.

Since $P$ is $n$-standard, we know that each thread will consist of $n+1$
$P$-sections separated by $n$ $Q$-sections. Indeed, it is clear that this
computation traces the path $b_{0}\ldots b_{n-1}$ through the decision tree
for $P$, with $k_{0},\ldots,k_{n-1}$ the corresponding internal node labels.
We may now, ‘with hindsight’, construe this as a semantic point
$\pi:{\mathbb{N}}_{n}\to\mathbb{B}$ (where $\pi(k_{j})=b_{j}$ for each $j$),
and call it the semantic point _associated with_ (the thread arising from) the
application occurrence $P~{}p$.

The following lemma now serves as a surrogate for Lemma 6.1:

###### Lemma 7.1.

Let $P$ be an $n$-standard predicate. For any semantic point
$\pi\in\mathbb{B}^{n}$, the evaluation of $K~{}P$ involves an application
occurrence $P~{}Q$ with which $\pi$ is associated.

The proof of this lemma is not too different from that of Lemma 6.1: if $\pi$
were a point with no associated thread, there would be an unvisited leaf in
the decision tree, and we could manufacture an $n$-standard predicate
$P^{\prime}$ whose tree differed from that of $P$ only at this leaf. We can
then show, by induction on length of reductions, that any portion of the
evaluation of $K~{}P$ can be suitably mimicked with $P$ replaced by
$P^{\prime}$. Naturally, this idea now needs to be formulated at the level of
_configurations_ rather than plain terms: in the course of reducing
$(K~{}P,0,[])$, we may encounter configurations $(M,l,s)$ in which residual
occurrences of $P$ have found their way into $s$ as well as $M$, so in order
to replace $P$ by $P^{\prime}$ we must abstract on all these occurrences via
an evident notion of _configuration context_. With this adjustment, however,
the argument of Lemma 6.1 goes through.

A further argument is then needed to show that any two threads are indeed
‘disjoint’ as regards their $P$-sections, so that there must be at least
$n2^{n}$ steps in the overall reduction sequence.

Table 1. SML/NJ: Runtime Relative to Effectful Implementation | Queens | Integration
---|---|---
| First solution | All solutions | Id | Squaring | Logistic
_Parameter_ | $20$ | $24$ | $28$ | $8$ | $10$ | $12$ | $20$ | $14$ | $17$ | $20$ | $1$ | $2$ | $3$ | $4$ | $5$
Naïve | $-$ | $-$ | $-$ | $\\!\\!217.74$ | $-$ | $-$ | $\\!\\!12.89$ | $\\!\\!45.04$ | $\\!\\!57.80$ | $\\!\\!69.86$ | $-$ | $-$ | $-$ | $-$ | $-$
Berger | $11.24$ | $15.70$ | $-$ | $2.06$ | $2.86$ | $3.64$ | $5.18$ | $\\!\\!20.62$ | $\\!\\!22.37$ | $\\!\\!23.46$ | $22.51$ | $28.97$ | $30.14$ | $29.30$ | $27.94$
Pruned | $2.13$ | $2.54$ | $2.91$ | $1.04$ | $1.24$ | $1.39$ | $2.07$ | $3.78$ | $4.05$ | $4.24$ | $4.10$ | $5.44$ | $6.42$ | $7.26$ | $7.94$
Bespoke | $0.12$ | $0.12$ | $0.12$ | $0.13$ | $0.13$ | $0.12$ |
Table 2. MLton: Runtime Relative to Effectful Implementation | Queens | Integration
---|---|---
| First solution | All solutions | Id | Squaring | Logistic
_Parameter_ | $20$ | $24$ | $28$ | $8$ | $10$ | $12$ | $20$ | $14$ | $17$ | $20$ | $1$ | $2$ | $3$ | $4$ | $5$
Naïve | $-$ | $-$ | $-$ | $17.31$ | $-$ | $-$ | $1.45$ | $4.51$ | $5.13$ | $5.82$ | $-$ | $-$ | $-$ | $-$ | $-$
Berger | $0.52$ | $0.66$ | $-$ | $0.19$ | $0.22$ | $0.20$ | $0.43$ | $2.02$ | $1.95$ | $1.92$ | $2.17$ | $3.59$ | $4.24$ | $4.34$ | $4.28$
Pruned | $0.11$ | $0.11$ | $0.13$ | $0.10$ | $0.10$ | $0.08$ | $0.14$ | $0.39$ | $0.35$ | $0.35$ | $0.39$ | $0.63$ | $0.86$ | $1.03$ | $1.21$
Bespoke | $0.005$ | $0.004$ | $0.004$ | $0.01$ | $0.009$ | $0.006$ |

##  8\. Experiments

The theoretical efficiency gap between realisations of $\lambda_{\textrm{b}}$
and $\lambda_{\textrm{h}}$ manifests in practice. We observe it empirically on
instantiations of $n$-queens and exact real number integration, which can be
cast as generic search. Table 1 shows the speedup of using an effectful
implementation of generic search over various pure implementations. We discuss
the benchmarks and results in further detail below.

#### Methodology

We evaluated an effectful implementation of generic search against three
“pure” implementations which are realisable in $\lambda_{\textrm{b}}$ extended
with mutable state:

  * •

Naïve: a simple, and rather naïve, functional implementation;

  * •

Pruned: a generic search procedure with space pruning based on Longley’s
technique (Longley, 1999) (uses local state);

  * •

Berger: a lazy pure functional generic search procedure based on Berger’s
algorithm.

Each benchmark was run 11 times. The reported figure is the median runtime
ratio between the particular implementation and the baseline effectful
implementation. Benchmarks that failed to terminate within a threshold (1
minute for single solution, 8 minutes for enumerations), are reported as $-$.
The experiments were conducted in SML/NJ (2020) v110.97 64-bit with factory
settings on an Intel Xeon CPU E5-1620 v2 @ 3.70GHz powered workstation running
Ubuntu 16.04. The effectful implementation uses an encoding of delimited
control akin to effect handlers based on top of SML/NJ’s call/cc. The complete
source code for the benchmarks is available at:

https://github.com/dhil/effects-for-efficiency-code

#### Queens

We phrase the $n$-queens problem as a generic search problem. As a control we
include a bespoke implementation hand-optimised for the problem. We perform
two experiments: finding the first solution for $n\in\\{20,24,28\\}$ and
enumerating all solutions for $n\in\\{8,10,12\\}$. The speedup over the naïve
implementation is dramatic, but less so over the Berger procedure. The pruned
procedure is more competitive, but still slower than the baseline.
Unsurprisingly, the baseline is slower than the bespoke implementation.

#### Exact Real Integration

The integration benchmarks are adapted from Simpson (1998). We integrate three
different functions with varying precision in the interval $[0,1]$. For the
identity function (Id) at precision $20$ the speedup relative to Berger is
$5.18\times$. For the squaring function the speedups are larger at higher
precisions: at precision $14$ the speedup is $3.78\times$ over the pruned
integrator, whilst it is $4.24\times$ at precision $20$. The speedups are more
extreme against the naïve and Berger integrators. We also integrate the
logistic map $x\mapsto 1-2x^{2}$ at a fixed precision of $15$. We make the
function harder to compute by iterating it up to $5$ times. Between the pruned
and effectful integrator the speedup ratio increases as the function becomes
harder to compute.

#### MLton

SML/NJ is compiled into CPS, thus providing a particularly efficient
implementation of call/cc. MLton (2020), a whole program compiler for SML,
implements call/cc by copying the stack. We repeated our experiments using
MLton 20180207. Table 2 shows the results. The effectful implementation
performs much worse under MLton than SML/NJ, being surpassed in nearly every
case by the pruned search procedure and in some cases by the Berger search
procedure. Table 3 summarises the runtime of MLton relative to SML/NJ. Berger,
Pruned, and Bespoke run between 1 and 3 times as fast with MLton compared to
SML/NJ. However, the effectful implementation runs between 2 and 14 times as
fast with SML/NJ compared with MLton.

Table 3. MLton: Runtime Relative to SML/NJ | Queens | Integration
---|---|---
| First solution | All solutions | Id | Squaring | Logistic
_Parameter_ | $20$ | $24$ | $28$ | $8$ | $10$ | $12$ | $20$ | $14$ | $17$ | $20$ | $1$ | $2$ | $3$ | $4$ | $5$
Naïve | $-$ | $-$ | $-$ | $0.49$ | $-$ | $-$ | $0.55$ | $0.35$ | $0.35$ | $0.35$ | $-$ | $-$ | $-$ | $-$ | $-$
Berger | $0.62$ | $0.64$ | $-$ | $0.73$ | $0.65$ | $0.68$ | $0.41$ | $0.35$ | $0.34$ | $0.34$ | $0.37$ | $0.37$ | $0.37$ | $0.37$ | $0.37$
Pruned | $0.70$ | $0.68$ | $0.71$ | $0.74$ | $0.70$ | $0.71$ | $0.34$ | $0.36$ | $0.35$ | $0.35$ | $0.36$ | $0.35$ | $0.35$ | $0.35$ | $0.36$
Effectful | $12.87$ | $13.99$ | $14.90$ | $8.00$ | $8.60$ | $12.19$ | $4.93$ | $3.53$ | $3.95$ | $4.20$ | $3.80$ | $3.00$ | $2.62$ | $2.46$ | $2.37$
Bespoke | $0.56$ | $0.56$ | $0.56$ | $0.69$ | $0.63$ | $0.59$ |

##  9\. Conclusions and Future Work

We presented a PCF-inspired language $\lambda_{\textrm{b}}$ and its extension
with effect handlers $\lambda_{\textrm{h}}$. We proved that
$\lambda_{\textrm{h}}$ supports an asymptotically more efficient
implementation of generic search than any possible implementation in
$\lambda_{\textrm{b}}$. We observed its effect in practice on several
benchmarks. We also proved that our $\Omega(n2^{n})$ lower bound applies to a
language $\lambda_{\textrm{s}}$ which extends $\lambda_{\textrm{b}}$ with
state.

Our positive result for $\lambda_{\textrm{h}}$ extends to other control
operators by appeal to existing results on interdefinability of handlers and
other control operators (Forster et al., 2019; Piróg et al., 2019). The result
no longer applies directly if we add an effect type system to
$\lambda_{\textrm{h}}$, as the implementation of the counting program would
require a change of type for predicates to reflect the ability to perform
effectful operations. In future we plan to investigate how to account for
effect type systems.

We have verified that our $\Omega(n2^{n})$ lower bound also applies to a
language $\lambda_{\textrm{e}}$ with (Benton-Kennedy style (Benton and
Kennedy, 2001)) _exceptions_ and handlers. The lower bound also applies to the
combined language $\lambda_{\textrm{se}}$ with both state and exceptions —
this seems to bring us close to the expressive power of real languages such as
Standard ML, Java, and Python, strongly suggesting that the speedup we have
discussed is unattainable in these languages.

In future work, we hope to establish the more general result that our
$\Omega(n2^{n})$ applies to a language with _affine effect handlers_ (handlers
which invoke the resumption $r$ at most once). This would not only subsume our
present results (since state and exceptions are examples of affine effects),
but would also apply e.g. to a richer language with _coroutines_. However, it
appears that our present methods do not immediately adapt to this more general
situation, as our arguments depend at various points on an orderly nesting of
subcomputations which coroutining would break.

One might object that the efficiency gap we have analysed is of merely
theoretical interest, since an $\Omega(2^{n})$ runtime is already
‘infeasible’. We claim, however, that what we have presented is an example of
a much more pervasive phenomenon, and our generic count example serves merely
as a convenient way to bring this phenomenon into sharp formal focus. Suppose,
for example, that our programming task was not to count all solutions to $P$,
but to find just one of them. It is informally clear that for many kinds of
predicates this would in practice be a feasible task, and also that we could
still gain our factor $n$ speedup here by working in a language with first-
class control. However, such an observation appears less amenable to a clean
mathematical formulation, as the runtimes in question are highly sensitive to
both the particular choice of predicate and the search order employed.

###### Acknowledgements.

We would like to thank James McKinna and Maciej Piróg for insightful
discussions, and Danel Ahman and the anonymous reviewers for helpful feedback
and suggestions for improvement. Daniel Hillerström was supported by EPSRC
grant EP/L01503X/1 and by ERC Consolidator Grant Skye (grant number 682315).
Sam Lindley was supported by EPSRC grant EP/K034413/1 (From Data Types to
Session Types—A Basis for Concurrency and Distribution).

## References

  * (1)