1642 LABEL:LastPageNov. 23, 2019Oct. 02, 2020

# On the Termination Problem
for Probabilistic Higher-Order Recursive Programs

Naoki Kobayashia  aThe University of Tokyo, Japan  ,  Ugo Dal Lagob
bUniversity of Bologna, Italy  and  Charles Grelloisc  cAix Marseille Univ,
Université de Toulon, CNRS, LIS, Marseille, France

###### Abstract.

In the last two decades, there has been much progress on model checking of
both _probabilistic_ systems and _higher-order_ programs. In spite of the
emergence of higher-order probabilistic programming languages, not much has
been done to combine those two approaches. In this paper, we initiate a study
on the probabilistic higher-order model checking problem, by giving some first
theoretical and experimental results. As a first step towards our goal, we
introduce PHORS, a probabilistic extension of higher-order recursion schemes
(HORS), as a model of probabilistic higher-order programs. The model of PHORS
may alternatively be viewed as a higher-order extension of recursive Markov
chains. We then investigate the probabilistic termination problem — or,
equivalently, the probabilistic reachability problem. We prove that almost
sure termination of order-2 PHORS is undecidable. We also provide a fixpoint
characterization of the termination probability of PHORS, and develop a sound
(although possibly incomplete) procedure for approximately computing the
termination probability. We have implemented the procedure for order-2 PHORS,
and confirmed that the procedure works well through preliminary experiments.

###### Key words and phrases:

model checking, probabilistic programs, higher-order programs, termination
probabilities

##  1\. Introduction

Computer science has interacted with probability theory in many fruitful ways,
since the very early days [dLMSS56]. Probability theory enables _state
abstraction_ , reducing in this way the state space’s cardinality. It has also
led to a new _model of computation_ , used for instance in randomized
computation [MR95] or in cryptography [GM84]. The trend of a rise of
probability theory’s importance in computer science has been followed by the
programming language community, up to the point that probabilistic programming
is nowadays a very active research area. Probabilistic choice can be modeled
in various ways in programming, and fair binary probabilistic choice is for
instance perfectly sufficient to obtain universality if the underlying
programming language is universal itself [San69, DZ12]. This has been the path
followed in probabilistic $\lambda$-calculi [Sah78, JP89, DH02, DZ12, ETP14,
DSA14, HKSY17].

In the present paper, we are interested in the analysis of probabilistic,
higher-order recursive programs. Model checking of probabilistic finite state
systems has been a very active research field (see [BK08, CHVB18] for a
survey). Over the last two decades, there has also been much interest and
progress in model checking of probabilistic _recursive_ programs [EY09, EY15,
BEKK13, BBFK14], which _cannot_ be modeled as finite state systems, and thus
escape the classic model checking framework and algorithms. None of the
proposals in the literature on probabilistic model checking, however, is
capable of handling _higher-order_ functions, which are a natural feature in
functional languages. This is in sharp contrast with what happens for _non-
probabilistic_ higher-order programs, for which model checking techniques can
be fruitfully employed for proving both reachability and safety properties, as
shown in the extensive literature on the subject (e.g. [Ong06, HMOS08, Kob13,
KO09, KSU11, GM15b, GM15a, TO14, SW11]). There have been some studies on the
termination of probabilistic higher-order programs [DLG17], but to our
knowledge, they have not provided a procedure for _precisely_ computing the
termination probability, nor discussed whether it is possible at all: see
Section 7 for more details. Summing up, little has been known about the
decidability and complexity of model checking of probabilistic higher-order
programs, and even less about the existence of practical procedures for
approximately solving model checking problems.

One may think that probabilistic _and_ higher-order computation is rather an
exotic research topic, but it is important for precisely modeling and
verifying any higher-order functional programs that interact with a
probabilistic environment. As a simple example, consider the following (non-
higher-order) OCaml-like program, which uses a primitive flip for generating
true or false with probability $\frac{1}{2}$.

⬇

let rec f() = if flip() then () else f() in f()

The program almost surely terminates (i.e., terminates with probability 1),
but if we ignore the probabilistic aspects and model flip() as a _non-
deterministic_ (rather than _probabilistic_) primitive, then we would conclude
that the program can _may_ diverge. The following program makes use of an
interesting combination of probabilistic choice and higher-order functions:

⬇

let boolgen() = flip()

let rec listgen f () =

if flip() then [] else f()::listgen f ()

in listgen (listgen boolgen) ()

The function listgen above takes a generator f of elements as an argument, and
creates a list of elements, each of them obtained by calling $f$. Thus, the
whole program generates a list of lists of Booleans. The length of such a list
of lists is randomized, and distributed according to the geometric
distribution. We may then wish to ask, for example, (i) whether it almost
surely terminates, and (ii) what is the probability that a list of even length
is generated. Generating random data structures like the one produced by
listgen is not an artificial task, being central to, e.g., random test
generation [PF17, MRH18].

As a model of probabilistic higher-order programs, we first introduce PHORS, a
probabilistic extension of higher-order recursion schemes (HORS) [KNU02,
Ong06]. Our model of PHORS is expressive enough to accurately model
probabilistic higher-order functions, but the underlying non-probabilistic
language (i.e., HORS, obtained by removing probabilistic choice) is _not_
Turing-complete; thus, we can hope for the existence of algorithmic solutions
to some of the verification problems. As an example, we can decide indeed
whether the termination probability of PHORS is $0$, by reduction to a model
checking problem for non-probabilistic HORS.

Through the well-known correspondence between HORS and (collapsible) higher-
order pushdown automata [KNU02, HMOS08], PHORS can be considered a higher-
order extension of probabilistic pushdown systems [BEKK13, BBFK14] and of
recursive Markov chains [YE05], the computation models used in previous work
on model checking of probabilistic recursive programs. We can also view PHORS
as an extension of the $\lambda Y$-calculus [Sta04] with probabilities, just
like HORS can be viewed as an alternative presentation of the $\lambda
Y$-calculus. The correspondence between HORS and the $\lambda Y$-calculus has
been useful for transferring techniques for typed $\lambda$-calculi (most
notably, game semantics [Ong06], intersection types [Kob09b, KO09] and Krivine
machines [SW11]) to HORS; thus, we expect similar benefits in using PHORS
(rather than probabilistic higher-order pushdown automata) as models of
probabilistic higher-order programs.

As a first step towards understanding the nature of the model checking problem
for probabilistic higher-order programs, the present paper studies the problem
of computing the termination (or equivalently, reachability) probabilities of
PHORS. Note that, as in a non-probabilistic setting, one can easily reduce a
safety property verification problem to a may-termination problem (i.e. the
problem of checking whether a program may terminate), by encoding safety
violation as termination. We can also verify certain liveness properties, by
encoding a good event as a termination and checking that the termination
probability is $1$. As we will see in Section 2, the two questions (i) and
(ii) mentioned earlier on the listgen program can also be reduced to the
problem of computing the termination probability of a PHORS. Note also that
computing the termination (or equivalently, reachability) probability has been
a key to solving more general model checking problems (such as LTL/CTL model
checking) for recursive programs [YE05, BBFK14].

As the first result on the problem of computing termination probabilities, we
prove that the almost sure termination problem, i.e., whether a given PHORS
terminates with probability $1$, is undecidable at order-2 or higher. This
contrasts with the case of recursive Markov chains, for which the almost sure
termination problem can be decided in PSPACE [EY09]. The proof of
undecidability is based on a reduction from the undecidability of Hilbert’s
tenth problem (i.e. unsolvability of Diophantine equations) [Mat93]. The
undecidability result also implies that it is not possible to compute the
_exact_ termination probability. More precisely, for any rational number
$r\in(0,1]$, the set $\\{\mathcal{G}\mid\Pr(\mathcal{G})\geq r\\}$ (where
$\Pr(\mathcal{G})$ denotes the termination probability of $\mathcal{G}$) is
not recursively enumerable (in other words, the set is $\Pi^{0}_{\\_}1$-hard
in the arithmetical hierarchy). Note, however, that this negative result does
not preclude the possibility to compute the termination probability with
arbitrary precision; there may exist an algorithm that, given a PHORS
$\mathcal{G}$ and $\epsilon>0$ as inputs, finds $r$ such that the termination
probability of $\mathcal{G}$ belongs to $(r,r+\epsilon)$. The existence of
such an approximation algorithm remains open.

As a positive result towards approximately computing the termination
probability, we show that the termination probability of order-$n$ PHORS can
be characterized by fixpoint equations on order-($n-1$) functions on real
numbers. The fixpoint characterization of the termination probability of
recursive Markov chains [EY09] can be viewed as a special case of our result
where $n=1$. The fixpoint characterization immediately provides a semi-
algorithm for the lower-bound problem: “Given a PHORS $\mathcal{G}$ and a
rational number $r\in[0,1]$, does $\Pr(\mathcal{G})>r$ hold?” Recall, however,
that $\\{\mathcal{G}\mid\Pr(\mathcal{G})\geq r\\}$ is _not_ recursively
enumerable, so there is no semi-algorithm for the variation: “Given a PHORS
$\mathcal{G}$ and a rational number $r\in[0,1]$, does $\Pr(\mathcal{G})\geq r$
hold?”

The remaining question is whether an upper-bound on the termination
probability can be computed with arbitrary precision. We have not settled this
question yet, but propose a procedure for _soundly estimating_ an upper-bound
of the termination probability of order-2 PHORS by using the fixpoint
characterization above, _à la_ FEM (finite element method). We have
implemented the procedure, and conducted preliminary experiments to confirm
that the procedure works fairly well in practice: combined with the lower-
bound computation based on the fixpoint characterization, the procedure was
able to instantly compute the termination probabilities of (small but) non-
trivial examples with precision $10^{-2}$. We also briefly discuss how to
generalize the procedure to deal with PHORS of arbitrary orders.

The contributions of this article can thus be summarized as follows:

  1. (1)

A formalization of probabilistic higher-order recursion schemes (PHORS) and
their termination probabilities. This is in Section 2.

  2. (2)

A proof of undecidability of the almost sure termination problem for PHORS (of
order 2 or higher), which can be found in Section 3.

  3. (3)

A fixpoint characterization of the termination probability of PHORS, which
immediately yields the semi-decidability of the lower-bound problem. This is
in Section 4.

  4. (4)

A sound procedure for computing an upper-bound to the termination probability
of order-2 PHORS (which is described in Section 5) accompanied by an
implementation and preliminary experiments with promising results, reported in
Section 6.

We also discuss related work in Section 7, and conclude the article in Section
8. A preliminary summary of this article appeared in Proceedings of LICS 2019
[KDLG19].

##  2\. Probabilistic Higher-Order Recursion Schemes (PHORS) and Termination
Probabilities

This section introduces _probabilistic higher-order recursion schemes_
(PHORS111We write PHORS for both singular and plural forms.), an extension of
higher-order recursion schemes [KNU02, Ong06] in which programs can at any
evaluation step perform a discrete probabilistic choice, then proceeding
according to its outcome. Higher-order recursion schemes are usually treated
as generators of infinite trees, but as we are only interested in the
termination probability, we consider only nullary tree constructors
$\mathtt{e}$ and $\Omega$, which represent termination and divergence
respectively.

We first define types and applicative terms. The set of _types_ , ranged over
by $\kappa$, is given by:

$\kappa::=\mathtt{o}\mid\kappa_{\\_}1\to\kappa_{\\_}2.$

Intuitively, $\mathtt{o}$ describes the unit value, and
$\kappa_{\\_}1\to\kappa_{\\_}2$ describes functions from $\kappa_{\\_}1$ to
$\kappa_{\\_}2$. As usual, the _order_ of a type $\kappa$ is defined by:

$\displaystyle\mathit{order}(\mathtt{o})$ $\displaystyle=0$
$\displaystyle\mathit{order}(\kappa_{\\_}1\to\kappa_{\\_}2)$
$\displaystyle=\max(\mathit{order}(\kappa_{\\_}1)+1,\mathit{order}(\kappa_{\\_}2)).$

We often write $\mathtt{o}^{\ell}\to\mathtt{o}$ for
$\underbrace{\mathtt{o}\to\cdots\to\mathtt{o}}_{\\_}\ell\to\mathtt{o}$, and
abbreviate $\kappa_{\\_}1\to\cdots\to\kappa_{\\_}k\to\kappa$ to
$\widetilde{\kappa}\to\kappa$. The set of _applicative terms_ , ranged over by
$t$, is given by:

$t::=\mathtt{e}\
\;\;\mbox{\Large{$\mid$}}\;\;\Omega\;\;\mbox{\Large{$\mid$}}\;\;\ x\
\;\;\mbox{\Large{$\mid$}}\;\;\ t_{\\_}1t_{\\_}2,$

where $\mathtt{e}$ and $\Omega$ are (the only) constants of type $\mathtt{o}$
and $x$ ranges over a set of variables. Intuitively, $\mathtt{e}$ and $\Omega$
denote termination and divergence respectively (the latter can be defined as a
derived form, but assuming it as a primitive is convenient for Section 4). We
consider the following standard simple type system for applicative terms,
where $\mathcal{K}$, called a _type environment_ , is a map from a finite set
of variables to the set of types.

$\mathcal{K}\vdash\mathtt{e}:\mathtt{o}\qquad\qquad\mathcal{K}\vdash\Omega:\mathtt{o}\qquad\qquad\mathcal{K}\vdash
x\mathbin{:}\kappa\mathcal{K}(x)=\kappa\qquad\qquad\mathcal{K}\vdash
t_{\\_}1t_{\\_}2:\kappa\mathcal{K}\vdash
t_{\\_}1:\kappa_{\\_}2\to\kappa\quad\quad\mathcal{K}\vdash
t_{\\_}2:\kappa_{\\_}2$

######  Definition  (PHORS).

A _probabilistic higher-order recursion scheme_ (PHORS) is a triple
$\mathcal{G}=(\mathcal{N},\mathcal{R},S)$, where:

  1. (1)

$\mathcal{N}$ is a map from a finite set of variables (called _non-terminals_
and typically denoted $F,\,G,\,\ldots$) to the set of types.

  2. (2)

$\mathcal{R}$ is a map from $\mathit{dom}(\mathcal{N})$ to terms of the form
$\lambda x_{\\_}1.\cdots\lambda x_{\\_}k.t_{\\_}L\,\oplus_{p}\,t_{\\_}R$,
where $p\in[0,1]$ is a rational number, and $t_{\\_}L,\,t_{\\_}R$ are
applicative terms. If
$\mathcal{N}(F)=\kappa_{\\_}1\to\cdots\to\kappa_{\\_}k\to\mathtt{o}$,
$\mathcal{R}(F)$ must be of the form $\lambda x_{\\_}1.\cdots\lambda
x_{\\_}k.t_{\\_}L\,\oplus_{p}\,t_{\\_}R$, where
$\mathcal{N},x_{\\_}1\mathbin{:}\kappa_{\\_}1,\ldots,x_{\\_}k\mathbin{:}\kappa_{\\_}k\vdash
t_{\\_}L:\mathtt{o}$ and
$\mathcal{N},x_{\\_}1\mathbin{:}\kappa_{\\_}1,\ldots,x_{\\_}k\mathbin{:}\kappa_{\\_}k\vdash
t_{\\_}R:\mathtt{o}$.

  3. (3)

$S\in\mathit{dom}(\mathcal{N})$, called the _start symbol_ , is a
distinguished non-terminal that satisfies $\mathcal{N}(S)=\mathtt{o}$.

The _order_ of a PHORS $(\mathcal{N},\mathcal{R},S)$ is
$\max_{\\_}{F\in\mathit{dom}(\mathcal{N})}\mathit{order}(\mathcal{N}(F))$,
i.e., the highest order of the types of its non-terminals. We write
$\mathcal{P}_{\\_}k$ for the set of order-$k$ PHORS.

When $\mathcal{R}(F)=\lambda x_{\\_}1.\cdots\lambda
x_{\\_}k.t_{\\_}L\,\oplus_{p}\,t_{\\_}R$, we often write
$F\,x_{\\_}1\,\cdots\,x_{\\_}k=t_{\\_}L\,\oplus_{p}\,t_{\\_}R$, and specify
$\mathcal{R}$ as a set of such equations. The rule
$F\,x_{\\_}1\,\cdots\,x_{\\_}k=t_{\\_}L\,\oplus_{p}\,t_{\\_}R$ intuitively
means that $F\,t_{\\_}1\,\cdots\,t_{\\_}k$ is reduced to
$[t_{\\_}1/x_{\\_}1,\ldots,t_{\\_}k/x_{\\_}k]t_{\\_}L$ and
$[t_{\\_}1/x_{\\_}1,\ldots,t_{\\_}k/x_{\\_}k]t_{\\_}R$ with probabilities $p$
and $1-p$, respectively. We often write just
$F\,x_{\\_}1\,\cdots\,x_{\\_}k=t_{\\_}L$ for
$F\,x_{\\_}1\,\cdots\,x_{\\_}k=t_{\\_}L\,\oplus_{1}\,t_{\\_}R$.

######  Definition  (Operational Semantics and Termination Probability of
PHORS).

Given a PHORS $\mathcal{G}=(\mathcal{N},\mathcal{R},S)$, the rewriting
relation $\xrightarrow{d,p}_{\mathcal{G}}$ (where $d\in\\{L,R\\}$ and
$p\in[0,1]$) is defined by:

$F\,t_{\\_}1\,\cdots\,t_{\\_}k\xrightarrow{L,p}_{\mathcal{G}}[t_{\\_}1/x_{\\_}1,\ldots,t_{\\_}k/x_{\\_}k]t_{\\_}{L}\mathcal{R}(F)=\lambda
x_{\\_}1.\cdots\lambda x_{\\_}k.t_{\\_}L\,\oplus_{p}\,t_{\\_}R\qquad\qquad
F\,t_{\\_}1\,\cdots\,t_{\\_}k\xrightarrow{R,1-p}_{\mathcal{G}}[t_{\\_}1/x_{\\_}1,\ldots,t_{\\_}k/x_{\\_}k]t_{\\_}{R}\mathcal{R}(F)=\lambda
x_{\\_}1.\cdots\lambda x_{\\_}k.t_{\\_}L\,\oplus_{p}\,t_{\\_}R$

We write $\ext@arrow 0359\Rightarrowfill@{}{\pi,p}_{\mathcal{G}}$ for the
relational composition of
$\xrightarrow{d_{\\_}1,p_{\\_}1}_{\mathcal{G}},\ldots,\xrightarrow{d_{\\_}n,p_{\\_}n}_{\mathcal{G}}$,
when $\pi=d_{\\_}1\cdots d_{\\_}n$ and $p=\prod_{\\_}{i=1}^{n}p_{\\_}i$. Note
that $n$ may be $0$, so that we have $t_{\\_}1\ext@arrow
0359\Rightarrowfill@{}{\epsilon,1}_{\mathcal{G}}t_{\\_}2$ iff
$t_{\\_}1=t_{\\_}2$. By definition, for each $\pi\in\\{L,R\\}^{*}$, there
exists at most one $p$ such that $S\ext@arrow
0359\Rightarrowfill@{}{\pi,p}_{\mathcal{G}}\ \\!\mathtt{e}$. For an
applicative term $t$, we define $\mathcal{P}(\mathcal{G},t,\pi)$ by:

$\mathcal{P}(\mathcal{G},t,\pi)=\left\\{\begin{array}[]{ll}p&\mbox{if
$t\ext@arrow 0359\Rightarrowfill@{}{\pi,p}_{\mathcal{G}}\mathtt{e}$}\\\
0&\mbox{if $t\ext@arrow 0359\Rightarrowfill@{}{\pi,p}_{\mathcal{G}}\mathtt{e}$
does not hold for any $p$}\end{array}\right..$

The _partial_ and _full_ _termination probabilities_ , written
$\mathcal{P}(\mathcal{G},t,n)$ and $\mathcal{P}(\mathcal{G},t)$, are defined
by:

$\mathcal{P}(\mathcal{G},t,n)=\displaystyle\sum_{\\_}{\pi\in\\{L,R\\}^{\leq
n}}\ \
\mathcal{P}(\mathcal{G},t,\pi)\qquad\text{and}\qquad\mathcal{P}(\mathcal{G},t)=\displaystyle\sum_{\\_}{\pi\in\\{L,R\\}^{*}}\
\ \mathcal{P}(\mathcal{G},t,\pi).$

Finally, we set $\mathcal{P}(\mathcal{G},n)\,=\,\mathcal{P}(\mathcal{G},S,n)$
and $\mathcal{P}(\mathcal{G})\,=\,\mathcal{P}(\mathcal{G},S)$.

We often omit the subscript $\mathcal{G}$ below and just write
$\xrightarrow{d,p}$ and $\ext@arrow 0359\Rightarrowfill@{}{\pi,p}$ for
$\xrightarrow{d,p}_{\mathcal{G}}$ and $\ext@arrow
0359\Rightarrowfill@{}{\pi,p}_{\mathcal{G}}$ respectively. The _termination
probability of_ $\mathcal{G}$ refers to its full termination probability
$\mathcal{P}(\mathcal{G})$.

######  Example 2.1.

Let $\mathcal{G}_{\\_}1$ be the order-1 PHORS
$(\mathcal{N}_{\\_}1,\mathcal{R}_{\\_}1,S)$, where:

$\begin{array}[]{l}\mathcal{N}_{\\_}1=\\{S\mapsto\mathtt{o},F\mapsto\mathtt{o}\to\mathtt{o}\\}\\\
\mathcal{R}_{\\_}1=\\{S\ =\ F\,\mathtt{e}\,\oplus_{1}\,\Omega,\quad F\,x\ =\
x\,\oplus_{p}\,F(F\,x)\\}.\end{array}$

The start symbol $S$ can be reduced, for example, as follows.

$S\xrightarrow{L,1}F(\mathtt{e})\xrightarrow{R,1-p}F(F\,\mathtt{e})\xrightarrow{L,p}F\,\mathtt{e}\xrightarrow{L,p}\mathtt{e}.$

Thus, we have $S\ext@arrow
0359\Rightarrowfill@{}{LRLL,p^{2}(1-p)}_{\,}\\!\mathtt{e}$. As we will see in
Section 4, the termination probability $\mathcal{P}(\mathcal{G}_{\\_}1)$ is
the least solution for $r$ of the fixpoint equation: $r=p+(1-p)r^{2}$.
Therefore, $\mathcal{P}(\mathcal{G}_{\\_}1)=\frac{p}{1-p}$ if $0\leq
p<\frac{1}{2}$ and $\mathcal{P}(\mathcal{G}_{\\_}1)=1$ if $\frac{1}{2}\leq p$.
The corresponding example of a recursive Markov chain is shown in Figure 1,
using the notational conventions from [EY09]. $\mathcal{G}_{\\_}1$ can be seen
as realizing a binary, random walk on the natural numbers, starting from $1$.
∎

Figure 1. A Recursive Markov Chain Modeling $\mathcal{G}_{\\_}1$.

As the previous example suggests, there is a mutual translation between
recursive Markov chains and order-1 PHORS; see the Appendix A.1 for details.

######  Example 2.2.

Let $\mathcal{G}_{\\_}2$ be the order-2 PHORS
$(\mathcal{N}_{\\_}2,\mathcal{R}_{\\_}2,S)$ where:

$\displaystyle\mathcal{N}_{\\_}2=$
$\displaystyle\;\\{S\mapsto\mathtt{o},H\mapsto\mathtt{o}\to\mathtt{o},F\mapsto(\mathtt{o}\to\mathtt{o})\to\mathtt{o},$
$\displaystyle\hskip
8.00003ptD\mapsto(\mathtt{o}\to\mathtt{o})\to\mathtt{o}\to\mathtt{o}\\}$
$\displaystyle\mathcal{R}_{\\_}2=$ $\displaystyle\;\\{S=\
(F\,H)\,\oplus_{1}\,\mathtt{e},\ H\,x=x\,\oplus_{\frac{1}{2}}\,\Omega,$
$\displaystyle\hskip
8.00003ptF\,g=(g\,\mathtt{e})\,\oplus_{\frac{1}{2}}\,(F(D\,g)),\
D\,g\,x=(g\,(g\,x))\,\oplus_{1}\,\Omega\\}.$

The start symbol $S$ can be reduced, for example, as follows.

$\displaystyle S$
$\displaystyle\xrightarrow{L,1}F\,H\xrightarrow{R,\frac{1}{2}}F(D\,H)\xrightarrow{L,\frac{1}{2}}D\,H\,\mathtt{e}\xrightarrow{L,1}H(H\,\mathtt{e})$
$\displaystyle\xrightarrow{L,\frac{1}{2}}H\,\mathtt{e}\xrightarrow{L,\frac{1}{2}}\mathtt{e}.$

Contrary to $\mathcal{G}_{\\_}1$, it is quite hard to find an RMC which models
the behavior of $\mathcal{G}_{\\_}2$. In fact, this happens for very good
reasons, as we will see in Section 3. ∎

The following result is obvious from the definition of
$\mathcal{P}(\mathcal{G})$.

######  Theorem 2.2.

For any rational number $r\in[0,1]$, the set
$\\{\mathcal{G}\mid\mathcal{P}(\mathcal{G})>r\\}$ is recursively enumerable.

######  Proof 2.3.

This follows immediately from the facts that $\mathcal{P}(\mathcal{G})>r$ if
and only if $\mathcal{P}(\mathcal{G},n)=\sum_{\\_}{\pi\in\\{L,R\\}^{\leq
n}}\,\mathcal{P}(\mathcal{G},S,\pi)>r$ for some $n$, and that
$\mathcal{P}(\mathcal{G},n)$ is computable.

In other words, whether $\mathcal{P}(\mathcal{G})>r$ is semi-decidable, i.e.,
there exists a procedure that eventually answers “yes” whenever
$\mathcal{P}(\mathcal{G})>r$. As we will see in Section 3, however, for every
$r\in(0,1]$, $\\{\mathcal{G}\mid\mathcal{P}(\mathcal{G})\geq r\\}$ is _not_
recursively enumerable.

######  Remark 2.4.

Given a PHORS $\mathcal{G}$, replacing each probabilistic operator
$\,\oplus_{p}\,$ s.t. $0<p<1$ with a binary tree constructor br and replacing
$t_{\\_}L\,\oplus_{1}\,t_{\\_}R$ ($t_{\\_}L\,\oplus_{0}\,t_{\\_}R$, resp.)
with $t_{\\_}L$ ($t_{\\_}R$, resp.), we obtain an ordinary HORS
$\mathcal{G}^{\mathit{ND}}$. Then $\mathcal{P}(\mathcal{G})=0$ if and only if
the tree generated by $\mathcal{G}^{\mathit{ND}}$ has no finite path to
$\mathtt{e}$. Thus, by [KO11] (see the paragraph below the proof of Theorem
4.5 about the complexity of the reachability problem), whether
$\mathcal{P}(\mathcal{G})=0$ is decidable, and $(n-1)$-EXPTIME complete. Note,
on the other hand, that there is no clear correspondence between the almost
sure termination problem
$\mathcal{P}(\mathcal{G})\stackrel{{\scriptstyle?}}{{=}}1$ and a model
checking problem for $\mathcal{G}^{\mathit{ND}}$. If the tree of
$\mathcal{G}^{\mathit{ND}}$ has neither $\Omega$ nor an infinite path (which
is decidable), then $\mathcal{P}(\mathcal{G}){=}1$, but the converse does not
hold.

######  Remark 2.5.

The restriction that a probabilistic choice may occur only at the top-level of
each rule is _not_ a genuine restriction. Indeed, whenever we wish to write a
rule of the form $F\;\widetilde{x}=C[t_{\\_}L\,\oplus_{p}\,t_{\\_}R]$, we can
normalize it to $F\;\widetilde{x}=C[G\;\widetilde{x}]$, where $G$ is defined
by $G\;\widetilde{x}=t_{\\_}L\,\oplus_{p}\,t_{\\_}R$. Keeping this in mind, we
sometimes allow probabilistic choices to occur inside terms. In fact, a PHORS
can be considered as a term (of type $\mathtt{o}$) of a probabilistic
extension of the (call-by-name) $\lambda Y$-calculus [Sta04]. We define the
set of probabilistic $\lambda Y$ terms by:

$s::=\mathtt{e}\;\;\mbox{\Large{$\mid$}}\;\;\Omega\;\;\mbox{\Large{$\mid$}}\;\;x\;\;\mbox{\Large{$\mid$}}\;\;\lambda
x.s\;\;\mbox{\Large{$\mid$}}\;\;s_{\\_}1s_{\\_}2\;\;\mbox{\Large{$\mid$}}\;\;Y(\lambda
f.\lambda x.s)\;\;\mbox{\Large{$\mid$}}\;\;s_{\\_}1\,\oplus_{p}\,s_{\\_}2.$

Here, $\,\oplus_{p}\,$ is a probabilistic choice operator of type
$\mathtt{o}\to\mathtt{o}\to\mathtt{o}$, and other terms are simply-typed in
the usual way. Then, PHORS and probabilistic $\lambda Y$ terms can be
converted to each other. We use PHORS in the present paper for the convenience
of the fixpoint characterizations discussed in Section 4.

######  Remark 2.6.

We adopt the call-by-name semantics, and allow probabilistic choices only on
terms of type $\mathtt{o}$. The call-by-value semantics, as well as
probabilistic choices at higher-order types can be modeled by applying a
standard CPS transformation. Moreover, a PHORS does not have data other than
functions, but as in ordinary HORS [Kob13], elements of a finite set (such as
Booleans) can be modeled by using Church encoding.

We provide a few more examples of PHORS below.

######  Example 2.7.

Recall the list generator example in Section 1, whose termination is
equivalent to that of the following program, obtained by replacing the output
of each function with the unit value ().

⬇

let boolgen() = flip() in

let rec listgen f ()=

if flip() then () else (f(); listgen f ())

in listgen (listgen boolgen) ()

With a kind of CPS transformation, termination of the above program is reduced
to that of the following PHORS $\mathcal{G}_{\\_}3$:

$\displaystyle S$
$\displaystyle=\textit{Listgen}\;(\textit{Listgen}\,\textit{Boolgen})\;\mathtt{e}$
$\displaystyle\textit{Boolgen}\;k$ $\displaystyle=k$
$\displaystyle\textit{Listgen}\;f\;k$
$\displaystyle=k\,\oplus_{\frac{1}{2}}\,f(\textit{Listgen}\,f\,k)$

It is not difficult to confirm that $\mathcal{P}(\mathcal{G}_{\\_}3)=1$ (using
the fixpoint characterization given in Section 4).

######  Example 2.8.

The following is a variation of the list generator example (Example 2.7),
which generates ternary trees instead of lists:

⬇

let boolgen() = flip() in

let rec treegen f =

if flip() then Leaf

else Node(f(), treegen f, treegen f, treegen f) in

treegen(boolgen)

The following PHORS $\mathcal{G}_{\\_}4$ captures the termination probability
of the aforementioned program:

$\displaystyle S$
$\displaystyle=\textit{Treegen}\;\textit{Boolgen}\;\mathtt{e}$
$\displaystyle\textit{Boolgen}\;k$ $\displaystyle=k$
$\displaystyle\textit{Treegen}\;f\;k$
$\displaystyle=k\,\oplus_{\frac{1}{2}}\,(f(\textit{Treegen}\,f\,(\textit{Treegen}\,f\,(\textit{Treegen}\,f\,k))))$

Interestingly, $\mathcal{G}_{\\_}4$ is _not_ almost surely terminating, since
$\mathcal{P}(\mathcal{G}_{\\_}4)=\frac{\sqrt{5}-1}{2}$.

To increase the chance of termination, let us change the original program as
follows:

⬇

let boolgen() = flip() in

let rec treegen p f =

if flipp(p) then Leaf

else Node(f(), treegen $\frac{\texttt{p}+1}{2}$ f, treegen
$\frac{\texttt{p}+1}{2}$ f, treegen $\frac{\texttt{p}+1}{2}$ f) in

treegen $\frac{1}{2}$ boolgen

where flipp is the natural generalization of flip. Here, treegen is
parameterized with probability p, which is increased upon each recursive call.
We assume that flipp(p) returns $\mathtt{true}$ with probability p and
$\mathtt{false}$ with $1-\texttt{p}$. The corresponding PHORS
$\mathcal{G}_{\\_}5$ is:

$\displaystyle S$
$\displaystyle=\textit{Treegen}\;H\;\textit{Boolgen}\;\mathtt{e}$
$\displaystyle\textit{Boolgen}\;k$ $\displaystyle=k$ $\displaystyle H\;x\;y$
$\displaystyle=x\,\oplus_{\frac{1}{2}}\,y$ $\displaystyle G\;p\;x\;y$
$\displaystyle=x\,\oplus_{\frac{1}{2}}\,(p\;x\;y)$
$\displaystyle\textit{Treegen}\;p\;f\;k$
$\displaystyle=p\;k\;(f(\textit{Treegen}\,(G\;p)\,f\,(\textit{Treegen}\,(G\;p)\,f\,(\textit{Treegen}\,(G\;p)\,f\,k))))$

The function Treegen is parameterized by a probabilistic choice function $p$,
which is initially set to the function $H$ (that chooses the first argument
with probability $\frac{1}{2}$). The function $G$ takes a probabilistic choice
function $p$, and returns a probabilistic function $\lambda x.\lambda
y.x\,\oplus_{\frac{1}{2}}\,(p\;x\;y)$, which chooses the first argument with
probability $\frac{\texttt{p}+1}{2}$ where p is the probability that $p$
chooses the first argument. As expected, $\mathcal{G}_{\\_}5$ is almost surely
terminating. ∎

######  Example 2.9.

Recall the list generator example again. Suppose that we wish to compute the
probability that listgen(boolgen) generates a list of even length. It can be
reduced to the problem of computing the termination probability of the
following program:

⬇

let boolgen() = flip() in

let rec loop() = loop() in

let rec listgenE f () =

if flip() then () else (f();listgenO f ())

and listgenO f () =

if flip() then loop() else (f();listgenE f ()) in

listgenE boolgen ()

Here, we have duplicated listgen to listgenE and listgenO, which are expected
to simulate the generation of even and odd lists respectively. Thus, the then-
branches of listgenE and listgenO have been replaced by termination and
divergence respectively. As in the previous example, the above program can
further be translated to the following PHORS $\mathcal{G}_{\\_}6$:

$\displaystyle S$
$\displaystyle=\textit{ListgenE}\;\textit{Boolgen}\;\mathtt{e}$
$\displaystyle\textit{Boolgen}\;k$ $\displaystyle=k$
$\displaystyle\textit{ListgenE}\;f\;k$
$\displaystyle=k\,\oplus_{\frac{1}{2}}\,(f(\textit{ListgenO}\,f\,k))$
$\displaystyle\textit{ListgenO}\;f\;k$
$\displaystyle=\Omega\,\oplus_{\frac{1}{2}}\,(f(\textit{ListgenE}\,f\,k)).$

The termination probability of the PHORS is

$\frac{1}{2}+\frac{1}{2}\cdot\frac{1}{4}+\frac{1}{2}\cdot\left(\frac{1}{4}\right)^{2}+\cdots=\frac{1}{2}\cdot\sum_{\\_}{i=0}^{\infty}\frac{1}{4^{i}}=\frac{2}{3}.$

Thus, the probability that the original program generates an even list is also
$\frac{2}{3}$.

Let us also consider the problem of computing the probability that
listgen(boolgen) generates a list containing an even number of
$\mathtt{true}$’s. It can be reduced to the termination probability of the
following PHORS.

$\displaystyle S$
$\displaystyle=\textit{ListgenE}\;\textit{Boolgen}\;\mathtt{e}$
$\displaystyle\textit{Boolgen}\;k_{\\_}1\;k_{\\_}2$
$\displaystyle=k_{\\_}1\,\oplus_{\frac{1}{2}}\,k_{\\_}2$
$\displaystyle\textit{ListgenE}\;f\;k$
$\displaystyle=k\,\oplus_{\frac{1}{2}}\,(f(\textit{ListgenO}\,f\,k)(\textit{ListgenE}\,f\,k))$
$\displaystyle\textit{ListgenO}\;f\;k$
$\displaystyle=\Omega\,\oplus_{\frac{1}{2}}\,(f(\textit{ListgenE}\,f\,k)(\textit{ListgenO}\,f\,k)).$

The function Boolgen now takes two continuations $k_{\\_}1$ and $k_{\\_}2$ as
arguments, and calls $k_{\\_}1$ or $k_{\\_}2$ according to whether
$\mathtt{true}$ or $\mathtt{false}$ is generated in the original program. The
function ListgenE (ListgenO, resp.) is called when the number of
$\mathtt{true}$’s generated so far is even (odd, resp.). The termination
probability of the PHORS above is $\frac{3}{4}$. ∎

In the following example, a standard program transformation for randomized
algorithms is captured as a PHORS. More specifically, a higher-order function
is defined, which turns any Las-Vegas algorithm that sometimes declares not to
be able to provide the correct answer into one that _always_ produces the
correct answer. (For more details about the use of the scheme above, please
refer to [Hro05]).

######  Example 2.10.

Consider a probabilistic function $f$, which takes a value of type $A$, and
returns a value of type $B$ with probability $p$ and Unknown with probability
$1-p$, where $p>0$. The following higher-order function determinize takes such
a function $f$ as an argument, and generates a function from $A$ to $B$.

⬇

type ’b pans = Ans of ’b | Unknown

let rec determinize(f:’a->’b pans)(x:’a)=

match f x with

Ans(r) -> r

| Unknown -> determinize f x

To confirm that $\texttt{determinize}\ f$ almost surely terminates and returns
a value of type $B$, it suffices to check that the PHORS term
$\textit{Determinize}\;g$ almost surely terminates for $g=\lambda y.\lambda
z.y\,\oplus_{p}\,z$, where Determinize is defined by:

$\textit{Determinize}\;g=g\;\mathtt{e}\;(\textit{Determinize}\;g).$

Here, the first argument of $g$ corresponds to the body of the clause
$\texttt{Ans(r)->}\cdots$, while the second argument corresponds to that of
the clause $\texttt{Unknown->}\cdots$. Almost sure termination of
$\textit{Determinize}(\lambda y.\lambda z.y\,\oplus_{p}\,z)$ for any $p>0$ can
further be encoded as that of the following PHORS $\mathcal{G}_{\\_}7$:

$\displaystyle S$
$\displaystyle=(\textit{Determinize}\;\textit{One})\,\oplus_{\frac{1}{2}}\,(\textit{ForallP}\;\textit{Zero}\;\textit{One})$
$\displaystyle\textit{One}\;y\;z$ $\displaystyle=y$
$\displaystyle\textit{Zero}\;y\;z$ $\displaystyle=z$
$\displaystyle\textit{Avg}\;p\;q\;y\;z$
$\displaystyle=(p\;y\;z)\,\oplus_{\frac{1}{2}}\,(q\;y\;z)$
$\displaystyle\textit{ForallP}\;p\;q$
$\displaystyle=(\textit{Determinize}\;(\textit{Avg}\;p\;q))\,\oplus_{\frac{1}{2}}\,$
$\displaystyle\qquad((\textit{ForallP}\;p\;(\textit{Avg}\;p\;q))\,\oplus_{\frac{1}{2}}\,(\textit{ForallP}\;(\textit{Avg}\;p\;q)\;q))$

It runs $\textit{Determinize}\;(\lambda y.\lambda z.y\,\oplus_{p}\,z)$ for
every $p\;(0<p\leq 1)$ of the form $\frac{k}{2^{n}}$ with non-zero
probability. Thus, $\mathcal{P}(\mathcal{G}_{\\_}7)=1$ if
$\textit{Determinize}(\lambda y.\lambda z.y\,\oplus_{p}\,z)$ almost surely
terminates for every $p>0$. Conversely, by the continuity of the termination
probability of $\textit{Determinize}\;(\lambda y.\lambda z.y\,\oplus_{p}\,z)$
except at $p=0$ (which we omit to discuss formally),
$\mathcal{P}(\mathcal{G}_{\\_}7)=1$ implies that $\textit{Determinize}(\lambda
y.\lambda z.y\,\oplus_{p}\,z)$ almost surely terminates for every $p>0$. ∎

######  Remark 2.11.

Although PHORS do not have probabilities as first-class values, as
demonstrated in the examples above, certain operations on probabilities can be
realized by encoding a probability $p$ into a probabilistic function $\lambda
x.\lambda y.x\,\oplus_{p}\,y$. The function Avg in Example 2.10 realizes the
average operation $\frac{p_{\\_}1+p_{\\_}2}{2}$. The multiplication
$p_{\\_}1p_{\\_}2$ can be represented by $\textit{Mult}\;p_{\\_}1\;p_{\\_}2$,
where $\textit{Mult}\;p_{\\_}1\;p_{\\_}2\;x\,y=p_{\\_}1\;(p_{\\_}2\;x\;y)\;y$.

##  3\. Undecidability of Almost Sure Termination of Order-2 PHORS

We prove in this section that the almost sure termination problem, i.e.,
whether the termination probability $\mathcal{P}(\mathcal{G})$ of a given
PHORS $\mathcal{G}$ is $1$, is undecidable even for order-2 PHORS. The proof
is by reduction from the undecidability of Hilbert’s 10th problem [Mat93]
(i.e. unsolvability of Diophantine equations). Note that almost sure
termination of an order-1 PHORS is decidable, as order-1 PHORS are essentially
equi-expressive with probabilistic pushdown systems and recursive Markov
chains [EY09, EY15, BEKK13, BBFK14]. In fact, by the fixpoint characterization
given in Section 4.3, the termination probability of an order-1 PHORS can be
expressed as the least solution of fixpoint equations over reals, which can be
solved as discussed in [EY09]. Thus, our undecidability result for order-2
PHORS is optimal.

We start by giving an easy reformulation of the unsolvability of Diophantine
equations in terms of polynomials with _non-negative_ coefficients, which
follows immediately from the original result.

######  Lemma 3.1.

Given two polynomials $P(x_{\\_}1,\ldots,x_{\\_}k)$ and
$Q(x_{\\_}1,\ldots,x_{\\_}k)$ with non-negative integer coefficients, whether
$P(x_{\\_}1,\ldots,x_{\\_}k)<Q(x_{\\_}1,\ldots,x_{\\_}k)$ for some
$x_{\\_}1,\ldots,x_{\\_}k\in\mathbf{Nat}$ is undecidable. More precisely, the
set of pairs of polynomials:
$\\{(P(x_{\\_}1,\ldots,x_{\\_}k),Q(x_{\\_}1,\ldots,x_{\\_}k))\mid\exists
x_{\\_}1,\ldots,x_{\\_}k\in\mathbf{Nat}.P(x_{\\_}1,\ldots,x_{\\_}k)<Q(x_{\\_}1,\ldots,x_{\\_}k)\\}$
is $\Sigma^{0}_{\\_}1$-complete in the arithmetical hierarchy.

######  Proof 3.2.

Let $D(x_{\\_}1,\ldots,x_{\\_}k)$ be a multivariate polynomial with integer
coefficients. Then, for all natural numbers
$x_{\\_}1,\ldots,x_{\\_}k\in\mathbf{Nat}$, $D(x_{\\_}1,\ldots,x_{\\_}k)=0$ if
and only if $(D(x_{\\_}1,\ldots,x_{\\_}k))^{2}-1<0$. Any such polynomial
$(D(x_{\\_}1,\ldots,x_{\\_}k))^{2}-1$ may be rewritten as
$P(x_{\\_}1,\ldots,x_{\\_}k)-Q(x_{\\_}1,\ldots,x_{\\_}k)$, where
$P(x_{\\_}1,\ldots,x_{\\_}k)$ and $Q(x_{\\_}1,\ldots,x_{\\_}k)$ have only non-
negative integer coefficients. Then, $D(x_{\\_}1,\ldots,x_{\\_}k)=0$ if and
only if $P(x_{\\_}1,\ldots,x_{\\_}k)<Q(x_{\\_}1,\ldots,x_{\\_}k)$. Since
whether $D(x_{\\_}1,\ldots,x_{\\_}k)=0$ for some
$x_{\\_}1,\ldots,x_{\\_}k\in\mathbf{Nat}$ is undecidable [Mat93], it is also
undecidable whether $P(x_{\\_}1,\ldots,x_{\\_}k)<Q(x_{\\_}1,\ldots,x_{\\_}k)$
for some $x_{\\_}1,\ldots,x_{\\_}k\in\mathbf{Nat}$. Furthermore, since the set
of sastisfiable Diophantine equations is $\Sigma^{0}_{\\_}1$-complete, the set
$\\{(P(x_{\\_}1,\ldots,x_{\\_}k),Q(x_{\\_}1,\ldots,x_{\\_}k))\mid\exists
x_{\\_}1,\ldots,x_{\\_}k\in\mathbf{Nat}.P(x_{\\_}1,\ldots,x_{\\_}k)<Q(x_{\\_}1,\ldots,x_{\\_}k)\\}$
is $\Sigma^{0}_{\\_}1$-hard. The set is also obviously recursively enumerable,
hence belongs to $\Sigma^{0}_{\\_}1$.

Roughly, the idea of our undecidability proof is to show that for every $P$
and $Q$ as above, one can effectively construct an order-$2$ PHORS that _does
not_ almost surely terminate if and only if
$P(x_{\\_}1,\ldots,x_{\\_}k)<Q(x_{\\_}1,\ldots,x_{\\_}k)$ _for some_
$x_{\\_}1,\ldots,x_{\\_}k$. Henceforth, we say $t$ is _non-AST_ if $t$ is not
almost surely terminating. For ease of understanding, we first construct an
order-$3$ PHORS $\mathcal{G}^{P,Q}_{3}$ that satisfies the property above in
Section 3.1 and then refine the construction to obtain an order-$2$ PHORS
$\mathcal{G}^{P,Q}_{2}$ with the same property in Section 3.2.

###  3.1. Construction of the Order-3 PHORS $\mathcal{G}^{P,Q}_{3}$

Let $P(x_{\\_}1,\ldots,x_{\\_}k)$ and $Q(x_{\\_}1,\ldots,x_{\\_}k)$ be, as
above, polynomials with non-negative coefficients. We give the construction of
$\mathcal{G}^{P,Q}_{3}$ in a top-down manner. We let $\mathcal{G}^{P,Q}_{3}$
enumerate all the tuples of natural numbers $(n_{\\_}1,\ldots,n_{\\_}k)$, and
for each tuple, spawn a process
$\mathit{Lt}\,(P(n_{\\_}1,\ldots,n_{\\_}k))\,(Q(n_{\\_}1,\ldots,n_{\\_}k))$
with non-zero probability, where $\mathit{Lt}\,m_{\\_}1\,m_{\\_}2$ is a
process that is non-AST if and only if $m_{\\_}1<m_{\\_}2$. Thus, we define
the start symbol $S$ of $\mathcal{G}^{P,Q}_{3}$ by:

$\displaystyle S=$ $\displaystyle\;\mathit{Loop}\;Zero\;\cdots\;Zero.$
$\displaystyle\mathit{Loop}\,x_{\\_}1\,\cdots\,x_{\\_}k=$
$\displaystyle\;(\mathit{Lt}\,(P\,x_{\\_}1\,\cdots\,x_{\\_}k)\,(Q\,x_{\\_}1\,\cdots\,x_{\\_}k))$
$\displaystyle\vspace{-20pt}\,\oplus_{\frac{1}{2}}\,(\mathit{Loop}\,(\mathit{Succ}\,x_{\\_}1)\,\cdots\,x_{\\_}k)\,\oplus_{\frac{1}{2}}\,\cdots$
$\displaystyle\vspace{-20pt}\,\oplus_{\frac{1}{2}}\,(\mathit{Loop}\,x_{\\_}1\,\cdots\,(\mathit{Succ}\,x_{\\_}k)).$

Here, for readability, we have extended the righthand sides of rules to
$n$-ary probabilistic choices:

$t_{\\_}1\,\oplus_{p_{\\_}1}\,t_{\\_}2\,\oplus_{p_{\\_}2}\,\cdots\,\oplus_{p_{\\_}{n-1}}\,t_{\\_}n.$

These can be expressed as
$t_{\\_}1\,\oplus_{p_{\\_}1}\,(F_{\\_}2\,x_{\\_}1\,\cdots\,x_{\\_}k)$, where
auxiliary non-terminals are defined by:

$F_{\\_}2\,x_{\\_}1\,\cdots\,x_{\\_}k=t_{\\_}2\,\oplus_{p_{\\_}2}\,(F_{\\_}3\,x_{\\_}1\,\cdots\,x_{\\_}k)\qquad\cdots\qquad
F_{\\_}{n-1}\,x_{\\_}1\,\cdots\,x_{\\_}k=t_{\\_}{n-1}\,\oplus_{p_{\\_}{n-1}}\,t_{\\_}n.$

We can express natural numbers and operations on them by using Church
encoding:

$\displaystyle Zero\;s\;z$ $\displaystyle=z$
$\displaystyle\mathit{Succ}\;n\;s\;z$ $\displaystyle=s\;(n\;s\;z)$
$\displaystyle\mathit{Add}\;n\;m\;s\;z$ $\displaystyle=n\;s\;(m\;s\;z)$
$\displaystyle\mathit{Mult}\;n\;m\;s\;z$ $\displaystyle=n\;(m\;s)\;z.$

Here, the types of non-terminals above are given by:

$\displaystyle\mathcal{N}(Zero)$ $\displaystyle=\mathsf{CT}$
$\displaystyle\qquad\qquad\mathcal{N}(\mathit{Succ})$
$\displaystyle=\mathsf{CT}\to\mathsf{CT}$
$\displaystyle\mathcal{N}(\mathit{Add})=\mathcal{N}(\mathit{Mult})$
$\displaystyle=\mathsf{CT}\to\mathsf{CT}\to\mathsf{CT},$

where $\mathsf{CT}=(\mathtt{o}\to\mathtt{o})\to\mathtt{o}\to\mathtt{o}$ is the
usual type of Church numerals. Note that the order of $\mathsf{CT}$ is $2$,
while that of $\mathcal{N}(\mathit{Succ})$, $\mathcal{N}(\mathit{Add})$, and
$\mathcal{N}(\mathit{Mult})$ is $3$. By using the just introduced operators,
we can easily define $P$ and $Q$ as order-3 non-terminals. By abuse of
notation, we often use symbols $P$ and $Q$ to denote both polynomials and the
representations of them as non-terminals; similarly for natural numbers.

It remains to define an order-3 non-terminal $\mathit{Lt}$, so that
$\mathit{Lt}\,m_{\\_}1\,m_{\\_}2$ is non-AST if and only if
$m_{\\_}1<m_{\\_}2$. Since $\mathcal{G}^{P,Q}_{3}$ runs
$\mathit{Lt}\,(P\,n_{\\_}1\,\cdots\,n_{\\_}k)\,(Q\,n_{\\_}1\,\cdots\,n_{\\_}k)$
for each tuple of Church numerals $(n_{\\_}1,\ldots,n_{\\_}k)$ with non-zero
probability, $\mathcal{G}^{P,Q}_{3}$ is non-AST if and only if
$P(n_{\\_}1,\ldots,n_{\\_}k)<Q(n_{\\_}1,\ldots,n_{\\_}k)$ for _some_ natural
numbers $n_{\\_}1,\ldots,n_{\\_}k$. The key ingredient used for the
construction of $\mathit{Lt}$ is the function $\mathit{CheckHalf}$ of type
$(\mathtt{o}\to\mathtt{o}\to\mathtt{o})\to\mathtt{o}$, defined as follows:

$\mathit{CheckHalf}\;g=F^{\prime}\;g\;\mathtt{e}\qquad
F^{\prime}\;g\;x=g\;x\;(F^{\prime}\,g\,(F^{\prime}\,g\,x)).$

Here, $F^{\prime}$ above is a parameterized version of $F$ from Example 2.1:
$F^{\prime}\;\,\oplus_{p}\,$ (where $\,\oplus_{p}\,$ is treated as a function
of type $\mathtt{o}\to\mathtt{o}\to\mathtt{o}$, which chooses the first
argument with probability $p$ and the second one with $1-p$) corresponds to
$F$. As discussed in Example 2.1, $F\,\mathtt{e}$ is non-AST if and only if
$p<\frac{1}{2}$. Thus, $\mathit{CheckHalf}\;g=F^{\prime}\;g\;\mathtt{e}$
(which is equivalent to $F\,\mathtt{e}$ when $g=\,\oplus_{p}\,$) is non-AST if
and only if the probability that $g$ chooses the first argument is smaller
than $\frac{1}{2}$. Let $\mathit{CheckLt}$ (which will be defined shortly) be
a function which takes Church numerals $m_{\\_}1$ and $m_{\\_}2$, and returns
a function of type $\mathtt{o}\to\mathtt{o}\to\mathtt{o}$ that chooses the
first argument with probability smaller than $\frac{1}{2}$ if and only if
$m_{\\_}1<m_{\\_}2$. Then, $\mathit{Lt}$ can be defined as:

$\mathit{Lt}\;m_{\\_}1\;m_{\\_}2=\mathit{CheckHalf}(\mathit{CheckLt}\;m_{\\_}1\;m_{\\_}2).$

Finally, $\mathit{CheckLt}$ can be defined by:

$\displaystyle\mathit{CheckLt}\;m_{\\_}1\;m_{\\_}2\;x\;y=(\mathit{NatToPr}\;m_{\\_}1\;x\;y)\,\oplus_{\frac{1}{2}}\,(\mathit{NatToPr}\;m_{\\_}2\;y\;x).$
$\displaystyle\mathit{NatToPr}\;m\;x\;y=m\;(H\;x)\;y.\qquad
H\;x\;y=x\,\oplus_{\frac{1}{2}}\,y.$

Let us write $[m]$ for the natural number represented by a Church numeral $m$.
For a Church numeral $m$, $\mathit{NatToPr}\;m\;x\;y$ (which is equivalent to
$(H\,x)^{[m]}y$) chooses $x$ with probability $1-\frac{1}{2^{[m]}}$ and $y$
with probability $\frac{1}{2^{[m]}}$. Thus, the probability that
$\mathit{CheckLt}\;m_{\\_}1\;m_{\\_}2\;x\;y$ chooses $x$ is

$\frac{1}{2}\cdot\left(1-\frac{1}{2^{[m_{\\_}1]}}\right)+\frac{1}{2}\cdot\frac{1}{2^{[m_{\\_}2]}}=\frac{1}{2}+\frac{1}{2}\cdot\left(\frac{1}{2^{[m_{\\_}2]}}-\frac{1}{2^{[m_{\\_}1]}}\right),$

which is smaller than $\frac{1}{2}$ if and only if $[m_{\\_}1]<[m_{\\_}2]$, as
required. This completes the construction of $\mathcal{G}^{P,Q}_{3}$. See
Figure 2 for the whole rules of $\mathcal{G}^{P,Q}_{3}$. From the discussion
above, it should be trivial that $\mathcal{G}^{P,Q}_{3}$ is non-AST if and
only if $P(x_{\\_}1,\ldots,x_{\\_}k)<Q(x_{\\_}1,\ldots,x_{\\_}k)$ holds for
some $x_{\\_}1,\ldots,x_{\\_}k\in\mathbf{Nat}$.

$\displaystyle S$ $\displaystyle=\mathit{Loop}\;Zero\;\cdots\;Zero.$
$\displaystyle\mathit{Loop}\,x_{\\_}1\,\cdots\,x_{\\_}k$
$\displaystyle=(\mathit{Lt}\,(P\,x_{\\_}1\,\cdots\,x_{\\_}k)\,(Q\,x_{\\_}1\,\cdots\,x_{\\_}k))$
$\displaystyle\,\oplus_{\frac{1}{2}}\,(TestAll\,(\mathit{Succ}\,x_{\\_}1)\,\cdots\,x_{\\_}k)\,\oplus_{\frac{1}{2}}\,\cdots\,\oplus_{\frac{1}{2}}\,(TestAll\,x_{\\_}1\,\cdots\,(\mathit{Succ}\,x_{\\_}k)).$
$\displaystyle\mathit{Lt}\;m_{\\_}1\;m_{\\_}2$
$\displaystyle=\mathit{CheckHalf}(\mathit{CheckLt}\;m_{\\_}1\;m_{\\_}2).$
$\displaystyle\mathit{CheckHalf}\;y$
$\displaystyle=F^{\prime}\;y\;\mathtt{e}.$ $\displaystyle F^{\prime}\;g\;x$
$\displaystyle=g\;x\;(F^{\prime}\,g\,(F^{\prime}\,g\,x)).$
$\displaystyle\mathit{CheckLt}\;m_{\\_}1\;m_{\\_}2\;x\;y$
$\displaystyle=(\mathit{NatToPr}\;m_{\\_}1\;x\;y)\,\oplus_{\frac{1}{2}}\,(\mathit{NatToPr}\;m_{\\_}2\;y\;x).$
$\displaystyle\mathit{NatToPr}\;m\;x\;y$ $\displaystyle=m\;(H\;x)\;y.$
$\displaystyle H\;x\;y$ $\displaystyle=x\,\oplus_{\frac{1}{2}}\,y.$
$\displaystyle Zero\,s\,z$ $\displaystyle=z.$
$\displaystyle\mathit{Succ}\,n\,s\,z$ $\displaystyle=s\,(n\,s\,z).$
$\displaystyle\mathit{Add}\,n\,m\,s\,z$ $\displaystyle=n\,s\,(m\,s\,z).$
$\displaystyle\mathit{Mult}\,n\,m\,s\,z$ $\displaystyle=n\,(m\,s)\,z.$
$\displaystyle P\,x_{\\_}1\,\cdots\,x_{\\_}k$ $\displaystyle=t_{\\_}P.$
$\displaystyle Q\,x_{\\_}1\,\cdots\,x_{\\_}k$ $\displaystyle=t_{\\_}Q.$

Figure 2. The rules of $\mathcal{G}^{P,Q}_{3}$, where $t_{\\_}P$ and
$t_{\\_}Q$ are terms encoding the polynomials $P$ and $Q$ by way of $Zero$,
$\mathit{Succ}$, $\mathit{Add}$, and $\mathit{Mult}$.

###  3.2. Decreasing the Order

We now refine the construction of $\mathcal{G}^{P,Q}_{3}$ to obtain an order-2
PHORS $\mathcal{G}^{P,Q}_{2}$ that satisfies the same property. The idea is,
instead of passing around a Church numeral $m$, to pass a probabilistic
function equivalent to $\mathit{NatToPr}\,m$, which takes two arguments and
chooses the first and second arguments with probabilities
$1-\frac{1}{2^{[m]}}$ and $\frac{1}{2^{[m]}}$, respectively. Note that a
Church numeral $m$ has an order-2 type
$\mathsf{CT}=(\mathtt{o}\to\mathtt{o})\to\mathtt{o}\to\mathtt{o}$, whereas
$\mathit{NatToPr}\,m$ has an order-1 type
$\mathtt{o}\to\mathtt{o}\to\mathtt{o}$. This ultimately allows us to decrease
the order of the PHORS.

Based on the idea above, we replace $\mathit{Lt}$ with $\mathit{LtPr}$, which
now takes probabilistic functions of type
$\mathtt{o}\to\mathtt{o}\to\mathtt{o}$ as arguments:

$\displaystyle\mathit{LtPr}\;g_{\\_}1\;g_{\\_}2$
$\displaystyle=\mathit{CheckHalf}(\mathit{CheckLtPr}\;g_{\\_}1\;g_{\\_}2).$
$\displaystyle\mathit{CheckLtPr}\;g_{\\_}1\;g_{\\_}2\;x\;y$
$\displaystyle=(g_{\\_}1\;x\;y)\,\oplus_{\frac{1}{2}}\,(g_{\\_}2\;y\;x).$

Here, $\mathit{CheckLtPr}$ is an analogous version of $\mathit{CheckLt}$, and
$\mathit{CheckHalf}$ is as before: $\mathit{CheckHalf}\;g$ is non-AST if and
only if the probability that $g$ chooses the first argument is smaller than
$\frac{1}{2}$. Then,
$\mathit{LtPr}\;(\mathit{NatToPr}\;(P\,n_{\\_}1\,\cdots\,n_{\\_}k))\;(\mathit{NatToPr}\;(Q\,n_{\\_}1\,\cdots\,n_{\\_}k))$
is non-AST if and only if
$P(n_{\\_}1,\ldots,n_{\\_}k)<Q(n_{\\_}1,\ldots,n_{\\_}k)$.

It remains to modify the top-level loop $\mathit{Loop}$, so that we can
enumerate (terms equivalent to)
$\mathit{LtPr}\;(\mathit{NatToPr}\;(P\,n_{\\_}1\,\cdots\,n_{\\_}k))\;(\mathit{NatToPr}\;(Q\,n_{\\_}1\,\cdots\,n_{\\_}k))$
for all $n_{\\_}1,\ldots,n_{\\_}k\in\mathbf{Nat}$, without explicitly
constructing Church numerals. Instead of using Church encodings, we can encode
natural numbers and operations on them (except multiplication) into
probabilistic functions as follows.

$\displaystyle\mathit{ZeroPr}\;x\;y$ $\displaystyle=y$
$\displaystyle\mathit{SuccPr}\;g\;x\;y$
$\displaystyle=x\,\oplus_{\frac{1}{2}}\,(g\;x\;y)$
$\displaystyle\mathit{OnePr}\;x\;y$ $\displaystyle=x\,\oplus_{\frac{1}{2}}\,y$
$\displaystyle\mathit{AddPr}\;g_{\\_}1\;g_{\\_}2\;x\;y$
$\displaystyle=g_{\\_}1\;x\;(g_{\\_}2\;x\;y).$

Basically, a natural number $m$ is encoded as a probabilistic function of type
$\mathtt{o}\to\mathtt{o}\to\mathtt{o}$, which chooses the first and second
arguments with probabilities $1-\frac{1}{2^{m}}$ and $\frac{1}{2^{m}}$
respectively. Notice that
$\mathit{AddPr}\;(\mathit{NatToPr}\;m_{\\_}1)\;(\mathit{NatToPr}\;m_{\\_}2)$
is equivalent to $\mathit{NatToPr}\;(\mathit{Add}\;m_{\\_}1\;m_{\\_}2)$,
because the probability that
$\mathit{AddPr}\;(\mathit{NatToPr}\;m_{\\_}1)\;(\mathit{NatToPr}\;m_{\\_}2)\;x\;y$
chooses $y$ is
$\frac{1}{2^{[m_{\\_}1]}}\cdot\frac{1}{2^{[m_{\\_}2]}}=\frac{1}{2^{[m_{\\_}1]+[m_{\\_}2]}}$.
We call this encoding the _probabilistic function encoding_ , or _PF encoding_
for short.

The multiplication cannot, however, be directly encoded. To compensate for the
lack of the multiplication operator, instead of passing around just
$n_{\\_}1,\ldots,n_{\\_}k$ in the top-level loop, we pass around the PF
encodings of the values of $n_{\\_}1^{i_{\\_}1}\cdots n_{\\_}k^{i_{\\_}k}$ for
each $i_{\\_}1\leq d_{\\_}1,\ldots,i_{\\_}k\leq d_{\\_}k$, where
$d_{\\_}1,\ldots,d_{\\_}k$ respectively are the largest degrees of
$P(x_{\\_}1,\ldots,x_{\\_}k)+Q(x_{\\_}1,\ldots,x_{\\_}k)$ in
$x_{\\_}1,\ldots,x_{\\_}k$. We thus define the start symbol $S$ of
$\mathcal{G}^{P,Q}_{2}$ by:

$\displaystyle S$
$\displaystyle=\mathit{LoopPr}\;\mathit{OnePr}\;\underbrace{\mathit{ZeroPr}\,\cdots\,\mathit{ZeroPr}}_{\\_}{(d_{\\_}1+1)\cdots(d_{\\_}k+1)-1\mbox{
times}}.$ $\displaystyle\mathit{LoopPr}\;\widetilde{x}$
$\displaystyle=(\mathit{LtPr}\;(P^{\prime}\;\widetilde{x})\;\;(Q^{\prime}\;\widetilde{x}))$
$\displaystyle\,\oplus_{\frac{1}{2}}\,(\mathit{LoopPr}\,(\mathit{Inc}_{\\_}{1,(0,\ldots,0)}\,\widetilde{x})\,\cdots\,(\mathit{Inc}_{\\_}{1,(d_{\\_}1,\ldots,d_{\\_}k)}\,\widetilde{x}))\,\oplus_{\frac{1}{2}}\,\cdots$
$\displaystyle\,\oplus_{\frac{1}{2}}\,(\mathit{LoopPr}\,(\mathit{Inc}_{\\_}{k,(0,\ldots,0)}\,\widetilde{x})\,\cdots\,(\mathit{Inc}_{\\_}{k,(d_{\\_}1,\ldots,d_{\\_}k)}\,\widetilde{x})).$

Here, $\widetilde{x}$ denotes the sequence of $(d_{\\_}1+1)\cdots(d_{\\_}k+1)$
variables $x_{\\_}{(0,\ldots,0)},\ldots,x_{\\_}{(d_{\\_}1,\ldots,d_{\\_}k)}$,
consisting of $x_{\\_}{(i_{\\_}1,\ldots,i_{\\_}k)}$ for each
$i_{\\_}1\in\\{0,\ldots,d_{\\_}1\\},\ldots,i_{\\_}k\in\\{0,\ldots,d_{\\_}k\\}$.
Each variable $x_{\\_}{(i_{\\_}1,\ldots,i_{\\_}k)}$ holds (the PF encoding of)
the value of $n_{\\_}1^{i_{\\_}1}\cdots n_{\\_}k^{i_{\\_}k}$.

Moreover, the functions $P^{\prime}$ and $Q^{\prime}$ are the PF encodings of
the polynomials $P$ and $Q$. Since $P$ and $Q$ can be represented as linear
combinations of monomials $x_{\\_}1^{i_{\\_}1}\cdots x_{\\_}k^{i_{\\_}k}$ for
$i_{\\_}1\leq d_{\\_}1,\ldots,i_{\\_}k\leq d_{\\_}k$, $P^{\prime}$ and
$Q^{\prime}$ can be defined using $\mathit{ZeroPr}$ and $\mathit{AddPr}$. For
example, if $P(x_{\\_}1,x_{\\_}2)=x_{\\_}1^{2}+2x_{\\_}1x_{\\_}2$, then
$P^{\prime}$ is defined by:
$P^{\prime}\;\widetilde{x}\;y\;z=\mathit{AddPr}\;x_{\\_}{(2,0)}\;(\mathit{AddPr}\;x_{\\_}{(1,1)}\;x_{\\_}{(1,1)})\;y\;z$.

The function $\mathit{Inc}_{\\_}{j,(i_{\\_}1,\ldots,i_{\\_}k)}\,\widetilde{x}$
represents the PF encoding of
$n_{\\_}1^{i_{\\_}1}\cdots(n_{\\_}j+1)^{i_{\\_}j}\cdots n_{\\_}k^{i_{\\_}k}$,
assuming that $\widetilde{x}$ represents (the PF encoding of) the values
$n_{\\_}1^{0}\cdots n_{\\_}k^{0},\ldots,n_{\\_}1^{d_{\\_}1}\cdots
n_{\\_}k^{d_{\\_}k}$. Note that
$\mathit{Inc}_{\\_}{j,(i_{\\_}1,\ldots,i_{\\_}k)}$ can also be defined by
using $\mathit{ZeroPr}$ and $\mathit{AddPr}$, since
$x_{\\_}1^{i_{\\_}1}\cdots(x_{\\_}j+1)^{i_{\\_}j}\cdots x_{\\_}k^{i_{\\_}k}$
can be expressed as a linear combination of monomials $x_{\\_}1^{0}\cdots
x_{\\_}k^{0},\ldots,x_{\\_}1^{d_{\\_}1}\cdots x_{\\_}k^{d_{\\_}k}$. For
example, if $k=2$, then $\mathit{Inc}_{\\_}{2,(1,2)}$ can be defined by
$\mathit{Inc}_{\\_}{2,(1,2)}\,\widetilde{x}\,y\,z=\mathit{AddPr}\;x_{\\_}{(1,2)}\;(\mathit{AddPr}\;x_{\\_}{(1,1)}\;(\mathit{AddPr}\;x_{\\_}{(1,1)}\;x_{\\_}{(1,0)}))\,y\,z$,
because
$x_{\\_}1(x_{\\_}2+1)^{2}=x_{\\_}1x_{\\_}2^{2}+2x_{\\_}1x_{\\_}2+x_{\\_}1$. ∎

This completes the construction of $\mathcal{G}^{P,Q}_{2}$. See Figure 3 for
the list of all rules of $\mathcal{G}^{P,Q}_{2}$.

$\displaystyle S$
$\displaystyle=\mathit{LoopPr}\;\mathit{OnePr}\;\underbrace{\mathit{ZeroPr}\,\cdots\,\mathit{ZeroPr}}_{\\_}{(d_{\\_}1+1)\cdots(d_{\\_}k+1)-1}.$
$\displaystyle\mathit{LoopPr}\;\widetilde{x}$
$\displaystyle=(\mathit{LtPr}\;(P^{\prime}\;\widetilde{x})\;\;(Q^{\prime}\;\widetilde{x}))$
$\displaystyle\,\oplus_{\frac{1}{2}}\,(\mathit{LoopPr}\,(\mathit{Inc}_{\\_}{1,(0,\ldots,0)}\,\widetilde{x})\,\cdots\,(\mathit{Inc}_{\\_}{1,(d_{\\_}1,\ldots,d_{\\_}k)}\,\widetilde{x}))$
$\displaystyle\,\oplus_{\frac{1}{2}}\,\cdots\,\oplus_{\frac{1}{2}}\,(\mathit{LoopPr}\,(\mathit{Inc}_{\\_}{k,(0,\ldots,0)}\,\widetilde{x})\,\cdots\,(\mathit{Inc}_{\\_}{k,(d_{\\_}1,\ldots,d_{\\_}k)}\,\widetilde{x})).$
$\displaystyle\mathit{LtPr}\;g_{\\_}1\;g_{\\_}2$
$\displaystyle=\mathit{CheckHalf}(\mathit{CheckLtPr}\;g_{\\_}1\;g_{\\_}2).$
$\displaystyle\mathit{CheckLtPr}\;g_{\\_}1\;g_{\\_}2\;x\;y$
$\displaystyle=(g_{\\_}1\;x\;y)\,\oplus_{\frac{1}{2}}\,(g_{\\_}2\;y\;x).$
$\displaystyle\mathit{CheckHalf}\;y$
$\displaystyle=F^{\prime}\;y\;\mathtt{e}.$ $\displaystyle F^{\prime}\;g\;x$
$\displaystyle=g\;x\;(F^{\prime}\,g\,(F^{\prime}\,g\,x)).$
$\displaystyle\mathit{ZeroPr}\;x\;y$ $\displaystyle=y.$
$\displaystyle\mathit{OnePr}\;x\;y$
$\displaystyle=x\,\oplus_{\frac{1}{2}}\,y.$
$\displaystyle\mathit{SuccPr}\;g\;x\;y$
$\displaystyle=x\,\oplus_{\frac{1}{2}}\,(g\;x\;y).$
$\displaystyle\mathit{AddPr}\;g_{\\_}1\;g_{\\_}2\;x\;y$
$\displaystyle=g_{\\_}1\;x\;(g_{\\_}2\;x\;y).$ $\displaystyle
P^{\prime}\,\widetilde{x}$ $\displaystyle=t^{\prime}_{\\_}P$ $\displaystyle
Q^{\prime}\,\widetilde{x}$ $\displaystyle=t^{\prime}_{\\_}Q$
$\displaystyle\mathit{Inc}_{\\_}{j,(i_{\\_}1,\ldots,i_{\\_}k)}$
$\displaystyle=t_{\\_}\mathit{Inc}^{j(i_{\\_}1,\ldots,i_{\\_}k)}$

Figure 3. The rules of $\mathcal{G}^{P,Q}_{2}$, where the terms
$t^{\prime}_{\\_}P$, $t^{\prime}_{\\_}Q$ and
$t_{\\_}\mathit{Inc}^{j,(i_{\\_}1,\ldots,i_{\\_}k)}$ are defined based on
$\mathit{ZeroPr}$, $\mathit{OnePr}$, and $\mathit{SuccPr}$ and
$\mathit{AddPr}$.

By the discussion above, we have:

######  Theorem 3.2.

The almost sure termination of order-2 PHORS is undecidable. More precisely,
the set $\\{\mathcal{G}\mid\mathcal{P}(\mathcal{G})=1,\mbox{$\mathcal{G}$ is
an order-2 PHORS{}}\\}$ is $\Pi^{0}_{\\_}1$-hard.

######  Proof 3.3.

By the construction of $\mathcal{G}^{P,Q}_{2}$ above,
$\mathcal{P}(\mathcal{G}^{P,Q}_{2})=1$ if and only if
$P(x_{\\_}1,\ldots,x_{\\_}k)\geq Q(x_{\\_}1,\ldots,x_{\\_}k)$ holds for all
$x_{\\_}1,\ldots,x_{\\_}k\in\mathbf{Nat}$. By Lemma 3.1, the set of pairs
$(P,Q)$ that satisfy the latter is $\Pi^{0}_{\\_}1$-complete, hence the set
$\\{\mathcal{G}\mid\mathcal{P}(\mathcal{G})=1,\mbox{$\mathcal{G}$ is an
order-2 PHORS{}}\\}$ is $\Pi^{0}_{\\_}1$-hard.

As a corollary, we also have:

######  Theorem 3.3.

For any rational number $r\in(0,1]$, the followings are undecidable:

  1. (1)

whether a given order-2 PHORS $\mathcal{G}$ satisfies
$\Pr(\mathcal{G}){\geq}r$.

  2. (2)

whether a given order-2 PHORS $\mathcal{G}$ satisfies $\Pr(\mathcal{G}){=}r$.

More precisely, the sets
$\\{\mathcal{G}\in\mathcal{P}_{\\_}2\mid\Pr(\mathcal{G}){\geq}r\\}$ and
$\\{\mathcal{G}\in\mathcal{P}_{\\_}2\mid\Pr(\mathcal{G}){=}r\\}$ are
$\Pi^{0}_{\\_}1$-hard.

######  Proof 3.4.

Let $\mathcal{G}$ be an order-2 PHORS with the start symbol $S$. Define
$\mathcal{G}^{\prime}$ as the PHORS obtained by replacing the start symbol
with $S^{\prime}$ and adding the rules $S^{\prime}=S\,\oplus_{r}\,\Omega$.
Then $\Pr(\mathcal{G}^{\prime})\geq r$ if and only if
$\Pr(\mathcal{G}^{\prime})=r$ if and only if $\Pr(\mathcal{G})=1$. Thus, the
result follows from Theorem 2.

######  Remark 3.5.

Let us write $\Psi_{\\_}{\sim r}$ for the set of order-2 PHORS $\mathcal{G}$
such that $\Pr(\mathcal{G})\sim r$ where
$\mathord{\sim}\in\\{<,\leq,=,\geq,>\\}$. By Theorem 1 and Theorem 2, we have:

  1. (1)

For any rational number $r\in[0,1]$, $\Psi_{\\_}{>r}$ is recursively
enumerable (or, belongs to $\Sigma^{0}_{\\_}1$).

  2. (2)

For any rational number $r\in(0,1]$, $\Psi_{\\_}{\geq r}$ is
$\Pi^{0}_{\\_}1$-hard (whereas $\Psi_{\\_}{\geq 0}$ is obviously recursive).

  3. (3)

For any rational number $r\in(0,1]$, $\Psi_{\\_}{=r}$ is $\Pi^{0}_{\\_}1$-hard
(whereas $\Psi_{\\_}{=0}$ is recursive; recall Remark 2.4).

It is open whether the following propositions hold or not.

  1. (4)

$\Psi_{\\_}{<r}$ is recursively enumerable for every rational number $r$.

  2. (5)

$\Psi_{\\_}{\leq r}$ is recursively enumerable for every rational number $r$.

  3. (6)

There exists an algorithm that takes an order-2 PHORS $\mathcal{G}$ and a
rational number $\epsilon>0$ as inputs, and returns a rational number $r$ such
that $|\Pr(\mathcal{G})-r|<\epsilon$.

Statements (iv) and (vi) are equivalent. In fact, if (iv) is true, we can
construct an algorithm for (vi) as follows. First, test whether
$\Pr(\mathcal{G})=0$ (which is decidable). If so, output $r=0$. Otherwise,
pick a natural number $m$ such that $\frac{1}{m}<\frac{1}{2}\epsilon$, and
divide the interval $(0,1+\frac{1}{2}\epsilon)$ to $m$ (overlapping) intervals

$\begin{array}[]{l}\left(0,\frac{1}{m}+\frac{1}{2}\epsilon\right),\left(\frac{1}{m},\frac{2}{m}+\frac{1}{2}\epsilon\right),\ldots,\left(\frac{m-2}{m},\frac{m-1}{m}+\frac{1}{2}\epsilon\right),\left(\frac{m-1}{m},1+\frac{1}{2}\epsilon\right).\end{array}$

By using procedures for (i) and (iv), one can enumerate all the order-2 PHORS
whose termination probabilities belong to each interval. Thus, $\mathcal{G}$
is eventually enumerated for one of the intervals
$(\frac{i}{m},\frac{i+1}{m}+\frac{1}{2}\epsilon)$; one can then output
$\frac{i}{m}$ as $r$. Conversely, suppose that we have an algorithm for (vi).
For each order-2 PHORS $\mathcal{G}$, repeatedly run the algorithm for
$\epsilon=\frac{1}{2},\frac{1}{4},\frac{1}{8},\ldots$, and output
$\mathcal{G}$ if the output $r^{\prime}$ for $(\mathcal{G},\epsilon)$
satisfies $r^{\prime}+\epsilon<r$. Then, $\mathcal{G}$ is eventually output
just if $\Pr(\mathcal{G})<r$ (note that if $\Pr(\mathcal{G})<r$, then
$\epsilon$ eventually becomes smaller than $\frac{1}{2}(r-\Pr(\mathcal{G}))$;
at that point, the output $r^{\prime}$ satisfies
$r^{\prime}+\epsilon<(\Pr(\mathcal{G})+\epsilon)+\epsilon<r$).

Proposition (v) implies (iv) (and hence also (vi)). If there is a procedure
for (v), one can enumerate all the elements of $\Psi_{\\_}{<r}$ by running the
procedure for enumerating $\Psi_{\\_}{\leq r-\epsilon}$ for
$\epsilon=\frac{1}{2},\frac{1}{4},\frac{1}{8},\ldots$ ∎

######  Remark 3.6.

Table 1 summarizes the hardness of termination problems in terms of the
arithmetical hierarchy for recursive Markov chains (RMC), PHORS, and a
probabilistic language whose underlying (non-probabilistic) language is
Turing-complete. The results for RMC and the Turing-complete language come
from [EY09] and [MMKK18]. As seen in the table, the results on PHORS are not
tight, except for the problem $\mathcal{P}(\mathcal{G})>0$. Since the
expressive power of PHORS is between those of RMC and the Turing complete
language, the hardness of each problem is between those of the two models.
Theorem 3 shows $\Sigma^{0}_{\\_}1$-hardness of $\mathcal{P}(\mathcal{G})<r$,
but we do not know yet whether the problem is $\Sigma^{0}_{\\_}1$-complete or
$\Sigma^{0}_{\\_}2$-complete, or lies between the two classes.

Table 1. Hardness of the termination problems in terms of the arithmetical hierarchy. For recursive sets (i.e. those in $\Delta^{0}_{\\_}1=\Sigma^{0}_{\\_}1\cap\Pi^{0}_{\\_}1$), more precise computational complexities of the membership problems are given. “PHORS” means order-$k$ PHORS where $k\geq 2$. Models | $\Psi_{\\_}{>0}$ |  $\Psi_{\\_}{>r}$ ($r\in(0,1)$) |  $\Psi_{\\_}{<r}$ ($r\in(0,1]$)
---|---|---|---
RMC | P | PSPACE | PSPACE
PHORS | Hardness |  $(k-1)$-EXPTIME |  $(k-1)$-EXPTIME | $\Sigma^{0}_{\\_}1$
| Containment |  $(k-1)$-EXPTIME | $\Sigma^{0}_{\\_}1$ | $\Sigma^{0}_{\\_}2$
Turing-complete language |  $\Sigma^{0}_{\\_}1$-complete |  $\Sigma^{0}_{\\_}1$-complete |  $\Sigma^{0}_{\\_}2$-complete

######  Remark 3.7.

Theorem 2 implies that, in contrast to the decidability of LTL model checking
of recursive Markov chains [BEKK13, EY12], the corresponding problem for
order-2 PHORS (of computing the probability that an infinite transition
sequence satisfies a given LTL property) is undecidable and there are even no
precise approximation algorithms. Let us extend terms with events:

$t::=\cdots\;\;\mbox{\Large{$\mid$}}\;\;\mathtt{event}\ a;t$

where $\mathtt{event}\ a;{t}$ raises an event $a$ and evaluates $t$. Consider
the problem of, given an order-2 PHORS $\mathcal{G}$, computing the
probability $\mathcal{P}_{\\_}{a^{\omega}}(\mathcal{G})$ that $a$ occurs
infinitely often. Then there is no algorithm to compute
$\mathcal{P}_{\\_}{a^{\omega}}(\mathcal{G})$ with arbitrary precision, in the
sense of (vi) of Remark 3.5. To see this, notice that by parametric
$\mathcal{G}^{P,Q}_{2}$ with $\mathtt{e}$, we can define a nonterminal
$F\mathbin{:}\mathtt{o}\to\mathtt{o}$ such that $F\;x$ almost surely reduces
to $x$ if and only if there exist no $n_{\\_}1,\ldots,n_{\\_}k$ such that
$P(n_{\\_}1,\ldots,n_{\\_}k)<Q(n_{\\_}1,\ldots,n_{\\_}k)$. Consider the
(extended) PHORS $\mathcal{G}^{P,Q,a^{\omega}}$ whose start symbol $S$ is
defined by $S=\mathtt{event}\ a;{F(S)}$. Then

$\mathcal{P}_{\\_}{a^{\omega}}(\mathcal{G}^{P,Q,a^{\omega}})=\left\\{\begin{array}[]{ll}0&\mbox{if
there exists $n_{\\_}1,\ldots,n_{\\_}k$}\mbox{ such that
$P(n_{\\_}1,\ldots,n_{\\_}k)<Q(n_{\\_}1,\ldots,n_{\\_}k)$}\\\
1&\mbox{otherwise}.\end{array}\right.$

Thus, there is no algorithm to approximately compute
$\mathcal{P}_{\\_}{a^{\omega}}(\mathcal{G})$ even within the precision of
$\epsilon=\frac{1}{2}$. ∎

######  Remark 3.8.

The PHORS $\mathcal{G}^{P,Q}_{2}$ obtained above satisfies the so called
“safety” restriction [KNU01, KS15]. Thus, based on the correspondence between
safe grammars and pushdown systems [KNU01], the undecidability result above
would also hold for probabilistic second-order pushdown systems (without
collapse operations [HMOS08]).

##  4\. Fixpoint Characterization of Termination Probability

Although, as observed in the previous section, there is no general algorithm
for exactly computing the termination probability of PHORS, there is still
hope that we can _approximately_ compute the termination probability. As a
possible route towards this goal, this section shows that the termination
probability of any PHORS $\mathcal{G}$ can be characterized as the least
solution of fixpoint equations on higher-order functions over $[0,1]$. As
mentioned in Section 1, the fixpoint characterization immediately yields a
procedure for computing lower-bounds of termination probabilities, and also
serves as a justification for the method for computing upper-bounds discussed
in Section 5. We first introduce higher-order fixpoint equations in Section
4.1. We then characterize the termination probability of an order-$n$ PHORS in
terms of fixpoint equations on order-$n$ functions over $[0,1]$ (Section 4.2),
and then improve the result by characterizing the same probability in terms of
order-($n-1$) fixpoint equations for the case $n\geq 1$ (Section 4.3). The
latter characterization can be seen as a generalization of the
characterization of termination probabilities of recursive Markov chains as
polynomial equations [EY09], which served as a key step in the analysis of
recursive Markov chains (or probabilistic pushdown systems) [EY09, EY15,
BEKK13, BBFK14].

###  4.1. Higher-order Fixpoint Equations

We define the syntax and semantics of fixpoint equations that are commonly
used in Sections 4.2 and 4.3. We first define the syntax of fixpoint
equations.

$\begin{array}[]{l}\mathcal{E}\mbox{
(equations)}::=\\{f_{\\_}1\,(\widetilde{x}_{\\_}{1,1})\,\cdots\,(\widetilde{x}_{\\_}{1,\ell_{\\_}1})=e_{\\_}1,\ldots,f_{\\_}m\,(\widetilde{x}_{\\_}{m,1})\,\cdots\,(\widetilde{x}_{\\_}{m,\ell_{\\_}m})=e_{\\_}m\\};\\\
e\mbox{
(expressions)}::=r\;\;\mbox{\Large{$\mid$}}\;\;x\;\;\mbox{\Large{$\mid$}}\;\;f\;\;\mbox{\Large{$\mid$}}\;\;e_{\\_}1+e_{\\_}2\;\;\mbox{\Large{$\mid$}}\;\;e_{\\_}1\cdot
e_{\\_}2\;\;\mbox{\Large{$\mid$}}\;\;e_{\\_}1e_{\\_}2\mid(e_{\\_}1,\ldots,e_{\\_}k).\end{array}$

Here, $r$ ranges over the set of real numbers in $[0,1]$, and
$(\widetilde{x})$ represents a tuple of variables
$(x_{\\_}1,\ldots,x_{\\_}k)$. In the set $\mathcal{E}$ of equations, we
require that each function symbol occurs at most once on the lefthand side.
The expression $e_{\\_}1\cdot e_{\\_}2$ represents the multiplication of the
values of $e_{\\_}1$ and $e_{\\_}2$, whereas $e_{\\_}1e_{\\_}2$ represents a
function application; however, we sometimes omit $\cdot$ when there is no
confusion (e.g., we write $0.5x$ for $0.5\cdot x$). Expressions must be well-
typed under the type system given in Figure 4. The _order of a system of
fixpoint equations_ $\mathcal{E}$ is the largest order of the types of
functions in $\mathcal{E}$, where the order of the type $\mathtt{R}$ of reals
is $0$, and the order of a function type is defined analogously to the order
of types for PHORS in Section 2.

######  Example 4.1.

The following is a system of order-2 fixpoint equations:

$\begin{array}[]{c}\\{f_{\\_}1=f_{\\_}2\;f_{\\_}3\;(0.5,0.5),f_{\\_}2\;g\;(x_{\\_}1,x_{\\_}2)=g(x_{\\_}1+x_{\\_}2),f_{\\_}3\,x=0.3\,x+0.7f_{\\_}3(f_{\\_}3\,x)\\}.\end{array}$

It is well-typed under
$f_{\\_}1\mathbin{:}\mathtt{R},f_{\\_}2\mathbin{:}(\mathtt{R}\to\mathtt{R})\to(\mathtt{R}\times\mathtt{R})\to\mathtt{R},f_{\\_}3\mathbin{:}\mathtt{R}\to\mathtt{R}$.
∎

$\tau\mbox{
(types)}::=\mathtt{R}\mid\tau_{\\_}1\to\tau_{\\_}2\mid\tau_{\\_}1\times\cdots\times\tau_{\\_}n.$
$\Gamma\vdash r:\mathtt{R}r\in\mathbf{R}\qquad\qquad\Gamma\vdash
e_{\\_}1+e_{\\_}2:\mathtt{R}\Gamma\vdash
e_{\\_}1:\mathtt{R}\quad\quad\Gamma\vdash
e_{\\_}2:\mathtt{R}\qquad\qquad\Gamma\vdash e_{\\_}1\cdot
e_{\\_}2:\mathtt{R}\Gamma\vdash e_{\\_}1:\mathtt{R}\quad\quad\Gamma\vdash
e_{\\_}2:\mathtt{R}$ $\Gamma\vdash
x\mathbin{:}\tau\Gamma(x)=\tau\qquad\quad\Gamma\vdash
e_{\\_}1e_{\\_}2:\tau\Gamma\vdash
e_{\\_}1:\tau_{\\_}2\to\tau\quad\quad\Gamma\vdash
e_{\\_}2:\tau_{\\_}2\qquad\quad\Gamma\vdash(e_{\\_}1,\ldots,e_{\\_}k):\tau_{\\_}1\times\cdots\times\tau_{\\_}k\Gamma\vdash
e_{\\_}i:\tau_{\\_}i\mbox{ for each $i\in\\{1,\ldots,k\\}$}$
$\Gamma\vdash\\{f_{\\_}i\,(\widetilde{x}_{\\_}{i,1})\,\cdots\,(\widetilde{x}_{\\_}{i,\ell_{\\_}i})=e_{\\_}i\mid
i\in\\{1,\ldots,m\\}\\}\lx@proof@logical@and\Gamma,(\widetilde{x}_{\\_}{i,1})\mathbin{:}\tau_{\\_}{i,1},\ldots,(\widetilde{x}_{\\_}{i,\ell_{\\_}i})\mathbin{:}\tau_{\\_}{i,\ell_{\\_}ii}\vdash
e_{\\_}i\Gamma(f_{\\_}i)=\tau_{\\_}{i,1}\to\cdots\to\tau_{\\_}{i,\ell_{\\_}i}\to\mathtt{R}\mbox{
(for each $i\in\\{1,\ldots,m\\}$)}$

Figure 4. Type system for fixpoint equations, where
$(x_{\\_}1,\ldots,x_{\\_}k)\mathbin{:}\tau$ denotes
$x_{\\_}1\mathbin{:}\tau_{\\_}1,\ldots,x_{\\_}k\mathbin{:}\tau_{\\_}k$
whenever $\tau=\tau_{\\_}1\times\cdots\times\tau_{\\_}k$.

The semantics of fixpoint equations is defined in an obvious manner. Let
$\mathbf{R}_{\infty}$ be the set consisting of non-negative real numbers and
$\infty$. We extend addition and multiplication by:
$x+\infty=\infty+x=\infty$, $0\cdot\infty=\infty\cdot 0=0$, and
$x\cdot\infty=\infty\cdot x=\infty$ if $x\neq 0$. Note that
$(\mathbf{R}_{\infty},\leq,0)$ forms an $\omega$-cpo, where $\leq$ is the
extension of the usual inequality on reals with $x\leq\infty$ for every
$x\in\mathbf{R}_{\infty}$. For each type $\tau$, we interpret $\tau$ as the
cpo
$\llbracket{\tau}\rrbracket=(X_{\\_}\tau,\sqsubseteq_{\\_}\tau,\bot_{\\_}\tau)$,
defined by induction on $\tau$:

$\displaystyle X_{\\_}\mathtt{R}$ $\displaystyle=\mathbf{R}_{\infty}$
$\displaystyle\sqsubseteq_{\\_}\mathtt{R}$ $\displaystyle=\mathord{\leq}$
$\displaystyle\bot_{\\_}\mathtt{R}$ $\displaystyle=0$ $\displaystyle
X_{\\_}{\tau_{\\_}1\to\tau_{\\_}2}$ $\displaystyle=\\{f\in
X_{\\_}{\tau_{\\_}1}\to X_{\\_}{\tau_{\\_}2}\mid\mbox{ $f$ is monotonic and
$\omega$-continuous}\\}$
$\displaystyle\sqsubseteq_{\\_}{\tau_{\\_}1\to\tau_{\\_}2}$
$\displaystyle=\\{(f_{\\_}1,f_{\\_}2)\in
X_{\\_}{\tau_{\\_}1\to\tau_{\\_}2}\times
X_{\\_}{\tau_{\\_}1\to\tau_{\\_}2}\mid\forall x\in
X_{\\_}{\tau_{\\_}1}.f_{\\_}1(x)\sqsubseteq_{\\_}{\tau_{\\_}2}f_{\\_}2(x)\\}$
$\displaystyle\ \bot_{\\_}{\tau_{\\_}1\to\tau_{\\_}2}$
$\displaystyle=\mathop{\hbox to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}x\in
X_{\\_}{\tau_{\\_}1}.\bot_{\\_}{\tau_{\\_}2}$ $\displaystyle
X_{\\_}{\tau_{\\_}1\times\cdots\times\tau_{\\_}k}$
$\displaystyle=X_{\\_}{\tau_{\\_}1}\times\cdots\times X_{\\_}{\tau_{\\_}k}$
$\displaystyle\sqsubseteq_{\\_}{\tau_{\\_}1\times\cdots\times\tau_{\\_}k}$
$\displaystyle=\\{((x_{\\_}1,\ldots,x_{\\_}k),(y_{\\_}1,\ldots,y_{\\_}k))\mid
x_{\\_}i\sqsubseteq_{\\_}{\tau_{\\_}i}y_{\\_}i\mbox{ for each
$i\in\\{1,\ldots,k\\}$}\\}$
$\displaystyle\bot_{\\_}{\tau_{\\_}1\times\cdots\times\tau_{\\_}k}$
$\displaystyle=(\bot_{\\_}{\tau_{\\_}1},\ldots,\bot_{\\_}{\tau_{\\_}k}).$

By abuse of notation, we often write $\llbracket{\tau}\rrbracket$ also for
$X_{\\_}\tau$. We also often omit the subscript $\tau$ and just write
$\sqsubseteq$ and $\bot$ for $\sqsubseteq_{\\_}\tau$ and $\bot_{\\_}\tau$
respectively. The interpretation of base type $\mathtt{R}$ can actually be
restricted to $[0,1]$, but for technical convenience (to make the existence of
a fixpoint trivial) we have defined $X_{\\_}{\mathtt{R}}$ as
$\mathbf{R}_{\infty}$.

For a type environment $\Gamma$, we write $\llbracket{\Gamma}\rrbracket$ for
the set of functions that map each $x\in\mathit{dom}(\Gamma)$ to an element of
$\llbracket{\Gamma(x)}\rrbracket$. Given $\rho\in\llbracket{\Gamma}\rrbracket$
and $e$ such that $\Gamma\vdash e:\tau$, its semantics
$\llbracket{e}\rrbracket_{\rho}\in\llbracket{\tau}\rrbracket$ is defined by:

$\displaystyle\llbracket{r}\rrbracket_{\rho}$ $\displaystyle=r$
$\displaystyle\llbracket{x}\rrbracket_{\rho}$ $\displaystyle=\rho(x)$
$\displaystyle\llbracket{f}\rrbracket_{\rho}$ $\displaystyle=\rho(f)$
$\displaystyle\llbracket{e_{\\_}1+e_{\\_}2}\rrbracket_{\rho}$
$\displaystyle=\llbracket{e_{\\_}1}\rrbracket_{\rho}+\llbracket{e_{\\_}2}\rrbracket_{\rho}$
$\displaystyle\llbracket{e_{\\_}1\cdot e_{\\_}2}\rrbracket_{\rho}$
$\displaystyle=\llbracket{e_{\\_}1}\rrbracket_{\rho}\cdot\llbracket{e_{\\_}2}\rrbracket_{\rho}$
$\displaystyle\llbracket{e_{\\_}1e_{\\_}2}\rrbracket_{\rho}$
$\displaystyle=(\llbracket{e_{\\_}1}\rrbracket_{\rho})(\llbracket{e_{\\_}2}\rrbracket_{\rho})$
$\displaystyle\llbracket{(e_{\\_}1,\ldots,e_{\\_}k)}\rrbracket_{\rho}$
$\displaystyle=(\llbracket{e_{\\_}1}\rrbracket_{\rho},\ldots,\llbracket{e_{\\_}k}\rrbracket_{\rho}).$

Given $\mathcal{E}$ such that $\Gamma\vdash\mathcal{E}$, we write
$\rho_{\\_}{\mathcal{E}}$ for the least solution of $\mathcal{E}$, i.e., the
least $\rho\in\llbracket{\Gamma}\rrbracket$ such that
$\llbracket{f(\widetilde{x}_{\\_}1)\cdots(\widetilde{x}_{\\_}\ell)}\rrbracket_{\rho\\{\widetilde{x}_{\\_}{1}\mapsto\widetilde{\bf
y}_{\\_}{1},\ldots,\widetilde{x}_{\\_}{\ell}\mapsto\widetilde{\bf
y}_{\\_}{\ell}\\}}=\llbracket{e}\rrbracket_{\rho\\{\widetilde{x}_{\\_}{1}\mapsto\widetilde{\bf
y}_{\\_}{1},\ldots,\widetilde{x}_{\\_}{\ell}\mapsto\widetilde{\bf
y}_{\\_}{\ell}\\}}$ for every equation
$f(\widetilde{x}_{\\_}1)\cdots(\widetilde{x}_{\\_}\ell)=e\in\mathcal{E}$ and
$(\widetilde{\bf
y}_{\\_}1)\in\llbracket{\tau_{\\_}1}\rrbracket,\ldots,(\widetilde{\bf
y}_{\\_}\ell)\in\llbracket{\tau_{\\_}\ell}\rrbracket$ with
$\Gamma(f)=\tau_{\\_}1\to\cdots\to\tau_{\\_}\ell\to\mathtt{R}$. Note that
$\rho_{\\_}{\mathcal{E}}$ always exists, and is given by:
$\rho_{\\_}{\mathcal{E}}=\mathbf{lfp}(\mathcal{F}_{\\_}\mathcal{E})=\bigsqcup_{\\_}{i\in\omega}\mathcal{F}_{\\_}\mathcal{E}^{i}(\bot_{\\_}{\llbracket{\Gamma}\rrbracket})$,
where
$\mathcal{F}_{\\_}\mathcal{E}\in\llbracket{\Gamma}\rrbracket\to\llbracket{\Gamma}\rrbracket$
is defined as the map such that

$\mathcal{F}_{\\_}\mathcal{E}(\rho)(f)=\mathop{\hbox
to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}(\widetilde{\bf
y}_{\\_}{1})\in\llbracket{\tau_{\\_}1}\rrbracket.\ldots\mathop{\hbox
to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}(\widetilde{\bf
y}_{\\_}{\ell})\in\llbracket{\tau_{\\_}\ell}\rrbracket.\llbracket{e}\rrbracket_{\rho\\{\widetilde{x}_{\\_}{1}\mapsto\widetilde{\bf
y}_{\\_}{1},\ldots,\widetilde{x}_{\\_}{\ell}\mapsto\widetilde{\bf
y}_{\\_}{\ell}\\}}$

for each
$f(\widetilde{x}_{\\_}1)\cdots(\widetilde{x}_{\\_}\ell)=e\in\mathcal{E}$ with
$\Gamma(f)=\tau_{\\_}1\to\cdots\to\tau_{\\_}\ell\to\mathtt{R}$. Note that
$\mathcal{F}_{\\_}\mathcal{E}$ is continuous in the $\omega$-cpo
$\llbracket{\Gamma}\rrbracket$.

######  Example 4.2.

Let $\mathcal{E}$ be the system of equations in Example 4.1. Then,
$\rho_{\\_}{\mathcal{E}}$ is:

$\left\\{f_{\\_}1\mapsto\frac{3}{7},f_{\\_}2\mapsto\mathop{\hbox
to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}g\in\mathbf{R}\to\mathbf{R}.\mathop{\hbox
to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}(x_{\\_}1,x_{\\_}2)\in\mathbf{R}\times\mathbf{R}.g(x_{\\_}1+x_{\\_}2),f_{\\_}3\mapsto\mathop{\hbox
to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}x\in\mathbf{R}.\frac{3}{7}x\right\\}.$

###  4.2. Order-$n$ Fixpoint Characterization

We now give a translation from an order-$n$ PHORS $\mathcal{G}$ to a system of
order-$n$ fixpoint equations $\mathcal{E}$, so that
$\mathcal{P}(\mathcal{G},S)=\rho_{\\_}{\mathcal{E}}(S)$. The translation is
actually straightforward: we just need to replace $\mathtt{e}$ and $\Omega$
with the termination probabilities $1$ and $0$, and probabilistic choices with
summation and multiplication of probabilities. The translation function
${(\cdot)}^{\\#}$ is defined by:

$\displaystyle{(\mathcal{N},\mathcal{R},S)}^{\\#}$
$\displaystyle=({\mathcal{R}}^{\\#},S)$ $\displaystyle\mathcal{R}^{\\#}$
$\displaystyle=\\{F\,\widetilde{x}=p\cdot(t_{\\_}L)^{\\#}+(1-p)\cdot(t_{\\_}R)^{\\#}\mid\mathcal{R}(F)=\lambda\widetilde{x}.t_{\\_}L\,\oplus_{p}\,t_{\\_}R\\}$
$\displaystyle\mathtt{e}^{\\#}$ $\displaystyle=1\qquad\Omega^{\\#}=0\qquad
x^{\\#}=x\qquad(st)^{\\#}=s^{\\#}t^{\\#}.$

We write $\mathcal{E}_{\\_}\mathcal{G}$ for $\mathcal{R}^{\\#}$. We define the
translation of types and type environments by:

$\displaystyle\mathtt{o}^{\\#}$ $\displaystyle=\mathtt{R}$
$\displaystyle(\kappa_{\\_}1\to\kappa_{\\_}2)^{\\#}$
$\displaystyle=\kappa_{\\_}1^{\\#}\to\kappa_{\\_}2^{\\#}$
$\displaystyle(x_{\\_}1\mathbin{:}\kappa_{\\_}1,\ldots,x_{\\_}n\mathbin{:}\kappa_{\\_}n)^{\\#}$
$\displaystyle=x_{\\_}1\mathbin{:}\kappa_{\\_}1^{\\#},\ldots,x_{\\_}n\mathbin{:}\kappa_{\\_}n^{\\#}.$

The following lemma states that the output of the translation is well-typed.

######  Lemma 4.3.

Let $\mathcal{G}=(\mathcal{N},\mathcal{R},S)$ be an order-$n$ PHORS. Then
$\mathcal{N}^{\\#}\vdash\mathcal{E}_{\\_}{\mathcal{G}}$ and
$\mathcal{N}^{\\#}\vdash S:\mathtt{R}$.

By the above lemma and the definition of the translation of type environments,
it follows that for an order-$n$ PHORS $\mathcal{G}$, the order of
$\mathcal{E}_{\\_}{\mathcal{G}}$ is also $n$. The following theorem states the
correctness of the translation (see Appendix B.1 for a proof).

######  Theorem 4.3.

Let $\mathcal{G}$ be an order-$n$ PHORS. Then
$\mathcal{P}(\mathcal{G})=\rho_{\\_}{\mathcal{E}_{\\_}{\mathcal{G}}}(S)$.

######  Example 4.4.

Recall $\mathcal{G}_{\\_}1=(\mathcal{N}_{\\_}1,\mathcal{R}_{\\_}1,S)$ from
Example 2.1:

$\displaystyle\mathcal{N}_{\\_}1$
$\displaystyle=\\{S\mapsto\mathtt{o},F\mapsto\mathtt{o}\to\mathtt{o}\\};$
$\displaystyle\mathcal{R}_{\\_}1$ $\displaystyle=\\{S\ =\
F\,\mathtt{e}\,\oplus_{1}\,\Omega,\quad F\,x\ =\ x\,\oplus_{p}\,F(F\,x)\\}.$

$\mathcal{N}_{\\_}1^{\\#}=\\{S\mapsto\mathbf{R},F\mapsto\mathbf{R}\to\mathbf{R}\\}$,
and $\mathcal{E}_{\\_}{\mathcal{G}_{\\_}1}$ consists of: $S=1\cdot F(1)$ and
$F\,x=p\cdot x+(1-p)\cdot F(F\,x)$. The least solution
$\rho_{\\_}{\mathcal{E}_{\\_}{\mathcal{G}_{\\_}1}}$ is

$\begin{array}[]{l}S=\left\\{\begin{array}[]{ll}\frac{p}{1-p}&\mbox{if $0\leq
p<\frac{1}{2}$}\\\ 1&\mbox{if $\frac{1}{2}\leq p\leq
1$}\end{array}\right.\qquad F=\mathop{\hbox to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}{\bf
x}.\left\\{\begin{array}[]{ll}\frac{p}{1-p}\cdot{\bf x}&\mbox{if $0\leq
p<\frac{1}{2}$}\\\ {\bf x}&\mbox{if $\frac{1}{2}\leq p\leq
1$.}\end{array}\right.\end{array}$

######  Example 4.5.

Recall $\mathcal{G}_{\\_}3$ from Example 2.7:

$\begin{array}[]{l}S=\textit{Listgen}\;(\textit{Listgen}\,\textit{Boolgen})\;\mathtt{e}\quad\textit{Boolgen}\;k=k\quad\textit{Listgen}\;f\;k=k\,\oplus_{\frac{1}{2}}\,(f(\textit{Listgen}\,f\,k)).\end{array}$

The corresponding fixpoint equations are:

$\displaystyle S$
$\displaystyle=\textit{Listgen}\;(\textit{Listgen}\,\textit{Boolgen})\;1$
$\displaystyle\textit{Boolgen}\;k$ $\displaystyle=k$
$\displaystyle\textit{Listgen}\;f\;k$
$\displaystyle=\frac{1}{2}k+\frac{1}{2}(f(\textit{Listgen}\,f\,k)).$

By specializing Listgen for the cases $f=\textit{Listgen}\,\textit{Boolgen}$
and $f=\textit{Boolgen}$, we obtain:

$\displaystyle S$ $\displaystyle=\textit{ListgenList}\;1$
$\displaystyle\textit{Boolgen}\;k$ $\displaystyle=k$
$\displaystyle\textit{ListgenList}\;k$
$\displaystyle=\frac{1}{2}k+\frac{1}{2}(\textit{ListgenBool}(\textit{ListgenList}\,k))$
$\displaystyle\textit{ListgenBool}\;k$
$\displaystyle=\frac{1}{2}k+\frac{1}{2}(\textit{Boolgen}(\textit{ListgenBool}\,k)).$

The least solution is:

$S=1\quad\textit{Boolgen}\;k=\textit{ListgenList}\;k=\textit{ListgenBool}\;k=k.$

###  4.3. Order-($n-1$) Fixpoint Characterization

We now characterize the termination probability of order-$n$ PHORS (where
$n>0$) in terms of order-($n-1$) equations, so that the fixpoint equations are
easier to solve. When $n=1$, the characterization yields polynomial equations
on probabilities; thus the result below may be considered as a generalization
of the now classic result on the reachability problem for recursive Markov
chains [EY09].

The basic observation (that is also behind the fixpoint characterization for
recursive Markov chains [EY09]) is that the termination behavior of an order-1
function of type $\mathtt{o}^{\ell}\to\mathtt{o}$ can be represented by a
tuple of _probabilities_ $(p_{\\_}0,p_{\\_}1,\ldots,p_{\\_}\ell)$, where (i)
$p_{\\_}0$ is the probability that the function terminates _without_ using any
of its arguments, and (ii) $p_{\\_}i$ is the probability that the function
uses the $i$-th argument. To see why, consider a term
$f\,t_{\\_}1\,\cdots\,t_{\\_}\ell$ of type $\mathtt{o}$, where $f$ is an
order-1 function of type $\mathtt{o}^{\ell}\to\mathtt{o}$. In order for
$f\,t_{\\_}1\,\cdots\,t_{\\_}\ell$ to terminate, the only possibilities are:
(i) $f$ terminates without calling any of the arguments, or (ii) $f$ calls
$t_{\\_}i$ for some $i\in\\{1,\ldots,\ell\\}$, and $t_{\\_}i$ terminates
(notice, in this case, that none of the other $t_{\\_}j$’s are called: since
$t_{\\_}i$ is of type $\mathtt{o}$, once $t_{\\_}i$ is called from $f$, the
control cannot go back to $f$). Thus, the probability that
$f\,t_{\\_}1\,\cdots\,t_{\\_}\ell$ terminates can be calculated by
$p_{\\_}0+p_{\\_}1q_{\\_}1+\cdots p_{\\_}\ell q_{\\_}\ell$, where each
$q_{\\_}i$ denotes the probability that $t_{\\_}i$ terminates. The termination
probability is, therefore, independent of the precise internal behavior of
$f$; only $(p_{\\_}0,p_{\\_}1,\ldots,p_{\\_}\ell)$ matters. Thus, information
about an order-1 function can be represented as a tuple of real numbers, which
is order 0. By generalizing this observation, we can represent information
about an order-$n$ function as an order-($n-1$) function on (tuples of) real
numbers. Since the general translation is quite subtle and requires a further
insight, however, let us first confirm the above idea by revisiting Example
2.1.

######  Example 4.6.

Recall $\mathcal{G}_{\\_}1$ from Example 2.1, consisting of: $S=F\;\mathtt{e}$
and $F\,x=x\,\oplus_{p}\,F(F\,x)$. Here, we have two functions: $S$ of type
$\mathtt{o}$ and $F$ of type $\mathtt{o}\to\mathtt{o}$. Based on the
observation above, their behaviors can be represented by $S_{\\_}0$ and
$(F_{\\_}0,F_{\\_}1)$ respectively, where $S_{\\_}0$ ($F_{\\_}0$, resp.)
denotes the probability that $S$ ($F$, resp.) terminates, and $F_{\\_}1$
represents the probability that $F$ uses the argument. Those values are
obtained as the least solutions for the following system of equations.

$\displaystyle S_{\\_}0$ $\displaystyle=F_{\\_}0+F_{\\_}1\cdot 1$
$\displaystyle F_{\\_}0$ $\displaystyle=p\cdot 0+(1-p)(F_{\\_}0+F_{\\_}1\cdot
F_{\\_}0)$ $\displaystyle F_{\\_}1$ $\displaystyle=p\cdot
1+(1-p)(F_{\\_}1\cdot F_{\\_}1\cdot 1).$

To understand the last equation, note that the possibilities that $x$ is used
are: (i) $F$ chooses the left branch (with probability $p$) and then uses $x$
with probability $1$, or (ii) $F$ chooses the right branch (with probability
$1-p$), the outer call of $F$ uses the argument $F\,x$ (with probability
$F_{\\_}1$), and the inner call of $F$ uses the argument $x$. By simplifying
the equations, we obtain:

$\displaystyle S_{\\_}0$ $\displaystyle=F_{\\_}0+F_{\\_}1$ $\displaystyle
F_{\\_}0$ $\displaystyle=(1-p)(F_{\\_}0+F_{\\_}1F_{\\_}0)$ $\displaystyle
F_{\\_}1$ $\displaystyle=p+(1-p)F_{\\_}1^{2}.$

The least solution is the following:

$F_{\\_}0=0\qquad
S_{\\_}0=F_{\\_}1=\left\\{\begin{array}[]{ll}\frac{p}{1-p}&\mbox{if $0\leq
p<\frac{1}{2}$}\\\ 1&\mbox{if $\frac{1}{2}\leq p\leq 1$.}\end{array}\right.$

The translation for general orders is more involved. For technical convenience
in formalizing the translation, we assume below that the rules of PHORS do not
contain $\mathtt{e}$; instead, the start symbol $S$ (which is now a non-
terminal of type $\mathtt{o}\to\mathtt{o}$) takes $\mathtt{e}$ from the
environment. Thus, the termination probability we consider is
$\mathcal{P}(\mathcal{G},S\,\mathtt{e})$, where $\mathtt{e}$ does not occur in
$\mathcal{R}$. This is without any loss of generality, since $\mathtt{e}$ can
be passed around as an argument without increasing the order of the underlying
PHORS, if it is higher than $0$.

To see how we can generalize the idea above to deal with higher-order
functions, let us now consider the following example of an order-2 PHORS:

$\displaystyle S\,x$ $\displaystyle=F\,(H\,x)\,x$ $\displaystyle F\,f\,y$
$\displaystyle=f(f\,y)$ $\displaystyle H\,x\,y$
$\displaystyle=x\,\oplus_{\frac{1}{2}}\,(y\,\oplus_{\frac{1}{2}}\,\Omega).$

Suppose we wish to characterize the termination probability of
$S\;\mathtt{e}$, i.e., the probability that $S$ uses the first argument. (In
this particular case, one can easily compute the termination probability by
unfolding all the functions, but we wish to find a compositional translation
which works well in presence of recursion.) We need to compute the probability
that $F\;(H\;x)\;x$ reaches (i.e., reduces to) $x$, which is the probability
$p_{\\_}1$ that $F\;(H\;x^{(1)})\;x^{(2)}$ reaches $x^{(1)}$, plus the
probability $p_{\\_}2$ that $F\;(H\;x^{(1)})\;x^{(2)}$ reaches $x^{(2)}$; we
have added annotations to distinguish between the two occurrences of $x$. What
information on $F$ is required for computing it? To compute $p_{\\_}2$, we
need to obtain the probability that $F$ uses the formal argument $y$. Since it
depends on $f$, we represent it as a function $F_{\\_}1$ defined by:

$F_{\\_}1\;f_{\\_}1=f_{\\_}1\cdot f_{\\_}1.$

Here, $f_{\\_}1$ represents the probability that the original argument $f$
uses its first argument. We can thus represent $p_{\\_}2$ as
$F_{\\_}1(H_{\\_}2)$, where $H_{\\_}2$ is $\frac{1}{4}$, the probability that
$f=H\,x$ uses the first argument, i.e., the probability that $H$ uses the
second argument. Now let us consider how to represent $p_{\\_}1$, the
probability that $F\,(H\,x^{(1)})\,x^{(2)}$ reaches $x^{(1)}$. We construct
another function $F_{\\_}0$ from the definition of $F$ for this purpose. A
challenge is that the variable $x$ is not visible in (the definition of) $F$;
only the caller of $F$ knows the reachability target $x$. Thus, we pass to
$F_{\\_}0$, in addition to $f_{\\_}1$ above, another argument $f_{\\_}0$,
which represents the probability that the argument $f$ reaches the current
target (which is $x$ in this case). Therefore, $p_{\\_}1$ is represented as
$F_{\\_}0\,(H_{\\_}1,H_{\\_}2)$, where

$F_{\\_}0\,(f_{\\_}0,f_{\\_}1)=f_{\\_}0+f_{\\_}1\cdot f_{\\_}0\qquad
H_{\\_}1=\frac{1}{2}.$

In $f_{\\_}0+f_{\\_}1\cdot f_{\\_}0$, the occurrence of $f_{\\_}0$ on the
lefthand side represents the probability that the outer call of $f$ in
$f(f\,x)$ reaches the target (without using $(f\,x)$), and $f_{\\_}1\cdot
f_{\\_}0$ represents the probability that the outer call of $f$ uses the
argument $f\,x$, and then the inner call of $f$ reaches the target. Now, the
whole probability that $S$ uses its argument is represented as $S_{\\_}1$,
where

$S_{\\_}1=F_{\\_}0(H_{\\_}1,H_{\\_}2)+F_{\\_}1(H_{\\_}2),$

with the functions $F_{\\_}0,F_{\\_}1,H_{\\_}1$ and $H_{\\_}2$ being as
defined above. Note that the order of the resulting equations is one. In
summary, as information about an order-1 argument $f$ of arity $k$, we pass
around a tuple of real numbers $(f_{\\_}0,f_{\\_}1,\ldots,f_{\\_}k)$ where
$f_{\\_}i\;(i>0)$ represents the probability that the $i$-th argument is
reached, and $f_{\\_}0$ represents the probability that the “current target”
(which is chosen by a caller) is reached.

A further twist is required in the case of order-3 or higher. Consider an
order-3 function $G$ defined by:

$G\;h\;z=h\,(H\,z)\,z$

where
$G\mathbin{:}((\mathtt{o}\to\mathtt{o})\to\mathtt{o}\to\mathtt{o})\to\mathtt{o}\to\mathtt{o}$,
and $H$ is as defined above. Following the definition of $F_{\\_}1$ above, one
may be tempted to define $G_{\\_}1$ (for computing the reachability
probability to $z$) as $G_{\\_}1\;h_{\\_}1=\cdots$, where $h_{\\_}1$ is a
function to be used for computing the probability that $h$ uses its order-0
argument. However, $h_{\\_}1$ is not sufficient for computing the reachability
probability to $z$; passing the reachability probability to the _current_
target (like $f_{\\_}0$ above) does not help either, since a caller of $G$
does not know the current target $z$. We thus need to add an additional
argument $h_{\\_}2$ for computing the probability to a target that is yet to
be set by a caller of $h$. Thus, the definition of $G_{\\_}1$ is:222 For the
sake of simplicity, the following translation slightly deviates from the
general translation defined later.

$G_{\\_}1\;(h_{\\_}1,h_{\\_}2)=h_{\\_}2(H_{\\_}1,H_{\\_}2)+h_{\\_}1(1).$

Here, $h_{\\_}2(H_{\\_}1,H_{\\_}2)$ and $h_{\\_}1(1)$ respectively represent
the probabilities that $G\,(H\,z^{(1)})\,z^{(2)}$ reaches $z^{(1)}$, and
$z^{(2)}$. The first argument of $h_{\\_}2$ (i.e., $H_{\\_}1$) represents the
probability that $H\,z$ reaches $z$, and the second argument of $h_{\\_}2$
(i.e., $H_{\\_}2$) represents the probability that $H\,z$ reaches its argument
(the second argument of $H$).

We can now formalize the general translation based on the intuitions above. We
often write
$\kappa_{\\_}1\to\cdots\to\kappa_{\\_}k\Rightarrow\mathtt{o}^{\ell}\to\mathtt{o}$
for $\kappa_{\\_}1\to\cdots\to\kappa_{\\_}k\to\mathtt{o}^{\ell}\to\mathtt{o}$
when either $\mathit{order}(\kappa_{\\_}k)>0$ or $k=0$. We define
$\mathtt{ar}(\kappa)$ as the number of the last order-0 arguments, i.e.,
$\mathtt{ar}(\kappa_{\\_}1\to\cdots\to\kappa_{\\_}k\Rightarrow\mathtt{o}^{\ell}\to\mathtt{o})=\ell$.

Given a rule $F\,z_{\\_}1\,\ldots\,z_{\\_}m=t_{\\_}L\,\oplus_{p}\,t_{\\_}R$ of
PHORS, we uniquely decompose $z_{\\_}1,\ldots,z_{\\_}m$ into two (possibly
empty) subsequences $z_{\\_}1,\ldots,z_{\\_}\ell$ and
$z_{\\_}{\ell+1},\ldots,z_{\\_}{m}$ so that the order of $z_{\\_}\ell$ is
greater than $0$ if $\ell>0$ (note, however, that the orders of
$z_{\\_}1,\ldots,z_{\\_}{\ell-1}$ may be $0$), and
$z_{\\_}{\ell+1},\ldots,z_{\\_}{m}$ are order-0 variables (in other words,
$z_{\\_}{\ell+1},\ldots,z_{\\_}{m}$ is the maximal postfix of
$z_{\\_}1,\ldots,z_{\\_}m$ consisting of only order-0 variables). Since (the
last consecutive occurrences of) order-0 arguments will be treated in a
special manner, as a notational convenience, when we write
$F\;\widetilde{y}\;\widetilde{x}=t_{\\_}L\,\oplus_{p}\,t_{\\_}R$ for a rule of
PHORS, we implicitly assume that $\widetilde{x}$ is the maximal postfix of the
sequence $\widetilde{y}\;\widetilde{x}$ consisting of only order-0 variables.
Similarly, when we write $F\,\widetilde{s}\,\widetilde{t}$ for a fully-applied
term (of order 0), we implicitly assume that $\widetilde{t}$ is the maximal
postfix of the sequence of arguments, consisting of only order-0 terms.

Consider a function definition of the form:

$F\;y_{\\_}1\;\cdots\;y_{\\_}m\;x_{\\_}1\;\cdots\;x_{\\_}k=t_{\\_}L\,\oplus_{p}\,t_{\\_}R$

where (following the notational convention above) the sequence
$x_{\\_}1,\ldots,x_{\\_}k$ is the maximal postfix of
$y_{\\_}1,\ldots,y_{\\_}m,x_{\\_}1,\ldots,x_{\\_}k$ consisting of only order-0
variables. We transform each subterm $t$ of the righthand side
$t_{\\_}L\,\oplus_{p}\,t_{\\_}R$ by using the translation relation of the
form:

$\mathcal{K};x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}t:\kappa\leadsto(e_{\\_}0,e_{\\_}1,\ldots,e_{\\_}{\ell+k+1})$

where $\mathcal{N}$ and $\mathcal{K}$ are type environments for the underlying
non-terminals and $y_{\\_}1,\ldots,y_{\\_}m$ respectively, and $\kappa$ is the
type of $t$ with $\mathtt{ar}(\kappa)=\ell$. We often omit the subscript
$\mathcal{N}$. The output of the translation,
$(e_{\\_}0,e_{\\_}1,\ldots,e_{\\_}{\ell+k+1})$, can be interpreted as
capturing the following information.

  * •

$e_{\\_}0$: the reachability probability (or a function that returns the
probability, given appropriate arguments; similarly for the other $e_{\\_}i$’s
below) to the current target (set by a caller of $F$).

  * •

$e_{\\_}{i}\;(i\in\\{1,\ldots,\ell\\})$: the reachability probability to $t$’s
$i$-th order-0 argument.

  * •

$e_{\\_}{\ell+i}\;(i\in\\{1,\ldots,k\\})$: the reachability probability to
$x_{\\_}i$.

  * •

$e_{\\_}{\ell+k+1}$: the reachability probability to a “fresh” target (that
can be set by a caller of $t$); this is the component that should be passed as
$h_{\\_}2$ in the discussion above. In a sense, this component represents the
reachability probability to a variable $x_{\\_}{k+1}$ that is “fresh” for $t$
(in that it does not occur in $t$).

In the translation, each variable $y$ (including non-terminals) of type
$\widetilde{\kappa}\Rightarrow\mathtt{o}^{m}\to\mathtt{o}$ is replaced by
$(y_{\\_}0,y_{\\_}1,\ldots,y_{\\_}m,y_{\\_}{m+1})$, which represents
information analogous to
$(e_{\\_}0,e_{\\_}1,\ldots,e_{\\_}\ell,e_{\\_}{\ell+k+1})$: $y_{\\_}0$
represents (a function for computing) the reachability probability to the
current target, $y_{\\_}i\;(i\in\\{1,\ldots,m\\})$ represents the reachability
probability to the $i$-th order-0 argument (among the last $m$ argument), and
$y_{\\_}{m+1}$ (which corresponds to $h_{\\_}2$ in the explanation above)
represents the reachability probability to a fresh target (to be set later).
In contrast, the variables $x_{\\_}1,\ldots,x_{\\_}k$ will be removed by the
translation.

The translation rules are given in Figure 5. In the rules, to clarify the
correspondence between source terms and target expressions, we use
metavariables $s,t,\ldots$ (with subscripts) also for target expressions
(instead of $e$). We write $e^{k}$ for the $k$ repetitions of $e$.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}\Omega:\mathtt{o}\leadsto(0^{k+2})\end{array}}$
(Tr-Omega)
$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}x_{\\_}i:\mathtt{o}\leadsto(0^{i},1,0^{k-i+1})\end{array}}$
(Tr-GVar)
$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K}(y)=\widetilde{\kappa}\Rightarrow\mathtt{o}^{\ell}\to\mathtt{o}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}y:\widetilde{\kappa}\Rightarrow\mathtt{o}^{\ell}\to\mathtt{o}\leadsto(y_{\\_}0,y_{\\_}1,\ldots,y_{\\_}\ell,(y_{\\_}{\ell+1})^{k+1})\end{array}}$
(Tr-Var)
$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{N}(F)=\widetilde{\kappa}\Rightarrow\mathtt{o}^{\ell}\to\mathtt{o}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}F:\widetilde{\kappa}\Rightarrow\mathtt{o}^{\ell}\to\mathtt{o}\leadsto(F_{\\_}0,F_{\\_}1,\ldots,F_{\\_}\ell,(F_{\\_}{0})^{k+1})\end{array}}$
(Tr-NT)
$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K};x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}s:\kappa_{\\_}1\to\widetilde{\kappa}\Rightarrow\mathtt{o}^{\ell}\to\mathtt{o}\leadsto(s_{\\_}0,\ldots,s_{\\_}{\ell+k+1})\\\
\mathcal{K};x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}t:\kappa_{\\_}1\leadsto(t_{\\_}0,\ldots,t_{\\_}{\ell^{\prime}+k+1})\quad\quad\mathtt{ar}(\kappa_{\\_}1)=\ell^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\widetilde{x}\vdash_{\mathcal{N}}st:\widetilde{\kappa}\Rightarrow\mathtt{o}^{\ell}\to\mathtt{o}\leadsto(s_{\\_}0(t_{\\_}0,\ldots,t_{\\_}{\ell^{\prime}},t_{\\_}{\ell^{\prime}+k+1}),s_{\\_}1(t_{\\_}1,\ldots,t_{\\_}{\ell^{\prime}},t_{\\_}{\ell^{\prime}+k+1}),\ldots,s_{\\_}\ell(t_{\\_}1,\ldots,t_{\\_}{\ell^{\prime}},t_{\\_}{\ell^{\prime}+k+1}),\\\
\hfill
s_{\\_}{\ell+1}(t_{\\_}{\ell^{\prime}+1},t_{\\_}1,\ldots,t_{\\_}{\ell^{\prime}},t_{\\_}{\ell^{\prime}+k+1})\ldots,s_{\\_}{\ell+k+1}(t_{\\_}{\ell^{\prime}+k+1},t_{\\_}1,\ldots,t_{\\_}{\ell^{\prime}},t_{\\_}{\ell^{\prime}+k+1}))\end{array}}$
(Tr-App)
$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K};x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}s:\mathtt{o}^{\ell+1}\to\mathtt{o}\leadsto(s_{\\_}0,\ldots,s_{\\_}{k+\ell+2})\quad\quad\mathcal{K};x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}t:\mathtt{o}\leadsto(t_{\\_}0,\ldots,t_{\\_}{k+1})\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}st:\mathtt{o}^{\ell}\to\mathtt{o}\leadsto(s_{\\_}0+s_{\\_}1\cdot
t_{\\_}0,s_{\\_}2,\ldots,s_{\\_}{\ell+1},s_{\\_}{\ell+2}+s_{\\_}1\cdot
t_{\\_}1,\ldots,s_{\\_}{\ell+k+2}+s_{\\_}1\cdot t_{\\_}{k+1})\end{array}}$
(Tr-AppG)
$\displaystyle\frac{\begin{array}[]{@{}c@{}}y_{\\_}1\mathbin{:}\kappa_{\\_}1,\ldots,y_{\\_}\ell\mathbin{:}\kappa_{\\_}\ell;x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}t_{\\_}d:\mathtt{o}\leadsto(t_{\\_}{d,0},\ldots,t_{\\_}{d,k+1})\mbox{
for each $d\in\\{L,R\\}$}\\\
\widetilde{y_{\\_}i}=(y_{\\_}{i,0},\ldots,y_{\\_}{i,\mathtt{ar}(\kappa_{\\_}i)+1})\quad\quad\widetilde{y_{\\_}i}^{\prime}=(y_{\\_}{i,1},\ldots,y_{\\_}{i,\mathtt{ar}(\kappa_{\\_}i)+1})\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{N}\vdash(F\,\widetilde{y}\;x_{\\_}1\,\cdots\,x_{\\_}k=t_{\\_}L\,\oplus_{p}\,t_{\\_}R)\leadsto\\\
\qquad\\{F_{\\_}i\,\widetilde{y_{\\_}1}^{\prime}\,\cdots\,\widetilde{y_{\\_}\ell}^{\prime}=pt_{\\_}{L,i}+(1-p)t_{\\_}{R,i}\mid
i\in\\{1,\ldots,k\\}\\}\cup\\{F_{\\_}0\,\widetilde{y_{\\_}1}\,\cdots\,\widetilde{y_{\\_}\ell}=pt_{\\_}{L,0}+(1-p)t_{\\_}{R,0}\\}\end{array}}$
(Tr-Rule)
$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{E}=\bigcup\\{\mathcal{E}_{\\_}i\mid\mathcal{N}\vdash(F\,\widetilde{y}\;x_{\\_}1\,\cdots\,x_{\\_}k=t_{\\_}L\,\oplus_{p}\,t_{\\_}R)\leadsto\mathcal{E}_{\\_}i,(F\,\widetilde{y}\;x_{\\_}1\,\cdots\,x_{\\_}k=t_{\\_}L\,\oplus_{p}\,t_{\\_}R)\in\mathcal{R}\\}\end{array}}{\begin{array}[]{@{}c@{}}(\mathcal{N},\mathcal{R},S)\leadsto(\mathcal{E},S_{\\_}1)\end{array}}$
(Tr-Gram)

Figure 5. Translation rules for the order-$(n-1)$ fixpoint characterization

We now explain the translation rules. In rule Tr-Omega for the constant
$\Omega$, all the components are $0$ because $\Omega$ represents divergence.
There is no rule for $\mathtt{e}$; this is due to the assumption that
$\mathtt{e}$ never occurs in the rules. Rule Tr-GVar is for order-0 variables,
for which only one component is 1 and all the others are 0. The ($i+1$)-th
component is $1$, because it represents the probability that $x_{\\_}i$ is
reached. In rule Tr-Var for variables, the first $\ell+1$ components are
provided by the environment. Since $y$ (that is provided by the environment)
does not “know” the local variables $x_{\\_}1,\ldots,x_{\\_}k$ (in other
words, $y$ cannot be instantiated to a term that contains $x_{\\_}i$), the
default parameter $y_{\\_}{\ell+1}$ (for computing the reachability
probability to a “fresh” target) is used for all of those components. The rule
Tr-NT for non-terminals is almost the same as Tr-Var, except that $F_{\\_}0$
is used instead of $F_{\\_}{\ell+1}$. This is because $F$ does not contain any
free variables; the reachability target for $F$ is not set yet, hence
$F_{\\_}0$ can be used for computing the reachability probability to a fresh
target. Rule Tr-App is for applications. Basically, the output of the
translation of $t$ is passed to $s_{\\_}i$; note however that $t_{\\_}0$ is
passed only to $s_{\\_}0$; since $s_{\\_}1,\ldots,s_{\\_}{\ell+k}$ should
provide the reachability probability to order-0 arguments of $s$ or local
variables, the reachability probability to the current target (that is
represented by $t_{\\_}0$) is irrelevant for them. For
$s_{\\_}{\ell+1},\ldots,s_{\\_}{\ell+k}$, the reachability targets are
$x_{\\_}1,\ldots,x_{\\_}k$; thus, information about how $t$ reaches those
variables is passed as the first argument of
$s_{\\_}{\ell+1},\ldots,s_{\\_}{\ell+k}$. For the last component,
$s_{\\_}{\ell+k+1}$ and $t_{\\_}{\ell^{\prime}+k+1}$ are used so that the
reachability target can be set later. In rule Tr-AppG, the reachability
probability to the current target (expressed by the first component) is
computed by $s_{\\_}0+s_{\\_}1\cdot t_{\\_}0$, because the current target is
reached without using $t$ (as represented by $s_{\\_}0$), or $t$ is used (as
represented by $s_{\\_}1$) and $t$ reaches the current target (as represented
by $t_{\\_}0$); similarly for the reachability probability to local variables.
Tr-Rule is the rule for translating a function definition. From the definition
for $F$, we generate definitions for functions $F_{\\_}0,\ldots,F_{\\_}{k}$.
For $i\in\\{1,\ldots,k\\}$, $t_{\\_}{d,i}$ is chosen as the body of
$F_{\\_}i$, since it represents the reachability probability to $x_{\\_}i$.
Rule Tr-Gram is the translation for the whole PHORS; we just collect the
output of the translation for each rule.

For a PHORS $\mathcal{G}=(\mathcal{N},\mathcal{R},S)$ (where
$\mathcal{N}(S)=\mathtt{o}\to\mathtt{o}$), we write
$\mathcal{E}^{\mathtt{ref}}_{\mathcal{G}}$ for $\mathcal{E}$ such that
$(\mathcal{N},\mathcal{R},S)\leadsto(\mathcal{E},S_{\\_}1)$. Such an
$\mathcal{E}$ is actually unique (up to $\alpha$-equivalence), given
$\mathcal{N}$ and $\mathcal{R}$. Note also that by definition of the
translation relation, the output of the translation always exists.

######  Example 4.7.

Recall the order-2 PHORS $\mathcal{G}_{\\_}2$ in Example 2.2:

$\displaystyle S\ $ $\displaystyle=\ F\,H$ $\displaystyle H\,x$
$\displaystyle=x\,\oplus_{\frac{1}{2}}\,\Omega$ $\displaystyle F\,g$
$\displaystyle=(g\,\mathtt{e})\,\oplus_{\frac{1}{2}}\,(F(D\,g))$
$\displaystyle D\,g\,x$ $\displaystyle=g\,(g\,x).$

It can be modified to the following rules so that $\mathtt{e}$ does not occur.

$\displaystyle S\,z$ $\displaystyle=F\,H\,z$ $\displaystyle H\,x$
$\displaystyle=x\,\oplus_{\frac{1}{2}}\,\Omega$ $\displaystyle F\,g\,z$
$\displaystyle=(g\,z)\,\oplus_{\frac{1}{2}}\,(F(D\,g)\,z)$ $\displaystyle
D\,g\,x$ $\displaystyle=g\,(g\,x).$

Here, $\mathtt{e}$ can be passed around through the variable $z$. Consider the
body $F\,H\,z$ of $S$. $F$ and $H$ are translated as follows.

$\begin{array}[]{l}\emptyset;z\vdash_{\mathcal{N}}F:(\mathtt{o}\to\mathtt{o})\to\mathtt{o}\to\mathtt{o}\leadsto(F_{\\_}0,F_{\\_}1,F_{\\_}0,F_{\\_}0)\\\
\emptyset;z\vdash_{\mathcal{N}}H:\mathtt{o}\to\mathtt{o}\leadsto(H_{\\_}0,H_{\\_}1,H_{\\_}0,H_{\\_}0)\\\
\end{array}$

By applying Tr-App, we obtain:

$\begin{array}[]{l}\emptyset;z\vdash_{\mathcal{N}}F\,H:\mathtt{o}\to\mathtt{o}\leadsto(F_{\\_}0(H_{\\_}0,H_{\\_}1,H_{\\_}0),F_{\\_}1(H_{\\_}1,H_{\\_}0),F_{\\_}0(H_{\\_}0,H_{\\_}1,H_{\\_}0),F_{\\_}0(H_{\\_}0,H_{\\_}1,H_{\\_}0)).\end{array}$

Using Tr-GVar, $z$ can be translated as follows.

$\emptyset;z\vdash_{\mathcal{N}}z:\mathtt{o}\leadsto(0,1,0).$

Thus, by applying Tr-AppG, we obtain:

$\begin{array}[]{l}\emptyset;z\vdash_{\mathcal{N}}F\,H\,z:\mathtt{o}\leadsto\\\
\qquad(F_{\\_}0(H_{\\_}0,H_{\\_}1,H_{\\_}0)+F_{\\_}1(H_{\\_}1,H_{\\_}0)\cdot
0,\\\
\qquad\;F_{\\_}0(H_{\\_}0,H_{\\_}1,H_{\\_}0)+F_{\\_}1(H_{\\_}1,H_{\\_}0)\cdot
1,F_{\\_}0(H_{\\_}0,H_{\\_}1,H_{\\_}0)+F_{\\_}1(H_{\\_}1,H_{\\_}0)\cdot
0).\end{array}$

By simplifying the output, we obtain:

$\begin{array}[]{l}\emptyset;z\vdash_{\mathcal{N}}F\,H\,z:\mathtt{o}\leadsto(F_{\\_}0(H_{\\_}0,H_{\\_}1,H_{\\_}0),F_{\\_}0(H_{\\_}0,H_{\\_}1,H_{\\_}0)+F_{\\_}1(H_{\\_}1,H_{\\_}0),F_{\\_}0(H_{\\_}0,H_{\\_}1,H_{\\_}0)).\end{array}$

Thus, we have the following equations for $S_{\\_}0$ and $S_{\\_}1$.

$\begin{array}[]{l}S_{\\_}0=F_{\\_}0(H_{\\_}0,H_{\\_}1,H_{\\_}0)\qquad
S_{\\_}1=F_{\\_}0(H_{\\_}0,H_{\\_}1,H_{\\_}0)+F_{\\_}1(H_{\\_}1,H_{\\_}0).\end{array}$

The following equations are obtained for the other non-terminals.

$\displaystyle H_{\\_}0$ $\displaystyle=0\qquad\qquad H_{\\_}1=\frac{1}{2}$
$\displaystyle F_{\\_}0\,(g_{\\_}0,g_{\\_}1,g_{\\_}2)$
$\displaystyle=\frac{1}{2}g_{\\_}0+F_{\\_}0(D_{\\_}0(g_{\\_}0,g_{\\_}1,g_{\\_}2),D_{\\_}1(g_{\\_}1,g_{\\_}2),D_{\\_}0(g_{\\_}2,g_{\\_}1,g_{\\_}2))$
$\displaystyle F_{\\_}1\,(g_{\\_}1,g_{\\_}2)$
$\displaystyle=\frac{1}{2}(g_{\\_}1+g_{\\_}2)+\frac{1}{2}(F_{\\_}0(D_{\\_}0(g_{\\_}2,g_{\\_}1,g_{\\_}2),D_{\\_}1(g_{\\_}1,g_{\\_}2),D_{\\_}0(g_{\\_}2,g_{\\_}1,g_{\\_}2))$
$\displaystyle\qquad+F_{\\_}1(D_{\\_}1(g_{\\_}1,g_{\\_}2),D_{\\_}0(g_{\\_}2,g_{\\_}1,g_{\\_}2))$
$\displaystyle D_{\\_}0(g_{\\_}0,g_{\\_}1,g_{\\_}2)$
$\displaystyle=g_{\\_}0+g_{\\_}1g_{\\_}0$ $\displaystyle
D_{\\_}1(g_{\\_}1,g_{\\_}2)$
$\displaystyle=g_{\\_}2+g_{\\_}1(g_{\\_}1+g_{\\_}2).$

We can observe that the values of the variables $g_{\\_}0$ and $g_{\\_}2$ are
always $0$. Thus, by removing redundant arguments, we obtain:

$\displaystyle S_{\\_}0$ $\displaystyle=F_{\\_}0(\frac{1}{2})$ $\displaystyle
S_{\\_}1$ $\displaystyle=F_{\\_}0(\frac{1}{2})+F_{\\_}1(\frac{1}{2})$
$\displaystyle F_{\\_}0(g_{\\_}1)$
$\displaystyle=F_{\\_}0(D_{\\_}1(g_{\\_}1))$ $\displaystyle
F_{\\_}1(g_{\\_}1)$
$\displaystyle=\frac{1}{2}g_{\\_}1+\frac{1}{2}(F_{\\_}0(D_{\\_}1(g_{\\_}1))+F_{\\_}1(D_{\\_}1(g_{\\_}1)))$
$\displaystyle D_{\\_}0(g_{\\_}1)$ $\displaystyle=0$ $\displaystyle
D_{\\_}1(g_{\\_}1)$ $\displaystyle=g_{\\_}1^{2}.$

By further simplification (noting that the least solution for $F_{\\_}0$ is
$\lambda g_{\\_}1.0$), we obtain:

$\begin{array}[]{c}S_{\\_}1=F_{\\_}1(\frac{1}{2})\qquad\qquad
F_{\\_}1(g_{\\_}1)=\frac{1}{2}g_{\\_}1+\frac{1}{2}F_{\\_}1(g_{\\_}1^{2}).\end{array}$

The least solution of $S_{\\_}1$ is $\Sigma_{\\_}{i\geq
0}\frac{1}{2^{2^{i}+i+1}}=0.3205\cdots$. ∎

######  Example 4.8.

Consider the following order-3 PHORS:

$S\,x=F(C\,x)\quad F\,g=g\,H\quad C\,x\,f=f\,x\quad
H\,x=x\,\oplus_{\frac{1}{2}}\,\Omega,$

where

$\begin{array}[]{l}S\mathbin{:}\mathtt{o}\to\mathtt{o},F\mathbin{:}((\mathtt{o}\to\mathtt{o})\to\mathtt{o})\to\mathtt{o},C\mathbin{:}\mathtt{o}\to(\mathtt{o}\to\mathtt{o})\to\mathtt{o},H\mathbin{:}\mathtt{o}\to\mathtt{o}.\end{array}$

This is a tricky example, where in the body of $S$, $x$ is embedded into the
closure $C\,x$ and passed to another function $F$; so, in order to compute how
$S$ uses $x$, we have to take into account how $F$ uses the closure passed as
the argument. The PHORS is translated to:

$\displaystyle S_{\\_}0$ $\displaystyle=F_{\\_}0(C_{\\_}0(0,0),C_{\\_}0(0,0))$
$\displaystyle S_{\\_}1$ $\displaystyle=F_{\\_}0(C_{\\_}0(1,0),C_{\\_}0(0,0))$
$\displaystyle F_{\\_}0\,(g_{\\_}0,g_{\\_}1)$
$\displaystyle=g_{\\_}0(H_{\\_}0,H_{\\_}1,H_{\\_}0)$ $\displaystyle
C_{\\_}0\,(x_{\\_}0,x_{\\_}1)\,(f_{\\_}0,f_{\\_}1,f_{\\_}2)$
$\displaystyle=f_{\\_}0+f_{\\_}1\cdot x_{\\_}0$ $\displaystyle H_{\\_}0$
$\displaystyle=0\qquad H_{\\_}1=\frac{1}{2},$

where

$\displaystyle S_{\\_}0$
$\displaystyle\mathbin{:}\mathtt{R},S_{\\_}1\mathbin{:}\mathtt{R},$
$\displaystyle F_{\\_}0$
$\displaystyle\mathbin{:}(\mathtt{R}\times\mathtt{R}\times\mathtt{R}\to\mathtt{R})\times(\mathtt{R}\times\mathtt{R}\times\mathtt{R}\to\mathtt{R})\to\mathtt{R},$
$\displaystyle C_{\\_}0$
$\displaystyle\mathbin{:}(\mathtt{R}\times\mathtt{R})\to(\mathtt{R}\times\mathtt{R}\times\mathtt{R})\to\mathtt{R},$
$\displaystyle H_{\\_}0$
$\displaystyle\mathbin{:}\mathtt{R},H_{\\_}1\mathbin{:}\mathtt{R}.$

The order of the equations is $2$ (where the largest order is that of the type
of $F_{\\_}0$). We have:

$S_{\\_}1=F_{\\_}0(C_{\\_}0(1,0),C_{\\_}0(0,0))=C_{\\_}0(1,0)(H_{\\_}0,H_{\\_}1,H_{\\_}0)=H_{\\_}0+H_{\\_}1\cdot
1=\frac{1}{2}.$

In fact, the probability that $S\,\mathtt{e}$ reaches $\mathtt{e}$ is
$\frac{1}{2}$. ∎

######  Example 4.9.

Recall PHORS $\mathcal{G}_{\\_}5$ from Example 2.8:

$\displaystyle S\;x$ $\displaystyle=\textit{Treegen}\;H\;\textit{Boolgen}\;x$
$\displaystyle\textit{Boolgen}\;k$ $\displaystyle=k$ $\displaystyle H\;x\;y$
$\displaystyle=x\,\oplus_{\frac{1}{2}}\,y$ $\displaystyle G\;p\;x\;y$
$\displaystyle=x\,\oplus_{\frac{1}{2}}\,(p\;x\;y)$
$\displaystyle\textit{Treegen}\;p\;f\;k$
$\displaystyle=p\;k\;(f(\textit{Treegen}\,(G\;p)\,f\,(\textit{Treegen}\,(G\;p)\,f\,(\textit{Treegen}\,(G\;p)\,f\,k)))).$

(Here, we have slightly modified the original PHORS so that $S$ is
parameterized with $\mathtt{e}$.) As the output of the translation as defined
above is too complex, we show below a hand-optimized version of the fixpoint
equations.

$\displaystyle S_{\\_}1$
$\displaystyle=\textit{Treegen}_{\\_}1\;(H_{\\_}1,H_{\\_}2)$ $\displaystyle
H_{\\_}1$ $\displaystyle=H_{\\_}2=\frac{1}{2}$ $\displaystyle
G_{\\_}1\;(p_{\\_}1,p_{\\_}2)$ $\displaystyle=\frac{1}{2}+\frac{1}{2}p_{\\_}1$
$\displaystyle G_{\\_}2\;(p_{\\_}1,p_{\\_}2)$
$\displaystyle=\frac{1}{2}p_{\\_}2$
$\displaystyle\textit{Treegen}_{\\_}1\;(p_{\\_}1,p_{\\_}2)$
$\displaystyle=p_{\\_}1+p_{\\_}2\cdot(\textit{Treegen}_{\\_}1\;(G_{\\_}1(p_{\\_}1,p_{\\_}2),G_{\\_}2(p_{\\_}1,p_{\\_}2)))^{3}.$

Here, $\textit{Treegen}_{\\_}1$ is the function that returns the probability
that $\textit{Treegen}\;p\;\textit{Boolgen}\;x$ reaches $x$, where the
parameters $p_{\\_}1$ and $p_{\\_}2$ represent the probabilities that $p$
chooses the first and second branches respectively. Let $\rho$ be the least
solution of the fixpoint equations above. We can find $\rho(S_{\\_}1)=1$ based
on the following reasoning (which is also confirmed by the experiment reported
in Section 6). Let us define an $m$-th approximation
$\textit{Treegen}_{\\_}1^{(m)}$ of $\rho(\textit{Treegen}_{\\_}1)$ by

$\displaystyle\textit{Treegen}_{\\_}1^{(0)}\;(p_{\\_}1,p_{\\_}2)$
$\displaystyle=0$
$\displaystyle\textit{Treegen}_{\\_}1^{(m+1)}\;(p_{\\_}1,p_{\\_}2)$
$\displaystyle=p_{\\_}1+p_{\\_}2\cdot(\textit{Treegen}_{\\_}1^{(m)}\;(G_{\\_}1(p_{\\_}1,p_{\\_}2),G_{\\_}2(p_{\\_}1,p_{\\_}2)))^{3}.$

Then
$\rho(\textit{Treegen}_{\\_}1)\;(p_{\\_}1,p_{\\_}2)\geq\textit{Treegen}_{\\_}1^{(m)}\;(p_{\\_}1,p_{\\_}2)$
for every $m\geq 0$. We show
$\textit{Treegen}_{\\_}1^{(m)}\;(1-\frac{1}{2^{n}},\frac{1}{2^{n}})\geq
1-\frac{1}{2^{n+m-1}}$ for every $n\geq 2$, $m\geq 1$ by induction on $n$.
When $m=1$, we have:

$\textit{Treegen}_{\\_}1^{(1)}\;\left(1-\frac{1}{2^{n}},\frac{1}{2^{n}}\right)=\left(1-\frac{1}{2^{n}}\right)+\frac{1}{2^{n}}\cdot
0=1-\frac{1}{2^{n}}=1-\frac{1}{2^{n+m-1}}.$

About the inductive step, we have

$\displaystyle\textit{Treegen}_{\\_}1^{(m+1)}\;\left(1-\frac{1}{2^{n}},\frac{1}{2^{n}}\right)$
$\displaystyle=1-\frac{1}{2^{n}}+\frac{1}{2^{n}}\cdot\left(\textit{Treegen}_{\\_}1^{(m)}\;\left(1-\frac{1}{2^{n+1}},\frac{1}{2^{n+1}}\right)\right)^{3}$
$\displaystyle\geq
1-\frac{1}{2^{n}}+\frac{1}{2^{n}}\cdot\left(1-\frac{1}{2^{n+m}}\right)^{3}$
$\displaystyle\geq
1-\frac{1}{2^{n}}+\frac{1}{2^{n}}\cdot\left(1-3\frac{1}{2^{n+m}}\right)$
$\displaystyle\geq 1-\frac{1}{2^{2n+m-2}}\geq 1-\frac{1}{2^{n+(m+1)-1}}$

as required. Thus,

$\textit{Treegen}_{\\_}1^{(m)}\left(\frac{1}{2},\frac{1}{2}\right)=\frac{1}{2}+\frac{1}{2}\left(\textit{Treegen}_{\\_}1^{(m-1)}\left(1-\frac{1}{2^{2}},\frac{1}{2^{2}}\right)\right)^{3}\geq\frac{1}{2}+\frac{1}{2}\left(1-\frac{1}{2^{(2+(m-1)-1)}}\right)^{3}$

for every $m\geq 2$. Thus,
$\rho(S_{\\_}1)=\rho(\textit{Treegen}_{\\_}1)(\frac{1}{2},\frac{1}{2})$ (which
should be no less than
$\textit{Treegen}_{\\_}1^{(m)}\;(\frac{1}{2},\frac{1}{2})$ for every $m$) must
be $1$. ∎

#### Correctness of the Translation

To state the well-formedness of the output of the translation, we define the
translation of types as follows.

$\begin{array}[]{l}{(\kappa_{\\_}1\to\cdots\to\kappa_{\\_}k\Rightarrow\mathtt{o}^{\ell}\to\mathtt{o})}^{\dagger}\\\
=({\kappa_{\\_}1}^{\dagger}\to\cdots\to{\kappa_{\\_}k}^{\dagger}\to\mathtt{R})\times({\kappa_{\\_}1}^{\dagger^{\prime}}\to\cdots\to{\kappa_{\\_}k}^{\dagger^{\prime}}\to\mathtt{R})^{\ell}\times({\kappa_{\\_}1}^{\dagger}\to\cdots\to{\kappa_{\\_}k}^{\dagger}\to\mathtt{R})\\\
{(\kappa_{\\_}1\to\cdots\to\kappa_{\\_}k\Rightarrow\mathtt{o}^{\ell}\to\mathtt{o})}^{\dagger^{\prime}}\\\
=({\kappa_{\\_}1}^{\dagger^{\prime}}\to\cdots\to{\kappa_{\\_}k}^{\dagger^{\prime}}\to\mathtt{R})^{\ell}\times({\kappa_{\\_}1}^{\dagger}\to\cdots\to{\kappa_{\\_}k}^{\dagger}\to\mathtt{R}).\end{array}$

We also write
${(\kappa_{\\_}1\to\cdots\to\kappa_{\\_}k\Rightarrow\mathtt{o}^{\ell}\to\mathtt{o})}^{\dagger+{m}}$
for

$\begin{array}[]{l}({\kappa_{\\_}1}^{\dagger}\to\cdots\to{\kappa_{\\_}k}^{\dagger}\to\mathtt{R})\times({\kappa_{\\_}1}^{\dagger^{\prime}}\to\cdots\to{\kappa_{\\_}k}^{\dagger^{\prime}}\to\mathtt{R})^{\ell}\times({\kappa_{\\_}1}^{\dagger}\to\cdots\to{\kappa_{\\_}k}^{\dagger}\to\mathtt{R})^{m+1}.\end{array}$

It represents the type of the tuple $(e_{\\_}0,\ldots,e_{\\_}{\ell+m+1})$
obtained by translating a term of type
$\kappa_{\\_}1\to\cdots\to\kappa_{\\_}k\Rightarrow\mathtt{o}^{\ell}\to\mathtt{o}$
with order-0 variables $x_{\\_}1,\ldots,x_{\\_}m$. The distinction between
${\kappa_{\\_}i}^{\dagger}$ and ${\kappa_{\\_}i}^{\dagger^{\prime}}$ reflects
the fact that in the output
$(e_{\\_}0,e_{\\_}1,\ldots,e_{\\_}\ell,e_{\\_}{\ell+1},\ldots,e_{\\_}{\ell+m+1})$
of the translation, $e_{\\_}1,\ldots,e_{\\_}\ell$ take one less argument
(recall Tr-App). The translation of the type environment $\mathcal{N}$ for
non-terminals is defined by:

$\begin{array}[]{l}(F_{\\_}1\mathbin{:}\kappa_{\\_}1,\ldots,F_{\\_}k\mathbin{:}\kappa_{\\_}k)^{\dagger}=(F_{\\_}{1,0},\ldots,F_{\\_}{1,\mathtt{ar}(\kappa_{\\_}1)})\mathbin{:}{\kappa_{\\_}1}^{\dagger-1},\ldots,(F_{\\_}{k,0},\ldots,F_{\\_}{k,\mathtt{ar}(\kappa_{\\_}k)})\mathbin{:}\kappa_{\\_}k^{\dagger-1}.\end{array}$

The following lemma states that the output of the translation is well-typed.

######  Lemma 4.10 (Well-typedness of the output of transformation).

Let $\mathcal{G}=(\mathcal{N},\mathcal{R},S)$ be a PHORS. If
$\mathcal{G}\leadsto(\mathcal{E},S_{\\_}1)$, then
${\mathcal{N}}^{\dagger}\vdash\mathcal{E}$ and
${\mathcal{N}}^{\dagger}(S_{\\_}1)=\mathtt{R}$.

As a corollary, it follows that for any order-$n$ PHORS $\mathcal{G}$ (where
$n>0$), the order of $\mathcal{E}^{\mathtt{ref}}_{\mathcal{G}}$ is $n-1$.

The following result is the main theorem of this section, which states the
correctness of the translation.

######  Theorem 4.10.

Let $\mathcal{G}=(\mathcal{N},\mathcal{R},S)$ be an order-$n$ PHORS, Then,
$\mathcal{P}(\mathcal{G},S\,\mathtt{e})=\rho_{\\_}{\mathcal{E}^{\mathtt{ref}}_{\mathcal{G}}}(S_{\\_}1)$.

A proof of the theorem is found in Appendix B.2. Here we only sketch the
proof. We first prove the theorem for _recursion-free_ PHORS (so that any term
is strongly normalizing; see Appendix B.1 for the precise definition), and
extend it to general PHORS $\mathcal{G}$ by using _finite approximations_ of
$\mathcal{G}$, obtained by unfolding each non-terminal a finite number of
times. To show the theorem for recursion-free PHORS, we prove that the
translation relation is preserved by reductions in a certain sense; this is,
however, much more involved than the corresponding proof for Section 4.2: we
introduce an alternative operational semantics for PHORS that uses _explicit_
substitutions. See Appendix B.2 for details.

##  5\. Computing Upper-Bounds of Termination Probability

Theorems 4 and 5 immediately provide procedures for computing _lower_ -bounds
of the termination probability as precisely as we need 333Theorem 1 also
provides a procedure for computing lower-bounds, but the fixpoint
characterizations by Theorems 4 and 5 provide a more efficient procedure. The
termination probability, in other words, is a _recursively enumerable_ real
number (see, e.g. [Cal02]), but it is still open whether it is a _recursive_
one. Indeed, computing good upper-bounds is non-trivial. For example, an
upper-bound for the _greatest_ solution of
$\mathcal{E}^{\mathtt{ref}}_{\mathcal{G}}$ can be easily computed, but it does
not provide a good upper-bound for the _least_ solution of
$\mathcal{E}^{\mathtt{ref}}_{\mathcal{G}}$, unless the solution is unique.
Take, as an example, the trivial PHORS consisting of a single equation $S=S$:
the greatest solution is $1$, while the least is $0$.

In this section, we will describe how _upper approximations_ to the
termination probability can be computed in practice. We focus our attention
mainly on order-2 PHORS, which yield equations over first-order functions on
real numbers. Order-$n$ case is only briefly discussed in Section 5.3.

###  5.1. Properties of the Fixpoint Equations Obtained from PHORS

Before discussing how to compute an upper-bound of the termination
probability, we first summarize several important properties of the (order-1)
fixpoint equations obtained from an order-2 PHORS (by the translation in
Section 4.3), which are exploited in computing upper-bounds.

  1. (1)

The fixpoint equations can be written in the form:

$f_{\\_}1(x_{\\_}1,\ldots,x_{\\_}{\ell_{\\_}1})=e_{\\_}1,\qquad\cdots\qquad
f_{\\_}k(x_{\\_}1,\ldots,x_{\\_}{\ell_{\\_}k})=e_{\\_}k,$ (1)

where each $e_{\\_}i$ consists of (i) non-negative constants, (ii) additions,
(iii) multiplications, and (iv) function applications. Each variable
$x_{\\_}i$ ranges over $[0,1]$.

  2. (2)

The formal arguments $x_{\\_}1,\ldots,x_{\\_}{\ell_{\\_}i}$ of each function
$f_{\\_}i$ can be partitioned into several groups of variables
$(x_{\\_}1,\ldots,x_{\\_}{d_{\\_}{i,1}}),(x_{\\_}{d_{\\_}{i,1}+1},\ldots,x_{\\_}{d_{\\_}{i,2}}),\ldots,(x_{\\_}{d_{\\_}{g_{\\_}{i}-1}+1},\ldots,x_{\\_}{\ell_{\\_}i})$,
so that the relevant input values are those such that _the sum_ of the values
of the variables in each group ranges over $[0,1]$. This is because each group
of variables $(x_{\\_}{d_{\\_}{i,j-1}+1},\ldots,x_{\\_}{d_{\\_}{i,h}})$ either
corresponds to an order-$0$ argument (and has thus length $1$) or to an
order-$1$ argument of an order-2 function $F_{\\_}i$ of the original PHORS,
where one of the variables represents the probability that $F_{\\_}i$
terminates without using any arguments, and each of the other variables
represents the probability that $F_{\\_}i$ uses each argument of $F_{\\_}i$.
Since these events are mutually exclusive, the sum of those values ranges over
$[0,1]$.

  3. (3)

The functions $f_{\\_}1,\ldots,f_{\\_}k$ can also be partitioned into several
groups of functions
$(f_{\\_}1,\ldots,f_{\\_}{j_{\\_}1}),(f_{\\_}{j_{\\_}1+1},\ldots,f_{\\_}{j_{\\_}2}),\ldots,(f_{\\_}{j_{\\_}{\ell-1}+1},\ldots,f_{\\_}{j_{\\_}\ell})$,
so that the sum
$f_{\\_}{j_{\\_}{m-1}+1}(\widetilde{x})+\cdots+f_{\\_}{j_{\\_}m}(\widetilde{x})$
of the return values of the functions in each group ranges over $[0,1]$
(assuming that the arguments $\widetilde{x}$ are in the valid domain, i.e.,
the sum of $\widetilde{x}$ ranges over $[0,1]$). This is because an order-2
function $F_{\\_}i$ is translated to a tuple of order-1 functions
$(F_{\\_}{i,0},\ldots,F_{\\_}{i,j})$, and the components of the tuple return
the probabilities to reach mutually different targets.444According to the
translation in Section 4.3, the first element $F_{\\_}{i,0}$ takes one more
argument than the other elements; for the sake of simplicity, we assume in
this section that all the functions in each partition take the same number of
arguments, by adding dummy arguments as necessary. We write $\mathtt{fgrp}(f)$
for the partition that $f$ belongs to, i.e.,
$\mathtt{fgrp}(f_{\\_}i)=\\{f_{\\_}{j_{\\_}{m-1}+1},\ldots,f_{\\_}{j_{\\_}m}\\}$
if $j_{\\_}{m-1}+1\leq i\leq j_{\\_}m$.

  4. (4)

Suppose that $(x_{\\_}1,\ldots,x_{\\_}{\ell_{\\_}i})$ ranges over the valid
domain of $f_{\\_}i$. Then, the value of each subexpression of $e_{\\_}i$
ranges over $[0,1]$; this is because each subexpression represents some
probability. This invariant is not necessarily preserved by simplifications
like $\frac{1}{2}x+\frac{1}{2}y=\frac{1}{2}(x+y)$; the value of $x+y$ may not
belong to $[0,1]$. We apply simplifications only so that the invariant is
maintained.

The properties above can be easily verified by inspecting the translations
from Section 4.3.

Finally, another important property is pointwise convexity. The least solution
$f$ of the fixpoint equations, as well as any finite approximations obtained
from $\bot$ by Kleene iterations, are _pointwise convex_ , i.e., convex on
each variable, i.e.,
$f(x_{\\_}1,\ldots,(1-p)x+py,\ldots,x_{\\_}n)\leq(1-p)f(x_{\\_}1,\ldots,x,\ldots,x_{\\_}n)+pf(x_{\\_}1,\ldots,y,\ldots,x_{\\_}n)$
whenever $0\leq p\leq 1$ and $0\leq x,y$. Note, however, that $f$ is not
necessarily convex in the usual sense:
$f((1-p)\vec{x}+p\vec{y})\leq(1-p)f(\vec{x})+pf(\vec{y})$ may not hold for
some $\vec{0}\leq\vec{x},\vec{y}$ and $0\leq p\leq 1$. For example, let
$f(x_{\\_}1,x_{\\_}2)$ be $x_{\\_}1\cdot x_{\\_}2$. Then,
$\frac{1}{4}=f\left(\frac{1}{2},\frac{1}{2}\right)=f\left(\frac{1}{2}(0,1)+\frac{1}{2}(1,0)\right)>\frac{1}{2}f(0,1)+\frac{1}{2}f(1,0)=0$.
Recall that $\mathcal{F}_{\\_}{\mathcal{E}^{\mathtt{ref}}_{\mathcal{G}}}$ is
the functional associated with the fixpoint equations
$\mathcal{E}^{\mathtt{ref}}_{\mathcal{G}}$; we simply write $\mathcal{F}$ for
$\mathcal{F}_{\\_}{\mathcal{E}^{\mathtt{ref}}_{\mathcal{G}}}$ below.

######  Lemma 5.1.

$\mathcal{F}^{m}(\bot)$ and $\mathbf{lfp}(\mathcal{F})$ are both pointwise
convex. They are also monotonic.

######  Proof 5.2.

The pointwise convexity and monotonicity of $\mathcal{F}^{m}(\bot)$ follow
from the fact that, following our first observation, it is (a tuple of) multi-
variate polynomials with non-negative integer coefficients. The pointwise
convexity of $\mathbf{lfp}(\mathcal{F})$ follows from the fact that, for every
$m$, when $\vec{x}$ and $\vec{y}$ differ by at most one coordinate,

$\begin{array}[]{lcl}(1-p)\mathbf{lfp}(\mathcal{F})(\vec{x})+p\mathbf{lfp}(\mathcal{F})(\vec{y})&\geq&(1-p)\mathcal{F}^{m}(\bot)(\vec{x})+p\mathcal{F}^{m}(\bot)(\vec{y})\\\
&\geq&\mathcal{F}^{m}(\bot)((1-p)\vec{x}+p\vec{y})\end{array}$

and we can then take the supremum to conclude. The monotonicity of
$\mathbf{lfp}(\mathcal{F})$ also follows from a similar argument.

###  5.2. Computing an Upper-Bound by Discretization

Given fixpoint equations as in (1), we can compute an upper-bound of the least
solution of the equations, by overapproximating the values of
$f_{\\_}1,\ldots,f_{\\_}k$ at a finite number of discrete points, _à la_
“Finite Element Method”. To clarify the idea, we first describe a method for
the simplest case of a single equation $f(x)=e$ on a unary function in Section
5.2.1. We then extend it to deal with a _binary_ function in Section 5.2.2,
and discuss the general case (where we need to deal with _multiple equations
on multi-variate functions_) in Section 5.2.3.

####  5.2.1. Computing an Upper-Bound for a Unary Function

Suppose that we are given a PHORS $\mathcal{G}$ and that
$\mathcal{E}^{\mathtt{ref}}_{\mathcal{G}}$ consists of a single equation
$f(x)=e$, where $f$ is a function $f$ from $[0,1]$ to $[0,1]$, and where $e$
consists of non-negative real constants, the variable $x$, additions,
multiplications, and applications of $f$. We abstract $f$ to a sequence of
real numbers $(r_{\\_}0,\ldots,r_{\\_}n)\in[0,1]^{n+1}$, where $r_{\\_}i$
represents the value of $f(\frac{i}{n})$. Thus, the abstraction function
$\alpha$ mapping any function $f:[0,1]\rightarrow[0,1]$ to its abstract form
$[0,1]^{n+1}$ is defined by

$\alpha(f)=\left(f\left(\frac{0}{n}\right),f\left(\frac{1}{n}\right),\ldots,f\left(\frac{n}{n}\right)\right).$

We write $\gamma$ for any concretization function, mapping any element of
$[0,1]^{n+1}$ back to a function in $[0,1]\rightarrow[0,1]$. The idea here is
that _if $\gamma$ satisfies certain assumptions_, to be given later in Lemma
5.3, then we can obtain an upper-bound of the least solution of
$f=\mathcal{F}(f)$ by solving the following system of inequalities on the real
numbers $\vec{r}=(r_{\\_}0,\ldots,r_{\\_}n)$:

$\vec{r}\geq\alpha(\mathcal{F}(\gamma(\vec{r}))).$ (2)

Let $\widehat{\mathcal{F}}$ be the functional $\mathop{\hbox
to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}\vec{s}.\alpha(\mathcal{F}(\gamma(\vec{s})))$.
Notice that solutions to (2) are precisely the pre-fixpoints of
$\widehat{\mathcal{F}}$, and we will thus call them _abstract pre-fixpoints_
of $\mathcal{F}$.

There are at least two degrees of freedom here:

  1. (1)

How could we define the concretization function? Here we have at least two
choices (see Figure 6):

     * (a)

$\gamma(\vec{r})$ could be the _step function_ $\hat{f}$ such that
$\hat{f}(0)=r_{\\_}0$ and $\hat{f}(x)=r_{\\_}i$ if
$x\in(\frac{i-1}{n},\frac{i}{n}]$.

     * (b)

$\gamma(\vec{r})$ could be the _piecewise linear function_ $\hat{f}$ such that
$\hat{f}(x)=r_{\\_}i+\frac{x-\frac{i}{n}}{\frac{1}{n}}(r_{\\_}{i+1}-r_{\\_}i)(=(i+1-nx)r_{\\_}i+(nx-i)r_{\\_}{i+1})$
if $x\in[\frac{i}{n},\frac{i+1}{n}]$.

The discussion above on abstract pre-fixpoints suggests that it is natural to
require that $(\alpha,\gamma)$ satisfies a Galois connection-like property.
The first choice indeed turns $(\alpha,\gamma)$ into a Galois connection
between the set of monotonic functions and that of non-decreasing sequences of
real numbers. The second choice of $(\alpha,\gamma)$ is not exactly a Galois
connection (because $\alpha(f)\leq\vec{r}$ does not imply
$f\leq\gamma(\vec{r})$ if $f$ is not convex), but is quite close: if an
abstraction $\vec{r}$ majorizes $\alpha(f)$ for some pointwise convex function
$f$, we immediately have $\gamma(\vec{r})\geq f$. This way, $\gamma$ satisfies
the assumption of Lemma 5.3 below.

  2. (2)

How could we solve inequalities? Again, we have at least two choices.

     * (c)

Use the decidability of _theories of real arithmetic_ (e.g., minimize
$\sum_{\\_}ir_{\\_}i$ so that all the inequalities are satisfied).

     * (d)

_Abstract_ also the values of $\vec{r}$ so that they can take only finitely
many discrete values, say, $0,\frac{1}{m},\ldots,\frac{m-1}{m},1$. The
inequality (2) is then replaced by:

$\vec{s}\geq\alpha_{\\_}h(\alpha(\mathcal{F}(\gamma(\vec{s})))),$

where every $s_{\\_}i$ is the “discretized version” of $r_{\\_}i$, and the
abstraction function $\alpha_{\\_}h$, given a tuple of reals as an input,
replaces each element $r\in[0,1]$ with $\frac{\lceil{rm}\rceil}{m}$. Since
they are now inequalities over a _finite_ domain, we can obtain the least
solution by a _finite_ number of Kleene iterations, starting from
$\vec{s}=\vec{0}$.

Figure 6. Overapproximation by a step-function (left) and a stepwise linear
function (right)

The following lemma ensures that the inequality (2) is indeed a sufficient
condition for $\gamma(\vec{r})$ to be an upper-bound on
$\mathbf{lfp}(\mathcal{F})$. Note that both step functions and stepwise linear
functions satisfy the assumption of the lemma below.

######  Lemma 5.3.

Suppose that the concretization function $\gamma$ is monotonic, and that
$\vec{r}\geq\alpha(f)$ implies $\gamma(\vec{r})\geq f$ for every pointwise
convex $f$. Then, any abstract pre-fixpoint of $\mathcal{F}$ is an upper bound
of $\mathbf{lfp}(\mathcal{F})$.

######  Proof 5.4.

First, we show that
$\gamma(\widehat{\mathcal{F}}^{m}(\bot))\geq\mathcal{F}^{m}(\bot)$ holds for
every $m$, by induction on $m$. The base case $m=0$ is trivial, since
$\mathcal{F}^{0}(\bot)=\bot$. If $m>0$, then we have

$\begin{array}[]{l}\widehat{\mathcal{F}}^{m}(\bot)=\alpha(\mathcal{F}(\gamma(\widehat{\mathcal{F}}^{m-1}(\bot))))\geq\alpha(\mathcal{F}(\mathcal{F}^{m-1}(\bot)))=\alpha(\mathcal{F}^{m}(\bot)).\end{array}$

Since, by hypothesis, $\vec{r}\geq\alpha(\mathcal{F}^{m}(\bot))$ implies that
$\gamma(\vec{r})\geq\mathcal{F}^{m}(\bot)$ (since $\mathcal{F}^{m}(\bot)$ is
pointwise convex), we can conclude that
$\gamma(\widehat{\mathcal{F}}^{m}(\bot))\geq\mathcal{F}^{m}(\bot)$. Now,
suppose $\vec{r}$ is an abstract pre-fixpoint of $\mathcal{F}$. Then
$\gamma(\vec{r})\geq\gamma(\widehat{\mathcal{F}}^{m}(\vec{r}))\geq\gamma(\widehat{\mathcal{F}}^{m}(\bot))\geq\mathcal{F}^{m}(\bot)$,
and as $\mathcal{F}$ is $\omega$-continuous, we have
$\gamma(\vec{r})\geq\sup_{\\_}{m\in\omega}\mathcal{F}^{m}(\bot)=\mathbf{lpf}(\mathcal{F})$
as required.

Below we consider the combination of (b) and (d). Figure 7 shows a pseudo code
for computing an upper-bound of $f(c)$ for the least solution $f$ of $f(x)=e$
and $c\in[0,1]$. In the figure, $\alpha_{\\_}h(x)=\frac{\lceil{mx}\rceil}{m}$.
The algorithm terminates under the assumptions that (i) $e$ consists of non-
negative constants, $x$, $+$, $\cdot$, and applications of $f$, and (ii) every
subexpression of $e$ evaluates to a value in $[0,1]$ (if $x\in[0,1]$ and
$f\in[0,1]\to[0,1]$), which are satisfied by the fixpoint equations obtained
from a PHORS (recall Section 5.1).

    main($e$, $c$){
      $r$ := $[0,\ldots,0]$;  $r^{\prime}$ := $[1,\ldots,1]$ (* dummy *);
      while not($r$=$r^{\prime}$) do {
        $r^{\prime}$ := $r$; (* copy the contents of array $r$ to $r^{\prime}$ *)
        for each $i\in\{0,\ldots,n\}$ do $r^{\prime}[i]$ := $\alpha_h$(eval($e$, $\{f\mapsto r,x\mapsto\frac{i}{n}\}$))};
      return apply($r$, $c$); }
    apply($r$, $c$) { (* apply the function represented by array $r$ to $c$ *)
      $i$ := $\lfloor{nc}\rfloor$; (* $\frac{i}{n}\leq c<\frac{i+1}{n}$ *)
      return $(i+1-nc)r[i]+(nc-i)r[i+1]$; }
    eval($e$, $\rho$){
      match $e$ with
         $x$ $\to$ return $\rho(x)$ |  $c$ $\to$ return $c$
       | $f(e^{\prime})$ $\to$ return apply($\rho(f)$, eval($e^{\prime}$, $\rho$))
       | $e_1+e_2$ $\to$ return eval($e_1$,$\rho$)+eval($e_2$,$\rho$)
       | $e_1\cdot{}e_2$ $\to$ return eval($e_1$,$\rho$)$\cdot$eval($e_2$,$\rho$) }