* Bauer (2018) Andrej Bauer. 2018\.  What is algebraic about algebraic effects and handlers?  _CoRR_ abs/1807.05923 (2018).
  * Bauer and Pretnar (2015) Andrej Bauer and Matija Pretnar. 2015.  Programming with algebraic effects and handlers.  _J. Log. Algebr. Meth. Program._ 84, 1 (2015), 108–123.
  * Bell and Stevens (2009) Jordan Bell and Brett Stevens. 2009.  A survey of known results and research areas for n-queens.  _Discret. Math._ 309, 1 (2009), 1–31.
  * Benton and Kennedy (2001) Nick Benton and Andrew Kennedy. 2001.  Exceptional Syntax Journal of Functional Programming.  _J. Funct. Program._ 11, 4 (2001), 395–410.
  * Berger (1990) Ulrich Berger. 1990\.  _Totale Objekte und Mengen in der Bereichstheorie_.  Ph.D. Dissertation. Ludwig Maximillians-Universtität, Munich.
  * Biernacki et al. (2019) Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. 2019.  Abstracting algebraic effects.  _PACMPL_ 3, POPL (2019), 6:1–6:28.
  * Biernacki et al. (2020) Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. 2020.  Binders by day, labels by night: effect instances via lexically scoped handlers.  _PACMPL_ 4, POPL (2020), 48:1–48:29.
  * Bird et al. (1997) Richard Bird, Geraint Jones, and Oege de Moor. 1997\.  More haste less speed: lazy versus eager evaluation.  _J. Funct. Program._ 7, 5 (1997), 541–547.
  * Bird (2006) Richard S. Bird. 2006\.  Functional Pearl: A program to solve Sudoku.  _J. Funct. Program._ 16, 6 (2006), 671–679.
  * Cartwright and Felleisen (1992) Robert Cartwright and Matthias Felleisen. 1992.  Observable Sequentiality and Full Abstraction. In _POPL_. ACM Press, 328–342.
  * Convent et al. (2020) Lukas Convent, Sam Lindley, Conor McBride, and Craig McLaughlin. 2020.  Doo bee doo bee doo.  _J. Funct. Program._ 30 (2020).  To appear.
  * Cormen et al. (2009) Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009.  _Introduction to Algorithms, Third Edition_ (3rd ed.).  MIT Press.
  * Daniels (2016) Robbie Daniels. 2016\.  _Efficient Generic Searches and Programming Language Expressivity_.  Master’s thesis. School of Informatics, the University of Edinburgh, Scotland.  http://homepages.inf.ed.ac.uk/jrl/Research/Robbie_Daniels_MSc_dissertation.pdf
  * Danvy and Filinski (1990) Olivier Danvy and Andrzej Filinski. 1990.  Abstracting Control. In _LISP and Functional Programming_. ACM, 151–160.
  * Dolan et al. (2015) Stephen Dolan, Leo White, KC Sivaramakrishnan, Jeremy Yallop, and Anil Madhavapeddy. 2015.  Effective Concurrency through Algebraic Effects.  OCaml Workshop.
  * Escardó (2007) Martín Hötzel Escardó. 2007\.  Infinite sets that admit fast exhaustive search. In _LICS_. IEEE Computer Society, 443–452.
  * Farvardin and Reppy (2020) Kavon Farvardin and John H. Reppy. 2020.  From folklore to fact: comparing implementations of stacks and continuations. In _PLDI_. ACM, 75–90.
  * Felleisen (1987) Matthias Felleisen. 1987\.  _The Calculi of Lambda-nu-cs Conversion: A Syntactic Theory of Control and State in Imperative Higher-order Programming Languages_.  Ph.D. Dissertation. Indianapolis, IN, USA.  AAI8727494.
  * Felleisen (1988) Matthias Felleisen. 1988\.  The Theory and Practice of First-Class Prompts. In _POPL_. ACM Press, 180–190.
  * Felleisen (1991) Matthias Felleisen. 1991\.  On the expressive power of programming languages.  _Sci. Comput. Prog._ 17, 1–3 (1991), 35–75.
  * Felleisen and Friedman (1987) Matthias Felleisen and Daniel P. Friedman. 1987.  Control Operators, the SECD-machine, and the $\lambda$-Calculus. In _The Proceedings of the Conference on Formal Description of Programming Concepts III, Ebberup, Denmark_. Elsevier, 193–217.
  * Flanagan et al. (1993) Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. 1993.  The Essence of Compiling with Continuations. In _PLDI_. ACM, 237–247.
  * Flatt and Dybvig (2020) Matthew Flatt and R. Kent Dybvig. 2020.  Compiler and runtime support for continuation marks. In _PLDI_. ACM, 45–58.
  * Forster et al. (2019) Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. 2019.  On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control.  _J. Funct. Program._ 29 (2019), e15.
  * Hillerström and Lindley (2016) Daniel Hillerström and Sam Lindley. 2016.  Liberating effects with rows and handlers. In _TyDe@ICFP_. ACM, 15–27.
  * Hillerström and Lindley (2018) Daniel Hillerström and Sam Lindley. 2018.  Shallow Effect Handlers. In _APLAS_ _(Lecture Notes in Computer Science, Vol. 11275)_. Springer, 415–435.
  * Hillerström et al. (2020a) Daniel Hillerström, Sam Lindley, and Robert Atkey. 2020a.  Effect handlers via generalised continuations.  _J. Funct. Program._ 30 (2020), e5.
  * Hillerström et al. (2017) Daniel Hillerström, Sam Lindley, Robert Atkey, and K. C. Sivaramakrishnan. 2017.  Continuation Passing Style for Effect Handlers. In _FSCD_ _(LIPIcs, Vol. 84)_. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 18:1–18:19.
  * Hillerström et al. (2020b) Daniel Hillerström, Sam Lindley, and John Longley. 2020b.  Effects for Efficiency: Asymptotic Speedup with First-Class Control (extended version).  arXiv:2007.00605 [cs.PL]
  * Hughes (1986) John Hughes. 1986\.  A Novel Representation of Lists and its Application to the Function "reverse".  _Inf. Process. Lett._ 22, 3 (1986), 141–144.
  * Jones (2001) Neil Jones. 2001\.  The expressive power of higher-order types, or, life without CONS.  _J. Funct. Program._ 11 (2001), 5–94.
  * Kammar et al. (2013) Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013.  Handlers in action. In _ICFP_. ACM, 145–158.
  * Kiselyov et al. (2013) Oleg Kiselyov, Amr Sabry, and Cameron Swords. 2013.  Extensible effects: an alternative to monad transformers. In _Haskell_. ACM, 59–70.
  * Kiselyov et al. (2005) Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, and Amr Sabry. 2005.  Backtracking, Interleaving, and Terminating Monad Transformers: (Functional Pearl).  (2005), 192–203.
  * Knuth (1997) Donald Knuth. 1997\.  _The Art of Computer Programming, Volume 1: Fundamental Algorithms (third edition)_.  Addison-Wesley.
  * Leijen (2017) Daan Leijen. 2017\.  Type directed compilation of row-typed algebraic effects. In _POPL_. ACM, 486–499.
  * Levy et al. (2003) Paul Blain Levy, John Power, and Hayo Thielecke. 2003\.  Modelling environments in call-by-value programming languages.  _Inf. Comput._ 185, 2 (2003), 182–210.
  * Lindley et al. (2017) Sam Lindley, Conor McBride, and Craig McLaughlin. 2017\.  Do be do be do. In _POPL_. ACM, 500–514.
  * Longley (1999) John Longley. 1999\.  When is a functional program not a functional program?. In _ICFP_. ACM, 1–7.
  * Longley (2018) John Longley. 2018\.  The recursion hierarchy for PCF is strict.  _Logical Methods in Comput. Sci._ 14, 3:8 (2018), 1–51.
  * Longley (2019) John Longley. 2019\.  Bar recursion is not computable via iteration.  _Computability_ 8, 2 (2019), 119–153.
  * Longley and Normann (2015) John Longley and Dag Normann. 2015.  _Higher-Order Computability_.  Springer.
  * Milner (1977) Robin Milner. 1977\.  Fully Abstract Models of Typed $\lambda$-Calculi.  _Theor. Comput. Sci._ 4, 1 (1977), 1–22.
  * MLton (2020) MLton. 2020.  MLton website.  http://www.mlton.org
  * Moggi (1991) Eugenio Moggi. 1991\.  Notions of Computation and Monads.  _Inf. Comput._ 93, 1 (1991), 55–92.
  * Okasaki (1999) Chris Okasaki. 1999\.  _Purely functional data structures_.  Cambridge University Press.
  * Pippenger (1996) Nicholas Pippenger. 1996\.  Pure versus impure Lisp. In _POPL_. ACM, 104–109.
  * Piróg et al. (2019) Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. 2019\.  Typed Equivalence of Effect Handlers and Delimited Control. In _FSCD_ _(LIPIcs, Vol. 131)_. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 30:1–30:16.
  * Plotkin (1977) Gordon Plotkin. 1977\.  LCF considered as a programming language.  _Theor. Comput. Sci._ 5, 3 (1977), 223–255.
  * Plotkin and Power (2001) Gordon D. Plotkin and John Power. 2001.  Adequacy for Algebraic Effects. In _FoSSaCS_ _(Lecture Notes in Computer Science, Vol. 2030)_. Springer, 1–24.
  * Plotkin and Pretnar (2013) Gordon D. Plotkin and Matija Pretnar. 2013.  Handling Algebraic Effects.  _Logical Methods in Computer Science_ 9, 4 (2013).
  * Pretnar (2015) Matija Pretnar. 2015\.  An Introduction to Algebraic Effects and Handlers.  _Electr. Notes Theor. Comput. Sci._ 319 (2015), 19–35.  Invited tutorial paper.
  * Scott and Strachey (1971) Dana Scott and Christopher Strachey. 1971.  _Proceedings of the Symposium on Computers and Automata_ 21 (1971).
  * Simpson (1998) Alex K. Simpson. 1998\.  Lazy Functional Algorithms for Exact Real Functionals. In _MFCS_ _(Lecture Notes in Computer Science, Vol. 1450)_. Springer, 456–464.
  * SML/NJ (2020) SML/NJ. 2020.  SML/NJ website.  http://www.smlnj.org
  * Sperber et al. (2009) Michael Sperber, Kent R. Dybvig, Matthew Flatt, Anton van Stratten, Robby Bruce Findler, and Jacob Matthews. 2009.  Revised6 Report on the Algorithmic Language Scheme.  _J. Funct. Program._ 19, S1 (2009), 1–301.

##  Appendix A Correctness of the Base Machine

We now show that the base abstract machine is correct with respect to the
operational semantics, that is, the abstract machine faithfully simulates the
operational semantics. Initial states provide a canonical way to map a
computation term onto the abstract machine. A more interesting question is how
to map an arbitrary configuration to a computation term. Figure 7 describes
such a mapping $\llparenthesis-\rrparenthesis$ from configurations to terms
via a collection of mutually recursive functions defined on configurations,
continuations, computation terms, value terms, and machine values. The mapping
makes use of two operations on environments, $\gamma$, which we define now.

###### Definition A.1.

We write $dom(\gamma)$ for the domain of $\gamma$, and
$\gamma\backslash\\{x_{1},\dots,x_{n}\\}$ for the restriction of environment
$\gamma$ to $dom(\gamma)\backslash\\{x_{1},\dots,x_{n}\\}$.

Configurations

$\displaystyle\llparenthesis\langle
M\mid\gamma\mid\sigma\rangle\rrparenthesis=\llparenthesis\sigma\rrparenthesis(\llparenthesis
M\rrparenthesis\gamma)$

Pure continuations

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\llparenthesis[]\rrparenthesis
M~{}&=\hfil~{}&M\\\ \llparenthesis(\gamma,x,N)::\sigma\rrparenthesis
M~{}&=\hfil~{}&\llparenthesis\sigma\rrparenthesis(\mathbf{let}\;x\leftarrow
M\;\mathbf{in}\;\llparenthesis N\rrparenthesis(\gamma\backslash\\{x\\}))\\\
\end{array}$

Computation terms

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\llparenthesis
V\,W\rrparenthesis\gamma~{}&=\hfil~{}&\llparenthesis
V\rrparenthesis\gamma\,\llparenthesis W\rrparenthesis{\gamma}\\\
\llparenthesis\mathbf{let}\;\langle
x;y\rangle=V\;\mathbf{in}\;N\rrparenthesis\gamma~{}&=\hfil~{}&\mathbf{let}\;\langle
x;y\rangle=\llparenthesis V\rrparenthesis\gamma\;\mathbf{in}\;\llparenthesis
N\rrparenthesis(\gamma\backslash\\{x,y\\})\\\ \hskip
56.9055pt\llparenthesis\mathbf{case}\;V\,\\{\mathbf{inl}\;x\mapsto
M;\mathbf{inr}\;y\mapsto
N\\}\rrparenthesis\gamma~{}&=\hfil~{}&\mathbf{case}\;\llparenthesis
V\rrparenthesis\gamma\,\\{\begin{array}[t]{@{}l@{}}\mathbf{inl}\;x\mapsto\llparenthesis
M\rrparenthesis(\gamma\backslash\\{x\\});\\\
\mathbf{inr}\;y\mapsto\llparenthesis
N\rrparenthesis(\gamma\backslash\\{y\\})\\}\\\ \end{array}\\\
\llparenthesis\mathbf{return}\;V\rrparenthesis\gamma~{}&=\hfil~{}&\mathbf{return}\;\llparenthesis
V\rrparenthesis\gamma\\\ \llparenthesis\mathbf{let}\;x\leftarrow
M\;\mathbf{in}\;N\rrparenthesis\gamma~{}&=\hfil~{}&\mathbf{let}\;x\leftarrow\llparenthesis
M\rrparenthesis\gamma\;\mathbf{in}\;\llparenthesis
N\rrparenthesis(\gamma\backslash\\{x\\})\\\ \end{array}$

Value terms and values

$\displaystyle\begin{array}[t]{@{}r@{~}c@{~}l@{}}\llparenthesis
x\rrparenthesis\gamma~{}&=\hfil~{}&\llparenthesis v\rrparenthesis,\quad\text{
if }\gamma(x)=v\\\ \llparenthesis
x\rrparenthesis\gamma~{}&=\hfil~{}&x,\quad\text{ if }x\notin dom(\gamma)\\\
\llparenthesis n\rrparenthesis\gamma~{}&=\hfil~{}&n\\\ \llparenthesis\lambda
x^{A}.M\rrparenthesis\gamma~{}&=\hfil~{}&\lambda x^{A}.\llparenthesis
M\rrparenthesis(\gamma\backslash\\{x\\})\\\
\llparenthesis\mathbf{rec}\,f\,x^{A}.M\rrparenthesis\gamma~{}&=\hfil~{}&\mathbf{rec}\,f\,x^{A}.\llparenthesis
M\rrparenthesis(\gamma\backslash\\{f,x\\})\\\
\llparenthesis\langle\rangle{}\rrparenthesis\gamma~{}&=\hfil~{}&\langle\rangle{}\\\
\llparenthesis\langle
V,W\rangle\rrparenthesis\gamma~{}&=\hfil~{}&\langle\llparenthesis
V\rrparenthesis\gamma,\llparenthesis W\rrparenthesis\gamma\rangle\\\
\llparenthesis(\mathbf{inl}\;V)^{B}\rrparenthesis\gamma~{}&=\hfil~{}&(\mathbf{inl}\;\llparenthesis
V\rrparenthesis\gamma)^{B}\\\
\llparenthesis(\mathbf{inr}\;W)^{A}\rrparenthesis\gamma~{}&=\hfil~{}&(\mathbf{inr}\;\llparenthesis
W\rrparenthesis\gamma)^{A}\\\ \end{array}\penalty 50\hskip 20.00003pt plus
0.5fil minus 5.0pt\begin{array}[t]{@{}r@{~}c@{~}l@{}}\llparenthesis
n\rrparenthesis~{}&=\hfil~{}&n\\\ \llparenthesis(\gamma,\lambda
x^{A}.M)\rrparenthesis~{}&=\hfil~{}&\lambda x^{A}.\llparenthesis
M\rrparenthesis(\gamma\backslash\\{x\\})\\\
\llparenthesis(\gamma,\mathbf{rec}\,f\,x^{A}.M)\rrparenthesis~{}&=\hfil~{}&\mathbf{rec}\,f\,x^{A}.\llparenthesis
M\rrparenthesis(\gamma\backslash\\{f,x\\})\\\
\llparenthesis\langle\rangle\rrparenthesis~{}&=\hfil~{}&\langle\rangle\\\
\llparenthesis\langle
v;w\rangle\rrparenthesis~{}&=\hfil~{}&\langle\llparenthesis
v\rrparenthesis;\llparenthesis w\rrparenthesis\rangle\\\
\llparenthesis(\mathbf{inl}\;v)^{B}\rrparenthesis~{}&=\hfil~{}&(\mathbf{inl}\;\llparenthesis
v\rrparenthesis)^{B}\\\
\llparenthesis(\mathbf{inr}\;w)^{A}\rrparenthesis~{}&=\hfil~{}&(\mathbf{inr}\;\llparenthesis
w\rrparenthesis)^{A}\\\
\llparenthesis\sigma^{A}\rrparenthesis~{}&=\hfil~{}&\lambda
x^{A}.\llparenthesis\sigma\rrparenthesis(\mathbf{return}\;x)\\\ \end{array}$

Figure 7. Mapping from Base Machine Configurations to Terms

The $\llparenthesis-\rrparenthesis$ function enables us to classify the
abstract machine reduction rules according to how they relate to the
operational semantics. The rule (M-Let) is administrative in the sense that
$\llparenthesis-\rrparenthesis$ is invariant under this rule. This leaves the
$\beta$-rules (M-App), (M-Split), (M-Case), and (M-RetCont). Each of these
corresponds directly with performing a reduction in the operational semantics.

###### Definition A.2 (Auxiliary reduction relations).

We write $\longrightarrow_{\textrm{a}}$ for administrative steps (M-Let) and
$\simeq_{\textrm{a}}$ for the symmetric closure of
$\longrightarrow_{\textrm{a}}^{*}$. We write $\longrightarrow_{\beta}$ for
$\beta$-steps (all other rules) and $\Longrightarrow$ for a sequence of steps
of the form $\longrightarrow_{\textrm{a}}^{*}\longrightarrow_{\beta}$.

The following lemma describes how we can simulate each reduction in the
operational semantics by a sequence of administrative steps followed by one
$\beta$-step in the abstract machine.

###### Lemma A.3.

Suppose $M$ is a computation and $\mathcal{C}$ is configuration such that
$\llparenthesis\mathcal{C}\rrparenthesis=M$, then if $M\leadsto N$ there
exists $\mathcal{C}^{\prime}$ such that
$\mathcal{C}\Longrightarrow\mathcal{C}^{\prime}$ and
$\llparenthesis\mathcal{C}^{\prime}\rrparenthesis=N$, or if $M\not\leadsto$
then $\mathcal{C}\not\Longrightarrow$.

###### Proof.

By induction on the derivation of $M\leadsto N$. ∎

The correspondence here is rather strong: there is a one-to-one mapping
between $\leadsto$ and $\Longrightarrow\mathbin{/}\simeq_{\textrm{a}}$ (where
we write $R/S$ for the quotient of relation $R$ by relation $S$). The inverse
of the lemma is straightforward as the semantics is deterministic. Notice that
Lemma A.3 does not require that $M$ be well-typed. We have chosen here not to
perform type-erasure, but the results can be adapted to semantics in which all
type annotations are erased.

###### Theorem A.4 (Base simulation).

If $\vdash M:A$ and $M\leadsto^{+}N$ such that $N$ is normal, then $\langle
M\mid\emptyset\mid[]\rangle\longrightarrow^{+}\mathcal{C}$ such that
$\llparenthesis\mathcal{C}\rrparenthesis=N$, or $M\not\leadsto$ then $\langle
M\mid\emptyset\mid[]\rangle\not\longrightarrow$.

###### Proof.

By repeated application of Lemma A.3. ∎

##  Appendix B Correctness of the Handler Machine

The correctness result for the base machine can mostly be repurposed for the
handler machine as we need only recheck the cases for $(\text{{M-Let}})$ and
$(\text{{M-RetCont}})$ and check the cases for handlers. Figure 8 shows the
necessary changes to the $\llparenthesis-\rrparenthesis$ function.

###### Lemma B.1.

Suppose $M$ is a computation and $\mathcal{C}$ is configuration such that
$\llparenthesis\mathcal{C}\rrparenthesis=M$, then if $M\leadsto N$ there
exists $\mathcal{C}^{\prime}$ such that
$\mathcal{C}\Longrightarrow\mathcal{C}^{\prime}$ and
$\llparenthesis\mathcal{C}^{\prime}\rrparenthesis=N$, or if $M\not\leadsto$
then $\mathcal{C}\not\Longrightarrow$.

###### Proof.

By induction on the derivation of $M\leadsto N$. ∎

###### Theorem B.2 (Handler simulation).

If $\vdash M:A$ and $M\leadsto^{+}N$ such that $N$ is normal, then $\langle
M\mid\emptyset\mid\kappa_{0}\rangle\longrightarrow^{+}\mathcal{C}$ such that
$\llparenthesis\mathcal{C}\rrparenthesis=N$, or $M\not\leadsto$ then $\langle
M\mid\emptyset\mid\kappa_{0}\rangle\not\longrightarrow$.

###### Proof.

By repeated application of Lemma B.1. ∎

Configurations

$\displaystyle\llparenthesis\langle
M\mid\gamma\mid\kappa\rangle\rrparenthesis=\llparenthesis\kappa\rrparenthesis(\llparenthesis
M\rrparenthesis\gamma)$

Continuations

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\llparenthesis[]\rrparenthesis
M~{}&=\hfil~{}&M\\\ \llparenthesis(\sigma,\chi)::\kappa\rrparenthesis
M~{}&=\hfil~{}&\llparenthesis\kappa\rrparenthesis(\llparenthesis\chi\rrparenthesis(\llparenthesis\sigma\rrparenthesis(M)))\end{array}$

Handler Closures and Definitions

$\displaystyle\begin{array}[t]{@{}r@{~}c@{~}l@{}}\llparenthesis(\gamma,H)\rrparenthesis
M~{}&=\hfil~{}&\mathbf{handle}\;M\;\mathbf{with}\;\llparenthesis
H\rrparenthesis\gamma\end{array}\begin{array}[t]{@{}r@{~}c@{~}l@{}}\llparenthesis\\{\mathbf{val}~{}x\mapsto
M\\}\rrparenthesis\gamma~{}&=\hfil~{}&\\{\mathbf{val}~{}x\mapsto\llparenthesis
M\rrparenthesis(\gamma\backslash\\{x\\})\\}\\\
\llparenthesis\\{\ell~{}x~{}r\mapsto M\\}\uplus
H\rrparenthesis\gamma~{}&=\hfil~{}&\\{\ell~{}x~{}r\mapsto\llparenthesis
M\rrparenthesis(\gamma\backslash\\{x,r\\})\\}\uplus\llparenthesis
H\rrparenthesis\gamma\end{array}$

Computation Terms and Machine Values

$\displaystyle\begin{array}[t]{@{}r@{~}c@{~}l@{}}\llparenthesis\mathbf{handle}\;M\;\mathbf{with}\;H\rrparenthesis\gamma~{}&=\hfil~{}&\mathbf{handle}\;\llparenthesis
M\rrparenthesis\gamma\;\mathbf{with}\;\llparenthesis H\rrparenthesis\gamma\\\
\llparenthesis\mathbf{do}\;\ell\,V\rrparenthesis\gamma~{}&=\hfil~{}&\mathbf{do}\;\ell\,\llparenthesis
V\rrparenthesis\gamma\end{array}\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt\begin{array}[t]{@{}r@{~}c@{~}l@{}}\llparenthesis(\gamma,H)^{D}\rrparenthesis\gamma~{}&=\hfil~{}&\lambda
x^{D}.\llparenthesis(\gamma,H)\rrparenthesis(\mathbf{return}\;x)\end{array}$

Figure 8. Mapping from Handler Machine Configurations to Terms

##  Appendix C Proof Details for the Complexity of Effectful Generic Count

In this appendix we give proof details and artefacts for Theorem 5.9.
Throughout this section we let $H_{\mathsf{count}}$ denote the handler
definition of $\mathsf{count}$, that is

$H_{\mathsf{count}}\mathrel{:=}\left\\{\begin{array}[m]{@{~}l@{~}c@{~}l}{}\lx@intercol\mathbf{val}~{}x\hfil~{}&\mapsto\hfil~{}&\mathbf{if}\;x\;\mathbf{then}\;\mathbf{return}~{}1\;\mathbf{else}\;\mathbf{return}~{}0\\\
{}\lx@intercol\mathsf{Branch}~{}\langle\rangle~{}r\hfil~{}&\mapsto\hfil~{}&\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}\right\\}$

The timed decision tree model embeds timing information. For the proof we must
also know the abstract machine environment and the pure continuation. Thus we
decorate timed decision trees with this information.

###### Definition C.1 (decorated timed decision trees).

A decorated timed decision tree is a partial function
$\tau:\mathsf{Addr}\rightharpoonup(\mathsf{Lab}\times\mathsf{Nat})\times\mathsf{Conf}_{q}$
such that its first projection $bs\mapsto\tau(bs).1$ is a timed decision tree.

We extend the projections $\mathsf{labs}$ and $\mathsf{steps}$ in the obvious
way to work over decorated timed decision trees. We define three further
projections. The first $\mathsf{comp}(\tau)\mathrel{:=}bs\mapsto\tau(bs).2.1$
projects the computation component of the configuration, the second
$\mathsf{env}(\tau)\mathrel{:=}bs\mapsto\tau(bs).2.2$ projects the
environment, and finally the third
$\mathsf{pure}(\tau)\mathrel{:=}bs\mapsto\mathsf{head}(t(bs).2.3).1$ projects
the pure continuation.

The following definition gives a procedure for constructing a decorated timed
decision tree. The construction is analogous to that of Definition 5.4.

###### Definition C.2.

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

$\displaystyle\begin{array}[]{@{}r@{~}c@{~}l@{\qquad}l@{}}\mathcal{D}(\langle\mathbf{return}\;W\mid\gamma\mid[]\rangle)\,[]~{}&~{}={}\hfil~{}&((!b,0),\langle\mathbf{return}\;W\mid\gamma\mid[]\rangle),&\text{if
}\llbracket W\rrbracket\gamma=b\vskip 3.0pt plus 1.0pt minus 1.0pt\\\
\mathcal{D}(\langle
z\,V\mid\gamma\mid\kappa\rangle)\,[]~{}&~{}={}\hfil~{}&((?\llbracket
V\rrbracket\gamma,0),\langle z\,V\mid\gamma\mid\kappa\rangle),&\text{if
}\gamma(z)=q\vskip 3.0pt plus 1.0pt minus 1.0pt\\\ \mathcal{D}(\langle
z\,V\mid\gamma\mid\kappa\rangle)\,(b::bs)~{}&~{}\simeq{}\hfil~{}&\mathcal{D}(\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{D}(\langle
M\mid\gamma\mid\kappa\rangle)\,bs~{}&~{}\simeq{}\hfil~{}&\mathsf{inc}\,(\mathcal{D}(\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),\mathcal{C})=((\ell,s+1),\mathcal{C})$, and in all
of the above equations $\gamma(q)=\gamma^{\prime}(q)=q$. Clearly
$\mathcal{D}(\mathcal{C})$ is a decorated timed decision tree for any
$\mathcal{C}\in\mathsf{Conf}_{q}$.

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

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

We define some functions, that given a list of booleans and a $n$-standard
predicate, compute configurations of the effectful abstract machine at
particular points of interest during evaluation of the given predicate. Let
$\chi_{\mathsf{count}}(V)\mathrel{:=}(\emptyset[pred\mapsto\llbracket
V\rrbracket\emptyset],H_{\mathsf{count}})$ denote the handler closure of
$H_{\mathsf{count}}$.

#### Notation.

For an $n$-standard predicate $P$ we write $|P|=n$ for the size of the
predicate. Furthermore, we define $\chi_{\text{id}}$ for the identity handler
closure $(\emptyset,\\{\mathbf{val}~{}x\mapsto x\\})$.

###### Definition C.3 (computing machine configurations).

For any $n$-standard predicate $P$ and a list of booleans $bs$, such that
$|bs|\leq n$, we can compute machine configurations at points of interest
during evaluation of $\mathsf{count}~{}P$.

To make the notation slightly simpler we use the following conventions
whenever $n$, $\tau$, and $c$ appear free: $n=|P|$, $\tau=\mathcal{D}(P)$, and
$c(bs)=\sharp(bs^{\prime}\mapsto\llbracket
P\rrbracket~{}(bs\mathbin{+\\!\\!+}bs^{\prime}))$. The definitions are
presented in a top-down manner.

  * •

The function $\mathsf{arrive}$ either computes the configuration at a query
node, if $|bs|<n$, or the configuration at an answer node.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\mathsf{arrive}~{}&:\hfil~{}&\mathsf{Addr}\times\mathrm{Val}\rightharpoonup\mathsf{Conf}\\\
\mathsf{arrive}(bs,P)~{}&\mathrel{:=}\hfil~{}&\langle
z~{}V\mid\gamma\mid(\sigma,\chi_{\mathsf{count}}(P))::\mathsf{residual}(bs,P)\rangle,\quad\text{if
}|bs|<n\\\ \lx@intercol\hfill\text{where
}\begin{array}[t]{@{~}l}{}\lx@intercol
z~{}V=\mathsf{comp}(\tau)(bs),\gamma=\mathsf{env}(\tau)(bs),\gamma(z)=(\mathsf{env}^{\bot}(P),\lambda\\_.\mathbf{do}\;\mathsf{Branch}~{}\langle\rangle)\\\
{}\lx@intercol?k=\mathsf{labs}(\tau)(bs),\llbracket V\rrbracket\gamma=k,\text{
and }\sigma=\mathsf{pure}(\tau)(bs)\end{array}\hfil\\\
\mathsf{arrive}(bs,P)~{}&\mathrel{:=}\hfil~{}&\langle\mathbf{return}\;W\mid\gamma\mid([],\chi_{\mathsf{count}}(P))::\mathsf{residual}(bs,P)\rangle,\quad\text{if
}|bs|=n\\\ \lx@intercol\hfill\text{where
}\mathbf{return}\;W=\mathsf{comp}(\tau)(bs),\gamma=\mathsf{env}(\tau)(bs),!b=\mathsf{labs}(\tau)(bs),\text{
and }\llbracket W\rrbracket\gamma=b\hfil\end{array}$

  * •

Correspondingly, the $\mathsf{depart}$ function computes the configuration
either after the completion of a query or handling of an answer.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\mathsf{depart}~{}&:\hfil~{}&\mathsf{Addr}\times\mathrm{Val}\rightharpoonup\mathsf{Conf}\\\
\mathsf{depart}(bs,P)~{}&\mathrel{:=}\hfil~{}&\langle\mathbf{return}\;m\mid\gamma\mid\mathsf{residual}(bs,P)\rangle,\quad\text{if
}|bs|<n\\\ \lx@intercol\hfill\text{where
}\gamma=\mathsf{env}^{\uparrow}_{\mathsf{false}}(bs,P)\text{ and
}m=c(bs)\hfil\\\
\mathsf{depart}(bs,P)~{}&\mathrel{:=}\hfil~{}&\langle\mathbf{return}\;m\mid\gamma\mid\mathsf{residual}(bs,P)\rangle,\quad\text{if
}|bs|=n\\\ \lx@intercol\hfill\text{where
}\begin{array}[t]{@{}l}m=c(bs),b=\begin{cases}\mathsf{true}&\text{if }m=1\\\
\mathsf{false}&\text{if }m=0\end{cases},\text{ and
}\gamma=\mathsf{env}^{\bot}(P)[x\mapsto b]\end{array}\hfil\end{array}$

The two clauses of $\mathsf{depart}$ yield slightly different configurations.
The first clause computes a configuration inside the operation clause of
$H_{\mathsf{count}}$. The configuration is exactly tail-configuration after
summing up the two respective values returned by the two invocations of
resumption. Whilst the second clause computes the tail-configuration inside of
the success clause of $H_{\mathsf{count}}$ after handling a return value of
the predicate.

  * •

The $\mathsf{residual}$ function computes the residual continuation structure
which contains the bits of computations to perform after handling a complete
path in a decision tree.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\mathsf{residual}~{}&:\hfil~{}&\mathsf{Addr}\times\mathrm{Val}\rightharpoonup\mathsf{Cont}\\\
\mathsf{residual}(bs,P)~{}&\mathrel{:=}\hfil~{}&[(\mathsf{purecont}(bs,P),\chi_{id})]\end{array}$

  * •

The function $\mathsf{purecont}$ computes the pure continuation.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\mathsf{purecont}~{}&:\hfil~{}&\mathsf{Addr}\times\mathrm{Val}\rightharpoonup\mathsf{PureCont}\\\
\mathsf{purecont}([],P)~{}&\mathrel{:=}\hfil~{}&[]\\\
\mathsf{purecont}(bs\mathbin{+\\!\\!+}[\mathsf{true}],P)~{}&\mathrel{:=}\hfil~{}&(\gamma,x_{\mathsf{true}},\mathbf{let}\;x_{\mathsf{false}}\leftarrow
r~{}\mathsf{false}\;\mathbf{in}\;x_{\mathsf{true}}+x_{\mathsf{false}})::\mathsf{purecont}(bs,P),\\\
\lx@intercol\hfill\text{where
}\gamma=\mathsf{env}^{\downarrow}_{\mathsf{true}}(bs\mathbin{+\\!\\!+}[\mathsf{true}],P)\hfil\\\
\mathsf{purecont}(bs\mathbin{+\\!\\!+}[\mathsf{false}],P)~{}&\mathrel{:=}\hfil~{}&(\gamma,x_{\mathsf{false}},x_{\mathsf{true}}+x_{\mathsf{false}})::\mathsf{purecont}(bs,P),\\\
\lx@intercol\hfill\text{where
}\gamma=\mathsf{env}^{\downarrow}_{\mathsf{false}}(bs\mathbin{+\\!\\!+}[\mathsf{false}],P)\hfil\\\
\end{array}$

  * •

The function $\mathsf{env}^{\bot}$ computes the initial environment of the
handler. The family of functions $\mathsf{env}^{\downarrow}_{b\in\mathbb{B}}$
contains two functions, one for each instantiation of $b$, which describe how
to compute the environment prior _descending_ down a branch as the result of
invoking a resumption with $b$. Analogously, the functions in the family
$\mathsf{env}^{\uparrow}_{b\in\mathbb{B}}$ describe how to compute the
environment after _ascending_ from the resumptive exploration of a branch.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\mathsf{env}^{\bot}~{}&:\hfil~{}&\mathrm{Val}\to\mathsf{Env}\\\
\mathsf{env}^{\bot}(P)~{}&\mathrel{:=}\hfil~{}&\emptyset[pred\mapsto\llbracket
P\rrbracket\emptyset]\\\\[6.45831pt] \end{array}$

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\mathsf{env}^{\downarrow}_{\mathsf{true}}~{}&:\hfil~{}&\mathsf{Addr}\times\mathrm{Val}\rightharpoonup\mathsf{Env}\\\
\mathsf{env}^{\downarrow}_{\mathsf{true}}(bs,P)~{}&\mathrel{:=}\hfil~{}&\mathsf{env}^{\bot}(P)[r\mapsto(\sigma,\chi_{\mathsf{count}}(P))],\\\
\lx@intercol\qquad\text{where
}\sigma=\mathsf{pure}(\tau)(bs)\hfil\\\\[6.45831pt]
\mathsf{env}^{\uparrow}_{\mathsf{true}}~{}&:\hfil~{}&\mathsf{Addr}\times\mathrm{Val}\rightharpoonup\mathsf{Env}\\\
\mathsf{env}^{\uparrow}_{\mathsf{true}}(bs,P)~{}&\mathrel{:=}\hfil~{}&\gamma[x_{\mathsf{true}}\mapsto
i],\\\ \lx@intercol\qquad\begin{array}[t]{@{}l@{}}\text{where
}\gamma=\mathsf{env}^{\downarrow}_{\mathsf{true}}(bs,P)\\\ \text{and
}i=c(bs\mathbin{+\\!\\!+}[\mathsf{true}])\end{array}\hfil\\\\[6.45831pt]
\end{array}$

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\mathsf{env}^{\downarrow}_{\mathsf{false}}~{}&:\hfil~{}&\mathsf{Addr}\times\mathrm{Val}\rightharpoonup\mathsf{Env}\\\
\mathsf{env}^{\downarrow}_{\mathsf{false}}(bs,P)~{}&\mathrel{:=}\hfil~{}&\mathsf{env}^{\uparrow}_{\mathsf{true}}\\\\[6.45831pt]
\mathsf{env}^{\uparrow}_{\mathsf{false}}~{}&:\hfil~{}&\mathsf{Addr}\times\mathrm{Val}\rightharpoonup\mathsf{Env}\\\
\mathsf{env}^{\uparrow}_{\mathsf{false}}(bs,P)~{}&\mathrel{:=}\hfil~{}&\gamma[x_{\mathsf{false}}\mapsto
j],\\\ \lx@intercol\qquad\begin{array}[t]{@{}l@{}}\text{where
}\gamma=\mathsf{env}^{\downarrow}_{\mathsf{false}}(bs,P)\\\ \text{ and
}j=c(bs\mathbin{+\\!\\!+}[\mathsf{false}])\end{array}\hfil\\\ \end{array}$

The proof of Theorem 5.9 works by alternating between two different modes of
reasoning: intensional and extensional. The former is used to reason directly
about the steps taken by $\mathsf{effcount}$ program and the latter is used to
reason about steps taken by the provided predicate. The number of steps taken
by an $n$-standard predicate is readily available by constructing its
corresponding decorated timed decision tree model. The model is constructed
using a distinguished free variable $q$ to denote a point. The following lemma
lets us reason about the number of steps taken by a predicate between its
initial application and its first query, between subsequent queries, and
between final query and answer when $q$ is instantiated to
$\lambda\\_.\mathbf{do}\;\mathsf{Branch}~{}\langle\rangle$.

###### Lemma C.4.

Suppose $P$ is an $n$-standard predicate, $bs\in\mathsf{Addr}$ is a list of
booleans, and for all $\chi\in\mathsf{HClo}$ and $\kappa\in\mathsf{Cont}$. Let
$q$ denote the distinguished free variable used to construct the decorated
timed decision tree $\tau$ of $P$.

  1. (1)

If $|bs|=0$ then

$\begin{array}[]{@{}r@{~}l@{}}~{}&\langle
pred~{}q\mid\mathsf{env}^{\bot}(P)[q\mapsto q]\mid([],\chi)::\kappa\rangle\\\
\longrightarrow~{}&{}^{\mathsf{steps}(\tau)([])}\\\ ~{}&\langle
z~{}V\mid\gamma[q\mapsto q]\mid(\sigma,\chi)::\kappa\rangle\end{array}$

where $z~{}V=\mathsf{comp}(\tau)([])$, $\gamma=\mathsf{env}(\tau)([])$,
$?k=\mathsf{labs}(\tau)([])$, $\llbracket V\rrbracket\gamma=k$, $\gamma(z)=q$,
and $\sigma=\mathsf{pure}(\tau)([])$; implies

$\begin{array}[]{@{}r@{~}l@{}}~{}&\langle
pred~{}(\lambda\\_.\mathbf{do}\;\mathsf{Branch}~{}\langle\rangle)\mid\mathsf{env}^{\bot}(P)\mid([],\chi)::\kappa\rangle\\\
\longrightarrow~{}&{}^{\mathsf{steps}(\tau)([])}\\\ ~{}&\langle
z~{}V\mid\gamma[z\mapsto(\mathsf{env}^{\bot}(P),\lambda\\_.\mathbf{do}\;\mathsf{Branch}~{}\langle\rangle)]\mid(\sigma,\chi)::\kappa\rangle\end{array}$

  2. (2)

If $|bs|<n-1$ then for all $b\in\mathbb{B}$ and $W\in\mathrm{Val}$

$\begin{array}[]{@{}r@{~}l@{}}~{}&\langle\mathbf{return}\;W\mid\mathsf{env}^{\downarrow}_{b}(bs,P)\mid(\sigma,\chi)::\kappa\rangle\\\
\longrightarrow~{}&{}^{\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[b])}\\\
~{}&\langle z~{}V\mid\gamma[q\mapsto
q]\mid(\sigma^{\prime},\chi)::\kappa\rangle\end{array}$

where $\llbracket W\rrbracket(\mathsf{env}^{\downarrow}_{b}(bs,P))=b$,
$\sigma=\mathsf{pure}(\tau)(bs)$,
$z~{}V=\mathsf{comp}(\tau)(bs\mathbin{+\\!\\!+}[b])$,
$\gamma=\mathsf{env}(\tau)(bs\mathbin{+\\!\\!+}[b])$, $\gamma(z)=q$,
$?k=\mathsf{labs}(\tau)(bs\mathbin{+\\!\\!+}[b])$, $\llbracket
V\rrbracket\gamma=k$, and
$\sigma^{\prime}=\mathsf{pure}(\tau)(bs\mathbin{+\\!\\!+}[b])$; implies

$\begin{array}[]{@{}r@{~}l@{}}~{}&\langle\mathbf{return}\;W\mid\mathsf{env}^{\downarrow}_{b}(bs,P)\mid(\sigma,\chi)::\kappa\rangle\\\
\longrightarrow~{}&{}^{\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[b])}\\\
~{}&\langle
z~{}V\mid\gamma[z\mapsto(\mathsf{env}^{\bot}(P),\lambda\\_.\mathbf{do}\;\mathsf{Branch}~{}\langle\rangle)]\mid(\sigma^{\prime},\chi)::\kappa\rangle\end{array}$

  3. (3)

If $|bs|=n-1$ then for all $b\in\mathbb{B}$ and $W\in\mathrm{Val}$

$\begin{array}[]{@{}r@{~}l@{}}~{}&\langle\mathbf{return}\;W\mid\mathsf{env}^{\downarrow}_{b}(bs,P)\mid(\sigma,\chi)::\kappa\rangle\\\
\longrightarrow~{}&{}^{\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[b])}\\\
~{}&\langle\mathbf{return}\;W^{\prime}\mid\gamma[q\mapsto
q]\mid([],\chi)::\kappa\rangle\end{array}$

where $\llbracket W\rrbracket(\mathsf{env}^{\downarrow}_{b}(bs,P))=b$,
$\sigma=\mathsf{pure}(\tau)(bs)$,
$\mathbf{return}\;W^{\prime}=\mathsf{comp}(\tau)(bs\mathbin{+\\!\\!+}[b])$,
$\gamma=\mathsf{env}(\tau)(bs\mathbin{+\\!\\!+}[b])$,
$\mathord{!}b^{\prime}=\mathsf{labs}(\tau)(bs\mathbin{+\\!\\!+}[b])$, and
$\llbracket W^{\prime}\rrbracket\gamma=b^{\prime}$; implies

$\begin{array}[]{@{}r@{~}l@{}}~{}&\langle\mathbf{return}\;W\mid\mathsf{env}^{\downarrow}_{b}(bs,P)\mid(\sigma,\chi)::\kappa\rangle\\\
\longrightarrow~{}&{}^{\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[b])}\\\
~{}&\langle\mathbf{return}\;W^{\prime}\mid\gamma\mid([],\chi)::\kappa\rangle\end{array}$

###### Proof.

By unfolding Definition C.2. ∎

Let $\mathsf{control}:\mathsf{Conf}\rightharpoonup\mathrm{Val}$ denote a
partial function that hoists a value out of a given machine configuration,
that is

$\mathsf{control}(\langle
M\mid\gamma\mid\kappa\rangle)\mathrel{:=}\begin{cases}\llbracket
V\rrbracket\gamma&\text{if }M=\mathbf{return}\;V\\\
\bot&\text{otherwise}\end{cases}$

#### Notation

For a given predicate $P$ we write $\chi_{\mathsf{count}}(P)^{\mathbf{val}}$
to mean
$\chi_{\mathsf{count}}(P)^{\mathbf{val}}=(\emptyset[pred\mapsto\llbracket
P\rrbracket\emptyset],H_{\mathsf{count}})^{\mathbf{val}}=H_{\mathsf{count}}^{\mathbf{val}}$,
that is the projection of the success clause of $H_{\mathsf{count}}$.

The following lemma performs most of the heavy lifting for the proof of
Theorem 5.9.

###### Lemma C.5.

Suppose $P$ is an $n$-standard predicate, then for any list of booleans
$bs\in\mathsf{Addr}$ such that $|bs|\leq n$

$\begin{array}[]{@{}l}\mathsf{arrive}(bs,P)\leadsto^{T(bs,n)}\mathsf{depart}(bs,P),\end{array}$

and $\mathsf{control}(\mathsf{depart}(bs,P))\leq 2^{n-|bs|}$ with the function
$T$ defined as

$T(bs,n)=\begin{cases}9*(2^{n-|bs|}-1)+2^{n-|bs|+1}+\sum_{bs^{\prime}\in\mathsf{Addr}}^{1\leq|bs^{\prime}|\leq
n-|bs|}\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}bs^{\prime})&\text{if
}|bs|<n\\\ 2&\text{if }|bs|=n\end{cases}$

###### Proof.

By downward induction on $bs$.

Base step:

We have that $|bs|=n$. Since the predicate is $n$-standard we further have
that $n\geq 1$. We proceed by direct calculation.

$\begin{array}[]{@{}r@{~}l@{}}~{}&\mathsf{arrive}(bs,P)\\\
=~{}&\quad(\text{definition of $\mathsf{arrive}$ when $n=|bs|$})\\\
~{}&\langle\mathbf{return}\;W\mid\gamma\mid([],\chi_{\mathsf{count}}(P))::\mathsf{residual}(bs,P)\rangle\\\
\lx@intercol\text{where
}\begin{array}[t]{@{~}l}{}\lx@intercol\mathbf{return}\;W=\mathsf{comp}(\tau)(bs),\gamma=\mathsf{env}(\tau)(bs),!b=\mathsf{labs}(\tau)(bs),\text{
and }\llbracket W\rrbracket\gamma=b\end{array}\hfil\lx@intercol\\\
\longrightarrow~{}&\quad(\text{\text{{M-RetHandler}},
$\chi_{\mathsf{count}}(P)^{\mathbf{val}}=\\{\mathbf{val}~{}x\mapsto\cdots\\}$})\\\
~{}&\langle\mathbf{if}\;x\;\mathbf{then}\;\mathbf{return}\;1\;\mathbf{else}\;\mathbf{return}\;0\mid\gamma^{\prime}[x\mapsto\llbracket
b\rrbracket\gamma^{\prime}]\mid\mathsf{residual}(bs,P)\rangle\\\
\lx@intercol\text{where
}\gamma^{\prime}=\chi_{\mathsf{count}}(P).1\hfil\lx@intercol\end{array}$

The value $b$ can assume either of two values. We consider first the case
$b=\mathsf{true}$.

$\begin{array}[]{@{}r@{~}l@{}}=~{}&\quad(\text{assumption $b=\mathsf{true}$,
definition of $\llbracket-\rrbracket$ (2 value steps)})\\\
~{}&\langle\mathbf{if}\;x\;\mathbf{then}\;\mathbf{return}\;1\;\mathbf{else}\;\mathbf{return}\;0\mid\gamma^{\prime}[x\mapsto\mathsf{true}]\mid\mathsf{residual}(bs,P)\rangle\\\
\longrightarrow~{}&\quad(\text{\text{{M-Case-inl}} (and
$\log|\gamma^{\prime}[x\mapsto\mathsf{true}]|=1$ environment operations)})\\\
~{}&\langle\mathbf{return}\;1\mid\gamma^{\prime}[x\mapsto\mathsf{true}]\mid\mathsf{residual}(bs,P)\rangle\\\
=~{}&\quad(\text{definition of $\mathsf{depart}$ when $n=|bs|$})\\\
~{}&\mathsf{depart}(bs,P)\end{array}$

We have that $\mathsf{control}(\mathsf{depart}(bs,P))=1\leq 2^{0}=2^{n-|bs|}$.
Next, we consider the case when $b=\mathsf{false}$.

$\begin{array}[]{@{}r@{~}l@{}}=~{}&\quad(\text{assumption $b=\mathsf{false}$,
definition of $\llbracket-\rrbracket$ (2 value steps)})\\\
~{}&\langle\mathbf{if}\;x\;\mathbf{then}\;\mathbf{return}\;1\;\mathbf{else}\;\mathbf{return}\;0\mid\gamma^{\prime}[x\mapsto\mathsf{false}]\mid\mathsf{residual}(bs,P)\rangle\\\
\longrightarrow~{}&\quad(\text{\text{{M-Case-Inl}} (and
$\log|\gamma^{\prime}[x\mapsto\mathsf{false}]|=1$ environment operations)})\\\
~{}&\langle\mathbf{return}\;0\mid\gamma^{\prime}[x\mapsto\mathsf{false}]\mid\mathsf{residual}(bs,P)\rangle\\\
=~{}&\quad(\text{definition of $\mathsf{depart}$ when $n=|bs|$})\\\
~{}&\mathsf{depart}(bs,P)\end{array}$

Again, we have that $\mathsf{control}(\mathsf{depart}(bs,P))=0\leq
2^{0}=2^{n-|bs|}$.

#### Step analysis

In either case, the machine uses exactly 2 transitions. Thus we get that

$2=T(bs,n),\quad\text{when }|bs|=n$

Inductive step:

The induction hypothesis states that for all $b\in\mathbb{B}$ and $|bs|<n$

$\mathsf{arrive}(bs\mathbin{+\\!\\!+}[b],P)\leadsto^{T(bs\mathbin{+\\!\\!+}[b],n)}\mathsf{depart}(bs\mathbin{+\\!\\!+}[b],P),$

such that $\mathsf{control}(\mathsf{depart}(bs\mathbin{+\\!\\!+}[b],P))\leq
2^{n-|bs\mathbin{+\\!\\!+}[b]|}$. We proceed by direct calculation.

$\begin{array}[]{@{}r@{~}l@{}}~{}&\mathsf{arrive}(bs,P)\\\
=~{}&\quad(\text{definition of $\mathsf{arrive}$ when $n<|bs|$})\\\
~{}&\langle
z~{}V\mid\gamma\mid(\sigma,\chi_{\mathsf{count}}(P))::\mathsf{residual}(bs,P)\rangle\\\
\lx@intercol\text{where }\begin{array}[t]{@{~}l}{}\lx@intercol
z~{}V=\mathsf{comp}(\tau)(bs),\gamma=\mathsf{env}(\tau)(bs)[z\mapsto(\mathsf{env}^{\bot}(P),\lambda\\_.\mathbf{do}\;\mathsf{Branch}~{}\langle\rangle)],\\\
{}\lx@intercol?k=\mathsf{labs}(\tau)(bs),\llbracket V\rrbracket\gamma=k,\text{
and }\sigma=\mathsf{pure}(\tau)(bs)\end{array}\hfil\lx@intercol\\\
\longrightarrow~{}&\quad(\text{\text{{M-App}}})\\\
~{}&\langle\mathbf{do}\;\mathsf{Branch}~{}\langle\rangle\mid\gamma^{\prime}[\\_\mapsto
k]\mid(\sigma,\chi_{\mathsf{count}}(P))::\mathsf{residual}(bs,P)\rangle\\\
\lx@intercol\text{where
}\gamma^{\prime}=\mathsf{env}^{\bot}(P)\hfil\lx@intercol\\\
\longrightarrow~{}&\quad(\text{\text{{M-Handle-Op}},
$\chi_{\mathsf{count}}(P)^{\mathsf{Branch}}=\\{\mathsf{Branch}~{}\langle\rangle~{}r\mapsto\cdots\\}$})\\\
~{}&\left\langle\begin{array}[m]{@{}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}\mid\gamma[r\mapsto\llbracket(\sigma,\chi_{\mathsf{count}}(P))\rrbracket\gamma]\mid\mathsf{residual}(bs,P)\right\rangle\\\
\lx@intercol\text{where }\gamma=\mathsf{env}^{\bot}(P)\hfil\lx@intercol\\\
=~{}&\quad(\text{definition of $\llbracket-\rrbracket$ (1 value step)})\\\
~{}&\left\langle\begin{array}[m]{@{}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}\mid\gamma^{\prime}\mid\mathsf{residual}(bs,P)\right\rangle\\\
\lx@intercol\text{where
}\gamma^{\prime}=\gamma[r\mapsto(\sigma,\chi_{\mathsf{count}}(P))]\hfil\lx@intercol\\\
\longrightarrow~{}&\quad(\text{\text{{M-Let}}, definition of
$\mathsf{residual}$})\\\ ~{}&\langle
r~{}\mathsf{true}\mid\gamma^{\prime}\mid\mathsf{residual}(bs\mathbin{+\\!\\!+}[\mathsf{true}]bs,P)\rangle\\\
\longrightarrow~{}&\quad(\text{\text{{M-Resume}}, $\llbracket
r\rrbracket\gamma^{\prime}=(\sigma,\chi_{\mathsf{count}}(P))$
($\log|\gamma^{\prime}|=1$ environment operations)})\\\
~{}&\langle\mathbf{return}\;\mathsf{true}\mid\gamma^{\prime}\mid(\sigma,\chi_{\mathsf{count}}(P))::\mathsf{residual}(bs\mathbin{+\\!\\!+}[\mathsf{true}],P)\rangle\end{array}$

We now use Lemma C.4 to reason about the progress of the predicate computation
$\sigma$. There are two cases consider, either $1+|bs|<n$ or $1+|bs|=n$.

Case:

$1+|bs|<n$. We obtain the following internal node configuration.

$\begin{array}[]{@{}r@{~}l@{}}\longrightarrow~{}&{}^{\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{true}])}\quad(\text{by
Lemma~{}\ref{lem:inductive-lem-aux}})\\\ ~{}&\langle
z~{}V\mid\gamma^{\prime\prime}\mid(\sigma^{\prime},\chi_{\mathsf{count}}(P))::\mathsf{residual}(bs\mathbin{+\\!\\!+}[\mathsf{true}],P)\rangle\\\
\lx@intercol\text{where }\begin{array}[t]{@{~}l}{}\lx@intercol
z~{}V=\mathsf{comp}(\tau)(bs),\gamma^{\prime\prime}=\mathsf{env}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{true}])[z\mapsto(\mathsf{env}^{\bot}(P),\lambda\\_.\mathbf{do}\;\mathsf{Branch}~{}\langle\rangle)],\\\
{}\lx@intercol?k=\mathsf{labs}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{true}]),\llbracket
V\rrbracket\gamma^{\prime\prime}=k,\text{ and
}\sigma^{\prime}=\mathsf{pure}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{true}])\end{array}\hfil\lx@intercol\\\
=~{}&\quad(\text{definition of $\mathsf{arrive}$ when $1+|bs|<n$})\\\
~{}&\mathsf{arrive}(bs\mathbin{+\\!\\!+}[\mathsf{true}],P)\\\
\longrightarrow~{}&{}^{T(bs\mathbin{+\\!\\!+}[\mathsf{true}],n)}\quad(\text{induction
hypothesis})\\\ ~{}&\mathsf{depart}(bs\mathbin{+\\!\\!+}[\mathsf{true}],P)\\\
=~{}&\quad(\text{definition of $\mathsf{depart}$ when $1+|bs|<n$})\\\
~{}&\langle\mathbf{return}\;i\mid\gamma\mid\mathsf{residual}(bs\mathbin{+\\!\\!+}[\mathsf{true}],P)\rangle\\\
\lx@intercol\text{where
}i=c(bs\mathbin{+\\!\\!+}[\mathsf{true}]\mathbin{+\\!\\!+}[\mathsf{true}])+c(bs\mathbin{+\\!\\!+}[\mathsf{true}]\mathbin{+\\!\\!+}[\mathsf{false}])\text{
and
}\gamma=\mathsf{env}^{\uparrow}_{\mathsf{false}}(bs\mathbin{+\\!\\!+}[\mathsf{true}],P)\hfil\lx@intercol\\\
=~{}&\quad(\text{definition of $\mathsf{residual}$ and
$\mathsf{purecont}$})\\\
~{}&\langle\mathbf{return}\;i\mid\gamma\mid[((\gamma^{\prime},x_{\mathsf{true}},\mathbf{let}\;x_{\mathsf{false}}\leftarrow
r~{}\mathsf{false}\;\mathbf{in}\;x_{\mathsf{true}}+x_{\mathsf{false}})::\mathsf{purecont}(bs,P),\chi_{id})]\rangle\\\
\lx@intercol\text{where
}\gamma^{\prime}=\mathsf{env}^{\downarrow}_{\mathsf{true}}(bs,P)\hfil\lx@intercol\\\
\longrightarrow~{}&\quad(\text{\text{{M-RetCont}}})\\\
~{}&\langle\mathbf{let}\;x_{\mathsf{false}}\leftarrow
r~{}\mathsf{false}\;\mathbf{in}\;x_{\mathsf{true}}+x_{\mathsf{false}}\mid\gamma^{\prime\prime}\mid[(\mathsf{purecont}(bs,P),\chi_{id})]\rangle\\\
\lx@intercol\text{where
}\gamma^{\prime\prime}=\gamma^{\prime}[x_{\mathsf{true}}\mapsto\llbracket
i\rrbracket\gamma^{\prime}]\hfil\lx@intercol\\\
\longrightarrow~{}&\quad(\text{\text{{M-Let}}})\\\ ~{}&\langle
r~{}\mathsf{false}\mid\gamma^{\prime\prime}\mid[((\gamma^{\prime\prime},x_{\mathsf{false}},x_{\mathsf{true}}+x_{\mathsf{false}})::\mathsf{purecont}(bs,P),\chi_{id})]\rangle\end{array}$
$\begin{array}[]{@{}r@{~}l@{}}=~{}&\quad(\text{definition of
$\mathsf{purecont}$ and $\mathsf{residual}$})\\\ ~{}&\langle
r~{}\mathsf{false}\mid\gamma^{\prime\prime}\mid\mathsf{residual}(bs\mathbin{+\\!\\!+}[\mathsf{false}],P)\rangle\\\
\longrightarrow~{}&\quad(\text{\text{{M-Resume}}})\\\
~{}&\langle\mathbf{return}\;\mathsf{false}\mid\gamma^{\prime\prime}\mid(\sigma,\chi_{\mathsf{count}}(P))::\mathsf{residual}(bs\mathbin{+\\!\\!+}[\mathsf{false}],P)\rangle\\\
\lx@intercol\text{where }\sigma=\mathsf{pure}(\tau)(bs)\hfil\lx@intercol\\\
\longrightarrow~{}&{}^{\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}])}\quad(\text{by
Lemma~{}\ref{lem:inductive-lem-aux}})\\\ ~{}&\langle
z~{}V\mid\gamma\mid(\sigma,\chi_{\mathsf{count}}(P))::\mathsf{residual}(bs\mathbin{+\\!\\!+}[\mathsf{false}],P)\rangle\\\
\lx@intercol\text{where }\begin{array}[t]{@{~}l}{}\lx@intercol
z~{}V=\mathsf{comp}(\tau)(bs),\gamma=\mathsf{env}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}])[q\mapsto(\mathsf{env}^{\bot}(P),\lambda\\_.\mathbf{do}\;\mathsf{Branch}~{}\langle\rangle)],\\\
{}\lx@intercol?k=\mathsf{labs}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}]),\llbracket
V\rrbracket\gamma=k,\text{ and
}\sigma=\mathsf{pure}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}])\end{array}\hfil\lx@intercol\\\
=~{}&\quad(\text{definition of $\mathsf{arrive}$ when $1+|bs|<n$})\\\
~{}&\mathsf{arrive}(bs\mathbin{+\\!\\!+}[\mathsf{false}],P)\\\
\longrightarrow~{}&{}^{T(bs\mathbin{+\\!\\!+}[\mathsf{false}],n)}\quad(\text{induction
hypothesis})\\\ ~{}&\mathsf{depart}(bs\mathbin{+\\!\\!+}[\mathsf{false}],P)\\\
=~{}&\quad(\text{definition of $\mathsf{depart}$ when $1+|bs|<n$})\\\
~{}&\langle\mathbf{return}\;j\mid\gamma\mid\mathsf{residual}(bs\mathbin{+\\!\\!+}[\mathsf{false}],P)\rangle\\\
\lx@intercol\text{where
}j=c(bs\mathbin{+\\!\\!+}[\mathsf{false}]\mathbin{+\\!\\!+}[\mathsf{true}])+c(bs\mathbin{+\\!\\!+}[\mathsf{false}]\mathbin{+\\!\\!+}[\mathsf{false}])\text{
and
}\gamma=\mathsf{env}^{\uparrow}_{\mathsf{false}}(bs\mathbin{+\\!\\!+}[\mathsf{false}],P)\hfil\lx@intercol\\\
=~{}&\quad(\text{definition of $\mathsf{residual}$ and
$\mathsf{purecont}$})\\\
~{}&\langle\mathbf{return}\;j\mid\gamma\mid[((\gamma^{\prime\prime},x_{\mathsf{false}},x_{\mathsf{true}}+x_{\mathsf{false}})::\mathsf{purecont}(bs,P),\chi_{id})]\rangle\\\
\longrightarrow~{}&\quad(\text{\text{{M-RetCont}}})\\\ ~{}&\langle
x_{\mathsf{true}}+x_{\mathsf{false}}\mid\gamma^{\prime\prime}[x_{\mathsf{false}}\mapsto\llbracket
j\rrbracket\gamma^{\prime\prime}]\mid\mathsf{residual}(bs,P)\rangle\\\
\longrightarrow~{}&\quad(\text{\text{{M-Plus}}})\\\
~{}&\langle\mathbf{return}\;m\mid\gamma^{\prime\prime}[x_{\mathsf{false}}\mapsto\llbracket
j\rrbracket\gamma^{\prime\prime}]\mid\mathsf{residual}(bs,P)\rangle\\\
~{}&\text{where}\begin{array}[t]{@{~}l@{~}l}{}\lx@intercol
m\hfil~{}&=c(bs\mathbin{+\\!\\!+}[\mathsf{true}]\mathbin{+\\!\\!+}[\mathsf{true}])+c(bs\mathbin{+\\!\\!+}[\mathsf{true}]\mathbin{+\\!\\!+}[\mathsf{false}])\\\
{}\lx@intercol\hfil~{}&+c(bs\mathbin{+\\!\\!+}[\mathsf{false}]\mathbin{+\\!\\!+}[\mathsf{true}])+c(bs\mathbin{+\\!\\!+}[\mathsf{false}]\mathbin{+\\!\\!+}[\mathsf{false}])\\\
{}\lx@intercol\hfil~{}&=c(bs\mathbin{+\\!\\!+}[\mathsf{true}])+c(bs\mathbin{+\\!\\!+}[\mathsf{false}])=c(bs)\leq
2^{n-|bs|}\end{array}\\\ =~{}&\quad(\text{definition of $\mathsf{depart}$ when
$|bs|<n$})\\\ ~{}&\mathsf{depart}(bs,P)\end{array}$

#### Step analysis

The total number of machine steps is given by

$\begin{array}[]{@{}r@{~}l@{}}~{}&9+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{true}])+T(bs\mathbin{+\\!\\!+}[\mathsf{true}],n)+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}])+T(bs\mathbin{+\\!\\!+}[\mathsf{false}],n)\\\
=~{}&\quad(\text{reorder})\\\
~{}&9+T(bs\mathbin{+\\!\\!+}[\mathsf{true}],n)+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}])+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{true}])+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}])\\\
=~{}&\quad(\text{definition of $T$})\\\
~{}&9+9*(2^{n-|bs\mathbin{+\\!\\!+}[\mathsf{true}]|}-1)+9*(2^{n-|bs\mathbin{+\\!\\!+}[\mathsf{false}]|}-1)+2^{n-|bs\mathbin{+\\!\\!+}[\mathsf{true}]|+1}+2^{n-|bs\mathbin{+\\!\\!+}[\mathsf{false}]|+1}\\\
~{}&+\displaystyle\sum_{bs^{\prime}\in\mathsf{Addr}}^{1\leq|bs^{\prime}|\leq
n-|bs\mathbin{+\\!\\!+}[\mathsf{true}]|}\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{true}]\mathbin{+\\!\\!+}bs^{\prime})+\displaystyle\sum_{bs^{\prime}\in\mathsf{Addr}}^{1\leq|bs^{\prime}|\leq
n-|bs\mathbin{+\\!\\!+}[\mathsf{false}]|}\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}]\mathbin{+\\!\\!+}bs^{\prime})\\\
~{}&+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{true}])+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}])\\\
=~{}&\quad(\text{simplify})\\\
~{}&9+9*(2^{n-|bs\mathbin{+\\!\\!+}[\mathsf{true}]|}-1)+9*(2^{n-|bs\mathbin{+\\!\\!+}[\mathsf{false}]|}-1)+2^{n-|bs|+1}\\\
~{}&+\displaystyle\sum_{bs^{\prime}\in\mathsf{Addr}}^{1\leq|bs^{\prime}|\leq
n-|bs\mathbin{+\\!\\!+}[\mathsf{true}]|}\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{true}]\mathbin{+\\!\\!+}bs^{\prime})+\displaystyle\sum_{bs^{\prime}\in\mathsf{Addr}}^{1\leq|bs^{\prime}|\leq
n-|bs\mathbin{+\\!\\!+}[\mathsf{false}]|}\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}]\mathbin{+\\!\\!+}bs^{\prime})\\\
~{}&+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{true}])+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}])\\\
\end{array}$ $\begin{array}[]{@{}r@{~}l@{}}=~{}&\quad(\text{merge sums})\\\
~{}&9+9*(2^{n-|bs\mathbin{+\\!\\!+}[\mathsf{true}]|}-1)+9*(2^{n-|bs\mathbin{+\\!\\!+}[\mathsf{false}]|}-1)+2^{n-|bs|+1}\\\
~{}&+\left(\displaystyle\sum_{bs^{\prime}\in\mathsf{Addr}}^{2\leq|bs^{\prime}|\leq
n-|bs|}\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}bs^{\prime})\right)+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{true}])+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}])\\\
=~{}&\quad(\text{rewrite binary sum})\\\
~{}&9+9*(2^{n-|bs\mathbin{+\\!\\!+}[\mathsf{true}]|}-1)+9*(2^{n-|bs\mathbin{+\\!\\!+}[\mathsf{false}]|}-1)+2^{n-|bs|+1}\\\
~{}&+\displaystyle\sum_{bs^{\prime}\in\mathsf{Addr}}^{2\leq|bs^{\prime}|\leq
n-|bs|}\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}bs^{\prime})+\displaystyle\sum_{bs^{\prime}\in\mathsf{Addr}}^{1\leq|bs^{\prime}|\leq
1}\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}bs^{\prime})\\\
=~{}&\quad(\text{merge sums})\\\
~{}&9+9*(2^{n-|bs\mathbin{+\\!\\!+}[\mathsf{true}]|}-1)+9*(2^{n-|bs\mathbin{+\\!\\!+}[\mathsf{true}]|}-1)+2^{n-|bs|+1}+\displaystyle\sum_{bs^{\prime}\in\mathsf{Addr}}^{1\leq|bs^{\prime}|\leq
n-|bs|}\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}bs^{\prime})\\\
=~{}&\quad(\text{factoring})\\\
~{}&9+2*9*(2^{n-|bs|-1}-1)+2^{n-|bs|+1}+\displaystyle\sum_{bs^{\prime}\in\mathsf{Addr}}^{1\leq|bs^{\prime}|\leq
n-|bs|}\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}bs^{\prime})\\\
=~{}&\quad(\text{distribute})\\\
~{}&9+9*(2^{n-|bs|}-2)+2^{n-|bs|+1}+\displaystyle\sum_{bs^{\prime}\in\mathsf{Addr}}^{1\leq|bs^{\prime}|\leq
n-|bs|}\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}bs^{\prime})\\\
=~{}&\quad(\text{distribute})\\\
~{}&9+9*2^{n-|bs|}-18+2^{n-|bs|+1}+\displaystyle\sum_{bs^{\prime}\in\mathsf{Addr}}^{1\leq|bs^{\prime}|\leq
n-|bs|}\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}bs^{\prime})\\\
=~{}&\quad(\text{simplify})\\\
~{}&9*2^{n-|bs|}-9+2^{n-|bs|+1}+\displaystyle\sum_{bs^{\prime}\in\mathsf{Addr}}^{1\leq|bs^{\prime}|\leq
n-|bs|}\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}bs^{\prime})\\\
=~{}&\quad(\text{factoring})\\\
~{}&9*(2^{n-|bs|}-1)+2^{n-|bs|+1}+\displaystyle\sum_{bs^{\prime}\in\mathsf{Addr}}^{1\leq|bs^{\prime}|\leq
n-|bs|}\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}bs^{\prime})\\\
=~{}&\quad(\text{definition of $T$})\\\ ~{}&T(bs,n)\end{array}$

Case:

$1+|bs|=n$. We obtain the following configuration.

$\begin{array}[]{@{}r@{~}l@{}}\longrightarrow~{}&{}^{\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{true}])}\quad(\text{by
Lemma~{}\ref{lem:inductive-lem-aux}})\\\
~{}&\langle\mathbf{return}\;W\mid\gamma^{\prime\prime}\mid([],\chi_{\mathsf{count}}(P))::\mathsf{residual}(bs\mathbin{+\\!\\!+}[\mathsf{true}],P)\rangle\\\
\lx@intercol\text{where
}\begin{array}[t]{@{~}l}{}\lx@intercol\mathbf{return}\;W=\mathsf{comp}(\tau)(s\mathbin{+\\!\\!+}[\mathsf{true}]),!b=\mathsf{labs}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{true}]),\\\
{}\lx@intercol\gamma^{\prime\prime}=\mathsf{env}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{true}]),\text{
and }\llbracket
W\rrbracket\gamma^{\prime\prime}=b\end{array}\hfil\lx@intercol\\\
=~{}&\quad(\text{definition of $\mathsf{arrive}$ when $1+|bs|=n$})\\\
~{}&\mathsf{arrive}(bs\mathbin{+\\!\\!+}[\mathsf{true}],P)\\\
\longrightarrow~{}&{}^{T(bs\mathbin{+\\!\\!+}[\mathsf{true}],n)}\quad(\text{induction
hypothesis})\\\ ~{}&\mathsf{depart}(bs\mathbin{+\\!\\!+}[\mathsf{true}],P)\\\
=~{}&\quad(\text{definition of $\mathsf{depart}$ when $1+|bs|=n$})\\\
~{}&\langle\mathbf{return}\;i\mid\gamma\mid\mathsf{residual}(bs\mathbin{+\\!\\!+}[\mathsf{true}],P)\rangle\\\
\lx@intercol\text{where }i=c(bs\mathbin{+\\!\\!+}[\mathsf{true}])\leq
2^{n-|bs\mathbin{+\\!\\!+}[\mathsf{true}]|}=1\text{ and
}\gamma=\mathsf{env}^{\bot}(P)\hfil\lx@intercol\\\ =~{}&\quad(\text{definition
of $\mathsf{residual}$ and $\mathsf{purecont}$})\\\
~{}&\langle\mathbf{return}\;i\mid\gamma\mid[((\gamma^{\prime},x_{\mathsf{true}},\mathbf{let}\;x_{\mathsf{false}}\leftarrow
r~{}\mathsf{false}\;\mathbf{in}\;x_{\mathsf{true}}+x_{\mathsf{false}})::\mathsf{purecont}(bs,P),\chi_{id})]\rangle\\\
\longrightarrow~{}&\quad(\text{\text{{M-RetCont}}})\\\
~{}&\langle\mathbf{let}\;x_{\mathsf{false}}\leftarrow
r~{}\mathsf{false}\;\mathbf{in}\;x_{\mathsf{true}}+x_{\mathsf{false}}\mid\gamma^{\prime}[x_{\mathsf{true}}\mapsto\llbracket
i\rrbracket\gamma^{\prime}]\mid[(\mathsf{purecont}(bs,P),\chi_{id})]\rangle\\\
=~{}&\quad(\text{definition of $\llbracket-\rrbracket$ (1 value step)})\\\
~{}&\langle\mathbf{let}\;x_{\mathsf{false}}\leftarrow
r~{}\mathsf{false}\;\mathbf{in}\;x_{\mathsf{true}}+x_{\mathsf{false}}\mid\gamma^{\prime\prime}\mid[(\mathsf{purecont}(bs,P),\chi_{id})]\rangle\\\
\lx@intercol\text{where
}\gamma^{\prime\prime}=\gamma^{\prime}[x_{\mathsf{true}}\mapsto
i]\hfil\lx@intercol\\\ \longrightarrow~{}&\quad(\text{\text{{M-Let}},
definition of $\mathsf{residual}$})\\\ ~{}&\langle
r~{}\mathsf{false}\mid\gamma^{\prime\prime}\mid\mathsf{residual}(bs\mathbin{+\\!\\!+}[\mathsf{false}],P)\rangle\\\
\longrightarrow~{}&\quad(\text{\text{{M-Resume}}})\\\
~{}&\langle\mathbf{return}\;\mathsf{false}\mid\gamma^{\prime\prime}\mid(\sigma,\chi_{\mathsf{count}}(P))::\mathsf{residual}(bs\mathbin{+\\!\\!+}[\mathsf{false}],P)\rangle\\\
\lx@intercol\text{where }\sigma=\mathsf{pure}(\tau)(bs)\hfil\lx@intercol\\\
\longrightarrow~{}&{}^{\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}])}\quad(\text{by
Lemma~{}\ref{lem:inductive-lem-aux}})\\\
~{}&\langle\mathbf{return}\;W\mid\gamma\mid([],\chi_{\mathsf{count}}(P))::\mathsf{residual}(bs\mathbin{+\\!\\!+}[\mathsf{false}],P)\rangle\\\
\lx@intercol\text{where
}\begin{array}[t]{@{~}l}{}\lx@intercol\mathbf{return}\;W=\mathsf{comp}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}]),!b=\mathsf{labs}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}]),\\\
{}\lx@intercol\gamma=\mathsf{env}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}]),\text{
and }\llbracket W\rrbracket\gamma=b\end{array}\hfil\lx@intercol\\\
=~{}&\quad(\text{definition of $\mathsf{arrive}$ when $1+|bs|=n$})\\\
~{}&\mathsf{arrive}(bs\mathbin{+\\!\\!+}[\mathsf{false}],P)\\\
\longrightarrow~{}&{}^{T(bs\mathbin{+\\!\\!+}[\mathsf{false}],n)}\quad(\text{induction
hypothesis})\\\ ~{}&\mathsf{depart}(bs\mathbin{+\\!\\!+}[\mathsf{false}],P)\\\
=~{}&\quad(\text{definition of $\mathsf{depart}$ when $1+|bs|=n$})\\\
~{}&\langle\mathbf{return}\;j\mid\gamma\mid\mathsf{residual}(bs\mathbin{+\\!\\!+}[\mathsf{false}],P)\rangle\\\
\lx@intercol\text{where }j=c(bs\mathbin{+\\!\\!+}[\mathsf{false}])\leq
2^{n-|bs\mathbin{+\\!\\!+}[\mathsf{false}]|}=1\text{ and
}\gamma=\mathsf{env}^{\bot}(P)\hfil\lx@intercol\\\ =~{}&\quad(\text{definition
of $\mathsf{residual}$ and $\mathsf{purecont}$})\\\
~{}&\langle\mathbf{return}\;j\mid\gamma\mid[((\gamma^{\prime},x_{\mathsf{false}},x_{\mathsf{true}}+x_{\mathsf{false}})::\mathsf{purecont}(bs,P),\chi_{id})]\rangle\\\
\lx@intercol\text{where
}\gamma^{\prime}=\mathsf{env}^{\downarrow}_{\mathsf{false}}(bs,P)\hfil\lx@intercol\\\
\longrightarrow~{}&\quad(\text{\text{{M-RetCont}}})\\\ ~{}&\langle
x_{\mathsf{true}}+x_{\mathsf{false}}\mid\gamma^{\prime\prime}\mid[(\mathsf{purecont}(bs,P),\chi_{id})]\rangle\\\
\lx@intercol\text{where
}\gamma^{\prime\prime}=\gamma^{\prime}[x_{\mathsf{false}}\mapsto\llbracket
j\rrbracket\gamma^{\prime}]=\gamma^{\prime}[x_{\mathsf{false}}\mapsto
j]\hfil\lx@intercol\\\ \longrightarrow~{}&\quad(\text{\text{{M-Plus}}})\\\
~{}&\langle\mathbf{return}\;m\mid\gamma^{\prime\prime}\mid[(\mathsf{purecont}(bs,P),\chi_{id})]\rangle\\\
\lx@intercol\text{where
}m=c(bs\mathbin{+\\!\\!+}[\mathsf{true}])+c(bs\mathbin{+\\!\\!+}[\mathsf{false}])\leq
2^{n-|bs|}\hfil\lx@intercol\\\ =~{}&\quad(\text{definition of
$\mathsf{residual}$ and $\mathsf{depart}$ when $|bs|<n$})\\\
~{}&\mathsf{depart}(bs,P)\end{array}$

#### Step analysis

The total number of machine steps is given by

$\begin{array}[]{@{}r@{~}l@{}}~{}&9+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{true}])+T(bs\mathbin{+\\!\\!+}[\mathsf{true}],n)+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}])+T(bs\mathbin{+\\!\\!+}[\mathsf{false}],n)\\\
=~{}&\quad(\text{reorder})\\\
~{}&9+T(bs\mathbin{+\\!\\!+}[\mathsf{true}],n)+T(bs\mathbin{+\\!\\!+}[\mathsf{false}],n)+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{true}])+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}])\\\
=~{}&\quad(\text{definition of $T$ when $|bs|+1=n$})\\\
~{}&9+2+2+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{true}])+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}])\\\
=~{}&\quad(\text{simplify})\\\
~{}&9+2^{2}+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{true}])+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}])\\\
=~{}&\quad(\text{rewrite $2=n-|bs|+1$})\\\
~{}&9+2^{n-|bs|+1}+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{true}])+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}])\\\
=~{}&\quad(\text{multiply by $1$})\\\
~{}&9*(2^{n-|bs|}-1)+2^{n-|bs|+1}+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{true}])+\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}[\mathsf{false}])\\\
=~{}&\quad(\text{rewrite binary sum})\\\
~{}&9*(2^{n-|bs|}-1)+2^{n-|bs|}+\displaystyle\sum_{bs^{\prime}\in\mathsf{Addr}}^{1\leq|bs^{\prime}|\leq
n-|bs|}\mathsf{steps}(\tau)(bs\mathbin{+\\!\\!+}bs^{\prime})\\\
=~{}&\quad(\text{definition of $T$})\\\ ~{}&T(bs,n)\end{array}$

∎

The following theorem is a copy of Theorem 5.9.

###### Theorem C.6.

For all $n>0$ and any $n$-standard predicate $P$ it holds that

  1. (1)

The program $\mathsf{effcount}$ is a generic count program

  2. (2)

The runtime complexity of $\mathsf{effcount}~{}P$ is given by the following
formula:

$\displaystyle\sum_{bs\in\mathsf{Addr}}^{|bs|\leq
n}\mathsf{steps}(\mathcal{T}(P))(bs)+\mathcal{O}(2^{n})$

###### Proof.

The proof begins by direct calculation.

$\begin{array}[]{@{}r@{~}l@{}}~{}&\langle\mathsf{effcount}\,P\mid\emptyset\mid[([],\chi_{id})]\rangle\\\
=~{}&\quad(\text{definition of $\mathsf{residual}$})\\\
~{}&\langle\mathsf{effcount}\,P\mid\emptyset\mid\mathsf{residual}([],P)\rangle\\\
\longrightarrow~{}&\quad(\text{\text{{M-App}},
$\llbracket\mathsf{effcount}\rrbracket\emptyset=(\emptyset,\lambda
pred.\cdots)$})\\\
~{}&\langle\mathbf{handle}\;pred~{}(\lambda\\_.\mathbf{do}\;\mathsf{Branch}~{}\langle\rangle)\;\mathbf{with}\;H_{\mathsf{count}}\mid\gamma\mid\mathsf{residual}([],P)\rangle\\\
\lx@intercol\text{where }\gamma=\mathsf{env}^{\bot}(P)\hfil\lx@intercol\\\
\longrightarrow~{}&\quad(\text{\text{{M-Handle}}})\\\ ~{}&\langle
pred~{}(\lambda\\_.\mathbf{do}\;\mathsf{Branch}~{}\langle\rangle)\mid\gamma\mid([],(\gamma,H_{\mathsf{count}}))::\mathsf{residual}([],P)\rangle\\\
=~{}&\quad(\text{definition of $\chi_{\mathsf{count}}$})\\\ ~{}&\langle
pred~{}(\lambda\\_.\mathbf{do}\;\mathsf{Branch}~{}\langle\rangle)\mid\gamma\mid([],\chi_{\mathsf{count}}(P))::\mathsf{residual}([],P)\rangle\\\
\longrightarrow~{}&{}^{\mathsf{steps}(\tau)([])}\quad(\text{by
Lemma~{}\ref{lem:inductive-lem-aux}})\\\ ~{}&\langle
z~{}V\mid\gamma^{\prime}\mid(\sigma,\chi_{\mathsf{count}}(P))::\mathsf{residual}([],P)\rangle\\\
\lx@intercol\text{where }\begin{array}[t]{@{~}l}{}\lx@intercol
z~{}V=\mathsf{comp}(\tau)(bs),\gamma^{\prime}=\mathsf{env}(\tau)([])[q\mapsto(\mathsf{env}^{\bot}(P),\lambda\\_.\mathbf{do}\;\mathsf{Branch}~{}\langle\rangle)],\\\
{}\lx@intercol?k=\mathsf{labs}(\tau)([]),\llbracket
V\rrbracket\gamma^{\prime}=k,\text{ and
}\sigma=\mathsf{pure}(\tau)([])\end{array}\hfil\lx@intercol\\\ \end{array}$
$\begin{array}[]{@{}r@{~}l@{}}=~{}&\quad(\text{definition of
$\mathsf{arrive}$})\\\ ~{}&\mathsf{arrive}([],P)\\\
\longrightarrow~{}&{}^{T([],n)}\quad(\text{by Lemma~{}\ref{lem:inductive-bit-
of-thm1}})\\\ ~{}&\mathsf{depart}([],P)\\\ =~{}&\quad(\text{definition of
$\mathsf{depart}$})\\\
~{}&\langle\mathbf{return}\;m\mid\gamma\mid\mathsf{residual}([],P)\rangle\\\
\lx@intercol\text{where }\gamma=\mathsf{env}^{\bot}(P)\text{ and }m=c([])\leq
2^{n-|bs|}=2^{n}\hfil\lx@intercol\\\ =~{}&\quad(\text{definition of
$\mathsf{residual}$})\\\
~{}&\langle\mathbf{return}\;m\mid\gamma\mid[([],\chi_{id})]\rangle\\\
\longrightarrow~{}&\quad(\text{\text{{M-Handle-Ret}},
$H_{id}^{\mathsf{val}}=\\{\mathbf{val}~{}x\mapsto\mathbf{return}\;x\\}$})\\\
~{}&\langle\mathbf{return}\;x\mid\emptyset[x\mapsto
m]\mid[]\rangle\end{array}$

#### Analysis

The machine yields the value $m$. By Lemma C.5 it follows that $m\leq
2^{n-|bs|}=2^{n-|[]|}=2^{n}$. Furthermore, the total number of transitions
used were

$\begin{array}[]{@{}r@{~}l@{}}~{}&3+\mathsf{steps}(\tau)([])+T([],n)\\\
=~{}&\quad(\text{definition of $T$})\\\
~{}&3+\mathsf{steps}(\tau)([])+9*2^{n}+2^{n+1}+\displaystyle\sum_{bs^{\prime}\in\mathbb{B}^{\ast}}^{1\leq|bs^{\prime}|\leq
n}\mathsf{steps}(\tau)(bs^{\prime})\\\ =~{}&\quad(\text{simplify})\\\
~{}&3+\mathsf{steps}(\tau)([])+9*2^{n}+2^{n+1}+\displaystyle\sum_{bs^{\prime}\in\mathbb{B}^{\ast}}^{1\leq|bs^{\prime}|\leq
n}\mathsf{steps}(\tau)(bs^{\prime})\\\ =~{}&\quad(\text{reorder})\\\
~{}&3+\left(\displaystyle\sum_{bs^{\prime}\in\mathbb{B}^{\ast}}^{1\leq|bs^{\prime}|\leq
n}\mathsf{steps}(\tau)(bs^{\prime})\right)+\mathsf{steps}(\tau)([])+9*2^{n}+2^{n+1}\\\
=~{}&\quad(\text{rewrite as unary sum})\\\
~{}&3+\left(\displaystyle\sum_{bs^{\prime}\in\mathbb{B}^{\ast}}^{1\leq|bs^{\prime}|\leq
n}\mathsf{steps}(\tau)(bs^{\prime})+\displaystyle\sum_{bs^{\prime}\in\mathsf{Addr}}^{0\leq|bs^{\prime}|\leq
0}\mathsf{steps}(\tau)(bs^{\prime})\right)+9*2^{n}+2^{n+1}\\\
=~{}&\quad(\text{merge sums})\\\
~{}&3+\left(\displaystyle\sum_{bs^{\prime}\in\mathbb{B}^{\ast}}^{0\leq|bs^{\prime}|\leq
n}\mathsf{steps}(\tau)(bs^{\prime})\right)+9*2^{n}+2^{n+1}\\\
=~{}&\quad(\text{definition of $\mathcal{O}$})\\\
~{}&\left(\displaystyle\sum_{bs^{\prime}\in\mathbb{B}^{\ast}}^{0\leq|bs^{\prime}|\leq
n}\mathsf{steps}(\tau)(bs^{\prime})\right)+\mathcal{O}(2^{n})\end{array}$

∎

##  Appendix D Berger Count

Here we present the $\mathsf{BergerCount}$ program alluded to in Section 6, in
order to fill out our overall picture of the relationship between language
expressivity and potential program efficiency.

Berger’s original program (Berger, 1990) introduced a remarkable search
operator for predicates on _infinite_ streams of booleans, and has played an
important role in higher-order computability theory (Longley and Normann,
2015). What we wish to highlight here is that if one applies the algorithm to
predicates on _finite_ boolean vectors, the resulting program, though no
longer interesting from a computability perspective, still holds some interest
from a complexity standpoint: indeed, it yields what seems to be the best
available implementation of generic count within a PCF-style ‘functional’
language (provided one accepts the use of a primitive for call-by-need
evaluation).

We give the gist of an adaptation of Berger’s search algorithm on finite
spaces.

$\begin{array}[t]{@{}l@{}}\mathsf{bestshot}_{n}:\mathsf{Predicate}_{n}\to\mathsf{Point}_{n}\\\
\mathsf{bestshot}_{n}~{}pred\mathrel{:=}\mathsf{bestshot}^{\prime}_{n}~{}pred~{}[]\vskip
6.0pt plus 2.0pt minus 2.0pt\\\
\mathsf{bestshot}^{\prime}_{n}:\mathsf{Predicate}_{n}\to\mathsf{List}_{\mathsf{Bool}}\to\mathsf{Point}_{n}\\\
\mathsf{bestshot}^{\prime}_{n}~{}pred~{}start\mathrel{:=}\begin{array}[t]{@{}l}\mathbf{let}\;f\leftarrow\mathsf{memoise}~{}(\lambda\langle\rangle.\mathsf{bestshot}^{\prime\prime}_{n}~{}pred~{}start)\;\mathbf{in}\\\
\mathbf{return}\;(\lambda
i.\mathbf{if}\;i<|start|\;\mathbf{then}\;start.i\;\mathbf{else}\;(f~{}\langle\rangle).i)\end{array}\vskip
6.0pt plus 2.0pt minus 2.0pt\\\
\mathsf{bestshot}^{\prime\prime}_{n}:\mathsf{Predicate}_{n}\to\mathsf{List}_{\mathsf{Bool}}\to\mathsf{List}_{\mathsf{Bool}}\\\
\mathsf{bestshot}^{\prime\prime}_{n}~{}pred~{}start\mathrel{:=}\begin{array}[t]{@{}l}\mathbf{if}\;|start|=n\;\mathbf{then}\;\mathbf{return}\;start\\\
\mathbf{else}\;\begin{array}[t]{@{}l}\mathbf{let}\;f\leftarrow\mathsf{bestshot}^{\prime}_{n}~{}pred~{}(\mathsf{append}~{}start~{}[\mathsf{true}])\;\mathbf{in}\\\
\mathbf{if}\;pred~{}f\;\mathbf{then}\;\mathbf{return}\;[f~{}0,\dots,f~{}(n-1)]\\\
\mathbf{else}\;\mathsf{bestshot}^{\prime\prime}_{n}~{}pred~{}(\mathsf{append}~{}start~{}[\mathsf{false}])\end{array}\end{array}\end{array}$

Given any $n$-standard predicate $P$ the function $\mathsf{bestshot}_{n}$
returns a point satisfying $P$ if one exists, or dummy point $\lambda
i.\mathsf{false}$ if not. It is implemented by via two mutually recursive
auxiliary functions whose workings are admittedly hard to elucidate in a few
words. The function $\mathsf{bestshot}^{\prime}_{n}$ is a generalisation of
$\mathsf{bestshot}_{n}$ that makes a best shot at finding a point $\pi$
satisfying given predicate and matching some specified list $start$ in some
initial segment of its components $[\pi(0),\dots,\pi(i-1)]$. It works
‘lazily’, drawing its values from $start$ wherever possible, and performing an
actual search only when required. This actual search is undertaken by
$\mathsf{bestshot}^{\prime\prime}_{n}$, which proceeds by first searching for
a solution that extends the specified list with true; but if no such solution
is forthcoming, it settles for false as the next component of the point being
constructed. The whole procedure relies on a subtle combination of laziness,
recursion and implicit nesting of calls to the provided predicate which means
that the search is self-pruning in regions of the binary tree where the
predicate only demands some initial segment $q~{}0$,…,$q~{}(i-1)$ of its
argument $q$.

The above program makes use of an operation

$\mathsf{memoise}:(\mathsf{Unit}\to\mathsf{List}~{}\mathsf{Bool})\to(\mathsf{Unit}\to\mathsf{List}~{}\mathsf{Bool})$

which transforms a given thunk into an equivalent ‘memoised’ version, i.e. one
that caches its value after its first invocation and immediately returns this
value on all subsequent invocations. Such an operation may readily be
implemented in $\lambda_{\textrm{s}}$, or alternatively may simply be added as
a primitive in its own right. The latter has the advantage that it preserves
the purely ‘functional’ character of the language, in the sense that every
program is observationally equivalent to a $\lambda_{\textrm{b}}$ program,
namely the one obtained by replacing $\mathsf{memoise}$ by the identity.

We now show how the above idea may be exploited to yield a generic count
program (this development appears to be new).

$\begin{array}[t]{@{}l@{}}\mathsf{BergerCount}_{n}:\mathsf{Predicate}_{n}\to\mathsf{Nat}\\\
\mathsf{BergerCount}_{n}~{}pred\mathrel{:=}\mathsf{count}^{\prime}_{n}~{}pred~{}[]~{}0\vskip
6.0pt plus 2.0pt minus 2.0pt\\\
\mathsf{count}^{\prime}_{n}:\mathsf{Predicate}_{n}\to\mathsf{List}_{\mathsf{Bool}}\to\mathsf{Nat}\to\mathsf{Nat}\\\
\mathsf{count}^{\prime}_{n}~{}pred~{}start~{}acc\mathrel{:=}\begin{array}[t]{@{}l}\mathbf{if}\;|start|=n\;\mathbf{then}\;acc+(\mathbf{if}\;pred\,(\lambda
i.start.i)\;\mathbf{then}\;\mathbf{return}\;1\;\mathbf{else}\;\mathbf{return}\;0)\\\
\mathbf{else}\;\begin{array}[t]{@{}l}\mathbf{let}\;f\leftarrow\mathsf{bestshot}^{\prime}_{n}~{}pred~{}start\;\mathbf{in}\\\
\mathbf{if}\;pred~{}f\;\mathbf{then}\;\mathsf{count}^{\prime\prime}_{n}~{}start~{}[f~{}0,\dots,f~{}(n-1)]~{}acc\;\mathbf{else}\;\mathbf{return}\;acc\end{array}\end{array}\vskip
6.0pt plus 2.0pt minus 2.0pt\\\
\mathsf{count}^{\prime\prime}_{n}:\mathsf{Predicate}_{n}\to\mathsf{List}_{\mathsf{Bool}}\to\mathsf{List}_{\mathsf{Bool}}\to\mathsf{Nat}\to\mathsf{Nat}\\\
\mathsf{count}^{\prime\prime}_{n}~{}pred~{}start~{}leftmost~{}acc\mathrel{:=}\begin{array}[t]{@{}l}\mathbf{if}\;|start|=n\;\mathbf{then}\;acc+1\\\
\mathbf{else}\;\begin{array}[t]{@{}l}\mathbf{let}\;b\leftarrow
leftmost.|start|\;\mathbf{in}\\\
\mathbf{let}\;acc^{\prime}\leftarrow\mathsf{count}^{\prime\prime}_{n}~{}pred~{}(\mathsf{append}~{}start~{}[b])~{}leftmost~{}acc\;\mathbf{in}\\\
\mathbf{if}\;b\;\mathbf{then}\;\mathsf{count}^{\prime}_{n}~{}pred~{}(\mathsf{append}~{}start~{}[\mathsf{false}])~{}acc^{\prime}\;\mathbf{else}~{}\mathbf{return}\;acc^{\prime}\end{array}\end{array}\end{array}$

Again, $\mathsf{BergerCount}_{n}$ is implemented by means of two mutually
recursive auxiliary functions. The function $\mathsf{count}^{\prime}_{n}$
counts the solutions to the provided predicate $pred$ that start with the
specified list of booleans, adding their number to a previously accumulated
total given by $acc$. The function $\mathsf{count}^{\prime\prime}_{n}$ does
the same thing, but exploiting the knowledge that a best shot at the
‘leftmost’ solution to $P$ within this subtree has already been computed. (We
are visualising $n$-points as forming a binary tree with $\mathsf{true}$ to
the left of $\mathsf{false}$ at each fork.) Thus,
$\mathsf{count}^{\prime\prime}_{n}$ will not re-examine the portion of the
subtree to the left of this candidate solution, but rather will start at this
solution and work rightward.

This gives rise to an $n$-count program that can work efficiently on
predicates that tend to ‘fail fast’: more specifically, predicates $P$ that
inspect the components of their argument $q$ in order $q~{}0$, $q~{}1$,
$q~{}2$, …, and which are frequently able to return $\mathsf{false}$ after
inspecting just a small number of these components. Generalising our program
from binary to $k$-ary branching trees, we see that the $n$-queens problem
provides a typical example: most points in the space can be seen _not_ to be
solutions by inspecting just the first few components. Our experimental
results in Section 8 attest to the viability of this approach and its
overwhelming superiority over the naïve functional method.

By contrast, the above program is _not_ able to exploit parts of the tree
where our predicate ‘succeeds fast’, i.e. returns $\mathsf{true}$ after seeing
just a few components. Unlike the effectful count program of Section 5.4,
which may sometimes add $2^{n-d}$ to the count in a single step, the Berger
approach can only count solutions one at a time. Thus, supposing $P$ is an
$n$-standard predicate the evaluation of $\mathsf{count}_{n}~{}P$ that returns
a natural number $c$ must take time $\Omega(c)$. These observations informally
indicate the likely extent of the efficiency gap between effectful and purely
functional computation when it comes to non-$n$-standard predicates.