Figure 7. Pseudo code for computing an upper-bound of $f(c)$ where $f(x)=e$
(unary function case)

######  Example 5.5.

Consider $f(x)=\frac{1}{4}x+\frac{3}{4}f(f(x))$ and let $n=2$ and $m=4$. The
value $r^{(j)}$ of $r$ after the $j$-th iteration is given by:

$r^{(0)}=[0,0,0];\qquad r^{(1)}=[0,0.25,0.25];\qquad
r^{(2)}=[0,0.25,0.5];\qquad r^{(3)}=[0,0.25,0.5].$

Thus, the upper-bound obtained for $f(1)$ is $0.5$. The exact value of
$f(1)=\frac{1}{3}$. A more precise upper-bound is obtained by increasing the
values of $n$ and $m$. For example, if $n=16$ and $m=256$, the upper-bound
(obtained by running the tool reported in a later section) is $0.3398\cdots$.
∎

####  5.2.2. Computing an upper-bound for a binary function

We now consider a fixpoint equation of the form $f(x_{\\_}1,x_{\\_}2)=e$,
where $x_{\\_}1$ and $x_{\\_}2$ are such that $0\leq x_{\\_}1,x_{\\_}2$, and
$x_{\\_}1+x_{\\_}2\leq 1$. Such an equation is obtained from an order-2 PHORS
by using the fixpoint characterization in the previous section. A new
difficulty compared with the unary case is that $f(x_{\\_}1,x_{\\_}2)$ may
take a value outside $[0,1]$, or may even be undefined for
$(x_{\\_}1,x_{\\_}2)\in[0,1]\times[0,1]$ such that $x_{\\_}1+x_{\\_}2>1$.
Figure 8 shows how we discretize the domain of $f$. The grey-colored and red-
colored areas show the valid domain of $f$, for which we wish to approximate
$f(x_{\\_}1,x_{\\_}2)$ using the values at discrete points. An upper-bound of
the value of $f$ at a point $(x_{\\_}1,x_{\\_}2)$ in the grey area can be
obtained by (pointwise) linear interpolations from (upper-bounds of) the
values at the surrounding four points, i.e.,
$(\frac{i_{\\_}1}{n},\frac{i_{\\_}2}{n}),(\frac{i_{\\_}1}{n},\frac{i_{\\_}2+1}{n}),(\frac{i_{\\_}1+1}{n},\frac{i_{\\_}2}{n}),(\frac{i_{\\_}1+1}{n},\frac{i_{\\_}2+1}{n})$
where $x_{\\_}1\in[\frac{i_{\\_}1}{n},\frac{i_{\\_}1+1}{n}]$ and
$x_{\\_}2\in[\frac{i_{\\_}2}{n},\frac{i_{\\_}2+1}{n}]$, as follows.

$\begin{array}[]{l}\hat{f}(x_{\\_}1,x_{\\_}2)\\\
=(i_{\\_}2+1-nx_{\\_}2)\hat{f}(x_{\\_}1,\frac{i_{\\_}2}{n})+(nx_{\\_}2-i_{\\_}2)\hat{f}(x_{\\_}1,\frac{i_{\\_}2+1}{n})\\\
=(i_{\\_}2+1-nx_{\\_}2)(i_{\\_}1+1-nx_{\\_}1)\hat{f}(\frac{i_{\\_}1}{n},\frac{i_{\\_}2}{n})\\\
\qquad+(i_{\\_}2+1-nx_{\\_}2)(nx_{\\_}1-i_{\\_}1)\hat{f}(\frac{i_{\\_}1+1}{n},\frac{i_{\\_}2}{n})\\\
\qquad+(nx_{\\_}2-i_{\\_}2)(i_{\\_}1+1-nx_{\\_}1)\hat{f}(\frac{i_{\\_}1}{n},\frac{i_{\\_}2+1}{n})\\\
\qquad+(nx_{\\_}2-i_{\\_}2)(nx_{\\_}1-i_{\\_}1)\hat{f}(\frac{i_{\\_}1+1}{n},\frac{i_{\\_}2+1}{n}).\end{array}$

Note that $\hat{f}(x,y)\geq f(x,y)$ at the four points imply that
$\hat{f}(x_{\\_}1,x_{\\_}2)\geq f(x_{\\_}1,x_{\\_}2)$, because $f(x,y)$ is
convex on each of $x$ and $y$ (recall Section 5.1).

Figure 8. Discretization in the case of a binary function $f(x,y)$, whose
domain is $\\{(x,y)\mid 0\leq x,0\leq y,x+y\leq 1\\}$ (i.e., the grey and red
areas). Outside the domain, the value of $f(x,y)$ may not belong to $[0,1]$,
or may be even undefined. The value at a point in the grey area can be
estimated by using those at discrete points $\bullet$. To estimate the value
at a point in the red area, we also need the value of $f(x,y)$ at a point
marked by
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\Diamond}$.

A difficulty is that to estimate the value of $f$ at a point in the red area,
we need the value at a red point $\Diamond$, but the value of $f$ at the red
point may be greater than 1 or even $\infty$, being outside $f$’s domain. To
this end, we discretize the codomain of $f$ to
$\\{0,\frac{1}{m},\ldots,\frac{mh-1}{m},h,\infty\\}$ (instead of
$\\{0,\frac{1}{m},\ldots,\frac{m-1}{m},1\\}$) for some $h\geq 1$. Any value
greater than $h$ is approximated to $\infty$. The value at a point in the red
area is then approximated in the same way as for the case of a point in the
grey area, except that if
$\hat{f}(\frac{i_{\\_}1+1}{m},\frac{i_{\\_}2+1}{m})=\infty$, then
$\hat{f}(x_{\\_}1,x_{\\_}2)=1$.

A further complication arises when the equation contains function
compositions, as in $f(x_{\\_}1,x_{\\_}2)=E[f(f(x_{\\_}1,x_{\\_}2),x_{\\_}2)]$
where $E$ denotes some context. In this case, the point
$(\hat{f}(x_{\\_}1,x_{\\_}2),x_{\\_}2)$ may even be outside the area
surrounded by $\Diamond$ and $\bullet$-points either if $(x_{\\_}1,x_{\\_}2)$
is a $\Diamond$-point or if $(x_{\\_}1,x_{\\_}2)$ is a $\bullet$-point but
$\hat{f}(x_{\\_}1,x_{\\_}2)+x_{\\_}2$ is too large due to an
overapproximation. In such a case, $(\hat{f}(x_{\\_}1,x_{\\_}2),x_{\\_}2)$
belongs to the purple area (lower left triangles) in the figure. To this end,
we also compute (upper-bounds of) the values at points marked by $\triangle$
and use them to estimate the value at a point in the purple area. If the point
$(\hat{f}(x_{\\_}1,x_{\\_}2),x_{\\_}2)$ is even outside the area surrounded by
$\bullet$, $\Diamond$, or $\triangle$, then we use $\infty$ as an upper-bound
of $f(f(x_{\\_}1,x_{\\_}2),x_{\\_}2)$ if $(x_{\\_}1,x_{\\_}2)$ is a
$\Diamond$-, or $\triangle$-point, and $1$ if $(x_{\\_}1,x_{\\_}2)$ is a
$\bullet$-point.

Except the above differences, the overall algorithm is similar to the unary
case in Figure 7, and essentially the same soundness argument as Lemma 5.3
applies.

######  Example 5.6.

Consider $f(x_{\\_}1,x_{\\_}2)=x_{\\_}1+x_{\\_}2(f(x_{\\_}1,x_{\\_}2))^{2}$,
and let $n=m=2$. The value of
$r=\left(\begin{array}[]{ccc}r_{\\_}{0,2}&r_{\\_}{1,2}&r_{\\_}{2,2}\\\
r_{\\_}{0,1}&r_{\\_}{1,1}&r_{\\_}{2,1}\\\
r_{\\_}{0,0}&r_{\\_}{1,0}&r_{\\_}{2,0}\end{array}\right)$, where
$r_{\\_}{i,j}$ is an upper-bound of the value of $f(\frac{i}{2},\frac{j}{2})$,
changes as follows.

$\begin{array}[]{l}\left(\begin{array}[]{ccc}0&0&0\\\ 0&0&0\\\
0&0&0\end{array}\right)\longrightarrow\left(\begin{array}[]{ccc}0&0.5&1\\\
0&0.5&1\\\
0&0.5&1\end{array}\right)\longrightarrow\left(\begin{array}[]{ccc}0&1&\infty\\\
0&1&\infty\\\
0&0.5&1\end{array}\right)\longrightarrow\left(\begin{array}[]{ccc}0&\infty&\infty\\\
0&1&\infty\\\ 0&0.5&1\end{array}\right)\end{array}$

Thus, for example, $f(0,0.5)$ and $f(0.3,0.3)$ are overapproximated
respectively by $0$ and
$0.36\hat{f}(0.5,0.5)+0.24\hat{f}(0.5,0)+0.24\hat{f}(0,0.5)+0.16\hat{f}(0,0)=0.48$.
The exact values for $f(0,0)$ and $f(0.3,0.3)$ are $0$ and $\frac{1}{3}$; so
the upper-bound for $f(0.3,0.3)$ is sound but imprecise. By choosing $n=16$
and $m=256$, we obtain $0.3359\cdots$ as an upper-bound of $f(0.3,0.3)$.

This is an example where the values of $f$ at red points in Figure 8 are
$\infty$. The exact value of $f(x_{\\_}1,x_{\\_}2)$ for general $x_{\\_}1$ and
$x_{\\_}2$ is given by:

$f(x_{\\_}1,x_{\\_}2)=\left\\{\begin{array}[]{ll}x_{\\_}1&\mbox{if
$x_{\\_}2=0$}\\\ \frac{1-\sqrt{1-4x_{\\_}1x_{\\_}2}}{2x_{\\_}2}&\mbox{if
$x_{\\_}1>0$}\end{array}\right.$

Thus, $f(0.5,0.5)=1$, but $f(x_{\\_}1,x_{\\_}2)$ is undefined whenever
$x_{\\_}1x_{\\_}2>0.25$; in particular $f(0.5,1)$ and $f(1,0.5)$ (the values
of red points in Figure 8 for the case $n=2$) are undefined. ∎

####  5.2.3. Computing an Upper-Bound: General Case

The binary case discussed above can be easily extended to handle the general
case, where the goal is to estimate the value of
$f_{\\_}1(c_{\\_}1,\ldots,c_{\\_}{\ell_{\\_}1})$ for the least solution of the
fixpoint equations:

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

Here, the formal arguments $x_{\\_}1,\ldots,x_{\\_}{\ell_{\\_}i}$ of each
function $f_{\\_}i$ are partitioned into several groups
$(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 sum of the values of the variables in each group ranges over
$[0,1]$. Following the binary case, we discretize the domain so that each
variable ranges over $\\{0,\frac{1}{n},\ldots,\frac{n-1}{n},1\\}$, where the
variables in each group
$(x_{\\_}{d_{\\_}{i,j-1}+1},\ldots,x_{\\_}{d_{\\_}{i,j}})$ are constrained by
$x_{\\_}{d_{\\_}{i,j-1}+1}+\cdots+x_{\\_}{d_{\\_}{i,j}}\leq\frac{n+2}{n}$.
Note that we choose $\frac{n+2}{n}$ instead of $1$ as the upper-bound of the
sum, to include the points $\Diamond$ and $\triangle$ in Figure 8. We write
$D_{\\_}i$ for the discretized domain of function $f_{\\_}i$, and
$D_{\\_}i^{\prime}$ for the subset of $D_{\\_}i$ where the variables in each
group are constrained by
$x_{\\_}{d_{\\_}{i,j-1}+1}+\cdots+x_{\\_}{d_{\\_}{i,j}}\leq 1$; note that
$f_{\\_}i(x_{\\_}1,\ldots,x_{\\_}{\ell_{\\_}i})\in[0,1]$ for
$(x_{\\_}1,\ldots,x_{\\_}{\ell_{\\_}i})\in D_{\\_}i^{\prime}$, but
$f_{\\_}i(x_{\\_}1,\ldots,x_{\\_}{\ell_{\\_}i})$ may be greater than $1$ or
undefined for $(x_{\\_}1,\ldots,x_{\\_}{\ell_{\\_}i})\in D_{\\_}i\setminus
D_{\\_}i^{\prime}$. We also write $\overline{D_{\\_}i}$ for the set
$\\{(x_{\\_}1,\ldots,x_{\\_}{\ell_{\\_}i})\mid(\lceil{nx_{\\_}1}\rceil/n,\ldots,\lceil{nx_{\\_}{\ell_{\\_}i}}\rceil/n)\in
D_{\\_}i\\}$ (i.e., the set of points for which the value of $f_{\\_}i$ can be
approximated by using values at points in $D_{\\_}i$).

The pseudo code for computing an upper-bound of
$f_{\\_}1(c_{\\_}1,\ldots,c_{\\_}{\ell_{\\_}1})$ is given in Figure 9. On the
9th line (“$\texttt{if }\vec{v}\in D_{\\_}i^{\prime}\texttt{ then ...}$”), we
also make use of the constraint that
$\Sigma_{\\_}{f^{\prime}\in\mathtt{fgrp}(f_{\\_}i)}f^{\prime}(\widetilde{v})$
ranges over $[0,1]$ if $\widetilde{v}$ belongs to the valid domain
$D_{\\_}i^{\prime}$ (recall the 3rd property in Section 5.1). We assume that
the procedure $\texttt{lb}(f^{\prime},\widetilde{v})$ returns a sound lower-
bound of $f^{\prime}(\widetilde{v})$, e.g., by using Kleene iteration. See
Remark 5.7 to understand the need for this additional twist.

    main($e_1,\ldots,e_k$, $\vec{c}$){
      $\rho$ := $[f_1\mapsto[\vec{0}],\ldots,f_k\mapsto[\vec{0}]]$;
          (* $\rho(f_i)$ is an array indexed by each element of $D_i$ *)
      $\rho^{\prime}$ := $[f_1\mapsto[\vec{1}],\ldots,f_k\mapsto[\vec{1}]]$; (* dummy *)
      while not($\rho$=$\rho^{\prime}$) do {
        $\rho^{\prime}$ := $\rho$; (* copy the contents *)
        for each $i\in\{0,\ldots,k\}$ do
           for each $\vec{v}\in{}D_i$ do
              let r = eval($e_i$, $\rho\{\vec{x}\mapsto\vec{v}\}$, $\vec{v}\stackrel{{\scriptstyle?}}{{\in}}D^{\prime}_i$) in
                if $\vec{v}\in D^{\prime}_i$ then $\rho^{\prime}(f_i)[\vec{v}]$ := $\alpha_h$(min(r, $1-\Sigma_{f^{\prime}\in\mathtt{fgrp}(f_i)\setminus\{f\}}$ lb($f^{\prime}$, $\vec{v}$)))
                else $\rho^{\prime}(f_i)[\vec{v}]$ := $\alpha_h$(r);
      return apply($\rho(f_1)$, $\vec{c}$); }

    eval($e$, $\rho$, $b$){
     (* $b$ represents whether we are computing the value of $f_i$ in the valid
        domain; in that case, the value of $e$ should range over $[0,1]$. *)
      let $r$ =
        match $e$ with
           $x$ $\to$ $\rho(x)$ | $c$ $\to$ $c$
         | $f_i(\vec{e^{\prime}})$ $\to$ let $\vec{v}$ = eval($\vec{e^{\prime}}$,$\rho$,$b$) in
                     if $\vec{v}\not\in\overline{D_i}$ then $\infty$ else apply($\rho(f_i)$, $\vec{v}$)
         | $e_1+e_2$ $\to$ eval($e_1$, $\rho$, $b$)+eval($e_2$, $\rho$, $b$)
         | $e_1\cdot{}e_2$ $\to$ eval($e_1$, $\rho$, $b$)$\cdot$eval($e_2$, $\rho$, $b$)
      in if $b$ then return min($r$,1) else return $r$ }

Figure 9. Pseudo code for computing an upper-bound for the general case

The function $\alpha_{\\_}h$ takes a real value (or $\infty$) $x$, and returns
the least element in $\\{0,\frac{1}{n},\ldots,\frac{mh-1}{m},h,\infty\\}$ that
is no less than $x$. The function apply in the figure takes the current
approximations of values of $f_{\\_}i$ at the points $D_{\\_}i$ and the
arguments $\vec{v}\in\overline{D_{\\_}i}$, and returns an approximation of
$f_{\\_}i(\vec{v})$. It is given by $\hat{f}(\vec{v})$, where:

$\begin{array}[]{l}\hat{f_{\\_}i}(x_{\\_}1,\ldots,x_{\\_}{\ell_{\\_}i})=\sum_{\\_}{b_{\\_}1,\ldots,b_{\\_}{\ell_{\\_}i}\in\\{0,1\\}}p_{\\_}1^{b_{\\_}1}(1-p_{\\_}1)^{1-b_{\\_}1}\cdots
p_{\\_}{\ell_{\\_}i}^{b_{\\_}{\ell_{\\_}i}}(1-p_{\\_}{\ell_{\\_}i})^{1-b_{\\_}{\ell_{\\_}i}}\hat{f_{\\_}i}\left(\frac{i_{\\_}1+b_{\\_}1}{n},\ldots,\frac{i_{\\_}{\ell_{\\_}i}+b_{\\_}{\ell_{\\_}i}}{n}\right)\end{array}$

Here, $i_{\\_}j=\lfloor{nx_{\\_}j}\rfloor$, $p_{\\_}j=nx-i_{\\_}j$, and
$\hat{f_{\\_}i}(\frac{i_{\\_}1+b_{\\_}1}{n},\ldots,\frac{i_{\\_}m+b_{\\_}m}{n})$
is the current approximation of the value of $f_{\\_}i$ at
$(\frac{i_{\\_}1+b_{\\_}1}{n},\ldots,\frac{i_{\\_}m+b_{\\_}m}{n})\in
D_{\\_}i$. The function $\hat{f}$ above is obtained by applying linear
interpolations coordinate-wise.

######  Remark 5.7.

To see the motivation for the 9th line in Figure 9, consider the following
fixpoint equations:

$\displaystyle S$ $\displaystyle=f_{\\_}1()$ $\displaystyle f_{\\_}1()$
$\displaystyle=0.5\cdot(f_{\\_}1()\cdot f_{\\_}1()+f_{\\_}2()\cdot
f_{\\_}2())$ $\displaystyle f_{\\_}2()$ $\displaystyle=0.5+f_{\\_}1()\cdot
f_{\\_}2().$

They are obtained from the following order-1 PHORS
$\mathcal{G}_{\\_}{\mathtt{treeeven}}$:

$\displaystyle S\,z$ $\displaystyle=F\,z\,\Omega$ $\displaystyle
F\;x_{\\_}1\;x_{\\_}2$
$\displaystyle=x_{\\_}2\,\oplus_{p}\,F\;(F\;x_{\\_}1\;x_{\\_}2)\;(F\;x_{\\_}2\;x_{\\_}1),$

where $p=0.5$, and $f_{\\_}1()$ ($f_{\\_}2()$, resp.) represents the
probability that $x_{\\_}1$ ($x_{\\_}2$, resp.) is used by $F$. This PHORS is
actually a variation of $\mathcal{G}_{\\_}6$ from Example 2.9 (with manual
optimization), whose termination probability represents the probability that a
program that randomly generates binary trees (instead of lists, unlike in the
case of Example 2.9) contains an even number of leaves. Since the events that
$F$ uses the first and second arguments are mutually exclusive, we have the
constraint $f_{\\_}1()+f_{\\_}2()\leq 1$. The exact solution for the equations
above is $f_{\\_}1()=1-\frac{1}{\sqrt{2}}$ and
$f_{\\_}2()=\frac{1}{\sqrt{2}}$. Since their lower-bounds can be computed with
arbitrary precision, thanks to the part
$1-\Sigma_{\\_}{f^{\prime}\in\mathtt{fgrp}(f_{\\_}i)\setminus\\{f\\}}$
lb($f^{\prime}$, $\vec{v}$) of the 9th line of Figure 9, we can also compute
upper-bounds with arbitrary precision (as upper-bounds of $f_{\\_}1()$ and
$f_{\\_}2()$ are respectively provided by $1-\texttt{lb}(f_{\\_}2,())$ and
$1-\texttt{lb}(f_{\\_}1,())$).

If the then-clause were the same as the else-clause on the 10th line, then we
would not get a precise upper-bound for the following reason. When the main
loop in Figure 9 stops, upper-bounds $\overline{f}_{\\_}1()$ and
$\overline{f}_{\\_}2()$ must either have reached the maximal value $1$, or
satisfy:

$\begin{array}[]{l}\overline{f}_{\\_}1()\geq
0.5\cdot(\overline{f}_{\\_}1()\cdot\overline{f}_{\\_}1()+\overline{f}_{\\_}2()\cdot\overline{f}_{\\_}2())\\\
\overline{f}_{\\_}2()\geq
0.5+\overline{f}_{\\_}1()\cdot\overline{f}_{\\_}2().\end{array}$

These conditions imply that:

$\overline{f}_{\\_}1()+\overline{f}_{\\_}2()\geq
0.5\cdot(\overline{f}_{\\_}1()\cdot\overline{f}_{\\_}1()+\overline{f}_{\\_}2()\cdot\overline{f}_{\\_}2())+0.5+\overline{f}_{\\_}1()\cdot\overline{f}_{\\_}2(),$

i.e.,

$0\geq(\overline{f}_{\\_}1()+\overline{f}_{\\_}2()-1)^{2},$

which is equivalent to $\overline{f}_{\\_}1()+\overline{f}_{\\_}2()=1$. Thus,
unless the co-domain of $\alpha_{\\_}h$ contains the exact values
$1-\frac{1}{\sqrt{2}}$ and $\frac{1}{\sqrt{2}}$, the main loop would only
return the imprecise upper-bound
$\overline{f}_{\\_}1()=\overline{f}_{\\_}2()=1$. ∎

###  5.3. Order-$n$ Case

We now briefly discuss how to extend the method discussed above to obtain a
sound (but incomplete) method for overapproximating the termination
probability of PHORS of order greater than 2. Recall that by the fixpoint
characterization given in Section 4.3, it suffices to overapproximate the
least solution of equations of the form $\vec{f}={\mathcal{F}}(\vec{f})$ where
$\vec{f}$ is a tuple of order-($n-1$) functions on reals.

The abstract interpretation framework [Cou97] provides a sound but incomplete
methodology: the reason why we decided to slightly divert from it in Section
5.2 is that this allows us to use piecewise linear functions, which are more
precise. We first recall a basic principle of abstract interpretation. Let
$(C,\sqsubseteq_{\\_}C,\bot_{\\_}C)$ and $(A,\sqsubseteq_{\\_}A,\bot_{\\_}A)$
be $\omega$-cpos. Suppose that
$\alpha:(C,\sqsubseteq_{\\_}C)\to(A,\sqsubseteq_{\\_}A)$ and
$\gamma:(A,\sqsubseteq_{\\_}A)\to(C,\sqsubseteq_{\\_}C)$ are continuous (hence
also monotonic) such that $\alpha(\gamma(a))=a$ for every $a\in A$, and
$c\sqsubseteq_{\\_}C\gamma(\alpha(c))$ for every $c\in C$. Suppose also that
$\mathcal{F}$ is a continuous function from
$(C,\sqsubseteq_{\\_}C,\bot_{\\_}C)$ to $(C,\sqsubseteq_{\\_}C,\bot_{\\_}C)$.
Let
$\widehat{\mathcal{F}}:(A,\sqsubseteq_{\\_}A,\bot_{\\_}A)\to(A,{\sqsubseteq_{\\_}A},\bot_{\\_}A)$
be $\lambda x\in A.\alpha(\mathcal{F}(\gamma(x)))$, which is an “abstract
version” of $\mathcal{F}$. Note that $\widehat{\mathcal{F}}$ is also
continuous. Then, we have:

######  Proposition 5.8.

$\mathbf{lfp}(\mathcal{F})\sqsubseteq_{\\_}C\gamma(\mathbf{lfp}(\widehat{\mathcal{F}}))$.

This result is standard (see, e.g., [Cou97], Proposition 18) but we provide a
proof for the convenience of the reader.

######  Proof 5.9 (Proof of Proposition 5.8).

By the monotonicity of $\mathcal{F}$ and $\widehat{\mathcal{F}}$, we have:
$\bot_{\\_}C\sqsubseteq_{\\_}C\mathcal{F}(\bot_{\\_}C)\sqsubseteq_{\\_}C\mathcal{F}^{2}(\bot_{\\_}C)\sqsubseteq_{\\_}C\cdots$
and
$\bot_{\\_}A\sqsubseteq_{\\_}A\widehat{\mathcal{F}}(\bot_{\\_}A)\sqsubseteq_{\\_}A{\widehat{\mathcal{F}}}^{2}(\bot_{\\_}A)\sqsubseteq_{\\_}A\cdots$;
hence both
${\bigsqcup_{\\_}C}\\{\mathcal{F}^{i}(\bot_{\\_}C)\mid{i\in\omega}\\}$ and
${\bigsqcup_{\\_}A}\\{{\widehat{\mathcal{F}}}^{i}(\bot_{\\_}A)\mid
i\in\omega\\}$ exist, and by the $\omega$-continuity of $\mathcal{F}$ and
$\widehat{\mathcal{F}}$, they are the least fixpoints of $\mathcal{F}$ and
$\widehat{\mathcal{F}}$ respectively. Therefore, it suffices to show that
$\mathcal{F}^{i}(\bot_{\\_}C)\sqsubseteq_{\\_}C\gamma({\widehat{\mathcal{F}}}^{i}(\bot_{\\_}C))$.
The proof proceeds by induction on $i$. The base case $i=0$ is trivial. If
$i>0$, we have:

$\displaystyle\gamma({\widehat{\mathcal{F}}}^{i}(\bot_{\\_}C))$
$\displaystyle=\gamma(\alpha(\mathcal{F}(\gamma({\widehat{\mathcal{F}}}^{i-1}(\bot_{\\_}C)))))$
(by the definition of $\widehat{\mathcal{F}}$)
$\displaystyle\sqsupseteq_{\\_}C\mathcal{F}(\gamma({\widehat{\mathcal{F}}}^{i-1}(\bot_{\\_}C)))$
(by $\gamma(\alpha(x))\sqsupseteq_{\\_}Cx$)
$\displaystyle\sqsupseteq_{\\_}C\mathcal{F}(\mathcal{F}^{i-1}(\bot_{\\_}C))$
(by induction hypothesis) $\displaystyle=\mathcal{F}^{i}(\bot_{\\_}C).$

By the proposition above, to overapproximate the least fixpoint of
$\mathcal{F}$, it suffices to find an appropriate abstract domain
$(A,\sqsubseteq_{\\_}A,\bot_{\\_}A)$ and $\alpha,\gamma$ that satisfy the
conditions above, so that the least fixpoint of $\widehat{\mathcal{F}}$ is
easily computable. In the case of overapproximation of the termination
probability of order-$n$ PHORS, we need to set up an abstract domain
$(A,\sqsubseteq_{\\_}A,\bot_{\\_}A)$ for a tuple of order-($n-1$) functions on
reals. A simple solution (that is probably too naive in practice) is to use
the abstract domain consisting of higher-order step functions, inductively
defined by:

$\displaystyle A^{\mathtt{R}}$
$\displaystyle=\\{\frac{0}{m},\frac{1}{m},\ldots,\frac{m-1}{m},\frac{m}{m},\infty\\}$
$\displaystyle\sqsubseteq_{\\_}{A^{\mathtt{R}}}$
$\displaystyle=\\{(\frac{i}{m},\frac{j}{m})\mid 0\leq i\leq j\leq
m\\}\cup\\{(\frac{i}{m},\infty)\mid 0\leq i\leq m\\}$
$\displaystyle\alpha^{\mathtt{R}}(x)$
$\displaystyle=\left\\{\begin{array}[]{ll}\frac{i}{m}&\mbox{if
$\frac{i-1}{m}\leq x\leq\frac{i}{m}$}\\\ \infty&\mbox{if
$x>1$}\end{array}\right.$ $\displaystyle\gamma^{\mathtt{R}}(x)$
$\displaystyle=x$ $\displaystyle A^{\tau_{\\_}1\to\tau_{\\_}2}$
$\displaystyle=\\{f\in A^{\tau_{\\_}1}\to A^{\tau_{\\_}2}\mid\mbox{$f$ is
monotonic}\\}$ $\displaystyle\sqsubseteq_{\\_}{A^{\tau_{\\_}1\to\tau_{\\_}2}}$
$\displaystyle=\\{(f_{\\_}1,f_{\\_}2)\in A^{\tau_{\\_}1\to\tau_{\\_}2}\times
A^{\tau_{\\_}1\to\tau_{\\_}2}\mid\forall x\in
A^{\tau_{\\_}1\to\tau_{\\_}2}.f_{\\_}1\,x\sqsubseteq_{\\_}{A^{\tau_{\\_}2}}f_{\\_}2\,x\\}$
$\displaystyle\alpha^{\tau_{\\_}1\to\tau_{\\_}2}(f)$
$\displaystyle=\\{(y,\alpha^{\tau_{\\_}2}(f(\gamma^{\tau_{\\_}1}(y))))\mid
y\in A^{\tau_{\\_}1}\\}$
$\displaystyle\gamma^{\tau_{\\_}1\to\tau_{\\_}2}(f^{\prime})$
$\displaystyle=\\{(x,\gamma^{\tau_{\\_}2}(f^{\prime}(\alpha^{\tau_{\\_}1}(x))))\mid
x\in C^{\tau_{\\_}1}\\}.$

Here, the concrete domain $C^{\tau}$ denotes $\llbracket{\tau}\rrbracket$ in
Section 4.1. Then, $\alpha^{\tau}$ and $\beta^{\tau}$ satisfy the required
conditions ($\alpha(\gamma(a))=a$ and $c\sqsubseteq_{\\_}C\gamma(\alpha(c))$).
Since $A^{\tau}$ is finite, we can effectively compute
$\mathbf{lfp}(\widehat{\mathcal{F}})$.

We note, however, that the above approach has the following shortcomings.
First, although $A^{\tau}$ is finite, its size is too large: $k$-fold
exponential for order-$k$ type $\tau$. As in the case of non-probabilistic
HORS model checking [Kob09a, BK13, RNO14], therefore, we need a practical
algorithm that avoids eager enumeration of abstract elements. Second, due to
the use of step functions, the obtained upper-bound will be too imprecise. To
see why step functions suffer from the incompleteness, consider the equations:
$s=f(\frac{1}{2})$ and $f(x)=\frac{1}{2}x+f(\frac{1}{2}x)$. The exact least
solution is $s=\frac{1}{2}$ and $f(x)=x$. With step functions (where
$\frac{1}{n}$ is the size of each interval), however, the abstract value
$\hat{f}(\frac{1}{n})$ must be no less than
$\frac{1}{2}\frac{1}{n}+f(\frac{1}{2}\cdot\frac{1}{n})$, but
$f(\frac{1}{2}\cdot\frac{1}{n})$ is overapproximated as $\hat{f}(\frac{1}{n})$
(because $\frac{1}{2n}$ belongs to the interval $(0,\frac{1}{n}]$). Therefore,
$\hat{f}(\frac{1}{n})$ should be no less than
$\frac{1}{2n}+\hat{f}(\frac{1}{n})$, which is impossible. Thus, the
computation diverges and $1$ is obtained as an obvious upper bound.

The step functions only use monotonicity of the least solution of fixpoint
equations. As in the use of stepwise multilinear functions in the case of
order-1 equations (for order-2 PHORS), exploiting an additional property like
convexity would be important for obtaining a more precise method; this is left
for future work.

##  6\. Experiments

We have implemented a prototype tool to compute lower/upper bounds of the
least solution of order-1 fixpoint equations (that are supposed to have been
obtained from order-2 or order-1 PHORS by using the translations in Section 4
modulo some simplifications; we have not yet implemented the translators from
PHORS to fixpoint equations, which is easy but tedious). The computation of a
lower bound is based on naive Kleene iterations, and that of an upper-bound is
based on the method discussed in Section 5.2. The tool uses floating point
arithmetic, and ignores rounding errors.

We have tested the tool on several small but tricky examples. The experimental
results are summarized in Table 2. The column “equations” lists the names of
systems of equations. The column “#iter” shows the number of Kleene iterations
used for computing a lower-bound. The columns “#dom” and “#codom” show the
numbers of partitions of the interval $[0,1]$ for the domain and codomain of a
function respectively. The default values for them were set to 12, 16, and
512, respectively in the experiment; they were, however, adjusted for some of
the equations. The columns “l.b.” and “u.b.” are lower/upper bounds computed
by the tool. The lower (upper, resp.) bounds shown in the table have been
obtained by rounding down (up, resp.) the outputs of the tool to 3-decimal
places. The column “step” shows the upper-bounds obtained by using step
functions instead of piecewise linear functions; this column has been prepared
to confirm the advantage of piecewise linear functions over step functions.
The column “exact” shows the exact value of the least solution when we know
it. The column “time” shows the total time for computing both lower and upper
bounds (excluding the time for “step”).

Table 2. Experimental results (times are in seconds). equations | #iter | #dom | #codom | l.b. | u.b. | step | exact | time
---|---|---|---|---|---|---|---|---
Ex2.3-1 | 12 | 16 | 512 | 0.333 | 0.336 | 1.0 | $\frac{1}{3}$ | 0.010
Ex2.3-0 | 12 | 16 | 512 | 0.333 | 0.334 | 0.334 | $\frac{1}{3}$ | 0.008
Ex2.3-v1 | 12 | 16 | 512 | 0.312 | 0.315 | 0.365 | - | 0.005
Ex2.3-v2 | 12 | 16 | 512 | 0.262 | 0.266 | 0.321 | - | 0.022
Ex2.3-v3 | 12 | 16 | 512 | 0.263 | 0.266 | 0.309 | - | 0.01
Ex2.4 | 12 | 16 | 512 | 0.320 | 0.323 | 0.329 | - | 0.011
Double | 12 | 16 | 512 | 0.649 | 0.653 | 1.0 | - | 0.010
Listgen | 15 | 16 | 512 | 0.999 | 1.0 | 1.0 | 1.0 | 0.009
Treegen | 15 | 64 | 4096 | 0.618 | 0.619 | 1.0 | $\frac{\sqrt{5}-1}{2}$ | 0.471
Treegenp | 12 | 16 | 512 | 1.0 | 1.0 | 1.0 | 1.0 | 0.011
ListEven | 12 | 32 | 1024 | 0.666 | 0.667 | 0.667 | $\frac{2}{3}$ | 0.009
ListEven2 | 12 | 16 | 512 | 0.749 | 0.75 | 0.75 | $\frac{3}{4}$ | 0.013
Determinize | 12 | 16 | 512 | 0.993 | 1.0 | 1.0 | 1.0 | 9.64
TreeEven(0.5) | 15 | 64 | 4096 | 0.286 | 0.299 | 0.300 | $1-\frac{1}{\sqrt{2}}$ | 0.050
TreeEven(0.49) | 15 | 64 | 4096 | 0.276 | 0.280 | 0.280 | 0.2774$\cdots$ | 0.052
TreeEven(0.51) | 15 | 64 | 4096 | 0.287 | 0.290 | 0.290 | 0.2887$\cdots$ | 0.055
Ex5.4(0,0) | 12 | 16 | 512 | 0.0 | 0.0 | 0.0 | 0 | 0.008
Ex5.4(0.3,0.3) | 12 | 16 | 512 | 0.333 | 0.336 | 0.35 | $\frac{1}{3}$ | 0.007
Ex5.4(0.5,0.5) | 10000 | 16 | 512 | 0.999 | 1.0 | 1.0 | 1 | 0.010
Discont(0,1) | 12 | 16 | 512 | 0.0 | 0.0 | 0.0 | 0 | 0.006
Discont(0.01,0.99) | 1000 | 16 | 512 | 0.999 | 1.0 | 1.0 | 1 | 0.006
Incomp | 10000 | 16 | 512 | 0.299 | 1.0 | 1.0 | 0.3 | 0.003
Incomp | 10000 | 10 | 100 | 0.299 | 0.3 | 0.3 | 0.3 | 0.003
Incomp2 | 12 | 16 | 512 | 0.249 | 1.0 | 1.0 | 0.25 | 0.003
Incomp2 | 12 | 256 | 65536 | 0.249 | 1.0 | 1.0 | 0.25 | 2.87

The equations “Ex2.3-1” and “Ex2.3-0” are order-1 and order-0 equations
obtained from the PHORS in Example 2.1 (see also Examples 4.4 and 4.6) by
using the translations in Sections 4.2 and 4.3 respectively; specifically,
“Ex2.3-1” consists of $s=f(1)$ and $f(x)=0.25x+0.75f(f(x))$. The equations
“Ex2.3-v1”, “Ex2.3-v2”, and “Ex2.3-v3” are variations of them, where the
equation on $f$ is replaced by $f(x)=0.25x+0.75f(f(x^{2}))$,
$f(x)=0.25x+0.75f(f(f(x^{2})))$, and $f(x)=0.25x+0.75(f(x))^{2}$,
respectively. “Ex2.4” is the equations obtained from the order-2 PHORS in
Example 2.2 (see also Example 4.7). The equations “Double” are those obtained
from the following order-2 PHORS:

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

with manual simplifications. The equations “Listgen”, “Treegen”, and
“Treegenp” are from Example 2.7, corresponding to $\mathcal{G}_{\\_}3$,
$\mathcal{G}_{\\_}4$ and $\mathcal{G}_{\\_}5$, respectively. The equations
“ListEven” and “ListEven2” are from Example 2.9, and “Determinize” is from
Example 2.10. “TreeEven($p$)” (for $p\in\\{0.5,0.49,0.51\\}$) is from Remark
5.7. If we disable the trick (the one on line 9 in Figure 7) we discussed in
the remark, the tool returns an imprecise upper-bound of $1.0$ for $p=0.5$
(for $p=0.49$ and $p=0.51$, however, the tool can compute a precise upper-
bound even without the trick). The equations “Ex5.4($x$,$y$)” (for
$(x,y)\in\\{(0,0),(0.3,0.3),(0.5,0.5)\\}$) are from Example 5.6. The equations
“Discont($p$,$1-p$)” consist of: $s=f(p,1-p)$ and
$f(x_{\\_}0,x_{\\_}1)=x_{\\_}0+x_{\\_}1f(x_{\\_}0,x_{\\_}1)$, which is
obtained from PHORS:

$S=F\,G\qquad F\,g=g\,\mathtt{e}\,(F\,g)\qquad
G\,x_{\\_}0\,x_{\\_}1=x_{\\_}0\,\oplus_{p}\,x_{\\_}1.$

Interestingly, $f$ is discontinuous at $(0,1)$ (in the usual sense of analysis
in mathematics; it is still $\omega$-continuous as functions on
$\omega$-cpo’s): the exact value of $f$ is given by:

$f(x_{\\_}0,x_{\\_}1)=\left\\{\begin{array}[]{ll}0&\mbox{if $x_{\\_}0=0$}\\\
\frac{x_{\\_}0}{1-x_{\\_}1}&\mbox{if $x_{\\_}0>0$}.\end{array}\right.$

The equations “Incomp” and “Incomp2” consist of:

$s=f(s)\qquad\qquad f\,x=x^{2}+0.4x+0.09,$

and

$s=f(s)\qquad\qquad f\,x=0.5x^{2}+2f(0.5x)$

respectively. They do not correspond to any PHORS — in fact, the value of
$f(1)$ for Incomp is $1.49$, which does not make sense as a probability. We
have included them since they show a source of the possible incompleteness of
our method. Indeed, the tool fails to find precise upper bounds. To see why
the tool does not work for Incomp1 (with the the default values of #dom and
#codom), note that since $s=f(s)=s^{2}+0.4s+0.09$,
$\hat{s}\geq\hat{s}^{2}+0.4\hat{s}+0.09$ must be satisfied for any valid
upper-bound $\hat{s}$. However, $\hat{s}\geq\hat{s}^{2}+0.4\hat{s}+0.09$ is
equivalent to $0\geq(\hat{s}-0.3)^{2}$, which is satisfied only by
$\hat{s}=0.3$. So, the only valid upper-bound for $s$ is actually the exact
one $0.3$. But then an upper-bound $\hat{f}$ of $f$ must satisfy
$\hat{f}(0.3)=0.3$, which can be found only if the set of discrete values
(used for abstracting the domain and codomain) contains $0.3$. That is why the
tool returns $1$ (which is the largest value, assuming that $s$ represents a
probability) for the default values of #dom and #codom. When we adjust them to
$10$ and $100$ (so that $0.3$ belongs to the sets of abstract values of
domains and codomains), the precise upper-bound (i.e., $0.3$) is obtained;
this is, however, impossible in general, without knowing the exact solution a
priori.

The reason for “Incomp2” is more subtle. Notice that the least solution for

$s=f(s)\qquad f\,x=0.5x^{2}+2f(0.5x)$

is $f(x)=x^{2}$. Let $\frac{1}{n}$ be the size of each interval used for
abstracting the domain. Suppose that, at some point, an upper-bound of
$f(\frac{1}{n})$ becomes $\frac{c}{n^{2}}$. Due to the linear interpolation
(and since the value at $x=0$ converges to $0$), the value of $f$ at $0.5r$
(which belongs to the domain $(0,\frac{1}{n})$) is overapproximated by
$0.5\cdot\frac{c}{n^{2}}$. Thus, at the next iteration, the upper-bound at
$\frac{1}{n}$ is further updated to a value greater than
$0.5\frac{1}{n^{2}}+2\cdot 0.5\cdot\frac{c}{n^{2}}=\frac{c+0.5}{n^{2}}$. Thus,
the computation of an upper-bound for the value at $x=\frac{1}{n}$ never
converges. In this case, changing the parameters #dom and #codom does not
help. We do not know, however, whether such situations occur in the fixpoint
equations that arise from actual order-2 PHORS; it is left for future work to
see whether our method (or a minor modification of it) is actually complete
(in the sense that upper-bounds can always be computed with arbitrary
precision by increasing the parameters #dom and #codom).

To summarize, for all the _valid_ inputs (i.e., except “Incomp” and “Incomp2”,
which are invalid in the sense that they do not correspond to PHORS), our tool
(with piecewise linear functions) could properly compute lower/upper bounds.
In contrast, from the column “step”, we can observe that the replacement of
piecewise (multi)linear functions with step functions not only worsens the
precision (as in “Ex2.3-v1”, “Ex2.3-v2”, and “Ex2.3-v3”) significantly, but
also makes the procedure obviously incomplete555As already mentioned, our
method with piecewise linear functions may also be incomplete, but that does
not show up in the current benchmark set., as in “Ex2.3-1” and “Double”
(recall the discussion on the incompleteness of step functions in Section
5.3).

##  7\. Related Work

As already mentioned in Section 1, this work is intimately related to both
probabilistic model checking, and higher-order model checking. Let us give
some hints on _how_ our work is related to the two aforementioned research
areas, without any hope to be exhaustive.

Model checking of probabilistic recursive systems. Model checking of
probabilistic systems with _recursion_ (but not higher-order functions), such
as recursive Markov chains and probabilistic pushdown systems, has been
actively studied [EY09, EY15, BBFK14]. Our PHORS are strictly more expressive
than those models, as witnessed by the undecidability result from Section 3,
and the encoding of recursive Markov chains into order-1 PHORSs given in
Appendix A.1. Our fixpoint characterization of the termination probability of
PHORS is a generalization of the fixpoint characterization of the termination
probability for recursive Markov models [EY09] to arbitrary orders. Various
methods have been studied for solving the order-0 fixpoint equations (or,
polynomial equations) obtained from recursive Markov chains [EY09, KLE07,
EGK10]. Interestingly, also in those methods, computing an upper-bound of the
least solution is more involved than computing a lower-bound. It is left for
future work to investigate whether some of the ideas in those methods can be
used also for solving order-1 fixpoint equations.

Termination of probabilistic infinite-data programs. Methods for computing the
termination probabilities of infinite-data programs (with real-valued
variables, but without higher-order recursion) have also been actively
studied, mainly in the realm of imperative programs (see, as an example,
[BG05, EGK12, FH15, CNZ17, MMKK18, ADLY18, CS13]); to the best of our
knowledge, none of those methods deal with higher-order programs, at least
directly. All these pieces of work present sound but _incomplete_
methodologies for checking almost sure termination of programs. Incompleteness
is of course inevitable due to the Turing completeness of the underlying
language considered. In fact, Kaminsiki and Katoen [KK15] have shown that
almost sure termination of probabilistic imperative programs is
$\Pi_{\\_}2^{0}$-complete. Since their proof relies on Turing completeness of
the underlying language, it does not apply to the setting of our model PHORS,
which is a probabilistic extension of a Turing-_incomplete_ language, namely
that of HORS.

Model checking of higher-order programs. Model checking of (non-probabilistic)
higher-order programs has been an active topic of research in the last fifteen
years, with many positive results [KNU02, Ong06, HMOS08, Kob13, KO09, KSU11,
GM15b, GM15a, TO14, SW11, Par18]. Strikingly, not only termination, but also a
much larger class of properties (those expressible in the modal
$\mu$-calculus) are known to be decidable for ordinary (i.e. non-
probabilistic) HORS. This is in stark contrast with our undecidability result
from Section 3: already at order-2 and for a very simple property like
termination, verification cannot be effectively solved.

Probabilistic functional programs. Probabilistic functional programs have
recently attracted the attention of the programming language community,
although probabilistic $\lambda$-calculi have been known for forty years now
[Sah78, JP89]. Most of the work in this field is concerned with operational
semantics [DZ12], denotational semantics (see, e.g., [JT98, DH02, ETP14,
SYW+16, BFK+18]), or program equivalence (see, e.g., [DSA14, CDL14, SV16]),
which sometimes becomes decidable (e.g. [MO05]), but only when higher-order
recursion is forbidden. The interest in probabilistic higher-order functional
languages stems from their use as a way of writing probabilistic graphical
models, as in languages like Church [GMR+08] or Anglican [WMM14]. There are
some studies to analyze the termination behavior of probabilistic higher-order
programs (with infinite data) by using types. Dal Lago and Grellois [DLG17]
generalized sized types [HPS96, BFG+04] to obtain a sound but highly
incomplete technique. Breuvart and Dal Lago [BL18] developed systems of
intersection types from which the termination probability of higher-order
programs can be inferred from (infinitely many) type derivations. This however
does _not_ lead to any practical verification methodology.

Relevant proof techniques. Our technique (of using the undecidability of
Hilbert’s 10th problem) for proving the undecidability of almost sure
termination of order-2 PHORS has been inspired by Kobayashi’s proof of
undecidability of the inclusion between order-2 (non-probabilistic) word
languages and the Dyck language [Kob19]. Other undecidability results on
probabilistic systems include the undecidability of the emptiness of
probabilistic automata [GO10]. Their proof is based on the reduction from Post
correspondence problem. The technique does not seem applicable to our context.

##  8\. Conclusion

We have introduced PHORS, a probabilistic extension of higher-order recursion
schemes, and studied the problem of computing their termination probability.
We have shown that almost sure termination is undecidable. As positive
results, we have also shown that the termination probability of order-$n$
PHORS can be characterized by order-($n-1$) fixpoint equations, which
immediately yields a method for computing a precise lower-bound of the
termination probability. Based on the fixpoint characterization, we have
proposed a sound procedure for computing an upper-bound of the termination
probability, which worked well on preliminary experiments.

It is left for future work to settle the question of whether it is possible to
compute the termination probability with arbitrary precision, which seems to
be a difficult problem. Another direction of future work is to develop a
(sound but incomplete) model checking procedure for PHORS, using the procedure
for computing the termination probability as a backend.

### Acknowledgments

We would like to thank Kazuyuki Asada and Takeshi Tsukada for discussions on
the topic, and anonymous referees for useful comments. This work was supported
by JSPS KAKENHI Grant Number JP15H05706, JP20H00577, and JP20H05703, and by
ANR PPS Grant Number 19-CE48-0014, and by ERC CoG DIAPASoN Grant Agreement
818616.

## References

  * [ADLY18] Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada.  On probabilistic term rewriting.  In John P. Gallagher and Martin Sulzmann, editors, FLOPS 2018, volume 10818 of LNCS, pages 132–148. Springer, 2018.
  * [BBFK14] Tomás Brázdil, Václav Brozek, Vojtech Forejt, and Antonín Kucera.  Branching-time model-checking of probabilistic pushdown automata.  J. Comput. Syst. Sci., 80(1):139–156, 2014.
  * [BEKK13] Tomás Brázdil, Javier Esparza, Stefan Kiefer, and Antonín Kucera.  Analyzing probabilistic pushdown automata.  Formal Methods in System Design, 43(2):124–163, 2013.
  * [BFG+04] Gilles Barthe, Maria João Frade, Eduardo Giménez, Luis Pinto, and Tarmo Uustalu.  Type-based termination of recursive definitions.  MSCS, 14(1):97–141, 2004.
  * [BFK+18] Giorgio Bacci, Robert Furber, Dexter Kozen, Radu Mardare, Prakash Panangaden, and Dana Scott.  Boolean-valued semantics for the stochastic $\lambda$-calculus.  In LICS 2018, pages 669–678, 2018.
  * [BG05] Olivier Bournez and Florent Garnier.  Proving positive almost-sure termination.  In Jürgen Giesl, editor, RTA 2005, volume 3467 of LNCS, pages 323–337. Springer, 2005.
  * [BK08] Christel Baier and Joost-Pieter Katoen.  Principles of Model Checking.  The MIT Press, 2008.
  * [BK13] Christopher H. Broadbent and Naoki Kobayashi.  Saturation-based model checking of higher-order recursion schemes.  In CSL 2013, volume 23 of LIPIcs, pages 129–148, 2013.
  * [BL18] Flavien Breuvart and Ugo Dal Lago.  On intersection types and probabilistic lambda calculi.  In David Sabel and Peter Thiemann, editors, PPDP 2018, pages 8:1–8:13. ACM, 2018.
  * [Cal02] Cristian Calude.  Information and Randomness: An Algorithmic Perspective.  Springer-Verlag, Berlin, Heidelberg, 2nd edition, 2002.
  * [CDL14] Raphaëlle Crubillé and Ugo Dal Lago.  On probabilistic applicative bisimulation and call-by-value $\lambda$-calculi.  In Zhong Shao, editor, ESOP 2014, volume 8410 of LNCS, pages 209–228. Springer, 2014.
  * [CHVB18] Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors.  Handbook of Model Checking.  Springer, 2018.
  * [CNZ17] Krishnendu Chatterjee, Petr Novotný, and Dorde Zikelic.  Stochastic invariants for probabilistic termination.  In Giuseppe Castagna and Andrew D. Gordon, editors, POPL 2017, pages 145–160. ACM, 2017.
  * [Cou97] Patrick Cousot.  Types as abstract interpretations.  In Peter Lee, Fritz Henglein, and Neil D. Jones, editors, POPL 1997, pages 316–331. ACM Press, 1997.
  * [CS13] Aleksandar Chakarov and Sriram Sankaranarayanan.  Probabilistic program analysis with martingales.  In Natasha Sharygina and Helmut Veith, editors, CAV 2013, pages 511–526, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg.
  * [DH02] Vincent Danos and Russell Harmer.  Probabilistic game semantics.  ACM Trans. Comput. Log., 3(3):359–382, 2002.
  * [DLG17] Ugo Dal Lago and Charles Grellois.  Probabilistic termination by monadic affine sized typing.  In ESOP 2017, pages 393–419, 2017.
  * [dLMSS56] Karel de Leeuw, Edward F. Moore, Claude E. Shannon, and Norman Shapiro.  Computability by probabilistic machines.  Automata Studies, 34:183–212, 1956.
  * [DSA14] Ugo Dal Lago, Davide Sangiorgi, and Michele Alberti.  On coinductive equivalences for higher-order probabilistic functional programs.  In POPL 2014, pages 297–308, 2014.
  * [DZ12] Ugo Dal Lago and Margherita Zorzi.  Probabilistic operational semantics for the lambda calculus.  RAIRO - Theor. Inf. and Applic., 46(3):413–450, 2012.
  * [EGK10] Javier Esparza, Andreas Gaiser, and Stefan Kiefer.  Computing least fixed points of probabilistic systems of polynomials.  In STACS 2010, volume 5 of LIPIcs, pages 359–370. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010.
  * [EGK12] Javier Esparza, Andreas Gaiser, and Stefan Kiefer.  Proving termination of probabilistic programs using patterns.  In P. Madhusudan and Sanjit A. Seshia, editors, CAV 2012, pages 123–138, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg.
  * [ETP14] Thomas Ehrhard, Christine Tasson, and Michele Pagani.  Probabilistic coherence spaces are fully abstract for probabilistic PCF.  In POPL 2014, pages 309–320, 2014.
  * [EY09] Kousha Etessami and Mihalis Yannakakis.  Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations.  J. ACM, 56(1):1:1–1:66, 2009.
  * [EY12] Kousha Etessami and Mihalis Yannakakis.  Model checking of recursive probabilistic systems.  ACM Trans. Comput. Log., 13(2):12:1–12:40, 2012.
  * [EY15] Kousha Etessami and Mihalis Yannakakis.  Recursive Markov decision processes and recursive stochastic games.  J. ACM, 62(2):11:1–11:69, 2015.
  * [FH15] Luis María Ferrer Fioriti and Holger Hermanns.  Probabilistic termination: Soundness, completeness, and compositionality.  In Sriram K. Rajamani and David Walker, editors, POPL 2015, pages 489–501. ACM, 2015.
  * [GM84] Shafi Goldwasser and Silvio Micali.  Probabilistic encryption.  J. Comput. Syst. Sci., 28(2):270–299, 1984.
  * [GM15a] Charles Grellois and Paul-André Melliès.  Finitary semantics of linear logic and higher-order model-checking.  In Italiano et al. [IPS15], pages 256–268.
  * [GM15b] Charles Grellois and Paul-André Melliès.  Relational semantics of linear logic and higher-order model checking.  In CSL 2015, volume 41 of LIPIcs, pages 260–276. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.
  * [GMR+08] Noah D. Goodman, Vikash K. Mansinghka, Daniel M. Roy, Keith Bonawitz, and Joshua B. Tenenbaum.  Church: A language for generative models.  In In UAI, pages 220–229, 2008.
  * [GO10] Hugo Gimbert and Youssouf Oualhadj.  Probabilistic automata on finite words: Decidable and undecidable problems.  In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, ICALP 2010, volume 6199 of LNCS, pages 527–538. Springer, 2010.
  * [HKSY17] Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang.  A convenient category for higher-order probability theory.  In LICS 2017, pages 1–12. IEEE Computer Society, 2017.
  * [HMOS08] Matthew Hague, Andrzej Murawski, C.-H. Luke Ong, and Olivier Serre.  Collapsible pushdown automata and recursion schemes.  In LICS 2008, pages 452–461. IEEE Computer Society, 2008.
  * [HPS96] John Hughes, Lars Pareto, and Amr Sabry.  Proving the correctness of reactive systems using sized types.  In Hans-Juergen Boehm and Guy L. Steele Jr., editors, POPL 1996, pages 410–423. ACM Press, 1996.
  * [Hro05] Juraj Hromkovic.  Design and Analysis of Randomized Algorithms - Introduction to Design Paradigms.  Texts in Theoretical Computer Science. An EATCS Series. Springer, 2005\.
  * [IPS15] Giuseppe F. Italiano, Giovanni Pighizzini, and Donald Sannella, editors.  MFCS 2015, volume 9234 of LNCS. Springer, 2015.
  * [JP89] C. Jones and Gordon D. Plotkin.  A probabilistic powerdomain of evaluations.  In LICS 1989, pages 186–195. IEEE Computer Society, 1989.
  * [JT98] Achim Jung and Regina Tix.  The troublesome probabilistic powerdomain.  ENTCS, 13:70 – 91, 1998.  Comprox III, Third Workshop on Computation and Approximation.
  * [KDLG19] Naoki Kobayashi, Ugo Dal Lago, and Charles Grellois.  On the termination problem for probabilistic higher-order recursive programs.  In Proceedings of LICS 2019. IEEE, 2019.
  * [KK15] Benjamin Lucien Kaminski and Joost-Pieter Katoen.  On the hardness of almost-sure termination.  In Italiano et al. [IPS15], pages 307–318.
  * [KLE07] Stefan Kiefer, Michael Luttenberger, and Javier Esparza.  On the convergence of newton’s method for monotone systems of polynomial equations.  In STOC 2007, pages 217–226. ACM, 2007.
  * [KNU01] Teodor Knapik, Damian Niwinski, and Pawel Urzyczyn.  Deciding monadic theories of hyperalgebraic trees.  In TLCA 2001, volume 2044 of LNCS, pages 253–267. Springer, 2001.
  * [KNU02] Teodor Knapik, Damian Niwinski, and Pawel Urzyczyn.  Higher-order pushdown trees are easy.  In FoSSaCS 2002, volume 2303 of LNCS, pages 205–222. Springer, 2002.
  * [KO09] Naoki Kobayashi and C.-H. Luke Ong.  A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes.  In LICS 2009, pages 179–188. IEEE Computer Society Press, 2009\.
  * [KO11] Naoki Kobayashi and C.-H. Luke Ong.  Complexity of model checking recursion schemes for fragments of the modal mu-calculus.  LMCS, 7(4), 2011.
  * [Kob09a] Naoki Kobayashi.  Model-checking higher-order functions.  In PPDP 2009, pages 25–36. ACM Press, 2009.
  * [Kob09b] Naoki Kobayashi.  Types and higher-order recursion schemes for verification of higher-order programs.  In POPL 2009, pages 416–428. ACM Press, 2009.
  * [Kob13] Naoki Kobayashi.  Model checking higher-order programs.  J. ACM, 60(3), 2013.
  * [Kob19] Naoki Kobayashi.  Inclusion between the frontier language of a non-deterministic recursive program scheme and the dyck language is undecidable.  Theor. Comput. Sci., 777:409–416, 2019.
  * [KS15] Gregory M. Kobele and Sylvain Salvati.  The IO and OI hierarchies revisited.  Inf. Comput., 243:205–221, 2015.
  * [KSU11] Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno.  Predicate abstraction and CEGAR for higher-order model checking.  In PLDI 2011, pages 222–233. ACM Press, 2011.
  * [Mat93] Yuri V. Matiyasevich.  Hilbert’s Tenth Problem.  The MIT Press, 1993.
  * [MMKK18] Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen.  A new proof rule for almost-sure termination.  POPL 2018, pages 33:1–33:28, 2018.
  * [MO05] Andrzej S. Murawski and Joël Ouaknine.  On probabilistic program equivalence and refinement.  In CONCUR 2005, pages 156–170, 2005.
  * [MR95] Rajeev Motwani and Prabhakar Raghavan.  Randomized Algorithms.  CUP, New York, NY, USA, 1995.
  * [MRH18] Agustín Mista, Alejandro Russo, and John Hughes.  Branching processes for quickcheck generators.  CoRR, abs/1808.01520, 2018.
  * [Ong06] C.-H. Luke Ong.  On model-checking trees generated by higher-order recursion schemes.  In LICS 2006, pages 81–90. IEEE Computer Society Press, 2006\.
  * [Par18] Pawel Parys.  Recursion schemes and the WMSO+U logic.  In STACS 2018, volume 96 of LIPIcs, pages 53:1–53:16, 2018\.
  * [PF17] Simon M. Poulding and Robert Feldt.  Automated random testing in multiple dispatch languages.  In ICST 2017, pages 333–344. IEEE Computer Society, 2017.
  * [RNO14] Steven Ramsay, Robin Neatherway, and C.-H. Luke Ong.  An abstraction refinement approach to higher-order model checking.  In POPL 2014, pages 61–72. ACM, 2014.
  * [Sah78] N. Saheb-Djahromi.  Probabilistic LCF.  In Józef Winkowski, editor, MFCS 1978, volume 64 of LNCS, pages 442–451. Springer, 1978.
  * [San69] Eugene S. Santos.  Probabilistic Turing machines and computability.  Proc. of the AMS, 22(3):704–710, 1969.
  * [Sta04] Richard Statman.  On the lambda _Y_ calculus.  APAL, 130(1-3):325–337, 2004.
  * [SV16] Davide Sangiorgi and Valeria Vignudelli.  Environmental bisimulations for probabilistic higher-order languages.  In POPL 2016, pages 595–607, 2016.
  * [SW11] Sylvain Salvati and Igor Walukiewicz.  Krivine machines and higher-order schemes.  In ICALP 2011, volume 6756 of LNCS, pages 162–173. Springer, 2011.
  * [SYW+16] Sam Staton, Hongseok Yang, Frank D. Wood, Chris Heunen, and Ohad Kammar.  Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints.  In LICS 2016, pages 525–534, 2016.
  * [TO14] Takeshi Tsukada and C.-H. Luke Ong.  Compositional higher-order model checking via _$\omega$_ -regular games over Böhm trees.  In CSL-LICS 2014, pages 78:1–78:10. ACM, 2014.
  * [WMM14] Frank Wood, Jan Willem Meent, and Vikash Mansinghka.  A new approach to probabilistic programming inference.  In Samuel Kaski and Jukka Corander, editors, Int. Conf. on Artificial Intelligence and Statistics, volume 33 of Proc. of Machine Learning Research, pages 1024–1032, Reykjavik, Iceland, 22–25 Apr 2014. PMLR.
  * [YE05] Mihalis Yannakakis and Kousha Etessami.  Checking LTL properties of recursive Markov chains.  In QEST 2005, pages 155–165. IEEE Computer Society, 2005.

## Appendix

##  Appendix A Relationship between PHORS and Recursive Markov Chains

In this section, we provide mutual translations between order-1 PHORS and
recursive Markov chains.

###  A.1. Encoding Recursive Markov Chains into Order-1 PHORS

In this section, we will give a sketch of a proof that any recursive Markov
chain (RMC in the following) can be faithfully encoded as an order-1 PHORS. In
doing that, we will closely follow the notational conventions and definitions
from [EY09], Section 2.

Let us first of all fix an RMC $A=(A_{\\_}1,\ldots,A_{\\_}k)$, where each
component graph is
$A_{\\_}i=(N_{\\_}i,B_{\\_}i,Y_{\\_}i,\mathit{En}_{\\_}i,\mathit{Ex}_{\\_}i,\delta_{\\_}i)$.
We fix a reachability problem, given in the form of a triple
$(i_{\\_}I,s_{\\_}I,q_{\\_}I)$ where $i_{\\_}I\in\\{1,\ldots,k\\}$, $s_{\\_}I$
is a vertex of $A_{\\_}{i_{\\_}I}$, and
$q_{\\_}I\in\mathit{Ex}_{\\_}{i_{\\_}I}$, where a vertex of each $A_{\\_}i$ is
defined as an element of

$N_{\\_}i\cup\bigcup_{\\_}{b\in
B_{\\_}i}\mathit{Call}_{\\_}b\cup\bigcup_{\\_}{b\in
B_{\\_}i}\mathit{Return}_{\\_}b.$

Here,
$\mathit{Call}_{\\_}b=\\{(b,\mathit{en})\mid\mathit{en}\in\mathit{En}_{\\_}{Y_{\\_}i(b)}\\}$
and
$\mathit{Return}_{\\_}b=\\{(b,\mathit{ex})\mid\mathit{ex}\in\mathit{Ex}_{\\_}{Y_{\\_}i(b)}\\}$
The reachability problem $(i_{\\_}I,s_{\\_}I,q_{\\_}I)$ specifies
$\langle\epsilon,s_{\\_}I\rangle$ as the initial state, where $s_{\\_}I$ is a
vertex of the component graph $i_{\\_}I$, and
$\langle\epsilon,q_{\\_}I\rangle$ as the reachability target (cf. Section 2.2
of [EY09]). The PHORS
$\mathcal{G}_{\\_}A=(\mathcal{N}_{\\_}A,\mathcal{R}_{\\_}A,S_{\\_}A)$ is
defined as follows:

  * •

Nonterminals are defined as symbols of the form $F_{\\_}{i,s}$ where
$i\in\\{1,\ldots,k\\}$, and $s$ is a vertex $A_{\\_}{i}$. The type
$\mathcal{N}_{\\_}A(F_{\\_}{i,s})$ is
$\mathtt{o}^{|\mathit{Ex}_{\\_}i|}\to\mathtt{o}$. There is also a nonterminal
$S_{\\_}A$ of type $\mathtt{o}$, which is taken to be
$(i_{\\_}I,s_{\\_}I,q_{\\_}I)$. The start symbol is $S_{\\_}A$.

  * •

Rules in $\mathcal{R}_{\\_}A$ are of four kinds:

    * •

There is a rule

$(i_{\\_}I,s_{\\_}I,q_{\\_}I)=S_{\\_}A=F_{\\_}{i_{\\_}I,s_{\\_}I}(\underbrace{\Omega,\ldots,\Omega}_{\\_}{\mbox{$j-1$
times}},\mathtt{e},\Omega,\ldots,\Omega)$

where $\mathit{Ex_{\\_}i}=\\{s_{\\_}1,\ldots,s_{\\_}{|\mathit{Ex_{\\_}i}|}\\}$
and $q_{\\_}I=s_{\\_}j$.

    * •

For every $i$ and for every exit node
$s_{\\_}j\in\mathit{Ex_{\\_}i}=\\{s_{\\_}1,\ldots,s_{\\_}{|\mathit{Ex_{\\_}i}}|\\}$,
there is a rule

$F_{\\_}{i,s_{\\_}j}(x_{\\_}1,\ldots,x_{\\_}{|\mathit{Ex}_{\\_}i|})=x_{\\_}j$

    * •

For each $i$ and for each non-exit node or return port $s$ of $A_{\\_}i$,
there is a rule

$F_{\\_}{i,s}(x_{\\_}1,\ldots,x)=\bigoplus_{\\_}{j}p_{\\_}{s,q}F_{\\_}{i,q}(x_{\\_}1,\ldots,x)$

where $p_{\\_}{s,q}$ is the probability to go from $s$ to $q$, as given by the
transition function $\delta_{\\_}i$.

    * •

For every $i$ and for every call port $s=(b,\mathit{en})$ of $A_{\\_}i$ which
is in $\mathit{Call}_{\\_}b$, there is a rule

$F_{\\_}{i,s}(\vec{x})=F_{\\_}{Y_{\\_}i(b),\mathit{en}}(F_{\\_}{i,(b,{\mathit{ex}_{\\_}1})}(\vec{x}),\ldots,F_{\\_}{i,(b,{\mathit{ex}_{\\_}v})}(\vec{x}))$

and
$\mathit{Ex}_{\\_}{Y_{\\_}i(b)}=\\{\mathit{ex}_{\\_}1,\ldots,\mathit{ex}_{\\_}v\\}$.

The next step is to put any global state in $M_{\\_}A$ in correspondence to a
term of $\mathcal{G}_{\\_}A$. This is actually quite easy, once one realizes
that:

  * •

$\mathcal{G}_{\\_}A$ is designed so that every term to which $S_{\\_}A$
reduces can be seen as a complete ordered tree.

  * •

The rules in $\mathcal{R}_{\\_}A$ have been designed so as to closely mimick
the four inductive clauses by which the transition relation $\Delta$ of the
Markov chain $M_{\\_}A$ is defined. In particular, any such pair
$\langle\beta,u\rangle$ is such that the length of $\beta$ corresponds to the
height of the corresponding term to which $S_{\\_}A$ reduces. The only caveat
is that the first such inductive clause needs to be restricted, because in
PHORS, contrarily to Markov chains, one needs to fix _one_ initial state.

  * •

$(\langle\beta,u\rangle,p,\langle\beta^{\prime},u^{\prime}\rangle)\in\Delta$
if and only if the term corresponding to $\langle\beta,u\rangle$ rewrites to
the term corresponding to $\langle\beta^{\prime},u^{\prime}\rangle$ with
probability $p$ in one step.

As a consequence, one easily derive that $\mathcal{P}(\mathcal{G}_{\\_}A)$ is
precisely the probability, in $M_{\\_}A$, to reach
$\langle{\epsilon,q_{\\_}I}\rangle$ starting from
$\langle{\epsilon,s_{\\_}I}\rangle$.

###  A.2. Encoding Order-1 PHORS into Recursive Markov Chains

In this section, we show that any order-1 PHORS can be encoded into a
recursive Markov chain that has the same termination probability.

First, we can normalize any order-1 PHORS to the one consisting of the
rewriting rules of the form:

$\begin{array}[]{l}S=F_{\\_}1\,\mathtt{e}\,\cdots\,\mathtt{e}\\\
F_{\\_}1\,x_{\\_}1\,\cdots\,x_{\\_}k=t_{\\_}{1,L}\,\oplus_{p_{\\_}1}\,t_{\\_}{1,R}\\\
\cdots\\\
F_{\\_}m\,x_{\\_}1\,\cdots\,x_{\\_}k=t_{\\_}{m,L}\,\oplus_{p_{\\_}1}\,t_{\\_}{m,R},\end{array}$

where each $t_{\\_}{i,d}$ ($i\in\\{1,\ldots,m\\},d\in\\{L,R\\}$) is a variable
$x_{\\_}j\ (j\in\\{1,\ldots,k\\})$, or is of the form:

$F_{\\_}i\,(F_{\\_}{j_{\\_}1}\,x_{\\_}1\,\cdots\,x_{\\_}k)\,\cdots\,(F_{\\_}{j_{\\_}k}\,x_{\\_}1\,\cdots\,x_{\\_}k).$

Note that $\Omega$ on the righthand side can be replaced by
$F\,x_{\\_}1\,\cdots\,x_{\\_}k$ where $F$ is defined by

$F\,x_{\\_}1,\cdots\,x_{\\_}k=F(F\,x_{\\_}1,\cdots\,x_{\\_}k)\cdots(F\,x_{\\_}1,\cdots\,x_{\\_}k).$

Given the normalized order-1 HORS above, let $M$ be a recursive Markov chain
consisting of a single component
$A_{\\_}1=(N_{\\_}1,B_{\\_}1,Y_{\\_}1,\mathit{En}_{\\_}1,\mathit{Ex}_{\\_}1,\delta_{\\_}1)$
where:

  * •

$B_{\\_}1$ is the set of terms of the form
$F_{\\_}i\,(F_{\\_}{j_{\\_}1}\,x_{\\_}1\,\cdots\,x_{\\_}k)\,\cdots\,(F_{\\_}{j_{\\_}k}\,x_{\\_}1\,\cdots\,x_{\\_}k)$
on the righthand side.

  * •

$Y_{\\_}1(b)=1$ for every $b\in B_{\\_}1$.

  * •

$\mathit{En}_{\\_}1=\\{F_{\\_}1,\ldots,F_{\\_}m\\}$.

  * •

$\mathit{Ex}_{\\_}1=\\{x_{\\_}1,\ldots,x_{\\_}k\\}$.

  * •

$N_{\\_}1=\mathit{En}_{\\_}1\cup\mathit{Ex}_{\\_}1$.

  * •

$\delta_{\\_}1$ is the least set of the transitions that satisfies:

    * –

$(F_{\\_}i,p,x_{\\_}j)\in\delta_{\\_}1$ for each transition rule
$F_{\\_}i\,x_{\\_}1,\cdots\,x_{\\_}k\xrightarrow{d,p}x_{\\_}j$
(recall that we write $F\,x_{\\_}1,\cdots\,x_{\\_}k\xrightarrow{L,p}t_{\\_}L$
and $F\,x_{\\_}1,\cdots\,x_{\\_}k\xrightarrow{R,1-p}t_{\\_}R$ if there is a
rule $F\,x_{\\_}1,\cdots\,x_{\\_}k=t_{\\_}L\,\oplus_{p}\,t_{\\_}R$).

    * –

$(F_{\\_}i,p,(t,F_{\\_}j))\in\delta_{\\_}1$
if $F_{\\_}i\,x_{\\_}1,\cdots\,x_{\\_}k\xrightarrow{d,p}t$ and $t$ is of the
form
$F_{\\_}j\,(F_{\\_}{j_{\\_}1}\,x_{\\_}1\,\cdots\,x_{\\_}k)\,\cdots\,(F_{\\_}{j_{\\_}k}\,x_{\\_}1\,\cdots\,x_{\\_}k)$.

    * –

$((t,x_{\\_}i),p,x_{\\_}\ell)\in\delta_{\\_}1$
if
$t=F_{\\_}j\,(F_{\\_}{j_{\\_}1}\,x_{\\_}1\,\cdots\,x_{\\_}k)\,\cdots\,(F_{\\_}{j_{\\_}k}\,x_{\\_}1\,\cdots\,x_{\\_}k)$,
and
$F_{\\_}{j_{\\_}i}\,x_{\\_}1\,\cdots\,x_{\\_}k\xrightarrow{d,p}x_{\\_}\ell$.

    * –

$((t,x_{\\_}i),p,(t^{\prime},F_{\\_}{j^{\prime}}))\in\delta_{\\_}1$
if
$t=F_{\\_}j\,(F_{\\_}{j_{\\_}1}\,x_{\\_}1\,\cdots\,x_{\\_}k)\,\cdots\,(F_{\\_}{j_{\\_}k}\,x_{\\_}1\,\cdots\,x_{\\_}k)$
and
$F_{\\_}{j_{\\_}i}\,x_{\\_}1\,\cdots\,x_{\\_}k\xrightarrow{d,p}t^{\prime}$,
where
$t^{\prime}=F_{\\_}{j^{\prime}}\,(F_{\\_}{j^{\prime}_{\\_}1}\,x_{\\_}1\,\cdots\,x_{\\_}k)\,\cdots\,(F_{\\_}{j^{\prime}_{\\_}k}\,x_{\\_}1\,\cdots\,x_{\\_}k)$,

Intuitively, a PHORS term of the form
$F_{\\_}j\,(F_{\\_}{j_{\\_}1}\,x_{\\_}1\,\cdots\,x_{\\_}k)\,\cdots\,(F_{\\_}{j_{\\_}k}\,x_{\\_}1\,\cdots\,x_{\\_}k)$
is modeled as a call of $F_{\\_}j$, where $F_{\\_}{j_{\\_}i}$ is executed when
the call exits from the exit port $x_{\\_}i$. That is why, in the third and
fourth kinds of transition rules above, the next node is determined by the
rule for $F_{\\_}{j_{\\_}i}$. From this intuition, it should be trivial that
the termination probabilities of the RMC and the original PHORS coincide.

##  Appendix B Proofs for Section 4

###  B.1. Proofs for Section 4.2

####  B.1.1. Proof of Lemma 4.3

We first prove the following lemma:

######  Lemma B.1.

If $\mathcal{K}\vdash t:\kappa$, then $\mathcal{K}^{\\#}\vdash
t^{\\#}:\kappa^{\\#}$.

######  Proof B.2.

This follows by straightforward induction on the derivation of
$\mathcal{K}\vdash t:\kappa$.

######  Proof B.3 (Proof of Lemma 4.3).

$\mathcal{N}^{\\#}\vdash S:\mathtt{R}$ follows immediately from
$\mathcal{N}(S)=\mathtt{o}$, Lemma B.1, and $\mathtt{o}^{\\#}=\mathtt{R}$. Let
$\mathcal{R}$ be
$\\{F_{\\_}i\,x_{\\_}1\,\cdots,x_{\\_}{\ell_{\\_}i}=t_{\\_}i\mid
i\in\\{1,\ldots,m\\}\\}$. Then, by the definition of PHORS, we have
$\mathcal{N},x_{\\_}1\mathbin{:}\kappa_{\\_}{i,1},\ldots,x_{\\_}{\ell_{\\_}i}\mathbin{:}\kappa_{\\_}{i,\ell_{\\_}i}\vdash
t_{\\_}i:\mathtt{o}$, with
$\mathcal{N}(F)=\kappa_{\\_}{i,1}\to\cdots\to\kappa_{\\_}{i,\ell_{\\_}i}\to\mathtt{o}$.
We need to show that

$\mathcal{N}^{\\#},x_{\\_}1\mathbin{:}\kappa_{\\_}{i,1}^{\\#},\ldots,x_{\\_}i\mathbin{:}\kappa_{\\_}{i,\ell_{\\_}i}^{\\#}\vdash
t_{\\_}i^{\\#}:\mathtt{R}$

for each $i$, but this follows immediately from the typing of $t_{\\_}i$ above
and Lemma B.1.

####  B.1.2. Proof of Theorem 4

We call a PHORS $\mathcal{G}$ _recursion-free_ if there is no cyclic
dependency on its non-terminals. More precisely, given a PHORS $\mathcal{G}$,
we define the relation $\succ_{\\_}{\mathcal{G}}$ on its non-terminals by:
$F_{\\_}i\succ_{\\_}{\mathcal{G}}F_{\\_}j$ iff $F_{\\_}j$ occurs on the
righthand side of the rule for $F_{\\_}i$. A PHORS $\mathcal{G}$ is defined to
be recursion-free if the transitive closure of $\succ_{\\_}{\mathcal{G}}$ is
irreflexive.

Below we write $t^{\\#}_{\rho}$ for $\llbracket{t^{\\#}}\rrbracket_{\rho}$.

######  Lemma B.4.

Let $\mathcal{G}=(\mathcal{N},\mathcal{R},S)$ be a recursion-free PHORS, and
$\rho$ be the least solution of $\mathcal{E}_{\\_}{\mathcal{G}}$. If
$\mathcal{N}\vdash t:\mathtt{o}$, then
$\mathcal{P}(\mathcal{G},t)=t^{\\#}_{\rho}$.

######  Proof B.5.

Since $\mathcal{G}$ is recursion-free, it follows from the strong
normalization of the simply-typed $\lambda$-calculus that $t$ does not have
any infinite reduction sequence. Because the reduction relation is finitely
branching, by König’s lemma, there are only finitely many reduction sequences
from $t$; thus a longest reduction sequence from $t$ exists, and we write
$\sharp(t)$ for its length. The proof proceeds by induction on $\sharp(t)$. If
$\sharp(t)=0$, then $t$ is either $\mathtt{e}$ (in which case, both sides of
the equation are $1$) or $\Omega$ (in which case, both sides of the equation
are $0$); thus, the result follows immediately. Otherwise, $t$ must be of the
form $F\;s_{\\_}1\cdots s_{\\_}k$ where $F\,x_{\\_}1\cdots
x_{\\_}k=t_{\\_}1\,\oplus_{p}\,t_{\\_}2$. Then

$\begin{array}[]{l}\mathcal{P}(\mathcal{G},t)=p\mathcal{P}(\mathcal{G},[s_{\\_}1/x_{\\_}1,\ldots,s_{\\_}k/x_{\\_}k]t_{\\_}1)\\\
\qquad\qquad+(1-p)\mathcal{P}(\mathcal{G},[s_{\\_}1/x_{\\_}1,\ldots,s_{\\_}k/x_{\\_}k]t_{\\_}2).\end{array}$

Since
$\sharp(t)>\sharp([s_{\\_}1/x_{\\_}1,\ldots,s_{\\_}k/x_{\\_}k]t_{\\_}i)$, by
the induction hypothesis, the righthand side equals:

$\begin{array}[]{l}p([s_{\\_}1/x_{\\_}1,\ldots,s_{\\_}k/x_{\\_}k]t_{\\_}1)^{\\#}_{\\_}{\rho}+(1-p)([s_{\\_}1/x_{\\_}1,\ldots,s_{\\_}k/x_{\\_}k]t_{\\_}2)^{\\#}_{\\_}{\rho}\\\
=p(t_{\\_}1)^{\\#}_{\\_}{\rho\\{\widetilde{x}\mapsto\widetilde{s}^{\\#}_{\\_}{\rho}\\}}+(1-p)(t_{\\_}2)^{\\#}_{\\_}{\rho\\{\widetilde{x}\mapsto\widetilde{s}^{\\#}_{\\_}{\rho}\\}}\\\
=(F\;s_{\\_}1\cdots
s_{\\_}k)^{\\#}_{\\_}{\rho}=t^{\\#}_{\\_}{\rho},\end{array}$

as required.

For a PHORS $\mathcal{G}=(\mathcal{N},\mathcal{R},S)$ with
$\mathit{dom}(\mathcal{N})=\\{F_{\\_}1,\ldots,F_{\\_}m\\}$, we define its _$k$
-th approximation_
$\mathcal{G}^{(k)}=(\mathcal{N}^{(k)},\mathcal{R}^{(k)},S^{(k)})$ by:

$\begin{array}[]{l}\mathcal{N}^{(k)}=\\{F_{\\_}j^{(i)}\mapsto\mathcal{N}(F_{\\_}j)\mid
j\in\\{1,\ldots,m\\},0\leq i\leq k\\}\\\
\mathcal{R}^{(k)}(F_{\\_}j^{(i)})=[F_{\\_}1^{(i-1)}/F_{\\_}1,\ldots,F_{\\_}m^{(i-1)}/F_{\\_}m]\mathcal{R}(F_{\\_}j)\\\
\hfill\mbox{ for each $i\in\\{1,\ldots,k\\}$}\\\
\mathcal{R}^{(k)}(F_{\\_}j^{(0)})=\lambda\widetilde{x}.\Omega\,\oplus_{1}\,\Omega.\end{array}$

The following properties follow immediately from the construction of
$\mathcal{G}^{(k)}$. (Recall that $\mathcal{F}_{\\_}{\mathcal{E}}$ denotes the
function associated with the fixpoint equations $\mathcal{E}$, as defined in
Section 4.1.)

######  Lemma B.6.

  1. (1)

$\mathcal{G}^{(k)}$ is recursion-free.

  2. (2)

$\mathcal{P}(\mathcal{G})=\bigsqcup_{\\_}{k\in\omega}\mathcal{P}(\mathcal{G}^{(k)})$.

  3. (3)

$\mathcal{F}_{\\_}{\mathcal{E}_{\\_}{\mathcal{G}}}^{k}(\bot_{\\_}{\llbracket{\mathcal{N}}\rrbracket})(F)=\mathcal{F}_{\\_}{\mathcal{E}_{\\_}{\mathcal{G}^{(k)}}}^{k}(\bot_{\\_}{\llbracket{\mathcal{N}^{(k)}}\rrbracket})(F^{(k)})=\mathbf{lfp}(\mathcal{F}_{\\_}{\mathcal{E}_{\\_}{\mathcal{G}^{(k)}}})(F^{(k)})$
for each non-terminal $F$ of $\mathcal{G}$.

######  Proof B.7.

  1. (1)

This follows immediately from the fact that
$F_{\\_}\ell^{(i)}\succ_{\\_}{\mathcal{G}^{(k)}}F_{\\_}{\ell^{\prime}}^{(j)}$
only if $j=i-1$.

  2. (2)

Let $P$ be the set $\\{(\pi,p)\mid S\ext@arrow
0359\Rightarrowfill@{}{\pi,p}_{\mathcal{G}}\mathtt{e}\\}$ and $P^{(k)}$ be
$\\{(\pi,p)\mid S^{(k)}\ext@arrow
0359\Rightarrowfill@{}{\pi,p}_{\mathcal{G}^{(k)}}\mathtt{e}\\}$. Then
$\mathcal{P}(\mathcal{G})=\sum_{\\_}{(\pi,p)\in P}p$ and
$\mathcal{P}(\mathcal{G}^{(k)})=\sum_{\\_}{(\pi,p)\in P^{(k)}}p$. Note that
for any reduction $s\xrightarrow{d,p}_{\mathcal{G}^{(k)}}t$ with
$t\neq\Omega$, there exists a corresponding reduction
$s^{!}\xrightarrow{d,p}_{\mathcal{G}}t^{!}$ where $s^{!}$ and $t^{!}$ are the
terms of $\mathcal{G}$ obtained from $s$ and $t$ respectively, by removing
indices, i.e. by replacing each $F^{(i)}$ with $F$. Thus, $P^{(k)}\subseteq P$
for any $k$. Conversely, if $S\xrightarrow{\pi,p}_{\mathcal{G}}\mathtt{e}$,
then $S^{(|\pi|)}\xrightarrow{\pi,p}_{\mathcal{G}^{(|\pi|)}}\mathtt{e}$,
because non-terminals are unfolded at most $|\pi|$ times in
$S\xrightarrow{\pi,p}_{\mathcal{G}}\mathtt{e}$. Therefore,
$P=\bigcup_{\\_}kP^{(k)}$, from which the result follows.

  3. (3)

We show that
$\mathcal{F}_{\\_}{\mathcal{E}_{\\_}{\mathcal{G}}}^{k}(\bot_{\\_}{\llbracket{\mathcal{N}}\rrbracket})(F)=\mathcal{F}_{\\_}{\mathcal{E}_{\\_}{\mathcal{G}^{(\ell)}}}^{k}(\bot_{\\_}{\llbracket{\mathcal{N}^{(\ell)}}\rrbracket})(F^{(k)})$
holds for any $\ell\geq k$, by induction on $k$, from which the first equality
follows. The base case $k=0$ is trivial. For $k>0$, By the definition of the
rule for $F^{(k)}$ and the induction hypothesis, we have:

$\begin{array}[]{l}\mathcal{F}_{\\_}{\mathcal{E}_{\\_}{\mathcal{G}^{(\ell)}}}^{k}(\bot_{\\_}{\llbracket{\mathcal{N}^{(\ell)}}\rrbracket})(F^{(k)})\\\
=\llbracket{([F_{\\_}1^{(k-1)}/F_{\\_}1,\ldots,F_{\\_}m^{(k-1)}/F_{\\_}m]\mathcal{R}(F))^{\\#}}\rrbracket_{\mathcal{F}_{\\_}{\mathcal{E}_{\\_}{\mathcal{G}^{(\ell)}}}^{k-1}(\bot_{\\_}{\llbracket{\mathcal{N}^{(\ell)}}\rrbracket})}\\\
=\llbracket{\mathcal{R}(F)^{\\#}}\rrbracket_{\\{F_{\\_}i\mapsto\mathcal{F}_{\\_}{\mathcal{E}_{\\_}{\mathcal{G}^{(\ell)}}}^{k-1}(\bot_{\\_}{\llbracket{\mathcal{N}^{(\ell)}}\rrbracket})(F_{\\_}i^{(k-1)})\mid
i\in\\{1,\ldots,m\\}\\}}\\\
=\llbracket{\mathcal{R}(F)^{\\#}}\rrbracket_{\mathcal{F}_{\\_}{\mathcal{E}_{\\_}{\mathcal{G}}}^{k-1}(\bot_{\\_}{\llbracket{\mathcal{N}}\rrbracket})}\mbox{
(by the induction hypothesis)}\\\
=\mathcal{F}_{\\_}{\mathcal{E}_{\\_}{\mathcal{G}}}^{k}(\bot_{\\_}{\llbracket{\mathcal{N}}\rrbracket})(F),\end{array}$

as required. (Here, we have extended $(\cdot)^{\\#}$ and
$\llbracket{t}\rrbracket_{\rho}$ for $\lambda$-terms in the obvious manner.)

For the second equality, we can show that
$\mathcal{F}_{\\_}{\mathcal{E}_{\\_}{\mathcal{G}^{(\ell)}}}^{k}(\bot_{\\_}{\llbracket{\mathcal{N}^{(\ell)}}\rrbracket})(F^{(k)})=\mathbf{lfp}(\mathcal{F}_{\\_}{\mathcal{E}_{\\_}{\mathcal{G}^{(\ell)}}})(F^{(k)})$
holds for any $\ell\geq k$, by straightforward induction on $k$.

Theorem 4 follows as a corollary of the above lemmas.

######  Proof B.8 (Proof of Theorem 4).

By Lemmas B.4 and B.6, we have

$\begin{array}[]{l}\mathcal{P}(\mathcal{G})=\bigsqcup_{\\_}k\mathcal{P}(\mathcal{G}^{(k)})=\bigsqcup_{\\_}k\mathbf{lfp}(\mathcal{F}_{\\_}{\mathcal{E}_{\\_}{\mathcal{G}^{(k)}}})(S^{(k)})\\\
\qquad=\bigsqcup_{\\_}k\mathcal{F}_{\\_}{\mathcal{E}_{\\_}\mathcal{G}}^{k}(\bot)(S)=\mathbf{lfp}(\mathcal{F}_{\\_}{\mathcal{E}_{\\_}\mathcal{G}})(S)\end{array}$

as required.

###  B.2. Proofs for Section 4.3

####  B.2.1. Proof of Lemma 4.10

We define the translation for a type environment on variables (other than non-
terminals; note that the translation is different from the one for
$\mathcal{N}$) by:

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

######  Lemma B.9.

If
$\mathcal{N}\cup\mathcal{K},\widetilde{x}\mathbin{:}\widetilde{\mathtt{o}}\vdash
t:\kappa$ and $\mathcal{K};\widetilde{x}\vdash_{\mathcal{N}}t:\kappa\leadsto
e$, then $\mathcal{N}^{\dagger}\cup\mathcal{K}^{\dagger}\vdash
e:{\kappa}^{\dagger+|\widetilde{x}|}$.

######  Proof B.10.

This follows by straightforward induction on the derivation of
$\mathcal{N}\cup\mathcal{K},\widetilde{x}\mathbin{:}\widetilde{\mathtt{o}}\vdash
t:\kappa$.

We also prepare the following lemma on the syntactic property of the
translation result, which is important for Lemma 4.10 and the substitution
lemma (Lemma B.22 below) proved later.

######  Lemma B.11.

Suppose:

$\mathcal{K};\widetilde{z}\vdash_{\mathcal{N}}t:\kappa\leadsto(t_{\\_}0,\ldots,t_{\\_}{\mathtt{ar}(\kappa)},t_{\\_}{\mathtt{ar}(\kappa)+1},\ldots,t_{\\_}{\mathtt{ar}(\kappa)+|\widetilde{z}|+1}).$

Then, for each $y_{\\_}i\in\mathit{dom}(\mathcal{K})$, $y_{\\_}{i,0}$ does not
occur in $t_{\\_}1,\ldots,t_{\\_}{\mathtt{ar}(\kappa)+|\widetilde{z}|+1}$.

######  Proof B.12.

This follows by straightforward induction on the structure of $t$.

######  Proof B.13 (Proof of Lemma 4.10).

${\mathcal{N}}^{\dagger}(S_{\\_}1)=\mathtt{R}$ follows immediately from
$\mathcal{N}(S)=\mathtt{o}\to\mathtt{o}$ and the definition of
${\mathcal{N}}^{\dagger}$. To prove
${\mathcal{N}}^{\dagger}\vdash\mathcal{E}$, let
$F\,y_{\\_}1\,\cdots\,y_{\\_}\ell\,x_{\\_}1\,\cdots\,x_{\\_}k=t_{\\_}L\,\oplus_{p}\,t_{\\_}R\in\mathcal{R}$,
with
$\mathcal{N}(F)=\kappa_{\\_}1\to\cdots\to\kappa_{\\_}\ell\Rightarrow\mathtt{o}^{k}\to\mathtt{o}$.
Suppose also

$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})$

for $d\in\\{L,R\\}$. We need to prove

$\mathcal{N}^{\dagger},(\widetilde{y_{\\_}1})\mathbin{:}{\kappa_{\\_}1}^{\dagger},\ldots,(\widetilde{y_{\\_}\ell})\mathbin{:}{\kappa_{\\_}\ell}^{\dagger}\vdash
t_{\\_}{d,0}:\mathtt{R}$

and

$\mathcal{N}^{\dagger},(\widetilde{y_{\\_}1}^{\prime})\mathbin{:}{\kappa_{\\_}1}^{\dagger^{\prime}},\ldots,(\widetilde{y_{\\_}\ell}^{\prime})\mathbin{:}{\kappa_{\\_}\ell}^{\dagger^{\prime}}\vdash
t_{\\_}{d,i}:\mathtt{R}$

for $i\in\\{1,\ldots,k\\}$, where $\widetilde{y_{\\_}i}$ and
$\widetilde{y_{\\_}i}^{\prime}$ are as given in the premises of the rule Tr-
Rule. The former follows immediately from Lemma B.9. For the latter, by Lemma
B.9, we have

$\mathcal{N}^{\dagger},(\widetilde{y_{\\_}1})\mathbin{:}{\kappa_{\\_}1}^{\dagger},\ldots,(\widetilde{y_{\\_}\ell})\mathbin{:}{\kappa_{\\_}\ell}^{\dagger}\vdash
t_{\\_}{d,i}:\mathtt{R}.$

By Lemma B.11, $y_{\\_}{i,0}$ does not occur in $t_{\\_}{d,i}$. Thus we can
remove the type bindings on them and obtain

$\mathcal{N}^{\dagger},(\widetilde{y_{\\_}1}^{\prime})\mathbin{:}{\kappa_{\\_}1}^{\dagger^{\prime}},\ldots,(\widetilde{y_{\\_}\ell}^{\prime})\mathbin{:}{\kappa_{\\_}\ell}^{\dagger^{\prime}}\vdash
t_{\\_}{d,i}:\mathtt{R}$

as required.

####  B.2.2. Proof of Theorem 5

Given two expressions $e_{\\_}1,e_{\\_}2$ and fixpoint equations
$\mathcal{E}^{\mathtt{ref}}_{\mathcal{G}}$, we write
$e_{\\_}1\cong_{\\_}{\mathcal{E}^{\mathtt{ref}}_{\mathcal{G}}}e_{\\_}2$ if
$\llbracket{e_{\\_}1}\rrbracket_{\rho_{\\_}{\mathcal{E}^{\mathtt{ref}}_{\mathcal{G}}}}=\llbracket{e_{\\_}e}\rrbracket_{\rho_{\\_}{\mathcal{E}^{\mathtt{ref}}_{\mathcal{G}}}}$.
We often omit the subscript.

As sketched in Section 4.3, we first prove the theorem for recursion-free
PHORS. A key property used for showing it is that the translation relation is
preserved by reductions, roughly in the sense that if
$t\xrightarrow{L,p}t_{\\_}L$ and $t\xrightarrow{R,1-p}t_{\\_}R$, then
$t\leadsto e$ (i.e., $t$ is translated to $e$) implies that there exist
$e_{\\_}L$ and $e_{\\_}R$ such that $t_{\\_}L\leadsto e_{\\_}L$,
$t_{\\_}R\leadsto e_{\\_}R$ and $e\cong p\cdot e_{\\_}L+(1-p)\cdot e_{\\_}R$
(where $+$ and $\cdot$ are pointwise extended to operations on tuples). Thus,
the property that $e$ represents the termination probability of $t$ follows
from the corresponding properties of $e_{\\_}L$ and $e_{\\_}R$; by induction
(note that since we are considering recursion-free PHORS,
$\flat(t)>\flat(t_{\\_}L),\flat(t_{\\_}R)$, where $\flat(t)$ denotes the
length of the longest reduction sequence from $t$), it follows that if the
initial term is translated to $e_{\\_}0$, then $e_{\\_}0$ represents the
termination probability of the initial term.

Unfortunately, however, the translation relation is _not_ necessarily
preserved by the standard reduction relation $\xrightarrow{d,p}_{\mathcal{G}}$
defined in Section 2. We thus introduce another reduction relation that uses
_explicit substitutions_ on order-0 variables. To this end, we extend the
syntax of terms as follows.

$\begin{array}[]{l}t\mbox{ (extended terms)}::=\Omega\mid x\mid
t_{\\_}1t_{\\_}2\mid\\{t_{\\_}1/x_{\\_}1,\ldots,t_{\\_}k/x_{\\_}k\\}{t_{\\_}0}\end{array}$

Here, $\\{t_{\\_}1/x_{\\_}1,\ldots,t_{\\_}k/x_{\\_}k\\}{t_{\\_}0}$ represents
an _explicit_ substitution; the intended meaning is the same as the ordinary
substitution $[t_{\\_}1/x_{\\_}1,\ldots,t_{\\_}k/x_{\\_}k]{t_{\\_}0}$ (which
represents the term obtained from $t_{\\_}0$ by simultaneously substituting
$t_{\\_}i$ for $x_{\\_}i$), but the substitution is delayed until one of the
variables in $x_{\\_}1,\ldots,x_{\\_}k$ becomes necessary. We often abbreviate
$\\{t_{\\_}1/x_{\\_}1,\ldots,t_{\\_}k/x_{\\_}k\\}$ as
$\\{\widetilde{t}/\widetilde{x}\\}$. Note that we have omitted $\mathtt{e}$;
we consider an open term $S\,x$ as the initial term instead of
$S\,\mathtt{e}$. The type judgment relation for terms is extended by adding
the following rule:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K}\vdash
s_{\\_}i:\mathtt{o}\mbox{ (for each
$i\in\\{1,\ldots,k\\}$)}\quad\quad\mathcal{K},x_{\\_}1\mathbin{:}\mathtt{o},\ldots,x_{\\_}k\mathbin{:}\mathtt{o}\vdash
t:\mathtt{o}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K}\vdash\\{s_{\\_}1/x_{\\_}1,\ldots,s_{\\_}k/x_{\\_}k\\}{t}:\mathtt{o}\end{array}}$

Thus, explicit substitutions are allowed only for order-0 variables.

Reductions with explicit substitutions:
We now define a reduction relation for extended terms. The set of evaluation
contexts, ranged over by $E$, is defined by:

$E::=[\,]\mid\\{\widetilde{t}/\widetilde{x}\\}E.$

The new reduction relation
$t\xrightarrow{d,p}_{\texttt{es},\mathcal{G}}t^{\prime}$ (where
$d\in\\{L,R,\epsilon\\}$) is defined as follows.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}z\notin\\{x_{\\_}1,\ldots,x_{\\_}k\\}\end{array}}{\begin{array}[]{@{}c@{}}E[\\{t_{\\_}1/x_{\\_}1,\ldots,t_{\\_}k/x_{\\_}k\\}z]\xrightarrow{\epsilon,1}_{\texttt{es},\mathcal{G}}E[z]\end{array}}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}E[\\{t_{\\_}1/x_{\\_}1,\ldots,t_{\\_}k/x_{\\_}k\\}x_{\\_}i]\xrightarrow{\epsilon,1}_{\texttt{es},\mathcal{G}}E[t_{\\_}i]\end{array}}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{R}(F)=\lambda\widetilde{y}.\lambda\widetilde{z}.u_{\\_}L\,\oplus_{p}\,u_{\\_}R\\\
\mathcal{N}(F)=\widetilde{\kappa}\Rightarrow\mathtt{o}^{\ell}\to\mathtt{o}\quad\quad\ell=|\widetilde{z}|=|\widetilde{t}|\quad\quad|\widetilde{y}|=|\widetilde{s}|\\\
\mbox{$\widetilde{z}$ do not occur in
$E[F\,\widetilde{s}\,\widetilde{t}]$}\end{array}}{\begin{array}[]{@{}c@{}}E[F\,\widetilde{s}\,\widetilde{t}]\xrightarrow{L,p}_{\texttt{es},\mathcal{G}}E[\\{\widetilde{t}/\widetilde{z}\\}[\widetilde{s}/\widetilde{y}]u_{\\_}L]\end{array}}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{R}(F)=\lambda\widetilde{y}.\lambda\widetilde{z}.u_{\\_}L\,\oplus_{p}\,u_{\\_}R\\\
\mathcal{N}(F)=\widetilde{\kappa}\Rightarrow\mathtt{o}^{\ell}\to\mathtt{o}\quad\quad\ell=|\widetilde{z}|=|\widetilde{t}|\quad\quad|\widetilde{y}|=|\widetilde{s}|\\\
\mbox{$\widetilde{z}$ do not occur in
$E[F\,\widetilde{s}\,\widetilde{t}]$}\end{array}}{\begin{array}[]{@{}c@{}}E[F\,\widetilde{s}\,\widetilde{t}]\xrightarrow{R,1-p}_{\texttt{es},\mathcal{G}}E[\\{\widetilde{t}/\widetilde{z}\\}[\widetilde{s}/\widetilde{y}]u_{\\_}R]\end{array}}$

We call reductions using the first two rules (i.e., reductions labeled by
$\xrightarrow{\epsilon,p}_{\texttt{es},\mathcal{G}}$) _administrative
reductions_. In the last two rules, we assume that $\alpha$-conversion is
implicitly applied so that $\widetilde{z}$ do not clash with variables that
are already used in $E[F\,\widetilde{s}\,\widetilde{t}]$. In those rules,
recall also our notational convention that when we write
$F\,\widetilde{s}\,\widetilde{t}$, the second sequence $\widetilde{t}$ is the
maximal sequence of order-0 terms (that condition is made explicit in the
above rules, but below we often omit to state it). As before, we often omit
the subscript $\mathcal{G}$.

For an extended term $t$, we write $t^{*}$ for the term obtained by replacing
explicit substitutions with ordinary substitutions. For example,
$(\\{t/x\\}(F\,x))^{*}=F\,t$. The following lemma states that the new
reduction relation is essentially equivalent to the original reduction
relation:

######  Lemma B.14.

Let $s$ be an extended term.

  1. (1)

If $s\xrightarrow{\epsilon,1}_{\texttt{es}}{}t$, then $s^{*}=t^{*}$.

  2. (2)

If $s\xrightarrow{d,p}_{\texttt{es}}{}t$ with $d\in\\{L,R\\}$, then
$s^{*}\xrightarrow{d,p}t^{*}$.

  3. (3)

If $s^{*}\xrightarrow{d,p}u$, then there exists $t$ such that
$s(\xrightarrow{\epsilon,1}_{\texttt{es}})^{*}\xrightarrow{d,p}_{\texttt{es}}t$
and $t^{*}=u$.

######  Proof B.15.

Immediate from the definitions of $\xrightarrow{d,p}$ and
$\xrightarrow{d,p}_{\texttt{es}}{}$.

We define
$\stackrel{{\scriptstyle\pi,p}}{{\Longrightarrow}}_{\mathtt{es},\mathcal{G}}$
in an analogous manner to $\ext@arrow
0359\Rightarrowfill@{}{\pi,p}_{\mathcal{G}}$, where the label $\epsilon$ is
treated as an empty word. For an extended term $t$ that may contain an order-0
free variable $x$, we write $\mathit{P}_{\\_}{\mathtt{es}}(\mathcal{G},t,x)$
for the set $\\{(\pi,p)\mid
t\stackrel{{\scriptstyle\pi,p}}{{\Longrightarrow}}_{\mathtt{es},\mathcal{G}}x\\}$,
and write $\mathcal{P}_{\mathtt{es}}(\mathcal{G},t,x)$ for
$\sum_{\\_}{(\pi,p)\in\mathit{P}_{\\_}{\mathtt{es}}(\mathcal{G},t,x)}p$, based
on the new reduction relation. The following lemma follows immediately from
the above definitions and Lemma B.14.

######  Lemma B.16.

Let $t$ be a term of PHORS $\mathcal{G}=(\mathcal{N},\mathcal{R},S)$ such that
$\mathcal{N},x\mathbin{:}\mathtt{o}\vdash t:\mathtt{o}$ and $t$ does not
contain $\mathtt{e}$. Then
$\mathcal{P}(\mathcal{G},[\mathtt{e}/x]t)=\mathcal{P}_{\mathtt{es}}(\mathcal{G},t,x)$.

######  Proof B.17.

By Lemma B.14, $t\ext@arrow 0359\Rightarrowfill@{}{\pi,p}_{\mathtt{es}}x$ if
and only if $t^{*}\ext@arrow 0359\Rightarrowfill@{}{\pi,p}x$, if and only if
$[\mathtt{e}/x]t^{*}\ext@arrow 0359\Rightarrowfill@{}{\pi,p}\mathtt{e}$ (for
the second “if and only if”, recall the assumption that $\mathtt{e}$ does not
occur in $\mathcal{R}$), from which the result follows.

We extend the translation relation for terms with the following rule.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K};x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}s_{\\_}i:\mathtt{o}\leadsto(s_{\\_}{i,0},\ldots,s_{\\_}{i,k+1})\mbox{
(for each $i\in\\{1,\ldots,\ell\\}$)}\\\
\mathcal{K};z_{\\_}1,\ldots,z_{\\_}\ell,x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}t:\mathtt{o}\leadsto(t_{\\_}0,\ldots,t_{\\_}{k+\ell+1})\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}\\{s_{\\_}1/z_{\\_}1,\ldots,s_{\\_}\ell/z_{\\_}\ell\\}{t}:\mathtt{o}\leadsto\\\
\quad(t_{\\_}0+\Sigma_{\\_}{i=1}^{\ell}t_{\\_}{i}\cdot
s_{\\_}{i,0},t_{\\_}{\ell+1}+\Sigma_{\\_}{i=1}^{\ell}t_{\\_}{i}\cdot
s_{\\_}{i,1},\ldots,t_{\\_}{k+\ell+1}+\Sigma_{\\_}{i=1}^{\ell}t_{\\_}{i}\cdot
s_{\\_}{i,k+1})\end{array}}$ (Tr-Sub)

We shall prove that the translation relation is preserved by the new reduction
relation (Lemmas B.24, B.26, and B.28 below).

######  Lemma B.18 (Weakening).

  1. (1)

If $\mathcal{K};x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}t:\kappa\leadsto
e$, then
$\mathcal{K},y\mathbin{:}\kappa_{\\_}y;x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}t:\kappa\leadsto
e$.

  2. (2)

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

######  Proof B.19.

This follows by straightforward induction on the structure of $t$.

######  Lemma B.20 (Exchange).

If
$\mathcal{K};x_{\\_}1,\ldots,x_{\\_}{i},x_{\\_}{i+1},\ldots,x_{\\_}k\vdash_{\mathcal{N}}t:\kappa\leadsto(t_{\\_}0,\ldots,t_{\\_}{\mathtt{ar}(\kappa)+i},t_{\\_}{\mathtt{ar}(\kappa)+i+1},\ldots,t_{\\_}{\mathtt{ar}(\kappa)+k+1})$,
then
$\mathcal{K};x_{\\_}1,\ldots,x_{\\_}{i+1},x_{\\_}{i},\ldots,x_{\\_}k\vdash_{\mathcal{N}}t:\kappa\leadsto(t_{\\_}0,\ldots,t_{\\_}{\mathtt{ar}(\kappa)+i+1},t_{\\_}{\mathtt{ar}(\kappa)+i},\ldots,t_{\\_}{\mathtt{ar}(\kappa)+k+1})$.

######  Proof B.21.

This follows by straightforward induction on the structure of $t$.

As usual, the substitution lemma, stated below, is a critical lemma for
proving subject reduction. The statement of our substitution lemma is,
however, quite delicate, due to a special treatment of order-0 variables.

######  Lemma B.22 (Substitution).

Suppose $t$ does not contain any explicit substitutions (i.e., any subterms of
the form $\\{\widetilde{u}/\widetilde{x}\\}s$). If
$\widetilde{y}\mathbin{:}\widetilde{\kappa_{\\_}y};\widetilde{z}\vdash_{\mathcal{N}}t:\kappa\leadsto(\widetilde{t},t_{\\_}{m+1})$
and
$\emptyset;x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}s_{\\_}i:\kappa_{\\_}{y,i}\leadsto(\widetilde{s_{\\_}i},s_{\\_}{i,\ell_{\\_}i+1},\ldots,s_{\\_}{i,\ell_{\\_}i+k+1})$
with $\\{x_{\\_}1,\ldots,x_{\\_}k\\}\cap\\{\widetilde{z}\\}=\emptyset$ and
$\ell_{\\_}i=\mathtt{ar}(\kappa_{\\_}{y,i})$, then:

$\begin{array}[]{l}\emptyset;\widetilde{z},x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}[\widetilde{s}/\widetilde{y}]t:\kappa\leadsto(\theta_{\\_}0\widetilde{t},\theta_{\\_}{1}t_{\\_}{0},\ldots,\theta_{\\_}{k}t_{\\_}{0},\theta_{\\_}0t_{\\_}{m+1}),\end{array}$

where the substitutions $\theta_{\\_}j(j\in\\{0,\ldots,k\\})$ are defined by:

$\begin{array}[]{l}\theta_{\\_}j=\theta_{\\_}{1,j}\cdots\theta_{\\_}{|\widetilde{s}|,j}\mbox{
for $j\in\\{1,\ldots,k\\}$}\\\
\theta_{\\_}{i,0}=[s_{\\_}{i,0}/y_{\\_}{i,0},\ldots,s_{\\_}{i,\ell_{\\_}i}/y_{\\_}{i,\ell_{\\_}i},s_{\\_}{i,\ell_{\\_}i+k+1}/y_{\\_}{i,\ell_{\\_}i+1}]\mbox{
for $i\in\\{1,\ldots,|\widetilde{s}|\\}$}\\\
\theta_{\\_}{i,j}=[s_{\\_}{i,\ell_{\\_}i+j}/y_{\\_}{i,0},s_{\\_}{i,1}/y_{\\_}{i,1},\ldots,s_{\\_}{i,\ell_{\\_}i}/y_{\\_}{i,\ell_{\\_}i},s_{\\_}{i,\ell_{\\_}i+k+1}/y_{\\_}{i,\ell_{\\_}i+1}]\\\
\hfill\mbox{ for
$i\in\\{1,\ldots,|\widetilde{s}|\\},j\in\\{1,\ldots,k\\}$}.\end{array}$

Here, the part $\theta_{\\_}{1}t_{\\_}{0},\ldots,\theta_{\\_}{k}t_{\\_}{0}$
accounts for information about reachability to the newly introduced variables
$x_{\\_}1,\ldots,x_{\\_}k$.

######  Proof B.23.

Induction on the derivation of
$\widetilde{y}\mathbin{:}\widetilde{\kappa_{\\_}y};\widetilde{z}\vdash_{\mathcal{N}}t:\kappa\leadsto(\widetilde{t},t_{\\_}{m+1})$.

  * •

Case Tr-Omega: In this case, $t=\Omega$ with $\widetilde{t}=\widetilde{0}$ and
$t_{\\_}{m+1}=0$. Thus, the result follows immediately from the rule Tr-Omega.

  * •

Case Tr-GVar: In this case, $t=z_{\\_}i$ and $\kappa=\mathtt{o}$, with
$\widetilde{t}=0^{i},1,0^{|z|-i}$ and $t_{\\_}{m+1}=0$. By using Tr-GVar, we
obtain

$\emptyset;\widetilde{z},x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}[\widetilde{s}/\widetilde{y}]t(=z_{\\_}i):\kappa\leadsto(0^{i},1,0^{|\widetilde{z}|+k-i+1}).$

Since

$(\theta_{\\_}0\widetilde{t},\theta_{\\_}{1}t_{\\_}{0},\ldots,\theta_{\\_}{k}t_{\\_}{0},\theta_{\\_}0t_{\\_}{m+1})=(\widetilde{t},\underbrace{t_{\\_}{0},\ldots,t_{\\_}{0}}_{\\_}k,t_{\\_}{m+1})=(0^{i},1,0^{|\widetilde{z}|+k-i+1}),$

we have the required result.

  * •

Case Tr-Var: In this case, $t=y_{\\_}i$, with
$\widetilde{t}=y_{\\_}{i,0},\ldots,y_{\\_}{i,\ell_{\\_}i},y_{\\_}{i,\ell_{\\_}i+1}^{|\widetilde{z}|}$,
and $t_{\\_}{m+1}=y_{\\_}{i,\ell_{\\_}i+1}$. By applying Lemmas B.18 and B.20
to
$\emptyset;x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}s_{\\_}i:\kappa_{\\_}{y,i}\leadsto(\widetilde{s_{\\_}i},s_{\\_}{i,\ell_{\\_}i+1},\ldots,s_{\\_}{i,\ell_{\\_}i+k+1})$,
we obtain:

$\begin{array}[]{l}\emptyset;\widetilde{z},x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}s_{\\_}i:\kappa_{\\_}{y,i}\leadsto(\widetilde{s_{\\_}i},s_{\\_}{i,\ell_{\\_}i+k+1}^{|\widetilde{z}|},s_{\\_}{i,\ell_{\\_}i+1},\ldots,s_{\\_}{i,\ell_{\\_}i+k+1}).\end{array}$

Since
$\widetilde{t}=y_{\\_}{i,0},\ldots,y_{\\_}{i,\ell_{\\_}i},y_{\\_}{i,\ell_{\\_}i+1}^{|\widetilde{z}|}$,
and $t_{\\_}{m+1}=y_{\\_}{i,\ell_{\\_}i+1}$, we have

$\begin{array}[]{l}(\theta_{\\_}0\widetilde{t},\theta_{\\_}{1}t_{\\_}{0},\ldots,\theta_{\\_}{k}t_{\\_}{0},\theta_{\\_}0t_{\\_}{m+1})=(\widetilde{s_{\\_}i},s_{\\_}{i,\ell_{\\_}i+k+1}^{|\widetilde{z}|},s_{\\_}{i,\ell_{\\_}i+1},\ldots,s_{\\_}{i,\ell_{\\_}i+k+1}).\end{array}$

Thus we have the required result.

  * •

Case Tr-App: In this case, we have $t=uv$ and

$\begin{array}[]{l}\widetilde{y}\mathbin{:}\widetilde{\kappa_{\\_}y};\widetilde{z}\vdash_{\mathcal{N}}u:\kappa_{\\_}v\to\kappa\leadsto(u_{\\_}0,\widetilde{u},u_{\\_}{\ell^{\prime}+1},\ldots,u_{\\_}{\ell^{\prime}+|\widetilde{z}|+1})\\\
\widetilde{y}\mathbin{:}\widetilde{\kappa_{\\_}y};\widetilde{z}\vdash_{\mathcal{N}}v:\kappa_{\\_}v\leadsto(v_{\\_}0,\widetilde{v},v_{\\_}{\ell^{\prime\prime}+1},\ldots,v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1})\\\
\widetilde{t}=u_{\\_}0(v_{\\_}0,\widetilde{v},v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1}),\widetilde{u}(\widetilde{v},v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1}),\\\
\qquad\qquad
u_{\\_}{\ell^{\prime}+1}(v_{\\_}{\ell^{\prime\prime}+1},\widetilde{v},v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1}),\ldots,u_{\\_}{\ell^{\prime}+|\widetilde{z}|}(v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|},\widetilde{v},v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1})\\\
t_{\\_}{m+1}=u_{\\_}{\ell^{\prime}+|\widetilde{z}|+1}(v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1},\widetilde{v},v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1})\\\
\ell^{\prime}=|\widetilde{u}|=\mathtt{ar}(\kappa)\quad
m=\ell^{\prime}+|\widetilde{z}|\quad\ell^{\prime\prime}=\mathtt{ar}(\kappa_{\\_}v)=|\widetilde{v}|.\end{array}$

By the induction hypothesis, we have:

$\begin{array}[]{l}\emptyset;\widetilde{z},x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}[\widetilde{s}/\widetilde{y}]u:\kappa_{\\_}v\to\kappa\leadsto\\\
\qquad(\theta_{\\_}0(u_{\\_}0,\widetilde{u},u_{\\_}{\ell^{\prime}+1},\ldots,u_{\\_}{\ell^{\prime}+|\widetilde{z}|}),\theta_{\\_}{1}u_{\\_}0\ldots,\theta_{\\_}{k}u_{\\_}0,\theta_{\\_}0u_{\\_}{\ell^{\prime}+|\widetilde{z}|+1})\\\
\emptyset;\widetilde{z},x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}[\widetilde{s}/\widetilde{y}]v:\kappa_{\\_}v\leadsto\\\
\qquad(\theta_{\\_}0(v_{\\_}0,\widetilde{v},v_{\\_}{\ell^{\prime\prime}+1},\ldots,v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|}),\theta_{\\_}{1}v_{\\_}0,\ldots,\theta_{\\_}{k}v_{\\_}{0},\theta_{\\_}0v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1})\\\
\end{array}$

By applying Tr-App, we obtain:

$\begin{array}[]{l}\emptyset;\widetilde{z},x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}([\widetilde{s}/\widetilde{y}]u)([\widetilde{s}/\widetilde{y}]v):\kappa\leadsto\\\
\qquad((\theta_{\\_}0u_{\\_}0)(\theta_{\\_}0v_{\\_}0,\theta_{\\_}0\widetilde{v},\theta_{\\_}{0}v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1}),(\theta_{\\_}0\widetilde{u})(\theta_{\\_}0\widetilde{v},\theta_{\\_}{0}v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1}),\\\
\qquad(\theta_{\\_}{0}u_{\\_}{\ell^{\prime}+1})(\theta_{\\_}0v_{\\_}{\ell^{\prime\prime}+1},\theta_{\\_}0\widetilde{v},\theta_{\\_}{0}v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1}),\ldots,(\theta_{\\_}{0}u_{\\_}{\ell^{\prime}+|\widetilde{z}|})(\theta_{\\_}0v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|},\theta_{\\_}0\widetilde{v},\theta_{\\_}{0}v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1}),\\\
\qquad(\theta_{\\_}{1}u_{\\_}{0})(\theta_{\\_}{1}v_{\\_}0,\theta_{\\_}0\widetilde{v},\theta_{\\_}{0}v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1}),\ldots,(\theta_{\\_}{k}u_{\\_}{0})(\theta_{\\_}{k}v_{\\_}0,\theta_{\\_}0\widetilde{v},\theta_{\\_}{0}v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1})\\\
\qquad(\theta_{\\_}{0}u_{\\_}{\ell^{\prime}+|\widetilde{z}|+1})(\theta_{\\_}{0}v_{\\_}{\ell^{\prime}+|\widetilde{z}|+1},\theta_{\\_}0\widetilde{v},\theta_{\\_}{0}v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1}).\end{array}$

Since $y_{\\_}{i,0}$ does not occur in $\widetilde{v}$ and
$v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1}$ (Lemma B.11),
$\theta_{\\_}0\widetilde{v}$ and
$\theta_{\\_}{0}u_{\\_}{\ell^{\prime}+|\widetilde{z}|+1}$ are equivalent to
$\theta_{\\_}j\widetilde{v}$ and
$\theta_{\\_}{j}u_{\\_}{\ell^{\prime}+|\widetilde{z}|+1}$ respectively for any
$j\in\\{1,\ldots,k\\}$. Therefore, the whole output of transformation is
equivalent to:

$\begin{array}[]{l}(\theta_{\\_}0(u_{\\_}0(v_{\\_}0,\widetilde{v},v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1})),\theta_{\\_}0(\widetilde{u}(\widetilde{v},v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|})),\\\
\quad\theta_{\\_}{0}(u_{\\_}{\ell^{\prime}+1}(v_{\\_}{\ell^{\prime\prime}+1},\widetilde{v},v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1})),\ldots,\theta_{\\_}{0}(u_{\\_}{\ell^{\prime}+|\widetilde{z}|}(v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|},\widetilde{v},v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1})),\\\
\quad\theta_{\\_}{1}(u_{\\_}0(v_{\\_}0,\widetilde{v},v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1})),\ldots,\theta_{\\_}{k}(u_{\\_}0(v_{\\_}0,\widetilde{v},v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1})),\\\
\quad\theta_{\\_}{0}(u_{\\_}{\ell^{\prime}+|\widetilde{z}|+1}(v_{\\_}{\ell^{\prime}+|\widetilde{z}|+1},\widetilde{v},v_{\\_}{\ell^{\prime\prime}+|\widetilde{z}|+1}))).\\\
\end{array}$

Thus, we have the required result.

  * •

Case Tr-NT: The result follows immediately from Tr-NT.

  * •

Case Tr-AppG: In this case, we have $t=uv$ and:

$\begin{array}[]{l}\widetilde{y}\mathbin{:}\widetilde{\kappa_{\\_}y};\widetilde{z}\vdash_{\mathcal{N}}u:\mathtt{o}^{\ell^{\prime}+1}\to\mathtt{o}\leadsto(u_{\\_}0,\ldots,u_{\\_}{\ell^{\prime}+|\widetilde{z}|+2})\\\
\widetilde{y}\mathbin{:}\widetilde{\kappa_{\\_}y};\widetilde{z}\vdash_{\mathcal{N}}v:\mathtt{o}\leadsto(v_{\\_}0,\ldots,v_{\\_}{|\widetilde{z}|+1})\\\
(\widetilde{t},t_{\\_}{m+1})=(u_{\\_}0+u_{\\_}1\cdot
v_{\\_}0,u_{\\_}2,\ldots,u_{\\_}{\ell^{\prime}+1},u_{\\_}{\ell^{\prime}+2}+u_{\\_}1\cdot
v_{\\_}{1},\ldots,u_{\\_}{\ell^{\prime}+|\widetilde{z}|+2}+u_{\\_}1\cdot
v_{\\_}{|\widetilde{z}|+1})\\\
\kappa=\mathtt{o}^{\ell^{\prime}}\to\mathtt{o}.\end{array}$

By the induction hypothesis, we have:

$\begin{array}[]{l}\emptyset;\widetilde{z},x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}[\widetilde{s}/\widetilde{y}]u:\mathtt{o}^{\ell^{\prime}+1}\to\mathtt{o}\leadsto(\theta_{\\_}{0}u_{\\_}0,\ldots,\theta_{\\_}{0}u_{\\_}{\ell^{\prime}+|\widetilde{z}|+1},\theta_{\\_}{1}u_{\\_}0,\ldots,\theta_{\\_}{k}u_{\\_}0,\theta_{\\_}{0}u_{\\_}{\ell^{\prime}+|\widetilde{z}|+k+2})\\\
\emptyset;\widetilde{z},x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}[\widetilde{s}/\widetilde{y}]v:\mathtt{o}\leadsto(\theta_{\\_}{0}v_{\\_}0,\ldots,\theta_{\\_}{0}v_{\\_}{|\widetilde{z}|},\theta_{\\_}{1}v_{\\_}{0},\ldots,\theta_{\\_}{k}v_{\\_}0,\theta_{\\_}{0}v_{\\_}{|\widetilde{z}|+1}).\end{array}$

By applying Tr-AppG, we obtain:

$\begin{array}[]{l}\emptyset;\widetilde{z},x_{\\_}1,\ldots,x_{\\_}k\vdash_{\mathcal{N}}([\widetilde{s}/\widetilde{y}]u)([\widetilde{s}/\widetilde{y}]v):\mathtt{o}^{\ell^{\prime}}\to\mathtt{o}\leadsto\\\
\qquad(\theta_{\\_}0u_{\\_}0+\theta_{\\_}0u_{\\_}1\cdot\theta_{\\_}0v_{\\_}0,\theta_{\\_}0u_{\\_}2,\ldots,\theta_{\\_}0u_{\\_}{\ell^{\prime}+1},\\\
\qquad\theta_{\\_}0u_{\\_}{\ell^{\prime}+2}+\theta_{\\_}{0}u_{\\_}1\cdot\theta_{\\_}{0}v_{\\_}1,\ldots,\theta_{\\_}{0}u_{\\_}{\ell^{\prime}+|\widetilde{z}|+1}+\theta_{\\_}0u_{\\_}1\cdot\theta_{\\_}0v_{\\_}{|\widetilde{z}|},\\\
\qquad\theta_{\\_}{1}u_{\\_}0+\theta_{\\_}{0}u_{\\_}1\cdot\theta_{\\_}{1}v_{\\_}0,\ldots,\theta_{\\_}{k}u_{\\_}0+\theta_{\\_}{0}u_{\\_}1\cdot\theta_{\\_}{k}v_{\\_}0,\theta_{\\_}{0}u_{\\_}{\ell^{\prime}+|\widetilde{z}|+2}+\theta_{\\_}{0}u_{\\_}1\cdot\theta_{\\_}{0}v_{\\_}{|\widetilde{z}|+1}).\end{array}$

Since $u_{\\_}1$ does not contain any occurrence of $y_{\\_}{i,0}$ (Lemma
B.11), $\theta_{\\_}0u_{\\_}1=\theta_{\\_}ju_{\\_}1$ for any
$j\in\\{1,\ldots,k\\}$. Therefore, the output of the translation is equivalent
to:

$\begin{array}[]{l}(\theta_{\\_}0(u_{\\_}0+u_{\\_}1\cdot
v_{\\_}0),\theta_{\\_}0u_{\\_}2,\ldots,\theta_{\\_}0u_{\\_}{\ell^{\prime}+1},\\\
\qquad\theta_{\\_}0(u_{\\_}{\ell^{\prime}+2}+u_{\\_}1\cdot
v_{\\_}1),\ldots,\theta_{\\_}{0}(u_{\\_}{\ell^{\prime}+|\widetilde{z}|+1}+u_{\\_}1\cdot
v_{\\_}{|\widetilde{z}|}),\\\ \qquad\theta_{\\_}{1}(u_{\\_}0+u_{\\_}1\cdot
v_{\\_}0),\ldots,\theta_{\\_}{k}(u_{\\_}0+u_{\\_}1\cdot
v_{\\_}0),\theta_{\\_}{0}(u_{\\_}{\ell^{\prime}+|\widetilde{z}|+2}+u_{\\_}1\cdot
v_{\\_}{|\widetilde{z}|+1})).\end{array}$

Thus, we have the required result.

We are now ready to prove that the translation relation is preserved by
reductions (Lemmas B.24, B.26, and B.28 below).

######  Lemma B.24 (Subject Reduction).

If
$\emptyset;\widetilde{x}\vdash_{\mathcal{N}}F\,\widetilde{s}\,\widetilde{t}:\mathtt{o}\leadsto(v_{\\_}0,\ldots,v_{\\_}{|\widetilde{x}|+1})$
and
$\mathcal{R}(F)=\lambda\widetilde{y}.\lambda\widetilde{z}.u_{\\_}L\,\oplus_{p}\,u_{\\_}R$
(where $\\{\widetilde{x}\\}\cap\\{\widetilde{z}\\}=\emptyset$), then there
exist $w_{\\_}{L,i},w_{\\_}{R,i}\ (i\in\\{0,\ldots,|\widetilde{x}|+1\\})$ such
that
$\emptyset;\widetilde{x}\vdash_{\mathcal{N}}\\{\widetilde{t}/\widetilde{z}\\}[\widetilde{s}/\widetilde{y}]u_{\\_}d\leadsto(w_{\\_}{d,0},\ldots,w_{\\_}{d,|\widetilde{x}|+1})$
and $v_{\\_}i\cong pw_{\\_}{L,i}+(1-p)w_{\\_}{R,i}$ for each
$i\in\\{0,\ldots,|\widetilde{x}|+1\\}$.

######  Proof B.25.

By the assumptions, we have:

$\begin{array}[]{l}\emptyset;\widetilde{x}\vdash_{\mathcal{N}}s_{\\_}i:\kappa_{\\_}i\leadsto(s_{\\_}{i,0},\ldots,s_{\\_}{i,\mathtt{ar}(\kappa_{\\_}i)+|\widetilde{x}|+1})\hfill\mbox{
for each $i\in\\{1,\ldots,|\widetilde{s}|\\}$}\\\
\emptyset;\widetilde{x}\vdash_{\mathcal{N}}t_{\\_}i:\mathtt{o}\leadsto(t_{\\_}{i,0},\ldots,t_{\\_}{i,|\widetilde{x}|+1})\mbox{
for each $i\in\\{1,\ldots,|\widetilde{z}|\\}$}\\\
v^{\prime}_{\\_}0=F_{\\_}0(s_{\\_}{1,0},\ldots,s_{\\_}{1,\mathtt{ar}(\kappa_{\\_}1)},s_{\\_}{1,\mathtt{ar}(\kappa_{\\_}1)+|\widetilde{x}|+1})\cdots(s_{\\_}{|\widetilde{s}|,0},\ldots,s_{\\_}{|\widetilde{s}|,\mathtt{ar}(\kappa_{\\_}{|\widetilde{s}|})},s_{\\_}{|\widetilde{s}|,\mathtt{ar}(\kappa_{\\_}{|\widetilde{s}|})+|\widetilde{x}|+1})\\\
v^{\prime}_{\\_}j=F_{\\_}j(s_{\\_}{1,1},\ldots,s_{\\_}{1,\mathtt{ar}(\kappa_{\\_}1)},s_{\\_}{1,\mathtt{ar}(\kappa_{\\_}1)+|\widetilde{x}|+1})\cdots(s_{\\_}{|\widetilde{s}|,1},\ldots,s_{\\_}{|\widetilde{s}|,\mathtt{ar}(\kappa_{\\_}{|\widetilde{s}|})},s_{\\_}{|\widetilde{s}|,\mathtt{ar}(\kappa_{\\_}{|\widetilde{s}|})+|\widetilde{x}|+1})\\\
\hfill\mbox{ for each $j\in\\{1,\ldots,|\widetilde{z}|\\}$}\\\
v^{\prime}_{\\_}{|\widetilde{z}|+j}=F_{\\_}0(s_{\\_}{1,\mathtt{ar}(\kappa_{\\_}1)+j},s_{\\_}{1,1},\ldots,s_{\\_}{1,\mathtt{ar}(\kappa_{\\_}1)},s_{\\_}{1,\mathtt{ar}(\kappa_{\\_}1)+|\widetilde{x}|+1})\cdots\\\
\qquad\qquad\quad(s_{\\_}{|\widetilde{s}|,\mathtt{ar}(\kappa_{\\_}1)+j},s_{\\_}{|\widetilde{s}|,1},\ldots,s_{\\_}{|\widetilde{s}|,\mathtt{ar}(\kappa_{\\_}{|\widetilde{s}|})},s_{\\_}{|\widetilde{s}|,\mathtt{ar}(\kappa_{\\_}{|\widetilde{s}|})+|\widetilde{x}|+1})\\\
\hfill\mbox{ for each $j\in\\{1,\ldots,|\widetilde{x}|\\}$}\\\
v^{\prime}_{\\_}{|\widetilde{z}|+|\widetilde{x}|+1}=F_{\\_}{0}(s_{\\_}{1,\mathtt{ar}(\kappa_{\\_}1)+|\widetilde{x}|+1},s_{\\_}{1,1},\ldots,s_{\\_}{1,\mathtt{ar}(\kappa_{\\_}1)},s_{\\_}{1,\mathtt{ar}(\kappa_{\\_}1)+|\widetilde{x}|+1})\cdots\\\
\qquad\qquad\qquad(s_{\\_}{|\widetilde{s}|,\mathtt{ar}(\kappa_{\\_}{|\widetilde{s}|})+|\widetilde{x}|+1},s_{\\_}{|\widetilde{s}|,1}\ldots,s_{\\_}{|\widetilde{s}|,\mathtt{ar}(\kappa_{\\_}{|\widetilde{s}|})},s_{\\_}{|\widetilde{s}|,\mathtt{ar}(\kappa_{\\_}{|\widetilde{s}|})+|\widetilde{x}|+1})\\\
v_{\\_}0\cong v^{\prime}_{\\_}0+v^{\prime}_{\\_}1\cdot
t_{\\_}{1,0}+\cdots+v^{\prime}_{\\_}{|\widetilde{z}|}\cdot
t_{\\_}{|\widetilde{z}|,0}\\\ v_{\\_}{|\widetilde{z}|+i}\cong
v^{\prime}_{\\_}{|\widetilde{z}|+i}+v^{\prime}_{\\_}1\cdot
t_{\\_}{1,i}+\cdots+v^{\prime}_{\\_}{|\widetilde{z}|}\cdot
t_{\\_}{|\widetilde{z}|,i}\mbox{ for each
$i\in\\{1,\ldots,|\widetilde{x}|+1\\}$}\\\
\widetilde{y}\mathbin{:}\widetilde{\kappa};\widetilde{z}\vdash_{\mathcal{N}}u_{\\_}d:\mathtt{o}\leadsto(u_{\\_}{d,0},\ldots,u_{\\_}{d,|\widetilde{z}|+1})\mbox{
for $d\in\\{L,R\\}$}\end{array}$

By applying the substitution lemma (Lemma B.22) to the last condition, we
obtain:

$\begin{array}[]{l}\emptyset;\widetilde{z},\widetilde{x}\vdash_{\mathcal{N}}[\widetilde{s}/\widetilde{y}]u_{\\_}d:\mathtt{o}\leadsto(w^{\prime}_{\\_}{d,0},\ldots,w^{\prime}_{\\_}{d,|\widetilde{z}|+|\widetilde{x}|+1})\end{array}$

where

$\begin{array}[]{l}(w^{\prime}_{\\_}{d,0},\ldots,w^{\prime}_{\\_}{d,|\widetilde{z}|+|\widetilde{x}|+1})=(\theta_{\\_}0u_{\\_}{d,0},\ldots,\theta_{\\_}0u_{\\_}{d,|\widetilde{z}|},\theta_{\\_}1u_{\\_}{d,0},\ldots,\theta_{\\_}{|\widetilde{x}|}u_{\\_}{d,0},\theta_{\\_}0u_{\\_}{d,|\widetilde{z}|+1})\\\
\theta_{\\_}j=\theta_{\\_}{1,j}\cdots\theta_{\\_}{|\widetilde{s}|,j}\mbox{ for
$j\in\\{0,\ldots,|\widetilde{x}|\\}$}\\\
\theta_{\\_}{i,0}=[s_{\\_}{i,0}/y_{\\_}{i,0},\ldots,s_{\\_}{i,\mathtt{ar}(\kappa_{\\_}i)}/y_{\\_}{i,\mathtt{ar}(\kappa_{\\_}i)},s_{\\_}{i,\mathtt{ar}(\kappa_{\\_}i)+|\widetilde{x}|+1}/y_{\\_}{i,\mathtt{ar}(\kappa_{\\_}i)+1}]\mbox{
for $i\in\\{1,\ldots,|\widetilde{s}|\\}$}\\\
\theta_{\\_}{i,j}=[s_{\\_}{i,\mathtt{ar}(\kappa_{\\_}i)+j}/y_{\\_}{i,0},\ldots,s_{\\_}{i,\mathtt{ar}(\kappa_{\\_}i)}/y_{\\_}{i,\mathtt{ar}(\kappa_{\\_}i)},s_{\\_}{i,\mathtt{ar}(\kappa_{\\_}i)+|\widetilde{x}|+1}/y_{\\_}{i,\mathtt{ar}(\kappa_{\\_}i)+1}]\\\
\hfill\mbox{ for
$i\in\\{1,\ldots,|\widetilde{s}|\\},j\in\\{1,\ldots,|\widetilde{x}|\\}$}.\\\
\end{array}$

Then, we have $v_{\\_}j^{\prime}\cong
pw^{\prime}_{\\_}{L,j^{\prime}}+(1-p)w^{\prime}_{\\_}{R,j^{\prime}}$. (Here,
the only non-trivial case is for $j=|\widetilde{z}|+|\widetilde{x}|+1$, where
we need to show that $v_{\\_}j^{\prime}\cong
p\theta_{\\_}{|\widetilde{x}|+1}u_{\\_}{L,0}+(1-p)\theta_{\\_}{|\widetilde{x}|+1}u_{\\_}{R,0}$
is equivalent to
$pw^{\prime}_{\\_}{L,j^{\prime}}+(1-p)w^{\prime}_{\\_}{R,j^{\prime}}$; in this
case, by induction on the structure of $u_{\\_}d$, it follows that
$\theta_{\\_}{|\widetilde{x}|+1}u_{\\_}{d,0}=\theta_{\\_}0u_{\\_}{d,|\widetilde{z}|+1}$,
which implies the required property) Let $\widetilde{w}_{\\_}d$ be
$(w_{\\_}{d,0},\ldots,w_{\\_}{d,|\widetilde{x}|+1})$, where:

$\begin{array}[]{l}w_{\\_}{d,0}=w^{\prime}_{\\_}{d,0}+w^{\prime}_{\\_}{d,1}\cdot
t_{\\_}{1,0}+\cdots+w^{\prime}_{\\_}{d,{|\widetilde{z}|}}\cdot
t_{\\_}{|\widetilde{z}|,0}\\\
w_{\\_}{d,i}=w^{\prime}_{\\_}{d,{|\widetilde{z}|+i}}+w^{\prime}_{\\_}{d,1}\cdot
t_{\\_}{1,i}+\cdots+w^{\prime}_{\\_}{d,{|\widetilde{z}|}}\cdot
t_{\\_}{|\widetilde{z}|,i}\\\ \hfill\mbox{ for
$i\in\\{1,\ldots,|\widetilde{x}|+1\\}$}.\end{array}$

Then, the required result is obtained by applying Tr-Sub to

$\begin{array}[]{l}\emptyset;\widetilde{z},\widetilde{x}\vdash_{\mathcal{N}}[\widetilde{s}/\widetilde{y}]u_{\\_}d:\mathtt{o}\leadsto(w^{\prime}_{\\_}{d,0},\ldots,w^{\prime}_{\\_}{d,|\widetilde{z}|+|\widetilde{x}|+1}).\end{array}$

######  Lemma B.26 (Subject Reduction (for administrative steps)).

If
$\emptyset;\widetilde{x}\vdash_{\mathcal{N}}\\{\widetilde{s}/\widetilde{z}\\}x_{\\_}i:\mathtt{o}\leadsto(t_{\\_}0,\ldots,t_{\\_}{|\widetilde{x}|+1})$
with $x_{\\_}i\notin\\{\widetilde{z}\\}$, then
$\emptyset;\widetilde{x}\vdash_{\mathcal{N}}x_{\\_}i:\mathtt{o}\leadsto(u_{\\_}0,\ldots,u_{\\_}{|\widetilde{x}|+1})$
for some $u_{\\_}j\ (j\in\\{0,\ldots,|\widetilde{x}|+1\\})$ such that
$t_{\\_}j\cong u_{\\_}j$ for each $j\in\\{0,\ldots,|\widetilde{x}|+1\\}$.

######  Proof B.27.

By the assumption
$\emptyset;\widetilde{x}\vdash_{\mathcal{N}}\\{\widetilde{s}/\widetilde{z}\\}x_{\\_}i:\mathtt{o}\leadsto(t_{\\_}0,\ldots,t_{\\_}{|\widetilde{x}|+1})$,
we have:

$\begin{array}[]{l}\emptyset;\widetilde{z},\widetilde{x}\vdash_{\mathcal{N}}x_{\\_}i:\mathtt{o}\leadsto({0}^{i+|\widetilde{z}|+1},1,{0}^{|\widetilde{x}|-i+1})\\\
\emptyset;\widetilde{x}\vdash_{\mathcal{N}}s_{\\_}j:\mathtt{o}\leadsto(s_{\\_}{j,0},\ldots,s_{\\_}{j,|\widetilde{x}|+1})\mbox{
(for each $j\in\\{1,\ldots,|\widetilde{s}|\\}$)}\\\
t_{\\_}i=1+\Sigma_{\\_}{j=1}^{|\widetilde{s}|}0\cdot s_{\\_}{j,i}\cong 1\qquad
t_{\\_}{i^{\prime}}\cong 0\mbox{ for $i^{\prime}\neq i$}\end{array}$

Since
$\emptyset;\widetilde{x}\vdash_{\mathcal{N}}x_{\\_}i:\mathtt{o}\leadsto(0^{i},1,0^{|\widetilde{x}|-i+1})$,
we have the required condition for: $u_{\\_}i=1$ and $u_{\\_}j=0$ for $j\neq
i$.

######  Lemma B.28 (Subject Reduction (for administrative steps (ii))).

If
$\emptyset;\widetilde{x}\vdash_{\mathcal{N}}\\{\widetilde{s}/\widetilde{z}\\}z_{\\_}i:\mathtt{o}\leadsto(t_{\\_}0,\ldots,t_{\\_}{|\widetilde{x}|+1})$,
then
$\emptyset;\widetilde{x}\vdash_{\mathcal{N}}s_{\\_}i:\mathtt{o}\leadsto(u_{\\_}0,\ldots,u_{\\_}{|\widetilde{x}|+1})$
for some $u_{\\_}j\ (j\in\\{0,\ldots,|\widetilde{x}|+1\\})$ such that
$t_{\\_}j\cong u_{\\_}j$ for each $j\in\\{0,\ldots,|\widetilde{x}|+1\\}$.

######  Proof B.29.

By the assumption
$\emptyset;\widetilde{x}\vdash_{\mathcal{N}}\\{\widetilde{s}/\widetilde{z}\\}z_{\\_}i:\mathtt{o}\leadsto(t_{\\_}0,\ldots,t_{\\_}{|\widetilde{x}|+1})$,
we have:

$\begin{array}[]{l}\emptyset;\widetilde{z},\widetilde{x}\vdash_{\mathcal{N}}z_{\\_}i:\mathtt{o}\leadsto(0^{i},1,{0}^{|\widetilde{z}|-i+|\widetilde{x}|+1})\\\
\emptyset;\widetilde{x}\vdash_{\mathcal{N}}s:\mathtt{o}\leadsto(s_{\\_}0,\ldots,s_{\\_}{|\widetilde{x}|+1})\\\
t_{\\_}j\cong 0+1\cdot s_{\\_}j\cong s_{\\_}j\mbox{ for each
$j\in\\{0,\ldots,|\widetilde{x}|+1\\}$}.\end{array}$

Thus, the result holds for $u_{\\_}j=s_{\\_}j$.

We are now ready to prove Theorem 5, restricted to recursion-free PHORS (the
definition of recursion-free PHORS is found in Section B.1).

######  Lemma B.30.

Let $\mathcal{G}=(\mathcal{N},\mathcal{R},S)$ be a recursion-free PHORS, and
$\rho$ be the least solution of $\mathcal{E}^{\mathtt{ref}}_{\mathcal{G}}$.
Then, $\mathcal{P}(\mathcal{G},S\,\mathtt{e})=\rho(S_{\\_}1)$.

######  Proof B.31.

By Lemma B.16, it suffices to show that
$\emptyset;x\vdash_{\mathcal{N}}t\leadsto(t_{\\_}0,t_{\\_}1,t_{\\_}2)$ implies
$\mathcal{P}_{\mathtt{es}}(\mathcal{G},t,x)\cong t_{\\_}1$. This follows by
induction on $\flat(t)$, the length of the longest reduction sequence from $t$
by $\xrightarrow{d,p}_{\texttt{es}}{}$; note that $\flat(t)$ is well defined
because $t$ is finitely branching and strongly normalizing with respect to
$\xrightarrow{d,p}_{\texttt{es}}{}$; the strong normalization follows from
Lemma B.14 and the fact that there can be no infinite sequence of consecutive
administrative reductions (in fact, each administrative reduction consumes one
explicit substitution).

Suppose $\flat(t)=0$. Then, $t$ is either $x$ (in which case, $t_{\\_}1=1$) or
$\Omega$ (in which case, $t_{\\_}1=0$). Thus, the result follows immediately.

If $\flat(t)>0$, we perform a case analysis on a reduction of $t$. If
$t\xrightarrow{\epsilon,1}_{\texttt{es}}t^{\prime}$, then by Lemmas B.26 and
B.28,
$\emptyset;x\vdash_{\mathcal{N}}t\leadsto(t^{\prime}_{\\_}0,t^{\prime}_{\\_}1,t^{\prime}_{\\_}2)$
and $t_{\\_}1\cong t^{\prime}_{\\_}1$ for some
$(t^{\prime}_{\\_}0,t^{\prime}_{\\_}1,t^{\prime}_{\\_}2)$. By the induction
hypothesis, $\mathcal{P}_{\mathtt{es}}(\mathcal{G},t^{\prime},x)\cong
t^{\prime}_{\\_}1$. Therefore, we have
$\mathcal{P}_{\mathtt{es}}(\mathcal{G},t,x)=\mathcal{P}_{\mathtt{es}}(\mathcal{G},t^{\prime},x)\cong
t^{\prime}_{\\_}1\cong t_{\\_}1$ as required.

If $t\xrightarrow{d,p}_{\texttt{es}}t^{\prime}$ for $d\in\\{L,R\\}$, then $t$
must be of the form $E[F\,\widetilde{s}\,\widetilde{t}]$,
$\mathcal{R}(F)=\lambda\widetilde{y}.\lambda\widetilde{z}.u_{\\_}L\,\oplus_{p}\,u_{\\_}R$,
$t\xrightarrow{L,p}_{\texttt{es}}t_{\\_}L$, and
$t\xrightarrow{R,1-p}_{\texttt{es}}t_{\\_}R$ with
$t_{\\_}L=E[\\{\widetilde{t}/\widetilde{z}\\}[\widetilde{s}/\widetilde{y}]u_{\\_}L]$
and
$t_{\\_}R=E[\\{\widetilde{t}/\widetilde{z}\\}[\widetilde{s}/\widetilde{y}]u_{\\_}R]$.
By Lemma B.24, there exist $(t_{\\_}{L,0},t_{\\_}{L,1},t_{\\_}{L,2})$ and
$(t_{\\_}{R,0},t_{\\_}{R,1},t_{\\_}{R,2})$ such that
$\emptyset;x\vdash_{\mathcal{N}}t_{\\_}L\leadsto(t_{\\_}{L,0},t_{\\_}{L,1},t_{\\_}{L,2})$
and
$\emptyset;x\vdash_{\mathcal{N}}t_{\\_}R\leadsto(t_{\\_}{R,0},t_{\\_}{R,1},t_{\\_}{R,2})$
with $t_{\\_}1\cong pt_{\\_}{L,1}+(1-p)t_{\\_}{R,1}$. Thus, we have
$\mathcal{P}_{\mathtt{es}}(\mathcal{G},t,x)=p\mathcal{P}_{\mathtt{es}}(\mathcal{G},t_{\\_}L,x)+(1-p)\mathcal{P}_{\mathtt{es}}(\mathcal{G},t_{\\_}R,x)\cong
pt_{\\_}{L,1}+(1-p)t_{\\_}{R,1}\cong t_{\\_}1$ as required.

We are now ready to prove Theorem 5.

######  Proof B.32 (Proof of Theorem 5).

Consider the finite approximation $\mathcal{G}^{(k)}$ (defined in Section
B.1). Then, we have

$\begin{array}[]{l}\mathcal{P}(\mathcal{G},S\,\mathtt{e})=\bigsqcup_{\\_}k\mathcal{P}(\mathcal{G}^{(k)},S^{(k)}\,\mathtt{e})=\bigsqcup_{\\_}k\mathbf{lfp}(\mathcal{F}_{\\_}{\mathcal{G}^{(k)}})(S_{\\_}1^{(k)})\\\
=\bigsqcup_{\\_}k\mathcal{F}_{\\_}{\mathcal{G}}^{k}(\bot)(S_{\\_}1)=\mathbf{lfp}(\mathcal{F}_{\\_}{\mathcal{G}})(S_{\\_}1)=\rho_{\\_}{\mathcal{E}^{\mathtt{ref}}_{\mathcal{G}}}(S_{\\_}1)\end{array}$

as required. Here $\mathcal{F}_{\\_}\mathcal{G}$ is the functional associated
with fixpoint equations $\mathcal{E}^{\mathtt{ref}}_{\mathcal{G}}$, as defined
in Section 4.1, and we can use essentially the same reasoning as in the proofs
of Lemma B.6 and Theorem 4.