# On Model-Checking Higher-Order Effectful Programs

Ugo Dal Lago  University of Bologna, INRIAItaly<EMAIL_ADDRESS>1234-5678-9012 and  Alexis Ghyselen  University of BolognaItaly
<EMAIL_ADDRESS>
###### Abstract.

Model-checking is one of the most powerful techniques for verifying systems
and programs, which since the pioneering results by Knapik et al., Ong, and
Kobayashi, is known to be applicable to functional programs with higher-order
types against properties expressed by formulas of monadic second-order logic.
What happens when the program in question, in addition to higher-order
functions, also exhibits algebraic effects such as probabilistic choice or
global store? The results in the literature range from those, mostly positive,
about nondeterministic effects, to those about probabilistic effects, in the
presence of which even mere reachability becomes undecidable. This work takes
a fresh and general look at the problem, first of all showing that there is an
elegant and natural way of viewing higher-order programs producing algebraic
effects as ordinary higher-order recursion schemes. We then move on to
consider effect handlers, showing that in their presence the model checking
problem is bound to be undecidable in the general case, while it stays
decidable when handlers have a simple syntactic form, still sufficient to
capture so-called _generic effects_. Along the way we hint at how a general
specification language could look like, this way justifying some of the
results in the literature, and deriving new ones.

higher-order recursion schemes, algebraic effects, model checking, effect
handlers

††copyright: none

##  1\. Introduction

Verifying the correctness of programs endowed with higher-order functions is a
very challenging problem, which can be addressed with various methodologies,
from type systems (Hughes et al., 1996; Davies and Pfenning, 2000; Freeman and
Pfenning, 1991) to program logics (Jung et al., 2018; Brady, 2013), from
symbolic execution (King, 1976; Tobin-Hochstadt and Van Horn, 2012) to
verified compilation (Leroy, 2009). An approach with some peculiarities is
that of higher-order model checking (HOMC in the following), which consists in
seeing the program at hand as a structure, then checking whether it renders a
logical formula capturing the desired property true, namely whether it is a
_model_ of it. Saying it another way, HOMC can be seen as the application of
the model checking paradigm (Clarke, 1997; Clarke et al., 2018) to higher-
order programs. One of the characteristics of this approach is that, contrary
to most others, it is often both sound _and complete_. As a consequence, the
kind of languages to which the methodology can be applied are very often _not_
Turing-complete, the underlying verification problem being undecidable even
for very simple logics.

The feasibility of higher-order model checking was scrutinized in the early
2000s, the objective being to extend classic results about model checking
_recursion schemes_ (Courcelle, 1995) to higher-order generalizations of the
latter. The results obtained were initially very interesting but partial
(Knapik et al., 2002, 2001), only concerning certain restricted forms of
higher-order recursion schemes. The quest came to an end in 2006 with Ong’s
groundbreaking result (Ong, 2006) on the decidability of the model checking
problem for trees generated by general higher-order recursion schemes against
formulas of MSO (or, equivalently, of formulas the $\mu$-calculus or
alternating parity tree automata (Emerson and Jutla, 1991; Grädel et al.,
2003)). This result was followed by many other ones (Kobayashi, 2009;
Kobayashi and Ong, 2009; Hague et al., 2008; Salvati and Walukiewicz, 2011;
Broadbent et al., 2010; Carayol and Serre, 2012; Walukiewicz, 2016), whose
goal was that of understanding the deep computational nature of the problem,
at the same time generalizing the decidability result and building concrete
verification tools (Kobayashi, 2011; Neatherway et al., 2012; Broadbent and
Kobayashi, 2013; Ramsay et al., 2014), readers can refer to (Ong, 2015) for an
overview.

Among the various extensions of higher-order schemes considered in the
literature, we should certainly mention extensions aimed at capturing higher-
order recursion schemes subject to more permissive type disciplines than that
of simple types, namely the one to which Ong’s classic result applies. As an
example, higher-order recursion schemes with recursive types have been
recently considered (Kobayashi and Igarashi, 2013). We should also mention
some attempts at making the technique applicable to programs which are not
pure, but which can produce, for example, nondeterministic and probabilistic
effects. In the second case the decidability results scale back (Kobayashi et
al., 2020), with undecidability showing up already at order three and for mere
reachability properties. In the first case, instead results remain essentially
unchanged (Tsukada and Kobayashi, 2014).

The motivation from which this work originates is precisely that of
understanding the deep reasons for the aforementioned discrepancy, at the same
time giving a general account of the HOMC problem in presence of effects. In
doing so, we will consider effects as being captured by algebraic operations
(Plotkin and Power, 2003), the latter producing some pre-defined effects or
interpreted by way of effect handlers (Plotkin and Pretnar, 2009; Kammar et
al., 2013; Hillerström et al., 2017). In other words, we will consider well-
established ways of capturing effects in higher-order $\lambda$-calculi. On
the side of specifications, we analogously try not to consider ad-hoc
formalisms, and look for conservative extensions of MSO in which the
properties of interest can be captured in a unifying way. In particular, in
the algebraic approach to effects, trees are always considered up to an
equational theory, describing how the different algebraic operation should
behave. In our approach, this means that it is particularly important to be
able to define specifications that take into account this equational theory,
and this is captured in our approach by the notion of an observation (Johann
et al., 2010; Simpson and Voorneveld, 2019; Matache and Staton, 2019).

The contributions of this paper are threefold:

  * •

We first of all consider a finitary version of Simpson and Voorneveld’s EPCF,
a calculus with full recursion and algebraic effects, showing that the
computation tree semantics of any EPCF computation $C$ is precisely the one of
a $\lambda Y$-term $C^{*}$ obtained by CPS-translating $C$. Since the $\lambda
Y$-calculus is well-known to be equiexpressive to higher-order recursion
schemes (Nakamura et al., 2020), we obtain that computation trees generated by
EPCF can be automatically checked against MSO specifications. This is in
Section 4 and Section 5.

  * •

Then, we turn our attention to more general and more expressive
specifications. Among the many proposals for logic for algebraic effects, we
consider a variation on the one proposed by Simpson and Voorneveld, in which
any effectful computations can be tested through the notion of an observation.
We then prove that only certain notions of observations give rise to decidable
model-checking problems, this way justifying some of the existing results in
the literature, at the same time proving new ones. This is in Section 6.

  * •

Finally, we consider the impact of effect handlers to the HOMC problem. We
show that handlers are indeed harmful to decidability, at least when general,
well-established notions of handlers are considered, including shallow and
deep handlers. We conclude by considering a rather restricted class of
handlers which are sufficiently expressive to capture generic effects (Plotkin
and Power, 2003) but for which model checking remains decidable. This is in
Section 7 and Section 8.

All in all, the results above provide a rather clear picture about how far one
can go in applying existing HOMC methodologies to effectful programs. The
take-home messages are that in principle, such techniques can be reused,
provided the underlying notion of observation does not give rise to too
complex specifications, while handlers are potentially very dangerous, and
should be used with great care. The technical core of the paper is in Section
3 to Section 8, while Section 2 serves as a gentle introduction to higher-
order programming with effects and its verification. Related work is discussed
in Section 11.

##  2\. Higher-Order Effectful Programs, and how to Model-Check Them

While the $\lambda$-calculus is the reference paradigmatic model for pure
functional programming, a standard way of raising _effects_ from within
functional programs consists in invoking algebraic operations (Plotkin and
Power, 2003), each of them corresponding to a particular way of producing an
observable effect. Even when the underlying programming language does not
offer algebraic operations natively, many impure constructs can be interpreted
this way. Consider, as an example, the OCAML program in Figure 1(a), call it
$\mathtt{P}$, which manipulates two ground global variables $\mathrm{r}$ and
$\mathrm{q}$ through a recursive higher-order function $\mathrm{f}$.

⬇

let r = ref true;;

let q = ref true;;

let rec f g =

let y = !r in

let z = !q in

if (g y z) then failwith(”Failure”) else begin

r := (not z);

q := (not y);

f g;

end

in f (fun x y $\mapsto$ x <> y)

(a) An OCAML program $\mathtt{P}$ which never fails.

⬇

Set((r,true);$\lambda$_.

Set((q,true);$\lambda$_.

let F = return(fix f.$\lambda$g.

Get(r,$\lambda$y.

Get(q,$\lambda$z.

let x = (g y z) in

case(x, Raise(),

Set((r,not z);$\lambda$_.

Set((q,not y);$\lambda$_.

f g ))

))))

in F ($\lambda$(x,y). x $\oplus$ y)

))

(b) An EPCF term $M_{\mathtt{P}}$.

Figure 1.

As can be easily realized, whenever the conditional is executed the two
references $\mathrm{r}$ and $\mathrm{q}$ contain _the same_ boolean value. As
a consequence, the Failure exception is never raised, and the program can be
considered safe. Could we automatically verify the latter by way of higher-
order model checking? Let us try to see if this is possible.

We can assume $\mathtt{Loc}$ to be a type of locations inhabited by
$\mathrm{q}$ and $\mathrm{r}$ only, and that the program can invoke any
effect-raising operations from the following typed signature:

$\Sigma=\\{\mathbf{Get}:\mathtt{Loc}\rightsquigarrow
2,\mathbf{Set}:\mathtt{Loc}\times\mathtt{Bool}\rightsquigarrow
1,\mathbf{Raise}:\mathtt{Unit}\rightsquigarrow 0\\}.$

Some standard abbreviations allow us to form the term in Figure 1(b), call it
$M_{\mathtt{P}}$, whose structure is very similar to the one of $\mathtt{P}$.
In doing so, we have adopted a syntax close to Simpson and Voorneveld’s EPCF.
Observe how OCAML’s reference commands have become algebraic operations from
$\Sigma$, and how $\mathbf{Get}$ has arity equal to two, accounting for the
fact that the program can proceed depending on the value read from memory. By
the way, $M_{\mathtt{P}}$ closely corresponds to the way one would write
$\mathtt{P}$ in languages like EFF (Pretnar, 2015).

(a) Tree Generated by $M_{\mathtt{P}}$.

(b) Automaton Capturing the safety of a program working with the boolean
variables $\mathrm{r}$ and $\mathrm{Q}$.

Figure 2.

But why do algebraic operation could help in the task of verifying the safety
of $\mathtt{P}$? Actually, the evaluation of programs which invoke algebraic
operations naturally gives rise to a so-called _effect tree_. The effect tree
produced in output by $M_{\mathtt{P}}$ looks like one in Figure 2(a). Through
it, one can verify that $\mathbf{Raise}$ is never executed by exhaustively
considering all branches of the tree, and verifying that those which are
somehow coherent with the store operations do not end in a leaf labeled with
$\mathbf{Raise}$. Here, coherent branches are those that, e.g., when
encountering $\mathbf{Get}(q)$ proceed left (respectively, right) depending on
the last $\mathbf{Set}(q,a)$ operation performed. This reasoning can indeed be
encoded in an alternating parity tree automata, and thus by a MSO or
$\mu$-calculus formula (Grädel et al., 2003; Emerson and Jutla, 1991). Let us
briefly describe how this automaton can be constructed (here, by the way, we
only need a top-down deterministic automata). Its set of states comprises all
assignments of boolean values to the variables $\mathrm{r}$ and $\mathrm{q}$,
together with a special state $\mathsf{OK}$. Intuitively, the latter captures
incoherent states, and any action is accepted from there. Some example
transitions are those in Figure 2(b). The first two capture the expected
behavior of $\mathbf{Set}$ and $\mathbf{Get}$ on stores, while the last three
are there to model the fact that every action, including $\mathbf{Raise}$ is
allowed in the state $\mathsf{OK}$. Of course, the latter is _not_ available
in ordinary stores instead.

All in all, then, we indeed have a way to turn impure functional programs into
terms of a calculus called EPCF which generate trees which are, at least
superficially, amenable to model checking. There is still a missing link
though: it could well be that EPCF is simply too expressive, and that the
model-checking problem is undecidable. Fortunately, however, we can turn EPCF
programs into $\lambda Y$-terms, for which MSO model checking is indeed
decidable (Nakamura et al., 2020). This is precisely what we prove in Section
5 below.

Summing up, HOMC indeed seems to be helpful when considered on effect trees,
because the program we are interested in verifying, and arguably any term
working with global references over finite domains can be turned into a term
in the $\lambda$Y-calculus, while the property becomes an MSO formula. But how
about other effects? Can we turn the construction above into something more
general and systematic? While specific kinds of effects are considered in the
literature (Kobayashi, 2009; Kobayashi et al., 2020; Ong, 2015), no general
result is known. In fact, each effect comes equipped with its intended notion
of observation (Johann et al., 2010; Matache and Staton, 2019; Simpson and
Voorneveld, 2019; Dal Lago et al., 2017). Which ones of those are simple
enough to guarantee that model checking useful properties stays decidable?

For the sake of convincing the reader that the questions above are not
trivial, let us consider another example of an effectful higher-order program,
borrowed from (Kobayashi et al., 2020)

⬇

let F = return(fix f. $\lambda$_.

Flip($\lambda$ b.

case(b, return(),

let x = f () in let y = f() in f()

))) in F ()

The algebraic operation $\mathbf{Flip}(\lambda b.C)$ should be understood as
flipping a random coin, storing the result in $b$, and continuing as $C$.
Intuitively, the program described above creates a procedure $f$ that throws a
coin. If the coin returns head, the procedure stop. Otherwise, the procedure
is executed three times. This program generates an effect tree $T_{0}$ where
for every $n$, the tree $T_{n}$ can be defined as:

$T_{0}\triangleq\Tree[.\mathbf{Flip()}[.\mathtt{return}()][.T_{2}]]\qquad\qquad\qquad
T_{n+1}\triangleq\Tree[.\mathbf{Flip()}[.T_{n}][.T_{n+3}]]$

Indeed, the sequential composition in the third argument of the
$\mathtt{case}$ operator gives raise to a stack of continuations, meaning that
a leaf $\mathtt{return}()$ is replaced by the tree computed by the
continuation. Here, the tree $T_{n}$ should be understood as a call to the
recursive function $f$ with a continuation corresponding to $n$ calls to this
function. This behavior is similar to the one of a random walk, but the
program described above does not use any infinite type, which is essential for
Higher-Order Model Checking. In fact, this tree can be computed by a term of
the $\lambda$Y-calculus, using a CPS translation, see Example 2.10 from
(Kobayashi et al., 2020):

$\displaystyle(Y(\lambda
F,k,x.\mathbf{Flip}~{}(k~{}x)~{}(F~{}(F~{}(F~{}k))~{}x)))~{}(\lambda
x.x)~{}\mathtt{return}$

Here, the use of higher-order functions is important, since the function $F$
takes as a first input a continuation, and this continuation determines the
number of calls to the procedure that still need to be executed. For such a
program, it is natural to wonder whether $\mathtt{return}$ is called or not
(if the program terminates), but given the presence of (probabilistic)
nondeterminism, there are various ways in which this can be spelled out. Do we
mean that the program must (or may) reach $\mathtt{return}$? Or do we rather
mean that the program reach $\mathtt{return}$ with probability $1$? The latter
question seems the most appropriate, given that probabilistic choice is
captured by the subdistribution monad $\mathsf{D}(\cdot)$ and that
$\mathsf{D}(\mathtt{return})$ is just a real number between $0$ and $1$, i.e.,
the probability of not diverging. If this is the case, however, recent results
by Kobayashi, Dal Lago, and Grellois (Kobayashi et al., 2020) show that HOMC
is _not_ decidable in general, so the construction of an MSO formula (or an
automaton) like the one above is simply not possible. May or must termination,
instead, can easily be captured: may termination consists in exploring the
tree and finding at least one $\mathtt{return}$, while must termination is
satisfied if the tree has no infinite branch, and all leaves are
$\mathtt{return}$ leaves, which is a property that can be encoded as a parity
condition of an alternating parity automaton.

To sum up, we can see effectful higher-order programs as effect trees,
computed by a term of the $\lambda$Y-calculus (or equivalently, higher-order
recursion schemes) for which we know that MSO model-checking is decidable.
This works particularly well for some effects, for example global store with
finite domains, since the properties of interest can be expressed as an MSO
formula. However, for some more involved effects, such as probabilistic
choice, some important properties are not expressible in MSO. The aim of this
work is to take a general look at this problem, and understand the deep reason
behind this discrepancy.

##  3\. Preliminaries about Higher-Order Model Checking

###  3.1. Infinite Trees Generated by $\lambda$Y-Terms

In Higher-Order Model Checking, models are traditionally taken to be infinite
trees produced by so-called Higher-Order Recursion Schemes (HORS in the
following). In this work, we rather consider Böhm trees generated by ground
type terms in the $\lambda Y$-calculus with first-order constants, which is
well known to express the same class of trees as HORSs (Nakamura et al.,
2020). This section is devoted to presenting some preliminaries about the
calculus and the model checking problem for it.

Formally, the $\lambda Y$-calculus can be seen as the simply-typed
$\lambda$-calculus extended with full recursion and with first-order function
symbols:

(Types) $\displaystyle T,U$
$\displaystyle::=o\;\mbox{\Large{$\mid$}}\;T\rightarrow U$ (Terms)
$\displaystyle M,N$ $\displaystyle::=x\;\mbox{\Large{$\mid$}}\;\lambda
x.M\;\mbox{\Large{$\mid$}}\;M~{}N\;\mbox{\Large{$\mid$}}\;YM\;\mbox{\Large{$\mid$}}\;f\in\Sigma$

The _signature_ $\Sigma$ is a set of first-order constants, such that each
$f\in\Sigma$ comes equipped with an arity $\mathtt{ar}(f)\geq 0$ capturing the
fact that the type of $f$ is $\underbrace{o\rightarrow o\rightarrow
o}_{\mathtt{ar}(f)}\rightarrow o$, often abbreviated as
$o^{\mathtt{ar}(f)}\rightarrow o$. By an abuse of notation, we usually write
$f:\mathtt{ar}(f)$ to specify the arity of $f$ in a given signature when this
does not cause ambiguity. Typing rules are standard, and can be found in
Figure 3.

$\Gamma,x:T\vdash x:T$ $\Gamma,x:T\vdash M:U$ $\Gamma\vdash\lambda
x.M:T\rightarrow U$ $\Gamma\vdash M:T\rightarrow U$ $\Gamma\vdash N:T$
$\Gamma\vdash M~{}N:U$ $\Gamma\vdash M:T\rightarrow T$ $\Gamma\vdash YM:T$
$\Gamma\vdash f:o^{\mathtt{ar}(f)}\rightarrow o$

Figure 3. Typing Rules for $\lambda$Y-terms

We see the $\lambda Y$-calculus as a tool to generate infinite trees. In order
to precisely define the tree generated by a typable term, one has to define a
form of dynamic semantics, which we here take as _weak head reduction_ : we
never reduce the argument of any application, and we never evaluate terms in
the scope of $\lambda$-abstractions. Rules are again standard, and can be
found in Figure 4.

$(\lambda x.M)N\rightarrow M[N/x]$ $YM\rightarrow M(YM)$ $M\rightarrow
M^{\prime}$ $M~{}N\rightarrow M^{\prime}~{}N$

Figure 4. Weak Head Reduction Rules

It is relatively easy to see that typed closed terms in _weak head normal
form_ , i.e. typed terms with no free variables that cannot be further reduced
are precisely the (typable) terms generated by the following grammar:

$WHNF::=\lambda
x.M\;\mbox{\Large{$\mid$}}\;f~{}M_{1}~{}M_{2}~{}\cdots~{}M_{n}$

Indeed, a $\lambda$-abstraction is in normal form, constants are in normal
form, and $M~{}N$ is in normal form if and only if $M$ is in normal form and
$M$ is not a $\lambda$-abstraction. As a consequence, we can easily realize
that terms of ground types in weak head normal form have the shape
$f~{}M_{1}~{}M_{2}~{}\cdots~{}M_{\mathtt{ar}(f)}$, where each $M_{i}$ is
itself a term of ground type. This naturally suggests a potentially infinite
process turning any such term of ground type into a tree with root $f$ and
$\mathtt{ar}(f)$ subtrees obtained by evaluating
$M_{1}~{}\cdots~{}M_{\mathtt{ar}(f)}$, respectively. This can be made formal
as follows:

###### Definition 0 (Infinite Trees).

The set of (potentially infinite) trees generated by a signature $\Sigma$,
denoted $\mathbf{Tree}_{\Sigma}$, is coinductively defined by the grammar:

$t::=f(t_{1},\cdots,t_{\mathtt{ar}(f)})\;\mbox{\Large{$\mid$}}\;\bot$

where $f:\mathtt{ar}(f)\in\Sigma$.

The constant $\bot$ represents a non-terminating non-productive computation
that does not generate any function symbol. As an example, if $\Sigma$ is the
signature $\\{g:2,f:1,a:0\\}$, one can form the non-regular infinite tree
$g(a,g(f(a),g(f(f(a)),\cdots))$. We are now ready to define how any closed
ground $\lambda$Y-term generates such an infinite tree:

###### Definition 0 (Böhm Trees of Closed Ground Terms).

Given a closed term $M$ of type $o$, i.e. we have $\cdot\vdash M:o$, the _Böhm
tree_ of $M$, denoted $BT(M)$, is defined by way of the following essentially
infinitary process. Starting from $M$, we apply $\rightarrow$ _ad infinitum_.
This can have two possible outcomes:

  * •

$M$ can be reduced infinitely, and in this case $BT(M)$ is simply $\bot$

  * •

$M$ can be reduced to a term $N$ in weak head normal form
$N=f~{}M_{1}~{}M_{2}~{}\cdots~{}M_{ar(f)}$ such that for all $1\leq i\leq n$,
we have $\vdash M_{i}:o$. Then,
$BT(M)=f(BT(M_{1}),BT(M_{2}),\cdots,BT(M_{\mathtt{ar}(f)}))$.

The aforementioned process is infinitary in two different ways: the evaluation
of $M$ can diverge, and $BT(M)$ can be infinite. The process above is well-
defined only for closed terms of ground type and is thus less general than the
one generating Böhm Trees for arbitrary terms of the $\lambda Y$-calculus
(Clairambault and Murawski, 2013) (there, in particular, one has to deal with
$\lambda$-abstractions).

###### Example 0.

As an example, with the signature $\Sigma=\\{g:2,f:1,a:0\\}$, consider the
term

$M\triangleq(Y~{}(\lambda F.\lambda x.g~{}x~{}(F~{}(f~{}x))))$

We pose $M_{\mathit{step}}\triangleq(\lambda F.\lambda
x.g~{}x~{}(F~{}(f~{}x)))$. By applying weak head reduction rules, we obtain

$M~{}a\rightarrow M_{\mathit{step}}~{}M~{}a\rightarrow(\lambda
x.g~{}x~{}(M~{}(f~{}x)))~{}a\rightarrow g~{}a~{}(M~{}(f~{}a))$

Thus, $BM(M~{}a)=g(a,BM(M~{}(f~{}a)))$, and similarly
$BM(M~{}(f~{}a))=g(f(a),BM(M~{}(f~{}(f~{}a))))$, finally we obtain that
$BM(M~{}a)=g(a,g(f(a),g(f(f(a)),\cdots)))$ the infinite tree described above.

###  3.2. Expressing Properties As Alternating Parity Tree Automata

Now that we have defined the class of models for higher-order model checking,
we can define the specification language. The gold standard in model-checking
consists in properties expressed by formulas of monadic second order logic
(Knapik et al., 2001) (MSO for short). However, several equiexpressive
specification languages have been defined in the literature, notably
$\mu$-calculus (Walukiewicz, 1993) and alternating parity tree automata (APT
for short) (Emerson and Jutla, 1991; Grädel et al., 2003). The latter is
commonly used in the HOMC literature (Ong, 2006, 2015; Kobayashi and Ong,
2009), and as examples we will define through the paper have a simple
representation as automata, contrary to MSO formulas, we also chose this
specification language.

Given a set $X$ of variables, we define the _positive Boolean formulas_ over
$X$, denoted $B^{+}(X)$, with the grammar:

$\phi,\psi::=\mathtt{tt}\;\mbox{\Large{$\mid$}}\;\mathtt{ff}\;\mbox{\Large{$\mid$}}\;x\;\mbox{\Large{$\mid$}}\;\phi\land\psi\;\mbox{\Large{$\mid$}}\;\phi\lor\psi$

with $x\in X$. A subset $Y\subseteq X$ satisfies a formula $\phi$, denoted
$Y\vDash\phi$ if and only if the formula $\phi$ in which all elements $x\in Y$
are replaced by $\mathtt{tt}$ and all elements $x\notin Y$ are replaced by
$\mathtt{ff}$ is semantically true. We can now give the formal definition of
an APT automaton:

###### Definition 0 (Alternating Parity Tree Automaton).

An _alternating parity tree automaton_ is a tuple
$\mathcal{A}=(\Sigma,Q,\delta,q_{i},\Omega)$ where

  * •

$\Sigma$ is a signature, defining tree constructors with their arity.

  * •

$Q$ is a _finite_ set of states, with $q_{i}\in Q$ the initial state.

  * •

$\delta$ is the transition function, such that for each $f\in\Sigma$, we have
$\delta(q,f)\in B^{+}(\\{0,\dots,\mathtt{ar}(f)-1\\}\times Q)$. A translation
$\delta(q,f)$ is thus a positive formula on a state assignment to children
nodes.

  * •

$\Omega:Q\rightarrow\\{0,\dots,M\\}$ is the priority function, with $M\geq 0$
an integer.

To define the acceptance condition of an automaton, we need to introduce the
notion of positions in a tree.

###### Definition 0.

Let $\Sigma$ be a set of tree constructors with maximal arity $A$. The set of
all position of a tree $t$, denoted $dom(t)$, is a set of words on the
alphabet $\Gamma=\\{0,\cdots,A\\}$ defined by:

$dom(\bot)=\epsilon\qquad dom(f(t_{0},\dots,t_{k}))=\\{\epsilon\\}\cup 0\cdot
dom(t_{0})\cup\cdots\cup k\cdot dom(t_{k})$

where $\cdot$ is the concatenation operator for words.

For a tree $t$ and a position $\alpha\in dom(t)$ we define
$t(\alpha)\in\Sigma\cup\\{\bot\\}$ by:

$\bot(\epsilon)=\bot\qquad f(t_{1},\dots,t_{k})(\epsilon)=f\qquad
f(t_{1},\dots,t_{k})(n\cdot\alpha)=t_{n}(\alpha)$

essentially giving the node of the tree $t$ at position $\alpha$.

A _run-tree_ of an automaton $\mathcal{A}$ over a tree in
$\mathbf{Tree}_{\Sigma}$ is a tree with constructors in $dom(t)\times Q$. This
run-tree must satisfy the following two constraints:

  * •

The root is $(\epsilon,q_{i})$, representing the root of $t$ in the state
$q_{i}$.

  * •

For any node $(\alpha,q)$ of the run-tree, there is a set
$S\subseteq\\{0,\dots,\mathtt{ar}(t(\alpha))-1\\}$ which satisfies the
transition $\delta(q,t(\alpha))$. And, for each $(i,q^{\prime})\in S$, one of
the child of $(\alpha,q)$ in the run-tree is $(\alpha\cdot i,q^{\prime})$.

Finally, we say that an infinite branch
$(\epsilon,q_{i})\cdots(\alpha_{k},q_{k})\cdots$ of the run tree satisfies the
_parity condition_ if the largest priority that occurs infinitely often in
$\Omega(q_{i})\cdots\Omega(q_{k})\cdots$ is even. A run-tree is _accepting_ if
every infinite path in it satisfies the parity condition. And of course, a
tree $t\in\mathbf{Tree}_{\Sigma}$ is accepted by an automaton $\mathcal{A}$ if
there exists an accepting run-tree for $t$.

###### Example 0.

We define an automaton
$\mathcal{A}=(\\{a:2,b:1,c:0\\},\\{q_{0},q_{1}\\},\delta,q_{0},\Omega)$ such
that $\mathcal{A}$ accepts a tree $t$ if and only if for every path in $t$,
$c$ occurs eventually after $b$ occurs. We pose:

  * •

For all $q\in\\{q_{0},q_{1}\\}:$

$\delta(q,a)=(0,q)\land(1,q)\qquad\delta(q,b)=(1,q_{1})\qquad\delta(q,c)=\mathtt{tt}$

Meaning intuitively that a node $a$ propagates the state to both children,
seeing the letter $b$ changes the state to $q_{1}$ and a leaf $c$ is always
accepted.

  * •

$\Omega(q_{0})=2\qquad\Omega(q_{1})=1$

By definition, if $q_{1}$ appears infinitely often in a branch of the run
tree, and $q_{0}$ does not, then the largest priority is $1$ in this branch,
and the tree does not satisfy the parity condition. Thus, with this automata,
to accept a tree $t$, it must have only finite branches (that terminates with
the only available leaf $c$) or infinite branches in which $b$ does not occur
(in order to stay in the state $q_{0}$). This corresponds indeed to the
property that for every path in $t$, $c$ occurs eventually after $b$ occurs”.

We can now define the model-checking problem and give the theorem expressed in
(Ong, 2006).

###### Definition 0 (MSO Model-Checking for Böhm Trees (or APT Acceptance
Problem)).

Given a closed $\lambda$Y-term $M$ of with $\vdash M:o$ and an APT
$\mathcal{A}$, is $BT(M)$ accepted by $\mathcal{A}$ ?

The groundbreaking result of higher-order model checking (Ong, 2006) can then
be summed up with the following theorem:

###### Theorem 8 (Decidability (Ong, 2006, 2015)).

MSO model-checking on Böhm Trees of closed ground terms of the
$\lambda$Y-calculus is decidable.

The results obtained in (Ong, 2006) give the precise complexity of this
problem, which is exponential depending on the _order_ of the $\lambda$Y-term
(or, equivalently, the order of the higher-order recursion scheme (Nakamura et
al., 2020)). The aim of our work is on decidability, so we will not take
orders into account, but we plan to study complexity issues in the future,
given that finer complexity analysis for similar problems is already available
(Nakamura et al., 2020; Tsukada and Kobayashi, 2014).

Thanks to this theorem, to show that MSO model-checking is decidable for a
class of infinite trees, it is sufficient to show that this class of trees can
be computed as Böhm trees generated from $\lambda$Y-terms, and this can be
done via program transformation to the $\lambda$Y-calculus, as we will see in
many occasions starting from the next section.

##  4\. Higher-Order Programs with Effects

In this section, we introduce a calculus with algebraic operations and
fixpoints, called EPCF. This language can be seen as a fine-grained call-by-
value variation on Plotkin’s PCF endowed with effect-triggering operations, as
described in (Simpson and Voorneveld, 2019). We consider a finitary version of
this language which differs from Simpson and Voorneveld’s one only in minor
ways.

EPCF is built around two syntactic categories, namely _values_ , which denote
data or functions, and _computations_ , which are instead programs which
potentially produce effects when evaluated. Terms and types for EPCF are as
follows:

(Values) $\displaystyle V,W$
$\displaystyle::=v\;\mbox{\Large{$\mid$}}\;\underline{n}\;\mbox{\Large{$\mid$}}\;x\;\mbox{\Large{$\mid$}}\;\lambda
x.C\;\mbox{\Large{$\mid$}}\;\mathtt{fix}~{}x.V$ (Computations) $\displaystyle
C,B,A$
$\displaystyle::=V~{}W\;\mbox{\Large{$\mid$}}\;\mathtt{return}(V)\;\mbox{\Large{$\mid$}}\;\mathtt{let}~{}x=C~{}\mathtt{in}~{}B\;\mbox{\Large{$\mid$}}\;\sigma(V;x.C)\;\mbox{\Large{$\mid$}}\;$
$\displaystyle\phantom{::=}\mathtt{case}(V;C_{1},\dots,C_{k})$ (Types)
$\displaystyle T,U$
$\displaystyle::=\mathtt{B}\;\mbox{\Large{$\mid$}}\;\mathtt{k}\;\mbox{\Large{$\mid$}}\;T\rightarrow
U$

We suppose given a set of _finite_ ground types, ranged over by $\mathtt{B}$.
Examples include the unit type and the type of booleans. We similarly assume a
set $\mathcal{V}$ of constant values each of a ground type, ranged over by
$v$, e.g. a unique constructor $()\in\mathcal{V}$ with its associated type
$\mathtt{Unit}$. We also assume finite enumeration types $\mathtt{k}$ to be
present, each of them inhabited by the values
$\underline{0},\underline{1},\dots,\underline{k-1}$. We introduce enumeration
types, which support pattern matching, just to keep them distinct from finite
base types.

Algebraic operations have the shape $\sigma(V;x.C)$ where $V$ is said to be a
_parameter_ , and $C$ represents the _continuation_ of the computation. The
variable $x$ is bound in $C$ and represents the choice made by the algebraic
operation. We suppose given a signature set $\Sigma$ of symbols for algebraic
operations, where each $\sigma\in\Sigma$ is given an arity
$\mathtt{B}\rightsquigarrow k$, meaning that $\sigma$ is an algebraic
operation of arity $k$ depending on a parameter of type $\mathtt{B}$. In an
operation of arity $k$, the type of $x$ in the continuation $C$ is
$\mathtt{k}$. In particular, defining $k$ different continuations
$C_{1},\dots,C_{k}$ depending on the possible values of $x$ can be done by way
of the computation $\sigma(V;x.\mathtt{case}(x,C_{1},\dots,C_{k}))$. As common
in call-by-value calculi, the fixpoint operator $\mathtt{fix}~{}x.V$ is a
value and can only be attributed a function type without limiting the
expressive power of the language. Finally, the shape of computations is
restricted in that the only way to compose computations is to use the
$\mathtt{let}$ constructor. For example, if we want to apply the result of the
computation $D$ to the function computed by $C$, we need to define a
computation

$\mathtt{let}~{}x=D~{}\mathtt{in}~{}\mathtt{let}~{}y=C~{}\mathtt{in}~{}y~{}x\qquad\text{or}\qquad\mathtt{let}~{}y=C~{}\mathtt{in}~{}\mathtt{let}~{}x=D~{}\mathtt{in}~{}y~{}x$

As can be seen from this example, the order of evaluation is imposed by
sequencing, a property which turns out to be crucial in presence of effects,
as we will see when looking at the semantics.

As for the type system of EPCF, which is pretty natural and standard, we give
some of the rules in Figure 5.

$v:\mathtt{B}\in\mathcal{V}$ $\Gamma\vdash v:\mathtt{B}$ $n<k$
$\Gamma\vdash\underline{n}:\mathtt{k}$ $\Gamma,x:T\rightarrow U\vdash
V:T\rightarrow U$ $\Gamma\vdash\mathtt{fix}~{}x.V:T\rightarrow U$
$\Gamma\vdash V:T$ $\Gamma\vdash\mathtt{return}(V):T$ $\Gamma\vdash C:T$
$\Gamma,x:T\vdash D:U$ $\Gamma\vdash\mathtt{let}~{}x=C~{}\mathtt{in}~{}D:U$
$(\sigma:\mathtt{B}\rightsquigarrow k)\in\Sigma$ $\Gamma\vdash V:\mathtt{B}$
$\Gamma,x:\mathtt{k}\vdash C:T$ $\Gamma\vdash\sigma(V;x.C):T$ $\Gamma\vdash
V:\mathtt{k}$ $(\Gamma\vdash C_{i}:T)_{1\leq i\leq k}$
$\Gamma\vdash\mathtt{case}(V;C_{1},\dots,C_{k}):T$

Figure 5. Typing Rules for EPCF

The typing rule for algebraic operations stipulates that an effect does not
change the type of the whole computation, which is however arbitrary.
Intuitively this is because calling an algebraic operation induces an effect
$\sigma$, depending on the parameter $V$, and the computation will continue as
$C$ after throwing this effect.

We now introduce the dynamic semantics of EPCF using the reduction relation in
Figure 6.

$(\lambda x.C)~{}W\rightarrow C[W/x]$
$(\mathtt{fix}~{}x.V)~{}W\rightarrow(V[(\mathtt{fix}~{}x.V)/x])~{}W$
$\mathtt{case}(\underline{n},C_{0},\cdots,C_{k-1})\rightarrow C_{n}$
$\mathtt{let}~{}x=\mathtt{return}(V)~{}\mathtt{in}~{}C\rightarrow C[V/x]$
$C\rightarrow C^{\prime}$
$\mathtt{let}~{}x=C~{}\mathtt{in}~{}B\rightarrow\mathtt{let}~{}x=C^{\prime}~{}\mathtt{in}~{}B$
$\mathtt{let}~{}x=\sigma(V;y.C)~{}\mathtt{in}~{}D\rightarrow\sigma(V;y.\mathtt{let}~{}x=C~{}\mathtt{in}~{}D)$

Figure 6. Semantics for EPCF

The cornerstone of this relation is the last rule, allowing to algebraic
operations to “percolate out” of non-trivial evaluation contexts. Intuitively,
this rule means that if we have a computation of the shape
$\mathtt{let}~{}x=C~{}\mathtt{in}~{}D$, and $C$ is a computation that throws
an effect $\sigma$, then this effect is immediately visible from the outside,
its continuation now incorporating the $\mathtt{let}$ expression at hand. If
we go back to the aforementioned example describing the composition of
computations, namely the pair of terms

$\mathtt{let}~{}x=D~{}\mathtt{in}~{}\mathtt{let}~{}y=C~{}\mathtt{in}~{}y~{}x\qquad\qquad\mathtt{let}~{}y=C~{}\mathtt{in}~{}\mathtt{let}~{}x=D~{}\mathtt{in}~{}y~{}x$

we can see that in the first case, the effects thrown in $D$ appears first,
and then the one in $C$, and conversely for the other case.

###### Example 0.

Let us consider a computation which flips a fair coin, then returning the the
exclusive or of the obtained value and itself (which is thus always going to
be true). All this makes use of an algebraic operation $\mathbf{Flip}$ having
arity $\mathtt{unit}\rightsquigarrow 2$ and of a binary function $\oplus$
computing the exclusive or, and which can anyway be easily written as a term
itself:

$\mathtt{let}~{}x=\mathbf{Flip}(\cdot;y.y)~{}\mathtt{in}~{}(x\oplus x)$

In a call-by-value setting, this program should flip a coin, to obtain
$\underline{0}$ or $\underline{1}$ thus always returning $\underline{0}$.
Indeed, the dynamic semantics allows the $\mathbf{Flip}$ operation to be
visible from the outside:

$\mathtt{let}~{}x=\mathbf{Flip}(\cdot;y.y)~{}\mathtt{in}~{}(x\oplus
x)\rightarrow\mathbf{Flip}(\cdot;y.\mathtt{let}~{}x=y~{}\mathtt{in}~{}x\oplus
x)$

There are two observations one needs to make now. The first is that the
continuation $\mathtt{let}~{}x=y~{}\mathtt{in}~{}x\oplus x$ returns
$\underline{0}$ for all values of $y$, as expected, but since it occurs as the
argument of $\mathbf{Flip}$ it cannot be further reduced, and its evaluation
must be somehow be captured differently. The second one is that in presence of
effects, confluence is lost. If, indeed, we pass $\mathbf{Flip}(\cdot;y.y)$
unevaluated to the right-hand side, in a call-by-name fashion, we land on a
totally different term, namely one which flips _two_ coins, possibly returning
$\underline{1}$:

$\mathtt{let}~{}x=\mathbf{Flip}(\cdot;y.y)~{}\mathtt{in}~{}(x\oplus
x)\rightarrow_{name}(\mathbf{Flip}(\cdot;y.y)\oplus\mathbf{Flip}(\cdot;y.y)).$

The example above implicitly tells us that, similarly to what happens in the
$\lambda Y$-calculus, the terms of EPCF generate infinite trees that we
commonly call _effect trees_ , but that the dynamic semantics does not by
itself take care of the unfolding: indeed, typed closed computations in normal
form in EPCF are either of the shape $\mathtt{return}(V)$, which is expected,
or $\sigma(V;x.C)$, meaning that evaluation apparently stops as soon as an
algebraic operation is encountered. The effect tree of a computation is what
we are looking for as is defined as follows:

###### Definition 0 (Effect Trees for EPCF Computations).

For an algebraic effect signature $\Sigma$ and a type $T$, let us define the
signature $\Sigma_{T}$ as follows:

$\Sigma_{T}=\\{\sigma:k+1\mid((\sigma:\mathtt{B}\rightsquigarrow
k)\in\Sigma)\\}\cup\\{\mathtt{return}(V):0\mid\;\vdash
V:T\\}\cup\\{v:0\;\mbox{\Large{$\mid$}}\;v\in\mathcal{V}\\}$

Note that $\Sigma_{T}$ is infinite in the general case, but that it is
guaranteed to be finite when $\mathcal{V}$ is finite and $T$ is a ground (and
thus finite) type. The effect tree of a typed computation $\vdash C:T$,
denoted $ET(C)$, is a tree in $\mathbf{Tree}_{\Sigma_{T}}$ defined by the
following essentially infinite process. First of all, reduce $C$ ad infinitum,
and there are _three_ possible outcomes:

  * •

If $C$ can be reduced infinitely without reaching a normal form, then
$ET(C)=\bot$

  * •

If $C\rightarrow^{*}\mathtt{return}(V)$ then $ET(C)=\mathtt{return}(V)$

  * •

If $C\rightarrow^{*}\sigma(v;x.C)$ with $\sigma:\mathtt{B}\rightsquigarrow k$
then
$ET(C)=\sigma(v,ET(C[x:=\underline{0}]),\cdots,ET(C[x:=\underline{k-1}]))$

This definition of effect trees differs a bit from the one given in the
literature by the use of a special branch for parameters. Formally, standard
effect trees (Simpson and Voorneveld, 2019; Matache and Staton, 2019) would be
defined with the signature:

$\Sigma^{\prime}_{T}=\\{\sigma_{v}:k\mid((\sigma:\mathtt{B}\rightsquigarrow
k)\in\Sigma)\land(\vdash
v:\mathtt{B}\in\mathcal{V})\\}\cup\\{\mathtt{return}(V):0\mid\vdash V:T\\}$

with the expected definition when seeing an effect $\sigma(v;x.C))$. Our
definition is not harmful compared to this usual notion of effect trees in
which operations are indexed by their parameters because we are in a finite
case, where the parameters can only be a constant value for some finite type
$\mathtt{B}$. In particular, any MSO formula on a standard tree with indexed
effects for can be transferred to an equivalent formula on effect trees with
branching for parameters, see Section 6, Proposition 5 for more details.
Anyway, one can remark that this definition is similar to the notion of Böhm
trees we defined before. And indeed, we show that we can relate the notion of
effect trees in EPCF with the notion of Böhm trees in $\lambda Y$-calculus.
Formally, we need to use a CPS translation similar to the one described in
(Matache, 2018; Matache and Staton, 2019).

###### Example 0.

As an example, we can compute a tree with similarities with the one of Example
3 in the $\lambda$Y-calculus. We take
$\Sigma=\\{\sigma_{f}:\mathtt{Unit}\rightsquigarrow
1,\sigma_{g}:\mathtt{Unit}\rightsquigarrow 2\\}$, and the EPCF computation

$C\triangleq\mathtt{fix}~{}F.(\lambda
x.\sigma_{g}((),n.\mathtt{case}(n;,x~{}(),F(\lambda
z.\sigma_{f}((),\\_.x~{}()))))$

For the sake of clarity, let us ignore all the parameters for algebraic
effect, which do not bring anything interesting here because the parameter is
always $()$. Then, we have:

$C~{}(\lambda z.\mathtt{return}(()))\rightarrow\sigma_{g}((\lambda
z.\mathtt{return}(()))~{}(),C~{}(\lambda z^{\prime}.\sigma_{f}((\lambda
z.\mathtt{return}(()))~{}())~{}()))$

And if we continue the computation, we can see that the effect tree $t$ of
$C~{}(\lambda z.\mathtt{return}(()))$ is

$t\triangleq\sigma_{g}(\mathtt{return}(()),\sigma_{g}(\sigma_{f}(\mathtt{return}(())),\cdots)$

Note that because of the call-by-value paradigm, we need to use thunk
functions, something which is not needed in the $\lambda$Y-calculus. As
expected, in the translation from EPCF to $\lambda$Y-calculus, we have to take
into account of all this along the CPS translation.

##  5\. From EPCF to the $\lambda Y$-Calculus

It is now time to turn the informal arguments we made at the end of the last
section formal. Indeed, translating any EPCF computation into a term of the
$\lambda Y$-calculus is indeed possible, as we are going to show.

The fact that EPCF ground values, arities, and parameters are all taken from
finite types implies that for every algebraic effect signature $\Sigma$, the
signature $\Sigma_{Y}$ defined as $\\{v:0\mid
v\in\mathcal{V}\\}\cup\\{\sigma:k+1\mid((\sigma:\mathtt{B}\rightsquigarrow
k)\in\Sigma)\\}$ is itself finite. This enables the defining of a
transformation from EPCF to the $\lambda Y$-calculus with constants in
$\Sigma_{Y}$, which we first give on types:

###### Definition 0 (CPS Type Transform).

For the sake of conciseness, we use $\neg T$ to denote the type $T\rightarrow
o$. We pose

$\mathtt{B}^{*}=o\qquad\mathtt{k}^{*}=\neg o^{k}\qquad(T\rightarrow
U)^{*}=T^{*}\rightarrow\neg U^{*}\rightarrow o$

We extend this function to contexts, with $\emptyset^{*}=\emptyset$ and
$(\Gamma,x:U)^{*}=\Gamma^{*},x:U^{*}$.

Observe how base types and enumeration types are translated in two essentially
different ways, and that arrows are translated following the usual double-
negation scheme. The following Definition captures how our translation works
on _terms_ :

###### Definition 0 (CPS Term Transformation).

We define $V^{*}$ and $C^{*}$ with the intuition that if $\Gamma\vdash V:T$
and $\Gamma\vdash C:U$ then $\Gamma^{*}\vdash V^{*}:T^{*}$ and $\Gamma\vdash
C^{*}:\neg\neg U^{*}$.

$\displaystyle v^{*}$ $\displaystyle=v\text{ when }v\in\mathcal{V}$
$\displaystyle(\lambda x.C)^{*}$ $\displaystyle=\lambda x.C^{*}$
$\displaystyle x^{*}$ $\displaystyle=x$ $\displaystyle(\mathtt{fix}x.V)^{*}$
$\displaystyle=Y(\lambda x.V^{*})$ $\displaystyle\underline{n}^{*}$
$\displaystyle=\lambda x_{0},\dots,x_{k-1}.x_{n}$
$\displaystyle\mathtt{case}(V;C_{1},\dots,C_{k})^{*}$ $\displaystyle=\lambda
c.V^{*}~{}(C_{1}~{}c)~{}\cdots~{}(C_{k}~{}c)$ $\displaystyle(V~{}W)^{*}$
$\displaystyle=\lambda c.V^{*}~{}W^{*}~{}c$
$\displaystyle(\mathtt{let}~{}x=C~{}\mathtt{in}~{}B)$ $\displaystyle=\lambda
c.C^{*}~{}(\lambda x.B^{*}~{}c)$ $\displaystyle\mathtt{return}(V)^{*}$
$\displaystyle=\lambda c.c~{}V^{*}$ $\sigma(V;x.C)^{*}=\lambda
c.\sigma~{}V^{*}~{}(C^{*}[x:=\underline{0}^{*}]~{}c)~{}\cdots~{}(C^{*}[x:=\underline{k-1}^{*}]~{}c)$

Remark that this translation can be done because of our choice of effect trees
with a special branch for parameters, indeed it is not possible at runtime to
know exactly the value of the parameter $V$ of an algebraic operation, and
with our definition of effect trees, we can postpone the identification of
$V^{*}$ by just passing it as an argument. This translation is well-typed, as
shown by the following lemma, whose proof is straightforward:

###### Lemma 0.

If $\Gamma\vdash V:T$ then $\Gamma^{*}\vdash V^{*}:T^{*}$ and if $\Gamma\vdash
C:U$ then $\Gamma\vdash C^{*}:\neg\neg U^{*}$.

Then, we would like to show that this translation is a simulation. But, in
order to do that, we need to take into account that there are some reductions
that need to be done _outside_ weak head reduction in $\lambda$Y, but those
reductions are actually _administrative_ (Plotkin, 1975; de Groote, 1994;
Hillerström et al., 2017). Formally, we introduce a new reduction relation
$\rightarrow_{\mathit{adm}}$ by way of the following rules:

$(\lambda c.M_{i})~{}c\rightarrow_{\mathit{adm}}M_{i}$ $f$ constant
$(M_{i}\rightarrow_{\mathit{adm}}N_{i})_{1\leq i\leq n}$
$f~{}M~{}M_{1}~{}\cdots~{}M_{k}\rightarrow_{\mathit{adm}}f~{}M~{}N_{1}~{}\cdots~{}N_{k}$

Intuitively, an administrative reduction here consists in applying a
$\beta$-rule, and possibly in the argument of an application (which not
possible in head reduction). We take this small set of rules as it is exactly
what we need to have the simulation, and it should be intuitive that applying
those rules has no consequence in the construction of a Böhm tree of a
$\lambda$Y-term. Remark that we could have defined the transformation of a
$\sigma$ using $(\lambda x.C^{*})~{}\underline{0}^{*}$ instead of directly
$C^{*}[x:=\underline{0}^{*}]$ if we wanted to avoid using substitution in the
encoding. But this would induce more administrative reductions.

###### Lemma 0.

If $C\rightarrow B$ then for all continuation $c$, $C^{*}~{}c\rightarrow^{+}M$
such that $B^{*}~{}c\rightarrow_{\mathit{adm}}^{\leq 2}M$.

###### Proof.

The proof can be done by induction on $C\rightarrow B$. All cases are
straightforward and do not need administrative reduction except for the rule
$\mathtt{let}~{}x=\sigma(V;y.C)~{}\mathtt{in}~{}D\rightarrow\sigma(V;y.\mathtt{let}~{}x=C~{}\mathtt{in}~{}D)$,
in which we do need administrative reductions:

$\displaystyle\lambda c.\sigma~{}V^{*}~{}((\lambda
c.C^{*}[y:=\underline{0}^{*}]~{}(\lambda
x.D^{*}~{}c))~{}c)~{}\cdots~{}((\lambda
c.C^{*}[y:=\underline{k-1}^{*}]~{}(\lambda x.D^{*}~{}c))~{}c)~{}c$
$\displaystyle\rightarrow^{\leq 2}_{\mathit{adm}}$
$\displaystyle\sigma~{}V^{*}~{}(C^{*}[y:=\underline{0}^{*}]~{}(\lambda
x.D^{*}~{}c))~{}\cdots~{}(C^{*}[y:=\underline{k-1}^{*}]~{}(\lambda
x.D^{*}~{}c))$

∎

This means in particular that if a computation $C$ never reaches a normal
form, then $C^{*}~{}c$ does not too. Indeed, the only case when we use the
administrative reduction is the rule for a let with an algebraic operation,
and if this rule can be used in a computation, then the computation will have
a normal form, beginning with this effect. Then, by comparing the normal form
of $C$ and $C^{*}~{}c$, we obtain the following theorem.

###### Theorem 5.

For any $\vdash C:T$, for all $\vdash c:T^{*}\rightarrow o$,
$BT(C^{*}~{}c)=ET(C)[\mathtt{return}(V)\leftarrow BT(c~{}V^{*})]$

Thus, $BT(C^{*}~{}c)$ simulates perfectly the effects of $C$, but for the
return values, instead of a leaf we have a tree representing the effect
applied to this value by the continuation. As a consequence, using standard
results of Higher-Order Model Checking, we have:

###### Corollary 0.

For any $\vdash C:T$ and $\vdash c:T^{*}\rightarrow o$, MSO model-checking on
$ET(C)[\mathtt{return}(V)\leftarrow BT(c~{}V^{*})]$ is decidable.

In particular, if the continuation always return a new constant $K$ for
example, then $BT(C^{*}~{}c)$ is equal to $ET(C)$ with all return leaves
replaced by $K$. Also, if the type $T$ is a ground type, then $c$ can be taken
as the identity, and we have exactly decidability of MSO model-checking for
$ET(C)$. In general, the set of all possible values in the form
$\mathtt{return}(V)$ for a type $T$ is infinite, as they could be
$\lambda$-abstractions for example, but the previous theorem gives us a degree
of freedom as we can always chose the continuation that we want in order to
distinguish some of those values.

##  6\. Specifications Through Observations

In the previous section, we proved that EPCF computations can be translated
into equivalent (in the sense of the tree they generate) $\lambda Y$-terms.
But how can we actually _exploit_ this result for the sake of verifying
interesting properties about the effect produced by EPCF programs? Of course,
we can automatically verify whether any MSO formula has (the effect tree
generated by) any EPCF term as its model. But, is it the end of the story?

As already, mentioned, there are many proposals in the literature (Plotkin and
Pretnar, 2008; Simpson and Voorneveld, 2019; Matache and Staton, 2019) about
_logics_ specifically designed for the sake of expressing properties of
interest for effectful (possibly higher-order) programs. In this paper we will
somehow follow the path recently hinted at by Simpson and Voorneveld (Simpson
and Voorneveld, 2019).

Effect trees as we have used them so far are not subject to any _equational
theory_ , the latter often being associated to effects and justified by a
monadic interpretation (Moggi, 1988). As an example, the following equations
hold in the state monad, itself a way to interpreting the first example from
Section 2:

$\mathbf{Set}(\ell,\mathtt{true},\\_.\mathbf{Get}(\ell,y.C))=\mathbf{Set}(\ell,\mathtt{true},\\_.C[y:=\underline{1}])\quad\mathbf{Set}(\ell,a,\\_.\mathbf{Set}(\ell,b,\\_.C))=\mathbf{Set}(\ell,b,\\_.C)$

As pointed out in (Simpson and Voorneveld, 2019), we can capture equations
between effect trees agnostically, without the need of explicitly referring to
monads, through the notion of an _observation_ , namely a set of _properties_
of effect trees:

###### Definition 0 (Observations (Simpson and Voorneveld, 2019)).

For a given set of algebraic operations $\Sigma$, we define a set of
_observations_ as a set, denoted $\mathcal{O}$, such that each
$o\in\mathcal{O}$ is a subset of the effect trees of type $\mathtt{unit}$.

On top of a set of observations $\mathcal{O}$, Simpson and Voorneveld define a
logic endowed with a modal operator of the form $o\phi$, where $o$ is an
element of $\mathcal{O}$ and $\phi$ is a formula. An effect tree satisfies
$o\phi$ if it is among the trees in $o$ _and_ all its leaves satisfy $\phi$.
This way, the logic can _observe_ the tree at hand through the lenses of the
observations in $\mathcal{O}$, implicitly accounting for equations: it is
necessary to define $\mathcal{O}$ such that all its elements are invariant by
the desired set of equations. The resulting logic is quite powerful, being
infinitary in nature, and turns out to precisely capture observational
equivalence (Dal Lago et al., 2017) for (a calculus closely related to) EPCF.
Noticeably, most notions of effects, including nondeterministic, probabilistic
and state effects can be captured this way (Simpson and Voorneveld, 2019)

Unfortunately, however, the aforementioned logic is strictly more powerful
than MSO or the $\mu$-calculus. This happens for two distinct reasons: on the
one hand, it is essentially infinitary in nature, this way accounting for the
fact that the target calculus has _countable_ types. On the other hand, the
underlying set of observations $\mathcal{O}$ can be arbitrarily complex, thus
injecting a huge discriminating power into the logic, something that MSO
cannot do natively.

Motivated by all that, we address the following question in the rest of this
section: can we express useful properties of effect trees as observations
_from within_ MSO itself? In other words, is it the case that for a given
notion of effect, all the elements of $\mathcal{O}$ are captured by MSO
formulas? This way, we could at least be sure, given the results from Section
5, that model-checking is decidable _relative to_ $\mathcal{O}$. This is
precisely what motivates the following definition of an extension of MSO (or
$\mu$-calculus) with observation.

###### Definition 0 (Observation Predicate).

Suppose given a signature $\Sigma$ for effect trees, containing a set of
algebraic operations, and a set of other possible constructors (that could
come, e.g., from parameter values, or special constants of the
$\lambda$Y-calculus). Fix a set of observations $\mathcal{O}$. Let
$t\in\mathbf{Tree}_{\Sigma}$, and $P$ a subset of all the possible
constructors of arity $0$. We define $t[\in P]$ as the tree obtained from $t$
by replacing the leaves in $P$ with $\mathtt{return}(())$ and all the other
leaves with $\bot$. We next define, for each $o\in\mathcal{O}$ and each $P$, a
formula $o_{P}$, called an observation predicate, such that for any effect
tree t, we have

$t\vDash o_{P}\text{ iff }t[\in P]\in o$

Note that we have indeed that $t[\in P]$ is an effect tree of type
$\mathtt{Unit}$, thus it can be an element of $o$. Write
$\mathsf{MSO}_{\mathcal{O}}$ for the conservative extension of MSO (on
infinite trees) obtained by enriching the class of formulas with observation
predicates.

This notion of observation predicate having access to a set $P$ is, thanks to
finiteness, equiexpressive to the formulas $o\phi$ defined in (Simpson and
Voorneveld, 2019), in which $\phi$ is supposed to be a formula that separates
the correct leaves from the incorrect ones in an _infinite_ set of leaves.
Here, because of finiteness, we have a finite number of such separations, thus
we can take a set $P$ instead of a formula $\phi$.

$\mathsf{MSO}_{\mathcal{O}}$ can thus be seen as a reasonable logic for
writing down specifications about higher-order effectful programs. But is the
model checking problem emerging out of it decidable? There are at least two
possible answers to this question:

  * •

Either the observation predicates from $\mathcal{O}$ are definable in MSO
_itself_ , in this case $\mathsf{MSO}_{\mathcal{O}}$ is equiexpressive with
MSO, and the model checking problem remains decidable.

  * •

Or observation predicates are not MSO-definable, and we cannot conclude, with
the concrete risk of landing into an undecidable verification problem.

We will now see some cases of effects and observations, each of them
corresponding to one of the two cases above. Let us start from an example of
effect which is hard to capture.

###### Example 0 (Probabilistic Observations).

The typical counter-example of effects to MSO-definability of observation
predicates comes from probabilistic effects. The set of observations for
probabilistic choice, with a unique operation
$\mathbf{Flip}:\mathtt{unit}\rightsquigarrow 2$, is given by
$\mathcal{O}=\\{o_{>q}\;\mbox{\Large{$\mid$}}\;q\in\mathbb{Q},0\leq q<1\\}$.
Essentially, an observation predicate $o_{>q}$ means that the probability that
the program terminates is greater than $q$. This is _not_ a property which can
be defined in MSO on effect trees, and this happens for very good reasons,
since we know that higher-order model checking for probabilistic HORSs is in
general undecidable (Kobayashi et al., 2020)).

Before going into positive examples, we need to solve a small discrepancy
between the literature on algebraic effects, especially with the standard
definition of effect trees (Simpson and Voorneveld, 2019). Indeed, as
explained in Section 4, the Definition 2 that introduces effect trees in our
work is slightly different from the standard notion of effect tree, which was
essential for the translation of Section 5. However, in practice we would like
to work directly with standard effect trees, as we did in Section 2, since
they are simpler and corresponds to the literature. Concretely, we can show
that our definition is not harmful for the question of MSO model-checking,
since we can transfer any MSO properties (or APT) on standard effect trees to
properties on effect trees with a special branch for parameters. Formally, we
have:

###### Definition 0 (Adding a branch for parameters).

For any tree $t$ defined with the signature

$\Sigma^{\prime}=\\{\sigma_{v}:k\mid((\sigma:\mathtt{B}\rightsquigarrow
k)\in\Sigma)\land(\vdash v:\mathtt{B}\in\mathcal{V})\\}\cup S$

where $S$ is a set of possible other constructors (coming from a chosen
continuation in the $\lambda$Y-calculus according to Corollary 6 for example),
we define the tree $t_{p}$ with the signature

$\Sigma=\\{\sigma:k+1\mid((\sigma:\mathtt{B}\rightsquigarrow
k)\in\Sigma)\\}\cup\\{v:0\;\mbox{\Large{$\mid$}}\;v\in\mathcal{V}\\}\cup S$

as the tree $t$ in which all nodes $\sigma_{v}(t^{1},\cdots,t^{k})$ are
replaced by the tree $\sigma(v,t^{1}_{p},\cdots,t^{k}_{p})$. This translation
corresponds exactly to the translation of a standard effect tree to the one we
introduced in Definition 2.

We can show that any formula (or APT) that is definable in standard effect
tree in $\mathbf{Tree}_{\Sigma^{\prime}}$ is definable for the effect trees in
$\mathbf{Tree}_{\Sigma}$ of Definition 2.

###### Proposition 5 (Effect Trees and APT).

For any APT $\mathcal{A}$ that recognizes _standard_ effect trees in
$\mathbf{Tree}_{\Sigma^{\prime}}$, there exists an APT $\mathcal{A}_{p}$ that
recognizes the set
$\\{t_{p}\in\mathbf{Tree}_{\Sigma}\;\mbox{\Large{$\mid$}}\;t\text{ is accepted
by }\mathcal{A}\\}$

###### Proof.

The proof consists in adding a special state $q_{v}$ for each variable
$v\in\mathcal{V}$ and define transition as a big _or_ depending on the value
of the parameter. Formally, we define
$\mathcal{A}_{p}=(\Sigma,Q_{p},\delta_{p},q_{i},\Omega_{p})$ such that:

  * •

$Q_{p}\triangleq Q\sqcup\\{q_{v}\;\mbox{\Large{$\mid$}}\;v\in\mathcal{V}\\}$

  * •

$\Omega_{p}(q)=\Omega(q)$ for $q\in Q$ and $\Omega_{p}(q_{v})=0$.

  * •

For the transition function we have:

    * –

$\delta_{p}(q,s)=\delta(q,s)$ if $s\in S$

    * –

For all $\sigma:\mathtt{B}\rightsquigarrow k$, we have
$\delta_{p}(q,\sigma)=\bigvee\limits_{v:\mathtt{B}\in\mathcal{V}}(\delta(q,\sigma_{v})[+1]\land(0,q_{v}))$
where $\phi[+1]$ is the formula $\phi$ in which all couples $(n,r)$ are
replaced by $(n+1,r)$.

    * –

For all $v\in\mathcal{V}$, $\delta_{p}(q_{v},v)=\mathtt{tt}$ and
$\delta_{p}(q_{v},f)=\mathtt{ff}$ for all $f\neq v$.

Thus, intuitively, when we reach a node $\sigma$, only one of all the
$(0,q_{v})$ will be satisfied, the one corresponding to the actual parameter
$v$ of $\sigma$. And then, the only satisfiable formula in this big or would
be $\delta(q,\sigma_{v})[+1]\land(0,q_{v})$, meaning that the transition is
logically equivalent to $\delta(q,\sigma_{v})[+1]$. Thus, we can see that the
new transition $\delta_{p}(q,\sigma)$ is equivalent to the actual formula
$\delta(q,\sigma_{v})[+1]$ where $v$ is the parameter of $\sigma$ in the tree
$t_{p}$, and from this it is straightforward to see that $\mathcal{A}_{p}$
recognizes the set $\\{t_{p}\;\mbox{\Large{$\mid$}}\;t\text{ is accepted by
}\mathcal{A}\\}$. ∎

Let us now turn to examples of observations which are indeed MSO-definable.

###### Example 0 (Non-determinism).

Let us consider the unique effect $\\{or:\mathtt{Unit}\rightsquigarrow 2\\}$.
The notion of observations for non-determinism is given by the two modalities
$\diamond$ and $\square$, where $\diamond_{P}$ is the set of effect trees that
has at least one finite branch with a leaf in $P$, and $\square_{P}$ is the
set of effect trees that has only finite branches, and all of them has a leaf
in $P$.

Those observations are definable by an APT. For the sake of the example, we
explain informally the encoding of $\square_{P}$. We take a unique state
$q_{i}$. To impose finite branching everywhere, it is sufficient to pose
$\Omega(q_{i})=1$, because with this no infinite branch satisfies the parity
condition. Then, We can just explore through the tree, with the transition
$\delta(q_{i},or)=(0,q_{i})\land(1,q_{i})$. And finally, we can separate
leaves with $\delta(q_{i},a)=\mathtt{tt}$ if $a\in P$ and
$\delta(q_{i},a)=\mathtt{ff}$ if $a\notin P$ for all leaves $a$.

###### Example 0 (Finite State Monad).

Going back to the examples used in Section 2, we start with the state monad,
where the effects are $\mathbf{Get}$ and $\mathbf{Set}$, with finite domains.
As expressed in (Simpson and Voorneveld, 2019), the set of observations for
this effect is defined by

$\mathcal{O}=\\{o_{p\mapsto q}\;\mbox{\Large{$\mid$}}\;p,q\text{ are memory
states}\\}$

with the intuitive semantics that $o_{p\mapsto q}$ contains all effect trees
mapping the state $p$ to the state $q$ (this computation is deterministic
because the initial state is fixed, so we always know which branch should be
taken on a $\mathbf{Get}$). It is easy to see that the observations predicates
coming from this set are definable in an APT, because an observation predicate
$(o_{p\mapsto q})_{P}$ can be represented by an automaton starting from the
state $p$, that accepts only when the unique path leads to a leaf $x\in P$ in
the state $q$, similarly to the automata defined in Section 2. Thus, as
expected, we can deduce that many interesting properties can be decided on
programs using a finite state monad, since the observations are MSO-definable.

##  7\. A Calculus of Effects and Handlers

An algebraic operation in a language such as EPCF comes out _uninterpreted_ :
a computation produces an effect tree, in which all algebraic operations are
tree constructors, and no meaning is given to operations in this tree. The
notion of observation can indeed be seen as a way to at least identify trees
which should be considered the same, implicitly capturing equations between
them. Observations, however, attribute a _static_ meaning to programs, and the
programmer has no control over them. There is however yet another way of
attributing meaning to effects in which the programmer has direct control on
what happens. This can be seen as an abstraction on the notion of an exception
handler, but also of, e.g., the HASKELL’s monad construction. We are referring
of course to the so-called _effect handlers_ (Kammar et al., 2013).

In this section, we present a calculus obtained by endowing EPCF with effect
handlers, called HEPCF, whose definition closely follows the literature on the
subject (Kammar et al., 2013; Hillerström et al., 2017). This is necessary to
even understand what doing model checking actually means in presence of
handlers, this way paving the way for positive and negative results about it,
which are deferred to the next Section.

The language HEPCF differs from EPCF both at the level of terms and at the
level of types. The former are extended with the $\mathtt{handle}$ clause, in
which a computation is evaluated in a protected environment, in such a way as
to be able to capture (and handle) the effects it raises. The latter are
enriched with annotations keeping track of which ones among the operations are
visible. The syntax of HEPCF is defined as follows:

(Types) $\displaystyle T,U$ $\displaystyle::=\mathtt{B}\mid k\mid
T\rightarrow_{E}U$ (Effects) $\displaystyle E$
$\displaystyle::=\emptyset\;\mbox{\Large{$\mid$}}\;\\{\sigma:\mathtt{B}\rightsquigarrow
k\\}\cup E$ (Values) $\displaystyle V,W$
$\displaystyle::=v\;\mbox{\Large{$\mid$}}\;\underline{n}\;\mbox{\Large{$\mid$}}\;x\;\mbox{\Large{$\mid$}}\;\lambda
x.C\;\mbox{\Large{$\mid$}}\;\mathtt{fix}~{}f.V$ (Computations) $\displaystyle
C,D$
$\displaystyle::=V~{}W\;\mbox{\Large{$\mid$}}\;\sigma(V;x.C)\;\mbox{\Large{$\mid$}}\;\mathtt{return}(V)\;\mbox{\Large{$\mid$}}\;\mathtt{let}~{}x=C~{}\mathtt{in}~{}D$
$\displaystyle\phantom{::=}\;\mbox{\Large{$\mid$}}\;\mathtt{with}~{}H~{}\mathtt{handle}~{}C\;\mbox{\Large{$\mid$}}\;\mathtt{case}(V;C_{1},\dots,C_{k})$
(Handlers) $\displaystyle H$ $\displaystyle::=\\{\mathtt{return}(x)\mapsto
C_{r}\\}\cup\\{\sigma_{i}(x;r)\mapsto C_{i}\mid 1\leq i\leq n\\}$

We add a new information in the type $T\rightarrow_{E}U$, denoting the set $E$
of available algebraic operation the function at hand can possibly perform
once applied to an argument of type $T$. An handler consists of a return
clause $\mathtt{return}(x)\mapsto C_{r}$ and one clause
$\sigma_{i}(x;r)\mapsto C_{i}$ for each handled operation $\sigma_{i}$ in some
effect set $E$. The intuition behind such an handler is that it takes a
computation using the effects in $\\{\sigma_{i}\mid 1\leq i\leq n\\}$, and
interprets each call to the algebraic operation $\sigma_{i}$ as the
computation $C_{i}$ in which the continuation is passed as a variable $r$. The
return computation $C_{r}$ is called when the initial computation returns a
value.

Selected rules of the type system are in Figure 7. A judgment attributing a
type to a computation $C$ now has the shape $\Gamma\vdash_{E}C:T$, meaning
that $C$ has the type $T$ in the effect context $E$.

$\Gamma,x:T\vdash_{E}C:U$ $\Gamma\vdash\lambda x.C:T\rightarrow_{E}U$
$\Gamma,f:T\rightarrow_{E}U\vdash V:T\rightarrow_{E}U$
$\Gamma\vdash\mathtt{fix}~{}f.V:T\rightarrow_{E}U$ $\Gamma\vdash
V:T\rightarrow_{E}U$ $\Gamma\vdash W:T$ $\Gamma\vdash_{E}V~{}W:U$
$(\sigma:\mathtt{B}\rightsquigarrow k)\in E$ $\Gamma\vdash V:\mathtt{B}$
$\Gamma,x:k\vdash_{E}C:T$ $\Gamma\vdash_{E}\sigma(V;x.C):T$ $\Gamma\vdash V:T$
$\Gamma\vdash_{E}\mathtt{return}(V):T$ $\Gamma\vdash_{E}C:U$
$\Gamma,x:U\vdash_{E}D:T$
$\Gamma\vdash_{E}\mathtt{let}~{}x=C~{}\mathtt{in}~{}D:T$ $\Gamma\vdash V:k$
$(\Gamma\vdash_{E}C_{i}:T)_{1\leq i\leq k}$
$\Gamma\vdash_{E}\mathtt{case}(V;C_{1},\dots,C_{k}):T$ $\Gamma\vdash
H:U_{E^{\prime}}\Rightarrow_{E}T$ $\Gamma\vdash_{E^{\prime}}C:U$
$\Gamma\vdash_{E}\mathtt{with}~{}H~{}\mathtt{handle}~{}C:T$
$E^{\prime}=\\{\sigma_{i}:\mathtt{B}_{i}\rightsquigarrow k_{i}\mid 1\leq i\leq
n\\}$ $\Gamma,x:U\vdash_{E}C_{r}:T$
$\Gamma,x:\mathtt{B}_{i},r:k\rightarrow_{E}T\vdash_{E}C_{i}:T$
$\Gamma\vdash\\{\mathtt{return}\mapsto C_{r}\\}\cup\\{\sigma_{i}(x;r)\mapsto
C_{i}\mid 1\leq i\leq n\\}:U_{E^{\prime}}\Rightarrow_{E}T$

Figure 7. Static Semantics of HEPCF

As the reader can see in the rule for a call to an algebraic operation, a
computation of type $\Gamma\vdash_{E}C:T$ can only give rise to the operations
in $E$. As expected, a handler takes a computation $C$ of some type $U$ that
uses the effects in $E^{\prime}$ and transforms this computation into a
computation of type $T$ using the effects in $E$. This operation is very
similar in principles to an application, that is why we describe the type of
an handler with an arrow type. In details, the type
$U_{E^{\prime}}\Rightarrow_{E}T$ means that all the computations defined in
the typed handler should use only the effect in $E$, and the handled
operations are exactly those in $E^{\prime}$. In such a context, a
continuation for an algebraic operation is given as the variable $r$ of type
$k\rightarrow_{E}T$, meaning that this continuation is, as expected, of type
$T$ with effects in $E$, and there are $k$ different continuations of this
type, corresponding to the $k$ possible branches of this algebraic operation.

Finally, the dynamic semantics of HEPCF is described in Figure 8 and Figure 6.

$C\rightarrow C^{\prime}$
$\mathtt{with}~{}H~{}\mathtt{handle}~{}C\rightarrow\mathtt{with}~{}H~{}\mathtt{handle}~{}C^{\prime}$
$H\equiv\\{\mathtt{return}(x)\mapsto C_{r}\\}\cup\\{\sigma_{i}(x;r)\mapsto
C_{i}\mid 1\leq i\leq n\\}$
$\mathtt{with}~{}H~{}\mathtt{handle}~{}\mathtt{return}(V)\rightarrow
C_{r}[x:=V]$ $H\equiv\\{\mathtt{return}(x)\mapsto
C_{r}\\}\cup\\{\sigma_{i}(x;r)\mapsto C_{i}\mid 1\leq i\leq n\\}$
$\mathtt{with}~{}H~{}\mathtt{handle}~{}\sigma_{i}(V;x.C)\rightarrow
C_{i}[x:=V,r:=(\lambda x.\mathtt{with}~{}H~{}\mathtt{handle}~{}C)]$

Figure 8. Semantics for HEPCF

As expected, handling a returned value consists in calling the return clause,
and for the case of an algebraic operation, it is important to note that the
handler acts also on the continuation. As for the definition of an effect
tree, we can see that as before, a closed typed computation $\vdash_{E}C:T$ in
normal form is either an algebraic operation in $E$ or $\mathtt{return}(V)$,
thus we can define effect trees similarly to Definition 2, with the signature
$E$ instead of $\Sigma$. Note that we can see the typing $\vdash
H:T_{E^{\prime}}\Rightarrow_{E}U$ as defining a tree operation from effect
trees on $E^{\prime}$ of type $T$ to effect trees on $E$ of type $U$. In
practice, this transformation takes a tree defined by $\vdash_{E^{\prime}}C:T$
and gives a tree defined by
$\vdash_{E}\mathtt{with}~{}H~{}\mathtt{handle}~{}C:U$. We will see in the next
section that, unfortunately, the tree transformations that can be expressed by
handlers form a very large class, definitely too broad for our purposes.

##  8\. Model Checking Handled Effects: Positive and Negative Results

In the previous section, we introduced effect handlers, a very powerful and
elegant linguistic construction by which the interpretation of algebraic
operations can somehow be delegated to the programmer. In this section that
this notion of handlers is too expressive for our purposes, meaning that MSO
model-checking of effect trees produced by terms of HEPCF is _not_ decidable.
We will also show that when handlers have a restricted but non-trivial form
model checking becomes decidable.

###  8.1. Undecidability Through the Halting’s Problem

The proof of undecidability is structured around the encoding of Plotkin’s PCF
into HEPCF. The encoding is not trivial, because PCF is taken in its full
generality (thus including a type of natural numbers) while HEPCF only has
_finite_ base types. Since the halting problem for PCF is well-known to be
undecidable, and can be written down as an MSO formula, undecidability of the
HOMC problem for HEPCF easily follows. Formally, we introduce standard PCF as
the following language:

###### Definition 0 (Plotkin’s PCF).

The PCF language (in fine-grained call-by-value) is defined by the following
grammar:

(Types) $\displaystyle T$ $\displaystyle::=\mathtt{Nat}\mid T\rightarrow U$
(Values) $\displaystyle V,W$
$\displaystyle::=0\;\mbox{\Large{$\mid$}}\;\mathtt{succ}(V)\;\mbox{\Large{$\mid$}}\;x\;\mbox{\Large{$\mid$}}\;\lambda
x.C\;\mbox{\Large{$\mid$}}\;\mathtt{fix}~{}f.V$ (Computations) $\displaystyle
C,D$
$\displaystyle::=V~{}W\;\mbox{\Large{$\mid$}}\;\mathtt{return}(V)\;\mbox{\Large{$\mid$}}\;\mathtt{let}~{}x=C~{}\mathtt{in}~{}D\;\mbox{\Large{$\mid$}}\;\mathtt{case}(V;0\mapsto
C;\mathtt{succ}(x)\mapsto D)$

This is a well-known language for which the halting problem is not decidable:
encoding all partial recursive functions is an easy exercise. We omit the
definition of the static and dynamic semantics, which are anyway natural and
very standard.

In order to prove the undecidability of HEPCF we show a translation from PCF
to HEPCF. Again, note that the crucial difference between the two languages is
that PCF has access to an infinite type $\mathtt{Nat}$ for natural numbers,
with a pattern matching constructor, whereas in HEPCF there are handlers and
algebraic effects but all base types must be finite. But how could we encode
the infinite type of natural numbers using finite types, effects and handlers?
In order to do this, we introduce the effect
$E=\\{\sigma:\mathtt{Unit}\rightsquigarrow 1\\}$. For the sake of simplicity,
we will ignore the parameter for this operation, of type $\mathtt{Unit}$.
Intuitively, we will represent a natural number $n$ by a computation in which
this operation $\sigma$ is called exactly $n$ times, and then the computation
halts by returning the only inhabitant of the type $\mathtt{Unit}$. But,
because a natural number $n$ is supposed to be a value, we will use a thunk
function $f_{n}$ along the encoding, and each time we need to inspect the
value of a natural number $n$, we can call $f_{n}()$ to produce the effect
tree corresponding to the tree representation of this number $n$.

###### Definition 0 (Translation from PCF to HEPCF).

For any type $T$ of HEPCF we define the _zero_ of this type, denoted
$\mathtt{Z}_{T}$ as follows:

$\mathtt{Z}_{\mathtt{Unit}}=()\qquad\mathtt{Z}_{k}=\underline{0}\qquad\mathtt{Z}_{T\rightarrow_{E}U}=\lambda
x.\mathtt{return}(\mathtt{Z}_{U})$

Intuitively, the zero of a type is just a particular closed value of this type
chosen arbitrarily, in which no effects are used. For the sake of clarity, we
introduce a notation for several $\lambda$-abstractions and several
applications in a row:

$\lambda f,g.C\triangleq\lambda f.\mathtt{return}(\lambda g.C)\qquad
V~{}W_{1}~{}W_{2}\triangleq\mathtt{let}~{}x=V~{}W_{1}~{}\mathtt{in}~{}(x~{}W_{2})$

for which we obtain, as expected, that $(\lambda
f,g.C)W_{1}~{}W_{2}\rightarrow^{+}C[f:=W_{1}][g:=W_{2}]$. The translation
$\llbracket\cdot\rrbracket$ from PCF to finitary HEPCF is then given by

$\llbracket\mathtt{Nat}\rrbracket=\mathtt{Unit}\rightarrow_{E}\mathtt{Unit}\qquad\llbracket
T\rightarrow U\rrbracket=\llbracket T\rrbracket\rightarrow_{E}\llbracket
U\rrbracket$ $\displaystyle\llbracket 0\rrbracket$
$\displaystyle\triangleq\mathtt{Z}_{\llbracket Nat\rrbracket}$
$\displaystyle\llbracket\mathtt{succ}(V)\rrbracket$
$\displaystyle\triangleq\lambda x.\sigma(y.\llbracket V\rrbracket())$
$\displaystyle\llbracket x\rrbracket$ $\displaystyle\triangleq x$
$\displaystyle\llbracket\lambda x.C\rrbracket$ $\displaystyle\triangleq\lambda
x.\llbracket C\rrbracket$ $\displaystyle\llbracket\mathtt{fix}f.V\rrbracket$
$\displaystyle\triangleq\mathtt{fix}f.\llbracket V\rrbracket$
$\displaystyle\llbracket V~{}W\rrbracket$ $\displaystyle\triangleq\llbracket
V\rrbracket~{}\llbracket W\rrbracket$
$\displaystyle\llbracket\mathtt{return}(V)\rrbracket$
$\displaystyle\triangleq\mathtt{return}(\llbracket V\rrbracket)$
$\displaystyle\llbracket\mathtt{let}~{}x=C~{}\mathtt{in}~{}D\rrbracket$
$\displaystyle\triangleq(\mathtt{let}~{}x=\llbracket
C\rrbracket~{}\mathtt{in}~{}\llbracket D\rrbracket)$
$\llbracket\mathtt{case}(V;0\mapsto C;\mathtt{succ}(n)\mapsto
D)\rrbracket\triangleq\mathtt{let}~{}a=(\mathtt{with}~{}H(C,D)~{}\mathtt{handle}~{}\llbracket
V\rrbracket~{}())~{}\mathtt{in}~{}(a~{}(\lambda f,g.g~{}()))$

where $H(C,D)$ is defined, when $C$ and $D$ have type $T$, by:

$\displaystyle\mathtt{return}(V)$ $\displaystyle\mapsto\mathtt{return}(\lambda
p.p~{}\mathtt{Z}_{\mathtt{Unit}\rightarrow\mathtt{Unit}}~{}(\lambda
x.\llbracket C\rrbracket))$ $\displaystyle\sigma(r)$
$\displaystyle\mapsto\mathtt{let}~{}n=\mathtt{return}(\lambda
x.\mathtt{let}~{}y=r~{}\underline{0}~{}(\lambda
f,g.\mathtt{let}~{}z=f~{}()~{}\mathtt{in}~{}\mathtt{Z}_{\llbracket
T\rrbracket})~{}\mathtt{in}~{}\mathtt{return}(\mathtt{Z}_{\mathtt{Unit}}))~{}\mathtt{in}$
$\displaystyle\phantom{\mapsto}~{}\mathtt{return}(\lambda p.p~{}(\lambda
x.\sigma(z.n~{}()))~{}(\lambda x.\llbracket D\rrbracket))$

Let us now give some hints about the translation. As expected, zero is just
the function that return $()$ when called, and a successor is a call to the
effect $\sigma$. In order to do the pattern matching for a natural number $V$
given as a thunk function $\llbracket V\rrbracket$, we produce the effect tree
representing $n$, by calling $\llbracket V\rrbracket()$, and we handle it.
This handler produces a pair of thunk computations. The first computation is
just a copy of the initial computation $\llbracket V\rrbracket()$. This is
rather obvious for the return clause, and for the case of $\sigma$, the value
$n$ corresponds intuitively to just taking the first computation in $r$, thus
a copy of the predecessor, and in the returned pair of computation, the first
pair is $\sigma$ applied to this $n$, which gives the successor of the
predecessor, i.e. a copy of the current number. The second computation
simulates the initial pattern matching. For the case of a zero, the second
computation is just $C$, and for the case of a successor (an operation
$\sigma$), the second computation takes the copy of the predecessor given by
$n$, and then returns the computation $D$ that uses this predecessor.

The proof that this translation is correct is inspired by the proof of the
encoding of shallow handlers using deep handlers, described in (Hillerström
and Lindley, 2018). Intuitively, this is because a shallow handler is a
handler that only handles the root of an effect tree, which is exactly what a
pattern matching here is supposed to do. First, we can show that this
translation is well-typed:

###### Lemma 0.

If $\Gamma\vdash V:T$ then $\llbracket\Gamma\rrbracket\vdash\llbracket
V\rrbracket:\llbracket T\rrbracket$ and if $\Gamma\vdash C:T$ then
$\llbracket\Gamma\rrbracket\vdash_{E}\llbracket C\rrbracket:\llbracket
T\rrbracket$

###### Proof.

The proof is direct except for the $\mathtt{case}$ construct, where we need to
prove this intermediate result:

If $\Gamma\vdash C:T$, $\Gamma,n:\mathtt{Nat}\vdash D:T$,
$\llbracket\Gamma\rrbracket\vdash\llbracket C\rrbracket:\llbracket
T\rrbracket$ and
$\llbracket\Gamma\rrbracket,n:\llbracket\mathtt{Nat}\rrbracket\vdash\llbracket
D\rrbracket:\llbracket T\rrbracket$, then

$\llbracket\Gamma\rrbracket\vdash
H:\mathtt{Unit}_{E}\Rightarrow_{E}((\mathtt{Unit}\rightarrow\mathtt{Unit})\rightarrow(\mathtt{Unit}\rightarrow\llbracket
T\rrbracket)\rightarrow\llbracket T\rrbracket)\rightarrow\llbracket
T\rrbracket$

With this type in mind, the proof that $H(C,D)$ respects this type is
straightforward, and we can conclude that the translation for $\mathtt{case}$
is well-typed. ∎

We want to prove that the translation is a correct simulation. In order to do
this, we need to introduce formally an approximation of a term up to some
administrative context, as in (Hillerström and Lindley, 2018), because in this
translation we encode integers as functions, and we will sometimes have a term
that is overly complex because all the computation is hidden behind a
$\lambda$, but this term will behave exactly like another simple term
corresponding to the encoding of an integer. This is exactly what happens
here; the variable $n$ in the handler is essentially a copy of the
predecessor, but syntactically $n$ is described as a complex computation.

###### Definition 0 (Administrative Contexts (See (Hillerström and Lindley,
2018),Definition 6)).

Evaluation contexts are defined with the following grammar:

$\displaystyle\mathcal{E}::=[]\;\mbox{\Large{$\mid$}}\;\mathtt{let}~{}x=\mathcal{E}~{}\mathtt{in}~{}C\;\mbox{\Large{$\mid$}}\;\mathtt{with}~{}H~{}\mathtt{handle}~{}\mathcal{E}$

They corresponds exactly to context in which a computation can be reduced. An
evaluation context $\mathcal{E}$ for a computation is called _administrative_
, denoted adm($\mathcal{E}$) if and only if:

  * •

For all values $V$,
$\mathcal{E}[\mathtt{return}(V)]\rightarrow^{*}\mathtt{return}(V)$

  * •

For all operations $\sigma$,
$\mathcal{E}[\sigma(V;x.C)]\rightarrow^{*}\sigma(V;x.D)$ with
$D\rightarrow^{*}\mathcal{E}[C]$.

Remark that the composition of two administrative contexts is also an
administrative context.

###### Definition 0 (Approximation up to Administrative Reductions (See
(Hillerström and Lindley, 2018),Definition 7)).

We define $\geq$ for terms as the closure under _any_ context of the following
rule:

$C\geq C$ $adm(\mathcal{E})$ $C\geq D$ $\mathcal{E}[C]\geq D$ $C\rightarrow
C^{\prime}$ $C^{\prime}\geq D$ $C\geq D$

Intuitively, we have $C\geq D$ when $C$ could be reduced to $D$ using strong
rules of reduction (reducing under any context) without changing normal forms
(of the form $\mathtt{return}$ or $\sigma$).

We can then prove the following lemma on this approximation, showing that the
properties of administrative context are valid for approximations.

###### Lemma 0.

If $C^{\prime}\geq C$ then:

  * •

If $C$ is $\mathtt{return}(V)$, then
$C^{\prime}\rightarrow^{*}\mathtt{return}(V^{\prime})$ with $V^{\prime}\geq V$

  * •

If $C$ is $\sigma(V;y.B)$, then
$C^{\prime}\rightarrow^{*}\sigma(V^{\prime};y.B^{\prime})$ with
$B^{\prime}\geq B$

###### Proof.

We proceed by induction on $C^{\prime}\geq C$. All the contextual rules are
straightforward because $C^{\prime}$ has directly the desired shape in this
case.

  * •

If $C^{\prime}\equiv\mathcal{E}[C^{\prime\prime}]$ with $C^{\prime\prime}\geq
C$, then we have, by induction hypothesis, if $C\equiv\mathtt{return}(V)$ then
$C^{\prime}\rightarrow^{*}\mathcal{E}[\mathtt{return}(V^{\prime})]\rightarrow^{*}\mathtt{return}(V^{\prime})$
with $V^{\prime}\geq V$ since $\mathcal{E}$ is administrative. Similarly, if
$C\equiv\sigma(V;y.B)$ then
$C^{\prime}\rightarrow^{*}\mathcal{E}[\sigma(V^{\prime};y.B^{\prime})]\rightarrow^{*}\sigma(V^{\prime},y.B^{\prime\prime})$
with $B^{\prime\prime}\rightarrow^{*}\mathcal{E}[B^{\prime}]$ and
$B^{\prime}\geq B$, thus $B^{\prime\prime}\geq B$. Moreover, $V^{\prime}\geq
V$.

  * •

If $C^{\prime}\rightarrow C^{\prime\prime}$ with $C^{\prime\prime}\geq C$,
then this is direct by induction hypothesis.

∎

We can then show that this approximation is a simulation.

###### Lemma 0.

If $C^{\prime}\geq C$ and $C\rightarrow D$ then there exists $D^{\prime}$ such
that $D^{\prime}\geq D$ and $C^{\prime}\rightarrow^{+}D^{\prime}$

###### Proof.

We proceed by induction on $C^{\prime}\geq C$.

  * •

If $C^{\prime}$ is $\mathcal{E}(C^{\prime\prime})$ with $C^{\prime\prime}\geq
C$ and $adm(\mathcal{E})$. Then, by induction hypothesis, there exists
$D^{\prime\prime}$ with $D^{\prime\prime}\geq D$ and
$C^{\prime\prime}\rightarrow^{+}D^{\prime\prime}$. We pose
$D^{\prime}\triangleq\mathcal{E}(D^{\prime\prime})$. Because $\mathcal{E}$ is
an evaluation context, we have
$\mathcal{E}(C^{\prime\prime})\rightarrow^{+}\mathcal{E}(D^{\prime\prime})$,
and because $\mathcal{E}$ is administrative, we have
$\mathcal{E}(D^{\prime\prime})\geq D$. This concludes this case.

  * •

If $C^{\prime}\rightarrow C^{\prime\prime}$ with $C^{\prime\prime}\geq C$.
Then by induction hypothesis, there exists $D^{\prime\prime}$ such that
$C^{\prime\prime}\rightarrow^{+}D^{\prime\prime}$ with $D^{\prime\prime}\geq
D$, and we can pose $D^{\prime}\triangleq D^{\prime\prime}$.

  * •

If $C^{\prime}$ is $V^{\prime}~{}W^{\prime}$ with $V^{\prime}\geq V$ and
$W^{\prime}\geq W$, and $C=V~{}W$. Then, there are two cases to consider
depending on the reduction $C\rightarrow D$.

    * –

$V=\lambda x.E$ for some computation $E$. Then, by definition,
$V^{\prime}=\lambda x.E^{\prime}$ with $E^{\prime}\geq E$. The reduction gives
us $C\rightarrow E[x:=W]$. But, we have $C^{\prime}\rightarrow
E^{\prime}[x:=W^{\prime}]$, and $E^{\prime}[x:=W^{\prime}]\geq E[x:=W]$. This
concludes this case.

    * –

The case $V=\mathtt{fix}f.U$ is similar to the previous one, we take the
obvious reduction and it concludes.

  * •

$C^{\prime}$ cannot be of the shape $\mathtt{return}(V)$ or $\sigma(V;x.B)$
because it would mean that $C$ is in normal form, and thus cannot be reduced.

  * •

If $C\equiv\mathtt{let}~{}x=C_{1}~{}\mathtt{in}~{}C_{2}$ and
$C^{\prime}\equiv\mathtt{let}~{}x=C_{1}^{\prime}~{}\mathtt{in}~{}C_{2}^{\prime}$
where $C_{1}^{\prime}\geq C_{1}$, $C_{2}^{\prime}\geq C_{2}$. There are three
cases to consider depending on the reduction $C\rightarrow D$.

    * –

$C_{1}$ is $\mathtt{return}(V)$ for some $V$. Then,
$C^{\prime}_{1}\rightarrow^{*}\mathtt{return}(V^{\prime})$ for some
$V^{\prime}\geq V$. Thus,

$C^{\prime}\rightarrow^{*}\mathtt{let}~{}x=\mathtt{return}(V^{\prime})~{}\mathtt{in}~{}C_{2}^{\prime}\rightarrow
C_{2}^{\prime}[x:=V^{\prime}]$

and $C_{2}^{\prime}[x:=V^{\prime}]\geq C_{2}[x:=V]$, this concludes this case.

    * –

$C_{1}$ is $\sigma(V;y.B)$. Then,
$C^{\prime}_{1}\rightarrow^{*}\sigma(V^{\prime};y.B^{\prime})$ for some
$V^{\prime}\geq V$ and $B^{\prime}\geq B$. Then,

$C^{\prime}\rightarrow^{*}\mathtt{let}~{}x=\sigma(V^{\prime};y.B^{\prime})~{}\mathtt{in}~{}C_{2}^{\prime}\rightarrow\sigma(V^{\prime};y.\mathtt{let}~{}x=B^{\prime}~{}\mathtt{in}~{}C_{2}^{\prime})$

and
$\sigma(V^{\prime};y.\mathtt{let}~{}x=B^{\prime}~{}\mathtt{in}~{}C_{2}^{\prime})\geq\sigma(V;y.\mathtt{let}~{}x=B~{}\mathtt{in}~{}C_{2})$,
this concludes this case.

    * –

If $C_{1}\rightarrow D_{1}$ for some $D_{1}$, then we have, by induction
hypothesis on $C_{1}^{\prime}$ the existence of $D_{1}^{\prime}$ such that

$C^{\prime}\rightarrow^{+}\mathtt{let}~{}x=\mathcal{E}[D_{1}^{\prime}]~{}\mathtt{in}~{}C_{2}^{\prime}$

and this computation is greater than
$\mathtt{let}~{}x=D_{1}~{}\mathtt{in}~{}C_{2}$. This concludes this case.

  * •

If $C\equiv\mathtt{with}~{}H~{}\mathtt{handle}~{}B$. Then
$C^{\prime}\equiv\mathtt{with}~{}H^{\prime}~{}\mathtt{handle}~{}B^{\prime}$.
Again, three cases to consider:

    * –

$IfB\rightarrow A$, then we can find, by induction hypothesis, $A^{\prime}$
such that $B^{\prime}\rightarrow^{+}A^{\prime}$ and $A^{\prime}\geq A$, and we
have
$C^{\prime}\rightarrow^{+}\mathtt{with}~{}H^{\prime}~{}\mathtt{handle}~{}\mathcal{E}[A^{\prime}]$.

    * –

If $B$ is $\mathtt{return}(V)$ for some $V$. Then,
$B^{\prime}\rightarrow^{*}\mathtt{return}(V^{\prime})$ for some
$V^{\prime}\geq V$. Thus,

$C^{\prime}\rightarrow^{*}\mathtt{with}~{}H^{\prime}~{}\mathtt{handle}~{}\mathtt{return}(V^{\prime})\rightarrow
C_{r}^{\prime}[x:=V^{\prime}]$

and we have $C_{r}^{\prime}[x:=V^{\prime}]\geq C_{r}[x:=V]$, this concludes
this case.

    * –

If $B$ is $\sigma_{i}(V;y.A)$. Then,
$B^{\prime}\rightarrow^{*}\sigma_{i}(V^{\prime};y.A^{\prime})$ for some
$V^{\prime}\geq V$ and $B^{\prime}\geq B$. Then,

$C^{\prime}\rightarrow^{*}\mathtt{with}~{}H^{\prime}~{}\mathtt{handle}~{}\sigma_{i}(V^{\prime};y.A^{\prime})\rightarrow
C_{i}^{\prime}[x:=V^{\prime}][r:=\lambda
y.\mathtt{with}~{}H^{\prime}~{}\mathtt{handle}~{}A^{\prime}]$

and

$C_{i}^{\prime}[x:=V^{\prime}][r:=\lambda
y.\mathtt{with}~{}H^{\prime}~{}\mathtt{handle}~{}A^{\prime}]\geq
C_{i}[x:=V][r:=\lambda y.\mathtt{with}~{}H~{}\mathtt{handle}~{}A]$

, this concludes this case.

  * •

If $C\equiv\mathtt{case}(V;C_{1},\dots,C_{k})$. Then
$C^{\prime}\equiv\mathtt{case}(V^{\prime};C_{1}^{\prime},\dots,C_{k}^{\prime})$.
And we can easily concludes because the only $V\geq\underline{n}$ for a given
$\underline{n}$ is $V\equiv\underline{n}$.

∎

Now that we have this lemma, we can prove that our translation is correct up
to approximation.

###### Lemma 0.

If $C\rightarrow D$, then there exists $D^{\prime}$ such that $\llbracket
C\rrbracket\rightarrow^{+}D^{\prime}$ and $D^{\prime}\geq\llbracket
D\rrbracket$.

###### Proof.

For this proof, we will consider that all values of type unit are equal. We
proceed by induction on $C\rightarrow D$. All cases are straightforward except
for the $\mathtt{case}$, that we detail here.

  * •

Consider the reduction $\mathtt{case}(0;0\mapsto C;\mathtt{succ}(x)\mapsto
D)\rightarrow C$. We have

$\displaystyle\llbracket\mathtt{case}(0;0\mapsto C;\mathtt{succ}(x)\mapsto
D\rrbracket$
$\displaystyle\triangleq\mathtt{let}~{}a=(\mathtt{with}~{}H(C,D)~{}\mathtt{handle}~{}\mathtt{Z}_{\llbracket\mathtt{Nat}\rrbracket}~{}())~{}\mathtt{in}~{}(a~{}(\lambda
f,g.g~{}()))$
$\displaystyle\rightarrow^{+}\mathtt{let}~{}a=(\mathtt{with}~{}H(C,D)~{}\mathtt{handle}~{}\mathtt{return}(()))~{}\mathtt{in}~{}(a~{}(\lambda
f,g.g~{}()))$
$\displaystyle\rightarrow^{+}\mathtt{let}~{}a=\mathtt{return}(\lambda
p.p~{}\mathtt{Z}_{\mathtt{Unit}\rightarrow\mathtt{Unit}}~{}(\lambda
x.\llbracket C\rrbracket))~{}\mathtt{in}~{}(a~{}(\lambda f,g.g~{}()))$
$\displaystyle\rightarrow^{+}(\lambda
f,g.g~{}())~{}(\mathtt{Z}_{\mathtt{Unit}\rightarrow\mathtt{Unit}})~{}(\lambda
x.\llbracket C\rrbracket)$ $\displaystyle\rightarrow^{+}\llbracket
C\rrbracket$

This concludes this case.

  * •

Consider the reduction $\mathtt{case}(\mathtt{succ}(V);0\mapsto
C;\mathtt{succ}(n)\mapsto D)\rightarrow D[n:=V]$. We have:

$\displaystyle\phantom{\triangleq}\llbracket\mathtt{case}(\mathtt{succ}(V);0\mapsto
C;\mathtt{succ}(x)\mapsto D\rrbracket$
$\displaystyle\triangleq\mathtt{let}~{}a=(\mathtt{with}~{}H(C,D)~{}\mathtt{handle}~{}\llbracket\mathtt{succ}(V)\rrbracket~{}())~{}\mathtt{in}~{}(a~{}(\lambda
f,g.g~{}()))$
$\displaystyle\rightarrow^{+}\mathtt{let}~{}a=(\mathtt{with}~{}H(C,D)~{}\mathtt{handle}~{}\sigma(y.\llbracket
V\rrbracket()))~{}\mathtt{in}~{}(a~{}(\lambda f,g.g~{}()))$

We can show that the following context:

$\mathcal{E}\triangleq\mathtt{let}~{}z=\mathtt{let}~{}\alpha=\mathtt{with}~{}H(C,D)~{}\mathtt{handle}~{}[]~{}\mathtt{in}~{}\alpha~{}(\lambda
f,g.\mathtt{let}~{}z=f~{}()~{}\mathtt{in}~{}\mathtt{Z}_{\llbracket
T\rrbracket})~{}\mathtt{in}~{}\mathtt{return}(\mathtt{Z}_{\mathtt{Unit}})$

is administrative.

    * –

We have:

$\displaystyle\phantom{\rightarrow^{*}}~{}\mathtt{with}~{}H(C,D)~{}\mathtt{handle}~{}\sigma(y.B)$
$\displaystyle\rightarrow^{+}\mathtt{let}~{}n=\mathtt{return}($
$\displaystyle\lambda x.\mathtt{let}~{}z=(\lambda
y.\mathtt{with}~{}H(C,D)~{}\mathtt{handle}~{}B)~{}\underline{0}~{}(\lambda
f,g.\mathtt{let}~{}z=f~{}()~{}\mathtt{in}~{}\mathtt{Z}_{\llbracket
T\rrbracket})~{}\mathtt{in}~{}\mathtt{return}(\mathtt{Z}_{\mathtt{Unit}}))~{}\mathtt{in}~{}...$

Also,

$\mathtt{let}~{}z=(\lambda
y.\mathtt{with}~{}H(C,D)~{}\mathtt{handle}~{}B)~{}\underline{0}~{}(\lambda
f,g.\mathtt{let}~{}z=f~{}()~{}\mathtt{in}~{}\mathtt{Z}_{\llbracket
T\rrbracket})~{}\mathtt{in}~{}\mathtt{return}(\mathtt{Z}_{\mathtt{Unit}})\rightarrow^{*}\mathcal{E}[B]$

so let us call this computation $B^{\prime}$ for the sake of clarity. We have:

$\displaystyle\phantom{\rightarrow^{*}}~{}\mathtt{with}~{}H(C,D)~{}\mathtt{handle}~{}\sigma(y.B)$
$\displaystyle\rightarrow^{+}\mathtt{let}~{}n=\mathtt{return}(\lambda
x.B^{\prime})~{}\mathtt{in}~{}\mathtt{return}(\lambda p.p~{}(\lambda
x.\sigma(z.n~{}()))~{}(\lambda x.\llbracket D\rrbracket))$

By going back to the previous computation in the whole context, we obtain:

$\displaystyle\phantom{\rightarrow^{*}}~{}\mathcal{E}[\sigma(V;y.B)]$
$\displaystyle\rightarrow^{+}\mathtt{let}~{}k=\sigma(z.(\lambda
x.B^{\prime})~{}())~{}\mathtt{in}~{}\mathtt{return}(\mathtt{Z}_{\mathtt{Unit}})$
$\displaystyle\rightarrow^{+}\mathtt{let}~{}k=\sigma(z.B^{\prime})~{}\mathtt{in}~{}\mathtt{return}(\mathtt{Z}_{\mathtt{Unit}})$
$\displaystyle\rightarrow^{+}\sigma(z.\mathtt{let}~{}k=B^{\prime}~{}\mathtt{in}~{}\mathtt{return}(\mathtt{Z}_{\mathtt{Unit}}))$

And $\mathtt{let}~{}k=C~{}\mathtt{in}~{}\mathtt{return}(())$ with $k$ of type
unit is $\eta$-equivalent to $C$. This concludes this case.

    * –

For the case of $\mathtt{return}$, we have:

$\displaystyle\phantom{\rightarrow^{*}}~{}\mathcal{E}[\mathtt{return}(())]$
$\displaystyle\rightarrow^{+}\mathtt{let}~{}z=\mathtt{let}~{}a=\mathtt{with}~{}H(C,D)~{}\mathtt{handle}~{}\mathtt{return}(())~{}\mathtt{in}$
$\displaystyle(a~{}(\lambda
f,g.\mathtt{let}~{}z=f~{}()~{}\mathtt{in}~{}\mathtt{Z}_{\llbracket
T\rrbracket}))~{}\mathtt{in}~{}\mathtt{return}(\mathtt{Z}_{\mathtt{Unit}})$
$\displaystyle\rightarrow^{+}\mathtt{return}(())$

And this concludes this case.

In particular, we have:

$\mathcal{E}[\llbracket V\rrbracket~{}()]\geq\llbracket V\rrbracket()$

for any $\Gamma\vdash V:\mathtt{Nat}$ in PCF. This show in particular that we
have:

$\displaystyle\phantom{equiv}\llbracket\mathtt{case}(\mathtt{succ}(V);0\mapsto
C;\mathtt{succ}(x)\mapsto D\rrbracket$
$\displaystyle\triangleq\mathtt{let}~{}a=(\mathtt{with}~{}H(C,D)~{}\mathtt{handle}~{}\llbracket\mathtt{succ}(V)\rrbracket~{}())~{}\mathtt{in}~{}(a~{}(\lambda
f,g.g~{}()))$
$\displaystyle\rightarrow^{+}\mathtt{let}~{}a=(\mathtt{with}~{}H(C,D)~{}\mathtt{handle}~{}\sigma(y.\llbracket
V\rrbracket()))~{}\mathtt{in}~{}(a~{}(\lambda f,g.g~{}()))$
$\displaystyle\rightarrow^{+}\llbracket D\rrbracket[n:=V^{\prime}]$

with $V^{\prime}\geq\lambda x.\llbracket V\rrbracket~{}()$, which is
$\eta$-equivalent with $\llbracket V\rrbracket$. Thus, we have indeed that

$\llbracket\mathtt{case}(\mathtt{succ}(V);0\mapsto C;\mathtt{succ}(x)\mapsto
D\rrbracket\rightarrow^{+}\llbracket D\rrbracket[n:=V^{\prime}]$

with $\llbracket D\rrbracket[n:=V^{\prime}]\geq\llbracket
D\rrbracket[n:=\llbracket V\rrbracket]$.

∎

###### Lemma 0.

If $\Gamma\vdash C:T$, $C\rightarrow D$ and $A\geq\llbracket C\rrbracket$,
then there exists $B$ such that $A\rightarrow^{+}B$ with $B\geq\llbracket
D\rrbracket$

###### Proof.

This is a consequence of the two previous lemmas. ∎

From this simulation, we obtain:

###### Theorem 10.

For any term $\vdash C:\mathtt{Nat}$ in PCF, there is a term of finitary HEPCF
$C_{f}\triangleq\mathtt{let}~{}a=\llbracket
C\rrbracket~{}\mathtt{in}~{}(a~{}())$ such that
$\vdash_{E}C_{f}:\mathtt{Unit}$ and $ET(C_{f})$ represents the normal form of
$C$ (if it exists, otherwise the $ET(C_{f})\equiv\bot$).

###### Proof.

Suppose that $\vdash C:\mathtt{Nat}$ has no normal form, then $\llbracket
C\rrbracket$ has no normal form, and thus the effect tree of $C_{f}$ is
$\bot$. Otherwise, suppose that $C\rightarrow^{*}\mathtt{return}(V)$ with $V$
a closed value of type $\mathtt{Nat}$. Then, $\llbracket
C\rrbracket\rightarrow^{*}D$ with
$D\geq\llbracket\mathtt{return}(V)\rrbracket$. In particular,
$D\rightarrow^{*}\mathtt{return}(V^{\prime})$ with $V^{\prime}\geq\llbracket
V\rrbracket$. Thus, the effect tree of $C_{f}$ is the same as $\llbracket
V\rrbracket$. Because $V$ is a closed value of type $\mathtt{Nat}$, this
effect tree is the tree representation of the integer $V$, this concludes the
proof. ∎

###### Corollary 0.

Effect trees produced by HEPCF terms are not MSO-decidable.

Indeed, given a PCF term of type $\mathtt{Nat}$, we can translate it into
HEPCF and ask if the effect tree of this HEPCF term contains a $\bot$, and
this would decide if the initial term halts. Thus, this shows that the power
of handlers are simply too expressive for MSO model-checking.

###### Remark 0.

Our proof heavily relies on the fact that handlers can change the output type,
which allows here to do this encoding of pairs of computation internally and
returns at the end only the second computation. A careful reader might wonder
if the control of this output type is necessary for undecidability, and that
we could have a decidable MSO model-checking for restrained handlers, with a
fixed output type, for example
$\mathtt{Unit}_{E}\Rightarrow_{E^{\prime}}\mathtt{Unit}$. We show in the next
section that this restriction still leads to a language for which MSO model-
checking is undecidable.

##  9\. Handlers in ECPS

In this section, we present a language written directly in CPS-style, with
handlers, called HECPS. This language is based on the language described in
(Matache, 2018; Matache and Staton, 2019). The handlers in ECPS seems less
expressive than the handlers available in HEPCF especially because we cannot
chose the output and input type, however we will show that we still have an
undecidability result for HECPS.

Formally, we define HECPS as the language with the following types and
grammar:

$\displaystyle T$
$\displaystyle::=\mathtt{B}\mid\neg_{E}(T_{1},\dots,T_{n})\mid\mathtt{k}$
$\displaystyle E$
$\displaystyle::=\emptyset\;\mbox{\Large{$\mid$}}\;\\{\sigma:\mathtt{B}\rightsquigarrow
k\\}\cup E$ $\displaystyle V,W$
$\displaystyle::=v\;\mbox{\Large{$\mid$}}\;\underline{n}\;\mbox{\Large{$\mid$}}\;x\;\mbox{\Large{$\mid$}}\;\lambda(x_{1},\dots,x_{n}).t\;\mbox{\Large{$\mid$}}\;\mathtt{fix}~{}f.V$
$\displaystyle t,u$
$\displaystyle::=V~{}(W_{1},\dots,W_{n})\;\mbox{\Large{$\mid$}}\;\sigma(V;x.t)\;\mbox{\Large{$\mid$}}\;\mathtt{return}\;\mbox{\Large{$\mid$}}\;\mathtt{with}~{}H~{}\mathtt{handle}~{}t\;\mbox{\Large{$\mid$}}\;\mathtt{case}(V;t_{1},\dots,t_{k})$
$\displaystyle H$ $\displaystyle::=\\{\mathtt{return}\mapsto
t_{r}\\}\cup\\{\sigma_{i}(x;r)\mapsto t_{i}\mid 1\leq i\leq n\\}$

The intuition behind this language is that all terms $t,u$ must be of type
$o$, where $o$ is intuitively a return type corresponding to the type of tree
in the $\lambda$-Y calculus. In particular, a value of HECPS is either of base
type, or a function that outputs in type $o$, described by the type
$\neg_{E}(T_{1},\dots,T_{n})$ meaning intuitively
$T_{1}\rightarrow_{E}\cdots\rightarrow_{E}T_{n}\rightarrow_{E}o$. Then, the
obvious difference with HEPCF is the absence of
$\mathtt{let}~{}\cdot~{}\mathtt{in}$ expressions, because it is captured by a
use of continuation, and there is no way to return a value, because we can
only stop the computation with a $\mathtt{return}$ of type $o$.

The typing rules that differs from HEPCF are given in Figure 9.

$\Gamma,x_{1}:T_{1},\dots,x_{n}:T_{n}\vdash t$
$\Gamma\vdash\lambda(x_{1},\dots,x_{n}).t:\neg(T_{1},\dots,T_{n})$
$\Gamma,f:\neg(T_{1},\dots,T_{n})\vdash V:\neg(T_{1},\dots,T_{n})$
$\Gamma\vdash\mathtt{fix}~{}f.V:\neg(T_{1},\dots,T_{n})$ $\Gamma\vdash
V:\neg(T_{1},\dots,T_{n})$ $(\Gamma\vdash W_{i}:T_{i})_{1\leq i\leq n}$
$\Gamma\vdash V~{}(W_{1},\dots,W_{n})$ $\Gamma\vdash\mathtt{return}$
$(\sigma:\mathtt{B}\rightsquigarrow k)\in\Sigma$ $\Gamma\vdash V:\mathtt{B}$
$\Gamma,x:\mathtt{k}\vdash t$ $\Gamma\vdash\sigma(V;x.t)$ $\Gamma\vdash
V:\mathtt{k}$ $(\Gamma\vdash t_{i})_{1\leq i\leq k}$
$\Gamma\vdash\mathtt{case}(V;t_{1},\dots,t_{k})$ $\Gamma\vdash
H:E^{\prime}\Rightarrow E$ $\Gamma\vdash_{E^{\prime}}t$
$\Gamma\vdash_{E}\mathtt{with}~{}H~{}\mathtt{handle}~{}t$
$E^{\prime}=\\{\sigma_{i}:\mathtt{B}_{i}\rightsquigarrow k_{i}\mid 1\leq i\leq
n\\}$ $\Gamma\vdash_{E}t_{r}$
$(\Gamma,x:\mathtt{B}_{i},r:\neg_{E}(k)\vdash_{E}t_{i})_{1\leq i\leq n}$
$\Gamma\vdash\\{\mathtt{return}\mapsto t_{r}\\}\cup\\{\sigma_{i}(x;r)\mapsto
t_{i}\mid 1\leq i\leq n\\}:E^{\prime}\Rightarrow E$

Figure 9. Static Semantics of HECPS

As for the semantics, it is similar to the one described in Figure 8. The
important difference with what we saw before is that we cannot control the
input or output type, we need to work with type $o$. Because of this, the
previous translation from PCF, that relied strongly on the output type, does
not work directly. However, we will again prove that we can encode PCF in this
language, and as before we rely on the idea to encode shallow handlers as deep
handlers. Formally, a shallow handler is syntactically similar to a deep
handler, but the typing rule and semantics are different, as described in
Figure 10. We differentiate shallow handlers from usual handlers by adding a
$\dagger$ in the handle operation. In the typing derivation the difference is
subtle, only the set of effect of the continuation $r$ changes. However, in
the semantics the difference is flagrant, the continuation is not called with
the handler again.

$\Gamma\vdash H:E^{\prime}\Rightarrow^{\dagger}E$ $\Gamma\vdash_{E^{\prime}}t$
$\Gamma\vdash_{E}\mathtt{with}~{}H~{}\mathtt{handle}^{\dagger}~{}t$
$E^{\prime}=\\{\sigma_{i}:\mathtt{B}_{i}\rightsquigarrow k_{i}\mid 1\leq i\leq
n\\}$ $\Gamma\vdash_{E}t_{r}$
$(\Gamma,x:\mathtt{B}_{i},r:\neg_{E^{\prime}}(k)\vdash_{E}t_{i})_{1\leq i\leq
n}$ $\Gamma\vdash\\{\mathtt{return}\mapsto
t_{r}\\}\cup\\{\sigma_{i}(x;r)\mapsto t_{i}\mid 1\leq i\leq
n\\}:E^{\prime}\Rightarrow^{\dagger}E$ $t\rightarrow t^{\prime}$
$\mathtt{with}~{}H~{}\mathtt{handle}^{\dagger}~{}t\rightarrow\mathtt{with}~{}H~{}\mathtt{handle}^{\dagger}~{}t^{\prime}$
For the following rules, we define $H=\\{\mathtt{return}\mapsto
t_{r}\\}\cup\\{\sigma_{i}(x;r)\mapsto t_{i}\mid 1\leq i\leq n\\}$
$\mathtt{with}~{}H~{}\mathtt{handle}^{\dagger}~{}\mathtt{return}\rightarrow
t_{r}$
$\mathtt{with}~{}H~{}\mathtt{handle}^{\dagger}~{}\sigma_{i}(V;x.t)\rightarrow
t_{i}[x:=V,r:=(\lambda x.t)]$

Figure 10. Shallow Handlers in ECPS

###  9.1. ECPS with Shallow Handlers

We introduce shallow handlers in order to decompose the translation from PCF,
we will first show that we can encode PCF in ECPS with shallow handlers, and
then we will see how we can encode shallow handlers using deep handlers in
ECPS (the important point being that the proof given in the previous section
and in (Hillerström and Lindley, 2018) does not work anymore).

###### Definition 0 (Translation from PCF to ECPS with Shallow Handlers).

As in the previous section, we need to encode the infinite type of natural
numbers into finite types. We introduce the effect
$E=\\{\sigma:\mathtt{Unit}\rightsquigarrow 1\\}$. We define the _zero_ term,
denoted $\mathtt{Z}_{o}$ by $\mathtt{Z}_{o}=\mathtt{return}$.

The translation $\llbracket\cdot\rrbracket$ from PCF to ECPS with shallow
handlers is given by

$\llbracket\mathtt{Nat}\rrbracket=\neg_{E}(1)\qquad\llbracket T\rightarrow
U\rrbracket=\neg_{E}(\llbracket T\rrbracket,\neg_{E}(\llbracket
U\rrbracket)).$

And we want, as usual for a CPS translation, that if $\Gamma\vdash V:T$ then
$\llbracket\Gamma\rrbracket\vdash\llbracket V\rrbracket:\llbracket
T\rrbracket$ and that if $\Gamma\vdash C:T$ then
$\llbracket\Gamma\rrbracket\vdash\llbracket
C\rrbracket:\neg_{E}(\neg_{E}(\llbracket T\rrbracket))$

$\displaystyle\llbracket 0\rrbracket$ $\displaystyle\triangleq\lambda
x.\mathtt{Z}_{o}$ $\displaystyle\llbracket\mathtt{succ}(V)\rrbracket$
$\displaystyle\triangleq\lambda x.\sigma(y.\llbracket V\rrbracket~{}y)$
$\displaystyle\llbracket x\rrbracket$ $\displaystyle\triangleq x$
$\displaystyle\llbracket\lambda x.C\rrbracket$
$\displaystyle\triangleq\lambda(x,k).\llbracket C\rrbracket~{}k$
$\displaystyle\llbracket\mathtt{fix}f.V\rrbracket$
$\displaystyle\triangleq\mathtt{fix}f.\llbracket V\rrbracket$
$\displaystyle\llbracket V~{}W\rrbracket$ $\displaystyle\triangleq\lambda
k.\llbracket V\rrbracket~{}(\llbracket W\rrbracket,k)$
$\displaystyle\llbracket\mathtt{return}(V)\rrbracket$
$\displaystyle\triangleq\lambda k.k~{}\llbracket V\rrbracket$
$\displaystyle\llbracket\mathtt{let}~{}x=C~{}\mathtt{in}~{}D\rrbracket$
$\displaystyle\triangleq\lambda k.\llbracket C\rrbracket(\lambda x.\llbracket
D\rrbracket~{}k)$ $\llbracket\mathtt{case}(V;0\mapsto
C;\mathtt{succ}(n)\mapsto D)\rrbracket\triangleq\lambda
k.\mathtt{with}~{}H(C,D,k)~{}\mathtt{handle}^{\dagger}~{}\llbracket
V\rrbracket\underline{0}$

where $H(C,D,k)$ is defined by, when $C$ and $D$ have type $T$, and $k$ of
type $\neg_{E}(T)$ by:

$\displaystyle\mathtt{return}$ $\displaystyle\mapsto\llbracket
C\rrbracket~{}k$ $\displaystyle\sigma(n)$ $\displaystyle\mapsto\llbracket
D\rrbracket~{}k$

This time, the encoding of case is rather simple. Indeed, we will show that
shallow handlers naturally encodes the conditional with this construction.

###### Lemma 0.

If $\Gamma\vdash V:T$ then $\llbracket\Gamma\rrbracket\vdash\llbracket
V\rrbracket:\llbracket T\rrbracket$ and if $\Gamma\vdash C:T$ then
$\llbracket\Gamma\rrbracket\vdash\llbracket
C\rrbracket:\neg_{E}(\neg_{E}(\llbracket T\rrbracket))$

###### Proof.

The proof is straighforard. ∎

Now, we want to prove that the translation is a correct simulation.

###### Lemma 0.

If $\Gamma\vdash C:T$ and $C\rightarrow D$ then for all
$\llbracket\Gamma\rrbracket\vdash k:\neg_{E}(\llbracket T\rrbracket)$,
$\llbracket C\rrbracket~{}k\rightarrow^{+}\llbracket D\rrbracket~{}k$.

###### Proof.

The only difference with a standard CPS translation is for the $\mathtt{case}$
constructor. Thus, only detail this case.

  * •

Consider the reduction $\mathtt{case}(0,0\mapsto C;\mathtt{succ}(n)\mapsto
D)\rightarrow C$. Then, we have:

$\displaystyle\llbracket\mathtt{case}(0,0\mapsto C;\mathtt{succ}(n)\mapsto
D)\rrbracket~{}k$
$\displaystyle\rightarrow\mathtt{with}~{}H(C,D,k)~{}\mathtt{handle}^{\dagger}~{}\llbracket
0\rrbracket()$
$\displaystyle\rightarrow\mathtt{with}~{}H(C,D,k)~{}\mathtt{handle}^{\dagger}~{}\mathtt{return}$
$\displaystyle\rightarrow\llbracket C\rrbracket~{}k$

This concludes this case.

  * •

Consider the reduction $\mathtt{case}(\mathtt{succ}(V),0\mapsto
C;\mathtt{succ}(n)\mapsto D)\rightarrow D[n:=V]$ Then, we have:

$\displaystyle\llbracket\mathtt{case}(\mathtt{succ}(V),0\mapsto
C;\mathtt{succ}(n)\mapsto D)\rrbracket~{}k$
$\displaystyle\rightarrow\mathtt{with}~{}H(C,D,k)~{}\mathtt{handle}^{\dagger}~{}\llbracket\mathtt{succ}(V)\rrbracket()$
$\displaystyle\rightarrow\mathtt{with}~{}H(C,D,k)~{}\mathtt{handle}^{\dagger}~{}\sigma(y.\llbracket
V\rrbracket~{}y)$ $\displaystyle\rightarrow\llbracket D\rrbracket[n:=\lambda
y.\llbracket V\rrbracket~{}y]~{}k$ $\displaystyle\equiv_{\eta}\llbracket
D\rrbracket[n:=\llbracket V\rrbracket]~{}k$

We need to use the $\eta$ equivalence to get exactly the result, but we could
always formally avoid it, but for the sake of simplicity we just consider that
we work with $\eta$-equivalence.

∎

From this, we can conclude the undecidability result for ECPS with shallow
handlers.

###### Lemma 0.

For any term $\vdash C:\mathtt{Nat}$ in PCF, there is a term of ECPS with
shallow handlers $t_{f}\triangleq\llbracket C\rrbracket~{}(\lambda
n.n~{}\underline{0})$ such that $\vdash_{E}t_{f}$ such that the effect tree of
$t_{f}$ represents the normal form of $C$ (if it exists, otherwise the effect
tree is $\bot$).

###### Proof.

Suppose that $\vdash C:\mathtt{Nat}$ has no normal form, then $\llbracket
C\rrbracket$ has no normal form, and thus the effect tree of $t_{f}$ is
$\bot$. Otherwise, $C\rightarrow^{*}\mathtt{return}(V)$ with $V$ a value of
type $\mathtt{Nat}$. Then, with the previous lemma, we obtain

$t_{f}\rightarrow^{*}\llbracket\mathtt{return}(V)\rrbracket~{}(\lambda
n.n~{}\underline{0})\rightarrow^{*}\llbracket V\rrbracket~{}\underline{0}$

and we can easily see that the effect tree of $\llbracket
V\rrbracket~{}\underline{0}$ represents exaclty the integer $V$. ∎

Thus, to conclude on the undecidability of HECPS, we need to show that we can
simulate shallow handlers using deep handlers.

###  9.2. Encoding Shallow Handlers with Deep Handlers

As we are only interested in encoding the previous translation, we fix the set
of effect $E=\\{\sigma:\mathtt{Unit}\rightsquigarrow 1\\}$. We introduce a
duplication of this effect, and consider the set
$E_{d}=\\{\sigma_{d}:\mathtt{Unit}\rightsquigarrow 1\\}$. We will use this
operation $\sigma_{d}$ as a ’marked’ effect, similarly to the use of ’marked’
letters that we can find in some Turing Machine problems. In the following
proof, we will mainly work directly on effect trees, because we will introduce
handlers and each of these handlers will slightly transform the computation by
just changing a bit the effect tree. We believe this proof is far more
intuitive. However, if we want to prove formally a simulation, we would need
to use administrative context like before.

As a first step toward this intuition of marked effects, we introduce the
marking handlers, denoted $H_{d}$, and described by:

$\displaystyle
H_{d}\triangleq\\{\mathtt{return}\mapsto\mathtt{return};\qquad\sigma(r)\mapsto\sigma_{d}(x.r~{}x);\qquad\sigma_{d}(r)\mapsto\sigma_{d}(x.r~{}x)\\}$

It is easy to see that the type of this handler is $(E\cup E_{d})\Rightarrow
E_{d}$ (it can also be the weaker type $(E\cup E_{d})\Rightarrow(E\cup E_{d})$
, and that this handler takes a computation $C$ and simulates $C$ but replace
all effects $\sigma(x.t)$ by $\sigma_{d}(x.t)$, without changing anything
else. We now introduce a handler that change everything except the root of the
tree, to do this we use the previous handler:

$\displaystyle H_{r}\triangleq\\{$
$\displaystyle\mathtt{return}\mapsto\mathtt{return};\qquad\sigma(r)\mapsto\sigma(y.\mathtt{with}~{}H_{d}~{}\mathtt{handle}~{}(r~{}y))$

This handler $H_{r}$ has type $E\Rightarrow(E\cup E_{d})$. We have,

  * •

If $\Gamma\vdash_{E}t$, if $t\rightarrow t^{\prime}$ then
$\mathtt{with}~{}H_{r}~{}\mathtt{handle}~{}t\rightarrow\mathtt{with}~{}H_{r}~{}\mathtt{handle}~{}t^{\prime}$.

  * •

$\mathtt{with}~{}H_{r}~{}\mathtt{handle}~{}\mathtt{return}\rightarrow\mathtt{return}$

  * •

$\mathtt{with}~{}H_{r}~{}\mathtt{handle}~{}\sigma(x.t)\rightarrow\sigma(y.\mathtt{with}~{}H_{d}~{}\mathtt{handle}~{}(\lambda
x.(\mathtt{with}~{}H_{r}~{}\mathtt{handle}~{}t)~{}y))$ Using
$\alpha$-equivalence, we obtain:
$\mathtt{with}~{}H_{r}~{}\mathtt{handle}~{}\sigma(x.t)\rightarrow^{+}\sigma(x.\mathtt{with}~{}H_{d}~{}\mathtt{handle}~{}(\mathtt{with}~{}H_{r}~{}\mathtt{handle}~{}t))$.

For the sake of clarity, let us note $\mathtt{with}~{}H_{d}\circ
H_{r}~{}\mathtt{handle}~{}t$ for
$\mathtt{with}~{}H_{d}~{}\mathtt{handle}~{}(\mathtt{with}~{}H_{r}~{}\mathtt{handle}~{}t)$.
We have:

  * •

If $\Gamma\vdash_{E\cup E_{d}}t$, if $t\rightarrow t^{\prime}$ then
$\mathtt{with}~{}H_{d}\circ
H_{r}~{}\mathtt{handle}~{}t\rightarrow^{+}\mathtt{with}~{}H_{d}\circ
H_{r}~{}\mathtt{handle}~{}t^{\prime}$.

  * •

$\mathtt{with}~{}H_{d}\circ
H_{r}~{}\mathtt{handle}~{}\mathtt{return}\rightarrow^{+}\mathtt{return}$.

  * •

$\mathtt{with}~{}H_{d}\circ
H_{r}~{}\mathtt{handle}~{}\sigma(x.t)\rightarrow^{+}\sigma_{d}(x.\mathtt{with}~{}H_{d}~{}\mathtt{handle}~{}(\mathtt{with}~{}H_{d}\circ
H_{r}~{}\mathtt{handle}~{}t))$.

Now remark that applying $H_{d}$ twice does not change anything, by definition
of $H_{d}$. And as we can see with the previous description, the effect tree
of $\mathtt{with}~{}H_{d}\circ H_{r}~{}\mathtt{handle}~{}t$ is the same as
$\mathtt{with}~{}H_{d}~{}\mathtt{handle}~{}t$ alone. Thus, we can show that
the effect tree of $\mathtt{with}~{}H_{r}~{}\mathtt{handle}~{}t$ is the effect
tree of $t$ when we replace all $\sigma$ by $\sigma_{d}$ except on the root.
Thus, we have just found a way to distinguish the root of the effect tree from
the rest, and we can use that to simulate a shallow handler.

Suppose that we want to simulate the following shallow handler $h$ with a type
corresponding to the shallow handlers we used in the previous translation:

$\Gamma\vdash_{E}t_{r}$ $\Gamma,r:\neg_{E}(1)\vdash_{E}t_{\sigma}$
$\Gamma\vdash\\{\mathtt{return}\mapsto t_{r}\\}\cup\\{\sigma(r)\mapsto
t_{\sigma}\\}:E\Rightarrow^{\dagger}E$

Consider the following (deep) handler:

$\displaystyle H_{h}\triangleq\\{\mathtt{return}\mapsto
t_{r};\qquad\sigma(r)\mapsto
t_{\sigma};\qquad\sigma_{d}(r)\mapsto\sigma(x.r~{}x)\\}$

that has the type $(E\cup E_{d})\Rightarrow E$ and consider the following
term: $\mathtt{with}~{}H_{h}\circ H_{r}~{}\mathtt{handle}~{}t$. We have:

  * •

If $t\rightarrow t^{\prime}$ then $\mathtt{with}~{}H_{h}\circ
H_{r}~{}\mathtt{handle}~{}t\rightarrow^{+}\mathtt{with}~{}H_{h}\circ
H_{r}~{}\mathtt{handle}~{}t^{\prime}$

  * •

$\mathtt{with}~{}H_{h}\circ
H_{r}~{}\mathtt{handle}~{}\mathtt{return}\rightarrow^{+}t_{r}$

  * •

$\mathtt{with}~{}H_{h}\circ
H_{r}~{}\mathtt{handle}~{}\sigma(y.t)\rightarrow^{+}t_{\sigma}[r:=(\lambda
x.\mathtt{with}~{}H_{h}\circ H_{d}\circ H_{r}~{}\mathtt{handle}~{}t))]$

And now we have to show that $\mathtt{with}~{}H_{h}\circ H_{d}\circ
H_{r}~{}\mathtt{handle}~{}t$ behaves like $t$ (the context is administrative).
We already know that $H_{d}\circ H_{r}$ behave like $H_{d}$, and on effect
tree with effect only in $E_{d}$, the handler $H_{h}$ will just replace every
$\sigma_{d}$ by $\sigma$. Thus, the effect tree of $t$ is exactly the effect
tree of $\mathtt{with}~{}H_{h}\circ H_{d}\circ H_{r}~{}\mathtt{handle}~{}t$.
Thus, $H_{h}\circ H_{r}$ behaves like a shallow handler. We can then take the
previous encoding of $PCF$ in ECPS with shallow handlers, and replace the use
of a shallow handler $h$ by the use of $H_{h}\circ H_{r}$, and we obtain a
valid encoding of $PCF$ to ECPS with deep handlers.

###### Theorem 5.

HECPS is not MSO-decidable

##  10\. EPCF with Restricted Handlers (Generic Effect)

Does the results in the last section mean that we can have algebraic effects
but that we have to get away with handlers if HOMC is our concern?
Essentially, it rather shows that general handlers, define a transformation on
effect trees that is simply _too expressive_ for HOMC. However, this does not
mean that _simpler_ tree transformations should not be expressible in HORS,
and this section is devoted to introducing a class of handlers whose
underlying tree transformations is amenable to HOMC. Intuitively, an
interpretation of an algebraic operation $\sigma:\mathtt{B}\rightsquigarrow k$
could be just a function of type $B\rightarrow k$, with no access to the
continuation. This is of course much less expressive than standard handlers,
but we will argue that what we obtain is not _too_ restrictive. Formally, we
could capture this by a restriction of handlers, defined in the following
language, called GEPCF (for Generic Effects PCF):

(Types) $\displaystyle T,U$ $\displaystyle::=\mathtt{B}\mid
T\rightarrow_{E}U\mid k$ (Effects) $\displaystyle E$
$\displaystyle::=\emptyset\;\mbox{\Large{$\mid$}}\;\\{\sigma:\mathtt{B}\rightsquigarrow
k\\}\cup E$ (Values) $\displaystyle V,W$
$\displaystyle::=v\;\mbox{\Large{$\mid$}}\;\underline{n}\;\mbox{\Large{$\mid$}}\;x\;\mbox{\Large{$\mid$}}\;\lambda
x.C\;\mbox{\Large{$\mid$}}\;\mathtt{fix}~{}f.V$ (Computations) $\displaystyle
C,D$
$\displaystyle::=V~{}W\;\mbox{\Large{$\mid$}}\;\sigma(V;x.C)\;\mbox{\Large{$\mid$}}\;\mathtt{return}(V)\;\mbox{\Large{$\mid$}}\;\mathtt{let}~{}x=C~{}\mathtt{in}~{}D$
$\displaystyle\phantom{::=}\;\mbox{\Large{$\mid$}}\;\mathtt{with}~{}H~{}\mathtt{handle}~{}C\;\mbox{\Large{$\mid$}}\;\mathtt{case}(V;C_{1},\dots,C_{k})$
(Handlers) $\displaystyle H$ $\displaystyle::=\\{\mathtt{return}(x)\mapsto
C_{r}\\}\cup\\{\sigma_{i}(x)\mapsto C_{i}\mid 1\leq i\leq n\\}$

Note that as expected, the handler for an algebraic operation does not have
access to the continuation. The static and dynamic semantics is in Figure 11.

$\Gamma\vdash H:T_{E}\Rightarrow_{E^{\prime}}U$ $\Gamma\vdash_{E}C:T$
$\Gamma\vdash_{E^{\prime}}\mathtt{with}~{}H~{}\mathtt{handle}~{}C:U$
$E=\\{\sigma_{i}:\mathtt{B}_{i}\rightsquigarrow k_{i}\mid 1\leq i\leq n\\}$
$\Gamma,x:T\vdash_{E^{\prime}}C_{r}:U$
$(\Gamma,x:\mathtt{B}_{i},\vdash_{E^{\prime}}C_{i}:k_{i})_{1\leq i\leq n}$
$\Gamma\vdash\\{\mathtt{return}(x)\mapsto C_{r}\\}\cup\\{\sigma_{i}(x)\mapsto
C_{i}\mid 1\leq i\leq n\\}:T_{E}\Rightarrow_{E^{\prime}}U$ $t\rightarrow
t^{\prime}$
$\mathtt{with}~{}H~{}\mathtt{handle}~{}t\rightarrow\mathtt{with}~{}H~{}\mathtt{handle}~{}t^{\prime}$
For the following rules, we define $H=\\{\mathtt{return}(x)\mapsto
C_{r}\\}\cup\\{\sigma_{i}(x)\mapsto C_{i}\mid 1\leq i\leq n\\}$
$\mathtt{with}~{}H~{}\mathtt{handle}~{}\mathtt{return}(V)\rightarrow
C_{r}[x:=V]$
$\mathtt{with}~{}H~{}\mathtt{handle}~{}\sigma_{i}(V;y.C)\rightarrow\mathtt{let}~{}y=C_{i}[x:=V]~{}\mathtt{in}~{}(\mathtt{with}~{}H~{}\mathtt{handle}~{}C)$

Figure 11. Interpretations in GPCF

Please observe that we e can always simulate a GEPCF handler by a HEPCF
handler:

$\mathtt{return}\mapsto
C_{r}\qquad\sigma_{i}(x;r)\mapsto\mathtt{let}~{}z=C_{i}~{}\mathtt{in}~{}(r~{}z)$

Thus, those restrained handlers are a specific case of standard handlers in
which the handling of an operation $\sigma_{i}$ always has the shape
$\mathtt{let}~{}z=C_{i}~{}\mathtt{in}~{}(r~{}z)$. Informally, if we look at it
with the point of view of tree transformations, this is exactly what we would
obtain from a generic effect for the effect tree monad, that is why we call
this language GEPCF.

Let us now show that this language can be translated into the $\lambda
Y$-calculus, thus proving the MSO-decidability.

###### Definition 0 (Translation from GEPCF to $\lambda$-Y calculus).

We define the translation $\cdot^{\star}$ on types and terms. For the sake of
conciseness, in types, we use some abuse of notations, such as pairs in the
left-hand side of an arrow type to denote the obvious curried version of this
type.

$\mathtt{B}^{\star}\triangleq o\qquad k^{\star}\triangleq o^{k}\rightarrow
o\qquad(T\rightarrow_{E}U)^{\star}\triangleq T^{\star}\rightarrow
E^{\star}\rightarrow\neg U^{\star}\rightarrow o$
$\emptyset^{\star}\triangleq()\qquad E\cup\sigma:\mathtt{B}\rightsquigarrow
k^{\star}\triangleq(E^{\star},o\rightarrow\neg k^{\star}\rightarrow o)$

And we want to show that if $\Gamma\vdash V:T$ then $\Gamma^{\star}\vdash
V^{\star}:T^{\star}$ and that if $\Gamma\vdash_{E}C:T$ then
$\Gamma^{\star}\vdash C^{\star}:E^{\star}\rightarrow(T^{\star}\rightarrow
o)\rightarrow o$ Informally, we will do a CPS-translation in which there is
also a _handler continuation_ , of type $E^{\star}$, giving an interpretation
for all algebraic effects in $E$. We take a $\lambda Y$-calculus with a
signature $\Sigma$ with at least all the constants values of EPCF.

$\displaystyle v^{\star}$ $\displaystyle\triangleq v$
$\displaystyle\underline{n}^{\star}$
$\displaystyle\triangleq\lambda(x_{1},\dots,x_{k}).x_{n}$ $\displaystyle
x^{\star}$ $\displaystyle\triangleq x$ $\displaystyle(\lambda x.C)^{\star}$
$\displaystyle\triangleq\lambda x.C^{\star}$
$\displaystyle(\mathtt{fix}~{}x.V)^{\star}$ $\displaystyle\triangleq
Y~{}(\lambda x.V^{\star})$ $\displaystyle(V~{}W)^{\star}$
$\displaystyle\triangleq V^{\star}~{}W^{\star}$
$\displaystyle(\mathtt{return}(V))^{\star}$
$\displaystyle\triangleq\lambda(\widetilde{h},c).c~{}V^{\star}$
$\displaystyle(\sigma_{i}(V;x.C))^{\star}$
$\displaystyle\triangleq\lambda(\widetilde{h},c).h_{i}~{}V^{\star}~{}(\lambda
x.C^{\star}~{}\widetilde{h}~{}c)$
$\displaystyle(\mathtt{let}~{}x=C~{}\mathtt{in}~{}D)^{\star}$
$\displaystyle\triangleq\lambda(\widetilde{h},c).C^{\star}~{}\widetilde{h}~{}(\lambda
x.D^{\star}~{}\widetilde{h}~{}c)$
$\displaystyle(\mathtt{case}(V;C_{1},\dots,C_{k}))^{\star}$
$\displaystyle\triangleq\lambda(\widetilde{h},c).V^{\star}~{}(C_{1}^{\star}~{}\widetilde{h}~{}c)~{}\cdots~{}(C_{k}^{\star}~{}\widetilde{h}~{}c)$
$\displaystyle\text{We suppose }H$ $\displaystyle=\\{\mathtt{return}(x)\mapsto
C_{r};\sigma_{i}(x)\mapsto C_{i}\mid 1\leq i\leq n\\}$
$\displaystyle(\mathtt{with}~{}H~{}\mathtt{handle}~{}C)^{\star}$
$\displaystyle\triangleq\lambda(\widetilde{h},c).C^{\star}~{}(\lambda(x,r).C_{1}^{\star}~{}\widetilde{h}~{}r)~{}\cdots~{}(\lambda(x,r).C_{n}^{\star}~{}\widetilde{h}~{}r)~{}(\lambda
x.C_{r}^{\star}~{}\widetilde{h}~{}c).$

###### Lemma 0.

If $\Gamma\vdash V:T$ then $\Gamma^{\star}\vdash V^{\star}:T^{\star}$ and that
if $\Gamma\vdash_{E}C:T$ then $\Gamma^{\star}\vdash
C^{\star}:E^{\star}\rightarrow\neg\neg T^{\star}$

The proof is straightforward.

###### Lemma 0.

If $\Gamma\vdash_{E}C:T$ and $C\rightarrow D$ then for any well-typed
continuations $(\widetilde{h},c)$, we have
$C^{\star}_{\widetilde{h},c}\rightarrow^{+}B=_{adm}D^{\star}_{\widetilde{h},c}$,
where $=_{adm}$ is the equivalence relation with
$(\lambda({h},c).C)~{}\widetilde{h}~{}c\equiv C$.

###### Proof.

The proof goes by induction on the derivation of $C\rightarrow D$. Some cases
are equivalent to the usual CPS translation so we can safely ignore them.
Similarly to Lemma 4, we have to take care of some administrative reductions.
The new cases correspond to the cases of handlers. The contextual case is
straightforward since we can reduce the head of the $\lambda-Y$-term. The most
interesting case is the handlers against an algebraic operation. For this
case, we have

$(\mathtt{with}~{}H~{}\mathtt{handle}~{}\sigma_{i}(V;y.C))^{\star}~{}\widetilde{h}~{}c\rightarrow^{+}(C_{i}^{\star})[x:=V^{\star}]~{}\widetilde{h}~{}(\lambda
y.C^{\star}~{}\widetilde{\mathcal{H}}~{}\mathcal{C})$

where $\widetilde{\mathcal{H}}$ and $\mathcal{C}$ denotes the continuations
such that

$(\mathtt{with}~{}H~{}\mathtt{handle}~{}C)^{\star}\triangleq\lambda(\widetilde{h},c).C^{\star}~{}\widetilde{\mathcal{H}}~{}\mathcal{C}$

On the other hand, we have:

$(\mathtt{let}~{}y=C_{i}[x:=V]~{}\mathtt{in}~{}(\mathtt{with}~{}H~{}\mathtt{handle}~{}C))^{\star}~{}\widetilde{h}~{}c\rightarrow_{adm}C_{i}^{\star}[x:=V]~{}\widetilde{h}~{}(\lambda
y.(\lambda(\widetilde{h},c).C^{\star}\widetilde{\mathcal{H}}~{}\mathcal{C})~{}\widetilde{h}~{}c)$

And those two terms are administratively equivalent. This concludes this
proof. ∎

We can now define a canonical continuation handler for a given set of effects.

###### Definition 0.

Consider a set $E=\\{\sigma_{i}:\mathtt{B}_{i}\rightsquigarrow k_{i}\\}$ of
effects. We pose $\Sigma_{E}=\\{\sigma_{i}:k_{i}+1\\}$ a signature for terms
of the $\lambda$Y-calculus. We define the identity continuation handler for
$E$ as the $\lambda$Y-term of type $E^{\star}$:

$(\widetilde{h}_{E})_{i}\triangleq\lambda(x,f).\sigma_{i}~{}x~{}(f~{}(\lambda
x_{1},\dots,x_{k}.x_{1}))~{}\cdots~{}(f~{}(\lambda x_{1},\dots,x_{k}.x_{k}))$

In particular, remark that $(\sigma_{i}(V;x.C))^{\star}_{\widetilde{h}_{E},c}$
becomes:

$(\sigma_{i}(V;x.C))^{\star}_{\widetilde{h}_{E},c}\rightarrow\sigma_{i}~{}V^{\star}~{}(C^{\star}[x:=\underline{0}^{\star}]~{}\widetilde{h}_{E}~{}c)~{}\cdots~{}(C^{\star}[x:=\underline{k-1}^{\star}]\widetilde{h}_{E}~{}c)$

which corresponds exactly to the effect tree of $\sigma_{i}(V;x.C)$.

With this remark, we can conclude with the following theorem:

###### Theorem 5.

For any $\vdash_{E}C:T$, for any continuation $\vdash c:T^{\star}\rightarrow
o$, we have:

$ET(C)[\mathtt{return}(V)\leftarrow
BT(c~{}V^{\star})]=BT(V^{\star}~{}\widetilde{h}_{E}~{}c)$

###### Proof.

We can proceed by induction on the effect tree of $C$.

  * •

If $C$ can be reduced infinitely, then by simulation,
$C^{\star}~{}\widetilde{h}_{E}~{}c$ can be reduced infinitely too.

  * •

If $C\rightarrow^{*}\mathtt{return}(V)$. Then
$C^{\star}~{}\widetilde{h}_{E}~{}c\rightarrow^{*}c~{}V^{\star}$ by definition
of $\mathtt{return}(V)^{\star}$.

  * •

If $C\rightarrow^{*}\sigma(V;x.D)$. Then
$C^{\star}~{}\widetilde{h}_{E}~{}c\rightarrow^{*}\sigma_{i}~{}V^{\star}~{}(D^{\star}[x:=\underline{0}^{\star}]~{}\widetilde{h}_{E}~{}c)~{}\cdots~{}(D^{\star}[x:=\underline{k-1}^{\star}]\widetilde{h}_{E}~{}c)$.
And we can conclude by induction hypothesis.

∎

In particular, if we have $T$ has a base type and a continuation that is the
encoding of the identity, we can recover exactly the initial effect tree.
Thus, we have:

###### Corollary 0.

For any GEPCF computation $\vdash C:T$ and $\vdash c:T^{\star}\rightarrow o$,
the MSO model-checking on $ET(C)[\mathtt{return}(V)\leftarrow BT(c~{}V^{*})]$
is decidable.

Similarly to what happened in Corollary 6, there are of course some degrees of
freedom in the choice of the continuation $c$.

##  11\. Related Work

#### Effectful Higher-Order Programs and their Verification

This is definitely not the first paper concerned with the verification of
higher-order effectful programs. the denotational semantics of calculi having
this nature has been studied since Moggi’s seminal work on monads (Moggi,
1988), thus implicitly providing notions of equivalence and refinement. All
this has been given a more operational flavor in Plotkin and Power’s account
on adequacy for algebraic effects (Plotkin and Power, 2003), from which the
operational semantics presented in this paper is greatly inspired. Logics for
algebraic effects have been introduced by Pretnar and Plotkin (Plotkin and
Pretnar, 2008), by Matache and Staton (Matache and Staton, 2019), and by
Simpson and Voorneveld (Simpson and Voorneveld, 2019). The latter has
certainly been another major source of inspiration although, as explicitly
stated by the authors 111In (Simpson and Voorneveld, 2019), Section 10,
paragraph 8: “We view the infinitary propositional logic of this paper as
providing a low-level language, into which practical high-level finitary
logics for expressing program properties can potentially be compiled. […] We
view the development of such high-level logics and their compositional
reasoning principles, aimed at practical specification and verification, as a
particularly promising topic for future research.”, automatic verification
techniques are to be considered out of the scope. In fact, we are not aware of
any attempt to study the decidability of the aforementioned theories.

#### Higher-Order Model Checking

Model checking of higher-order programs has been an active topic of
investigation in the last twenty years, with many positive results, staring
from the pioneering and partial results by Knapik et al.(Knapik et al., 2001,
2002) to the Ong’s already mentioned breakthrough result (Ong, 2006), followed
by Kobayashi and co-authors’ work on model checking as (intersection) type
checking (Kobayashi and Ong, 2009). Noticeably, some of these works go in the
direction of extending the aforementioned decidability results to higher-order
calculi endowed with some _specific_ form of effect, like probabilistic choice
(Kobayashi et al., 2020) or some form of resource usage (Kobayashi, 2009).
Outcomes are not always been on the positive side, as the undecidability of
the model checking problem for probabilistic variations on HORSs shows. Again,
we are not aware of any study aimed at giving general criteria for
decidability.

#### Effect Handlers

Effect handlers are a linguistic feature allowing to give computational
meaning to algebraic operations through handlers, i.e. routines specifically
dedicated to the management of these effects, which in this way can be managed
internally by the program itself rather than by the environment. Given their
elegance and naturalness in generalizing standard language construction like
the $\mathtt{try}~{}\mathtt{with}$ operator for exceptions, handlers has been
largely studied both theoretically and concretely (Plotkin and Pretnar, 2009;
Kammar et al., 2013; Hillerström et al., 2017; Hillerström and Lindley, 2018;
Bauer, 2019; Sekiyama et al., 2020; Biernacki et al., 2019). We are not aware
of any study about handlers in a finitary setting, and even less about
questions of decidability with regards to higher-order model checking.

##  12\. Conclusion

This paper tackles, for the first time in a general way, the problem of
evaluating the intrinsic difficulty of the higher-order model checking problem
when applied to programs that exhibit effects, possibly managed through
handlers. The results obtained are in two styles: while the problem of
capturing algebraic operations in calculi amenable to HOMC does not pose
particular problems and indeed can be solved in its generality, observing the
effects produced by such operations and handling them must be done with great
care: we observe that in general this leads to undecidability, but that in
both cases, criteria can be defined allowing to keep the problem decidable.
This consists, respectively, in observing the effects so that this observation
can be expressed in MSO and in a restricted class of handlers sufficient for
the modeling of the so-called generic effects.

There are aspects that this paper deliberately overlooks, but which certainly
deserve further study. First of all, it should be mentioned that the impact of
effects on (known) complexity results about HOMC is not studied in detail
here, but that the introduced translations (in particular those in Section 5
and Section 8) could be implemented more efficiently, following works on order
optimization (Nakamura et al., 2020). It should also be said that the
possibility of introducing logics more powerful than MSO this way capturing
quantitative observations without possibly falling back into the known cases
of undecidability (e.g., in the case of probabilistic effects) is a very
interesting direction that the authors intend to investigate in the immediate
future.

## References

  * (1)
  * Bauer (2019) Andrej Bauer. 2019\.  What is Algebraic About Algebraic Effects and Handlers?  arXiv:1807.05923 [cs.LO]
  * Biernacki et al. (2019) Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. 2019.  Abstracting Algebraic Effects.  _Proc. ACM Program. Lang._ 3, POPL, Article 6 (2019), 28 pages.