$\sqsubseteq^{\prime}$ be a point-wise lifting of $\preceq^{\prime}$, i.e.,
for an arbitrary domain $D$ and any $f,g\in(D\to D^{\prime})$,
$f\sqsubseteq^{\prime}g$ if and only if $\forall d\in
D.~{}f(d)\preceq^{\prime}g(d)$. Then, $(D\to D^{\prime},\sqsubseteq^{\prime})$
is a partial order.

###### Proof.

Let $f,g,h\in(D\to D^{\prime})$. We need to show that $\sqsubseteq$ is a
partial order, i.e., it is reflexive, antisymmetric and transitive.

(refl. of $\prec^{\prime}$) $\displaystyle\mathbf{Reflexivity:}$
$\displaystyle\forall d\in D.~{}f(d)\preceq^{\prime}f(d)$
$\displaystyle\implies$ $\displaystyle f\sqsubseteq^{\prime}f$
$\displaystyle\mathbf{Transitivity:}$ $\displaystyle
f\sqsubseteq^{\prime}h~{}\text{and}~{}h\sqsubseteq^{\prime}g$
$\displaystyle\implies$ $\displaystyle\forall d\in
D.~{}f(d)\preceq^{\prime}h(d)~{}\text{and}~{}h(d)\preceq^{\prime}g(d)$ (trans.
of $\preceq^{\prime}$) $\displaystyle\implies$ $\displaystyle\forall d\in
D.~{}f(d)\preceq^{\prime}g(d)$ $\displaystyle\implies$ $\displaystyle
f\sqsubseteq g^{\prime}$ $\displaystyle\mathbf{Antisymmetry:}$ $\displaystyle
f\sqsubseteq^{\prime}g~{}\text{and}~{}g\sqsubseteq^{\prime}g$
$\displaystyle\implies$ $\displaystyle\forall d\in
D.~{}f(d)\preceq^{\prime}g(d)~{}\text{and}~{}g(d)\preceq^{\prime}f(d)$
(antisym. of $\preceq^{\prime}$) $\displaystyle\implies$ $\displaystyle\forall
d\in D.~{}f(d)=g(d)$ ∎ $\displaystyle\implies$ $\displaystyle f=g$

∎

###### Lemma 7 (Point-Wise Lifting of Complete Lattices).

Let $(D^{\prime},\preceq^{\prime})$ be a complete lattice and
$\sqsubseteq^{\prime}$ be a point-wise lifting of $\preceq^{\prime}$, i.e. for
an arbitrary domain $D$ and any $f,g\in(D\to D^{\prime})$, let
$f\sqsubseteq^{\prime}g$ if and only if $~{}\forall f\in
D.~{}f(d)\preceq^{\prime}g(d).$ Then $(D\to D^{\prime},\sqsubseteq^{\prime})$
is a complete lattice.

###### Proof.

We claim that every subset $S\subseteq(D\to D^{\prime})$ has a least upper
bound given by

$\sup S=\lambda d.\sup S_{d},\quad\text{where}\quad S_{d}\coloneq\\{f(d)\mid
f\in S\\}\subseteq D^{\prime}~{}.$

First we show that $\sup S$ is an upper bound, as for every $f\in S$

$\displaystyle\forall d\in D.\quad f(d)\preceq^{\prime}\sup S_{d}=(\sup S)(d)$
$\displaystyle\implies$ $\displaystyle f\sqsubseteq^{\prime}\sup S$

Second, $\sup S$ is the _least_ upper bound. Therefore, let $\hat{f}$ be an
upper bound of $S$.

$\displaystyle\forall f\in S.\quad f\sqsubseteq^{\prime}\hat{f}$
$\displaystyle\implies$ $\displaystyle\forall f\in S.\quad\forall d\in
D.~{}f(d)\preceq^{\prime}\hat{f}(d)$ $\displaystyle\implies$
$\displaystyle\forall d\in D.\quad(\sup S)(d)=\sup
S_{d}\preceq^{\prime}\hat{f}(d)$ ∎ $\displaystyle\implies$ $\displaystyle\sup
S\sqsubseteq^{\prime}f$

∎

###### Theorem 8 (Fixed Point Theorems (Lassez et al., 1982; Abramsky and
Jung, 1994)).

Let $f\colon D\to D$ be a continuous function on a complete lattice
$(D,\sqsubseteq)$. Then $f$ possesses a least fixed point denoted lfp $f$,
which is given by:

  1. (1)

$\textup{lfp}\ f=\sup\\{f^{n}(\bot)\mid n\in\mathbb{N}\\}$, where $f^{n}$
denotes the $n$-fold application of $f$, and $\bot=\sup\emptyset$ is the least
element of $D$.

  2. (2)

$\textup{lfp}\ f=\inf\\{d\in D\mid f(d)\sqsubseteq d\\}$.

##  Appendix B Semantics Using eFPS

###### Corollary 1 (Partial Orders over eFPS).

$(\textnormal{{eFPS}},\preceq)$ as well as the point-wise lifting on functions
$(\textnormal{{eFPS}}\to\textnormal{{eFPS}},\sqsubseteq)$ are partial orders.

###### Proof.

Consider the coefficient function
$[\cdot]_{F}\in(\mathbb{N}^{k}\cup\\{\lightning\\}\to\mathbb{R}_{\geq
0}^{\infty})$ which uniquely determines the eFPS $F$. We think of the order
$\preceq$ as acting on the domain
$(\mathbb{N}^{k}\cup\\{\lightning\\}\to\mathbb{R}_{\geq 0}^{\infty})$. Thus,
$\preceq$ can be interpreted as the point-wise lifting of the (total) order
$\leq$ on $\mathbb{R}_{\geq 0}^{\infty}$, i.e.,
$(\textnormal{{eFPS}},\preceq)$ is a partial order by applying Lemma 6. Since
$\sqsubseteq$ is a point-wise lifting of $\preceq$, we can argue analogously
for $(\textnormal{{eFPS}}\to\textnormal{{eFPS}},\sqsubseteq)$. ∎

###### Corollary 2 (Complete Lattices over eFPS).

Both partial orders $(\textnormal{{eFPS}},\preceq)$ and
$(\textnormal{{eFPS}}\to\textnormal{{eFPS}},\sqsubseteq)$ are complete
lattices.

###### Proof.

Analogously to the proof of Corollary 1 we note that $\preceq$ is a point-wise
lifting of $\leq$ on $\mathbb{R}_{\geq 0}^{\infty}$, and $\sqsubseteq$ is a
point-wise lifting on $\preceq$. Therefore applying Lemma 7 twice yields the
claimed result. ∎

###### Lemma 3 (Continuity of $\Phi_{B,P}$).

Let $P$ be a cpGCL program and let $B$ be a Boolean guard. The characteristic
functional $\Phi_{B,P}$ is continuous on the domain
$\left(\textnormal{{eFPS}}\rightarrow\textnormal{{eFPS}},\sqsubseteq\right)$.

###### Proof.

$\displaystyle\Phi_{B,P}(\sup S)$ $\displaystyle=\Phi_{B,P}(\lambda
F.~{}\sup\left\\{\psi(F)\mid\psi\in S\right\\})$ $\displaystyle=\lambda
F.~{}[\lightning]_{F}\cdot X_{\lightning}+\langle{}F{}\rangle_{\neg B}$ (Def.
$\Phi_{B,P}$) $\displaystyle\qquad+(\lambda
F.~{}\sup\,\left\\{\psi(F)\mid\psi\in S\right\\})(\llbracket
P\rrbracket(\langle{}F{}\rangle_{B}))$ (Evaluate inner $\lambda$-function)
$\displaystyle=\lambda F.~{}[\lightning]_{F}\cdot
X_{\lightning}+\langle{}F{}\rangle_{\neg B}+\sup\,\left\\{\psi(\llbracket
P\rrbracket(\langle{}F{}\rangle_{B}))\mid\psi\in S\right\\}$ (Include
constants in $\sup$) $\displaystyle=\lambda
F.~{}\sup\,\left\\{[\lightning]_{F}\cdot
X_{\lightning}+\langle{}F{}\rangle_{\neg B}+\psi(\llbracket
P\rrbracket(\langle{}F{}\rangle_{B}))\mid\psi\in S\right\\}$ ($\sup$ defined
point-wise) $\displaystyle=\sup\,\left\\{\lambda F.~{}[\lightning]_{F}\cdot
X_{\lightning}+\langle{}F{}\rangle_{\neg B}+\psi(\llbracket
P\rrbracket(\langle{}F{}\rangle_{B}))\mid\psi\in S\right\\}$ (Def.
$\Phi_{B,P}$) $\displaystyle=\sup\,\left\\{\Phi_{B,P}(\psi)\mid\psi\in
S\right\\}$

∎

###### Lemma 4 (Continuity of Auxiliary Functions).

For all $\sigma\in\mathbb{N}^{k}\cup\\{\lightning\\}$ and Boolean guards $B$,
the following functions are continuous:

  1. (1)

the coefficient function $[\sigma]$

  2. (2)

the restriction $\langle{}\cdot{}\rangle_{B}$

  3. (3)

the mass $\left|\cdot\right|$

###### Proof.

1 and 2 follow directly from the coefficient-wise definition of $\sup$ on
eFPS. For 3, let $S=\left\\{F_{i}\mid
i\in\mathbb{N}\right\\}\subseteq\textnormal{{eFPS}}$ be an $\omega$-chain with
$F_{0}\preceq F_{1}\preceq F_{2}\preceq\dots$. Then:

$\displaystyle\left|\sup S\right|$
$\displaystyle=\sum_{\sigma\in\mathbb{N}^{k}}[\sigma]_{\sup S}$
$\displaystyle=\sum_{\sigma\in\mathbb{N}^{k}}\sup\left\\{[\sigma]_{F_{i}}\mid
i\in\mathbb{N}\right\\}$ (Monotone Convergence Theorem)
$\displaystyle=\sup\left\\{\sum_{\sigma\in\mathbb{N}^{k}}[\sigma]_{F_{i}}~{}\big{|}~{}i\in\mathbb{N}\right\\}$
$\displaystyle=\sup\left\\{\left|F_{i}\right|\mid i\in\mathbb{N}\right\\}$

∎

###### Theorem 5 (Continuity of $\llbracket\cdot\rrbracket$).

For every cpGCL program $P$, $\llbracket P\rrbracket$ is continuous on the
domain $\left(\textnormal{{eFPS}}\rightarrow\textnormal{{eFPS}}\right)$.

###### Proof.

Let $S\subseteq\textnormal{{eFPS}}$. The proof proceeds by induction over the
structure of $P$:

##### Case $P=\textnormal{{skip}}$:

$\displaystyle\llbracket P\rrbracket(\sup S)$ $\displaystyle=\sup
S=\sup\left\\{F\mid F\in S\right\\}=\sup\left\\{\llbracket P\rrbracket(F)\mid
F\in S\right\\}$

##### Case $P=x_{i}\mathrel{\textnormal{$\mathtt{\coloneqq}$}}E$:

$\displaystyle\llbracket P\rrbracket(\sup S)$ $\displaystyle=\llbracket
P\rrbracket\left([\lightning]_{\sup S}\cdot
X_{\lightning}+\sum_{\sigma\in\mathbb{N}^{k}}[\sigma]_{\sup
S}\cdot\mathbf{X}^{\sigma}\right)$ $\displaystyle=[\lightning]_{\sup S}\cdot
X_{\lightning}+\sum_{\sigma\in\mathbb{N}^{k}}[\sigma]_{\sup S}\cdot
X_{1}^{\sigma_{1}}\cdots X_{i}^{\mathrm{eval}_{\sigma}(E)}\cdots
X_{k}^{\sigma_{k}}$ $\displaystyle=\sup_{F\in S}\left\\{[\lightning]_{F}\cdot
X_{\lightning}+\sum_{\sigma\in\mathbb{N}^{k}}[\sigma]_{F}\cdot
X_{1}^{\sigma_{1}}\cdots X_{i}^{\mathrm{eval}_{\sigma}(E)}\cdots
X_{k}^{\sigma_{k}}\right\\}$ $\displaystyle=\sup_{F\in S}\left\\{\llbracket
P\rrbracket(F)\right\\}$

##### Case $P=\textnormal{{observe}}\,\left(\,{B}\,\right)$:

$\displaystyle\llbracket P\rrbracket(\sup S)$
$\displaystyle=\left([\lightning]_{\sup S}+\left|\langle{}\sup
S{}\rangle_{\neg B}\right|\right)\cdot X_{\lightning}+\langle{}\sup
S{}\rangle_{B}$ $\displaystyle=\left([\lightning]_{\sup
S}+\sup\left\\{\left|\langle{}F{}\rangle_{\neg B}\right|\mid F\in
S\right\\}\right)\cdot X_{\lightning}$ (Cont. of $\left|\cdot\right|$,
$\langle{}\cdot{}\rangle_{B}$)
$\displaystyle\qquad+\sup\left\\{\langle{}F{}\rangle_{B}\mid F\in S\right\\}$
$\displaystyle=\sup\left\\{\left([\lightning]_{F}+\left|\langle{}F{}\rangle_{\neg
B}\right|\right)\cdot X_{\lightning}+\langle{}F{}\rangle_{B}\right\\}$
$\displaystyle=\sup\left\\{\llbracket P\rrbracket(F)\mid F\in S\right\\}$

##### Case
$P=\left\\{\,{P_{1}}\,\right\\}\mathrel{\left[\,p\,\right]}\left\\{\,{P_{2}}\,\right\\}$:

$\displaystyle\llbracket P\rrbracket(\sup S)$ $\displaystyle=p\cdot\llbracket
P_{1}\rrbracket(\sup S)+(1-p)\cdot\llbracket P_{2}\rrbracket(\sup S)$
$\displaystyle=p\cdot\sup\left\\{\llbracket P_{1}\rrbracket(F)\mid F\in
S\right\\}$ (I.H. on $P_{1}$ and $P_{2}$)
$\displaystyle\qquad+(1-p)\cdot\sup\left\\{\llbracket P_{2}\rrbracket(F)\mid
F\in S\right\\}$ $\displaystyle=\sup\left\\{p\cdot\llbracket
P_{1}\rrbracket(F)+(1-p)\cdot\llbracket P_{2}\rrbracket(F)\mid F\in
S\right\\}$ $\displaystyle=\sup\left\\{\llbracket P\rrbracket(F)\mid F\in
S\right\\}$

##### Case
$P=\textnormal{{if}}\,\left(\,{B}\,\right)\,\left\\{\,{P_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{P_{2}}\,\right\\}$:

$\displaystyle\llbracket P\rrbracket(\sup S)$
$\displaystyle=[\lightning]_{\sup S}\cdot X_{\lightning}+\llbracket
P_{1}\rrbracket(\langle{}\sup S{}\rangle_{P})+\llbracket
P_{2}\rrbracket(\langle{}\sup S{}\rangle_{\neg B})$
$\displaystyle=[\lightning]_{\sup S}\cdot
X_{\lightning}+\sup\left\\{\llbracket
P_{1}\rrbracket(\langle{}F{}\rangle_{P})\mid F\in S\right\\}$ (I.H. on $P_{1}$
and $P_{2}$) $\displaystyle\qquad+\sup\left\\{\llbracket
P_{2}\rrbracket(\langle{}F{}\rangle_{\neg B})\mid F\in S\right\\}$
$\displaystyle=\sup\left\\{[\lightning]_{F}\cdot X_{\lightning}+\llbracket
P_{1}\rrbracket(\langle{}F{}\rangle_{P})+\llbracket
P_{2}\rrbracket(\langle{}F{}\rangle_{\neg B}\mid F\in S\right\\}$
$\displaystyle=\sup\left\\{\llbracket P\rrbracket(F)\mid F\in S\right\\}$

##### Case $P=P_{1}\fatsemi P_{2}$:

$\displaystyle\llbracket P\rrbracket(\sup S)$ $\displaystyle=\llbracket
P_{2}\rrbracket\left(\llbracket P_{1}\rrbracket(\sup S)\right)$ (I.H. on
$P_{1}$) $\displaystyle=\llbracket P_{2}\rrbracket\left(\sup\left\\{\llbracket
P_{1}\rrbracket(F)\mid F\in S\right\\}\right)$ (I.H. on $P_{2}$)
$\displaystyle=\sup\left\\{\llbracket P_{2}\rrbracket(\llbracket
P_{1}\rrbracket(F))\mid F\in S\right\\}$ $\displaystyle=\sup\left\\{\llbracket
P\rrbracket(F)\mid F\in S\right\\}$

##### Case
$P=\textnormal{{while}}\left(\,{B}\,\right)\left\\{\,{P_{1}}\,\right\\}$:

In this case, we use that for all $n\in\mathbb{N}$, $\Phi_{B,P_{1}}^{n}(\bot)$
is continuous, which we prove by induction:

##### Base case:

$n=0$.

$\displaystyle\Phi_{B,P_{1}}^{0}(\bot)(\sup S)$
$\displaystyle=0=\sup\left\\{\Phi_{B,P_{1}}^{0}(\bot)(F)\mid F\in S\right\\}$

##### Induction step:

$\displaystyle\Phi_{B,P_{1}}^{n+1}(\bot)(\sup S)$
$\displaystyle=\Phi_{B,P_{1}}\left(\Phi_{B,P_{1}}^{n}(\bot)\right)(\sup S)$
$\displaystyle=[\lightning]_{\sup S}+\langle{}\sup S{}\rangle_{\neg B}$ (Def.
$\Phi_{B,P_{1}}$) $\displaystyle\qquad+\Phi_{B,P_{1}}^{n}(\bot)(\llbracket
P_{1}\rrbracket(\langle{}\sup S{}\rangle_{B}))$
$\displaystyle=[\lightning]_{\sup S}+\sup\left\\{\langle{}F{}\rangle_{\neg
B}\mid F\in S\right\\}$ (Cont. of $\langle{}\cdot{}\rangle_{B}$, outer I.H. on
$P_{1}$)
$\displaystyle\qquad+\Phi_{B,P_{1}}^{n}(\bot)\left(\sup\left\\{\llbracket
P_{1}\rrbracket(\langle{}F{}\rangle_{B})\mid F\in S\right\\}\right)$
$\displaystyle=[\lightning]_{\sup S}+\sup\left\\{\langle{}F{}\rangle_{\neg
B}\mid F\in S\right\\}$ (Inner I.H.)
$\displaystyle\quad+\sup\left\\{\Phi_{B,P_{1}}^{n}(\bot)\left(\llbracket
P_{1}\rrbracket(\langle{}F{}\rangle_{B})\right)\mid F\in S\right\\}$
$\displaystyle=\sup_{F\in S}\left\\{[\lightning]_{F}+\langle{}F{}\rangle_{\neg
B}+\Phi_{B,P_{1}}^{n}(\bot)\left(\llbracket
P_{1}\rrbracket(\langle{}F{}\rangle_{B})\right)\right\\}$
$\displaystyle=\sup\left\\{\Phi_{B,P_{1}}^{n+1}(\bot)(F)\mid F\in S\right\\}$

With this, it follows:

$\displaystyle\llbracket P\rrbracket(\sup S)$
$\displaystyle=\left(\sup_{n\in\mathbb{N}}\Phi_{B,P_{1}}^{n}(\bot)\right)(\sup
S)$ $\displaystyle=\sup\left\\{\Phi_{B,P_{1}}^{n}(\bot)(\sup S)\mid
n\in\mathbb{N}\right\\}$ (Cont. of $\Phi_{B,P_{1}}^{n}(\bot)$)
$\displaystyle=\sup\left\\{\sup\left\\{\Phi_{B,P_{1}}^{n}(\bot)(F)\mid F\in
S\right\\}\mid n\in\mathbb{N}\right\\}$ (swap suprema)
$\displaystyle=\sup\left\\{\sup\left\\{\Phi_{B,P_{1}}^{n}(\bot)(F)\mid
n\in\mathbb{N}\right\\}\mid F\in S\right\\}$
$\displaystyle=\sup\left\\{\sup\left\\{\Phi_{B,P_{1}}^{n}(\bot)\mid
n\in\mathbb{N}\right\\}(F)\mid F\in S\right\\}$
$\displaystyle=\sup\left\\{\llbracket P\rrbracket(F)\mid F\in S\right\\}$

∎

###### Lemma 6 (Linearity of Auxiliary Functions).

For all $\sigma\in\mathbb{N}^{k}\cup\\{\lightning\\}$,
$\alpha\in\mathbb{R}_{\geq 0}^{\infty}$, $F,G\in\textnormal{{eFPS}}$ and
Boolean guards $B$, the following functions are linear:

  1. (1)

The coefficient function $[\sigma]$, i.e. $[\sigma]_{\alpha
F+G}=\alpha\cdot[\sigma]_{F}+[\sigma]_{G}$.

  2. (2)

The restriction $\langle{}\cdot{}\rangle_{B}$, i.e. $\langle{}\alpha
F+G{}\rangle_{B}=\alpha\cdot\langle{}F{}\rangle_{B}+\langle{}G{}\rangle_{B}$.

  3. (3)

The mass $\left|\cdot\right|$, i.e. $\left|\alpha
F+G\right|=\alpha\cdot\left|F\right|+\left|G\right|$.

###### Proof.

  1. (1)

follows from coefficient-wise addition and scalar multiplication on eFPS:

(2) $\displaystyle\alpha F+G$
$\displaystyle=\alpha\cdot\left([\lightning]_{F}\cdot
X_{\lightning}+\sum_{\sigma\in\mathbb{N}^{k}}[\sigma]_{F}\cdot\mathbf{X}^{\sigma}\right)$
$\displaystyle\qquad+\left([\lightning]_{G}\cdot
X_{\lightning}+\sum_{\sigma\in\mathbb{N}^{k}}[\sigma]_{G}\cdot\mathbf{X}^{\sigma}\right)$
($\sharp$)
$\displaystyle=\left(\alpha\cdot[\lightning]_{F}+[\lightning]_{G}\right)\cdot
X_{\lightning}+\sum_{\sigma\in\mathbb{N}^{k}}\left(\alpha\cdot[\sigma]_{F}+[\sigma]_{G}\right)\cdot\mathbf{X}^{\sigma}$
By Definition 2: ($\flat$) $\displaystyle\alpha F+G$
$\displaystyle=[\lightning]_{\alpha F+G}\cdot
X_{\lightning}+\sum_{\sigma\in\mathbb{N}^{k}}[\sigma]_{\alpha
F+G}\cdot\mathbf{X}^{\sigma}$

Comparing coefficients of Eq. $\sharp$ and Eq. $\flat$ yields
$[\sigma]_{\alpha F+G}=\alpha\cdot[\sigma]_{F}+[\sigma]_{G}$ for all
$\sigma\in\mathbb{N}^{k}\cup\\{\lightning\\}$.

  2. (2)

Using the result of 1:

$\displaystyle\langle{}\alpha F+G{}\rangle_{B}$
$\displaystyle=\sum_{\sigma\models B}[\sigma]_{\alpha
F+G}\cdot\mathbf{X}^{\sigma}$ $\displaystyle=\sum_{\sigma\models
B}\left(\alpha\cdot[\sigma]_{F}+[\sigma]_{G}\right)\cdot\mathbf{X}^{\sigma}$
$\displaystyle=\alpha\cdot\sum_{\sigma\models
B}[\sigma]_{F}\cdot\mathbf{X}^{\sigma}+\sum_{\sigma\models
B}[\sigma]_{G}\cdot\mathbf{X}^{\sigma}$
$\displaystyle=\alpha\cdot\langle{}F{}\rangle_{B}+\langle{}G{}\rangle_{B}$

  3. (3)

follows directly from the linearity of variable substitution:

$\displaystyle\left|\alpha F+G\right|=(\alpha F+G)(\mathbf{{1}})=\alpha\cdot
F(\mathbf{{1}})+G(\mathbf{{1}})=\alpha\cdot\left|F\right|+\left|G\right|$

∎

###### Lemma 7 ($\Phi_{B,P}$ Preserves Linearity).

Let $\psi\colon\textnormal{{eFPS}}\rightarrow\textnormal{{eFPS}}$ be a linear
function. If $\llbracket P\rrbracket$ is linear, then $\Phi_{B,P}(\psi)$ is
linear as well.

###### Proof.

$\displaystyle\Phi_{B,P}(\psi)(\alpha F+G)$ $\displaystyle=\;$
$\displaystyle\left(\lambda
F.~{}[\lightning]_{F}X_{\lightning}+\langle{}F{}\rangle_{\neg
B}+\psi(\llbracket P\rrbracket(\langle{}F{}\rangle_{B}))\right)(\alpha F+G)$
$\displaystyle=\;$ $\displaystyle[\lightning]_{\alpha
F+G}X_{\lightning}+\langle{}\alpha F+G{}\rangle_{\neg B}+\psi(\llbracket
P\rrbracket(\langle{}\alpha F+G{}\rangle_{B}))$ (Lin. of
$\langle{}\cdot{}\rangle_{B}$ (Lemma 6)) $\displaystyle=\;$
$\displaystyle(\alpha[\lightning]_{F}+[\lightning]_{G})\cdot
X_{\lightning}+\alpha\langle{}F{}\rangle_{\neg B}+\langle{}G{}\rangle_{\neg
B}+\psi(\llbracket
P\rrbracket(\alpha\langle{}F{}\rangle_{B}+\langle{}G{}\rangle_{B}))$
$\displaystyle=\;$
$\displaystyle(\alpha[\lightning]_{F}+[\lightning]_{G})\cdot
X_{\lightning}+\alpha\langle{}F{}\rangle_{\neg B}+\langle{}G{}\rangle_{\neg
B}$ (Lin. of $\llbracket P\rrbracket$)
$\displaystyle\qquad+\psi(\alpha\llbracket
P\rrbracket(\langle{}F{}\rangle_{B})+\llbracket
P\rrbracket(\langle{}G{}\rangle_{B}))$ $\displaystyle=\;$
$\displaystyle(\alpha[\lightning]_{F}+[\lightning]_{G})\cdot
X_{\lightning}+\alpha\langle{}F{}\rangle_{\neg B}+\langle{}G{}\rangle_{\neg
B}$ (Lin. of $\psi$) $\displaystyle\qquad+\alpha\cdot\psi(\llbracket
P\rrbracket(\langle{}F{}\rangle_{B}))+\psi(\llbracket
P\rrbracket(\langle{}G{}\rangle_{B}))$ $\displaystyle=\;$
$\displaystyle\alpha\cdot\left([\lightning]_{F}X_{\lightning}+\langle{}F{}\rangle_{\neg
B}+\psi(\llbracket P\rrbracket(\langle{}F{}\rangle_{B}))\right)$
$\displaystyle\qquad+\left([\lightning]_{G}X_{\lightning}+\langle{}G{}\rangle_{\neg
B}+\psi(\llbracket P\rrbracket(\langle{}G{}\rangle_{B}))\right)$
$\displaystyle=\;$
$\displaystyle\alpha\cdot\Phi_{B,P}(\psi)(F)+\Phi_{B,P}(\psi)(G)$

∎

###### Corollary 8.

If $\llbracket P\rrbracket$ is linear, then $\Phi_{B,P}^{n}(\bot)$ is linear
for all $n\in\mathbb{N}$, i.e.

$\Phi_{B,P}^{n}(\bot)(\alpha
F+G)=\alpha\cdot\Phi_{B,P}^{n}(\bot)(F)+\Phi_{B,P}^{n}(\bot)(G).$

###### Proof.

By induction:

##### Base case:

$n=0$. $\Phi_{B,P}^{0}(\bot)=\bot$ is linear, as $\bot(\alpha
F+G)=0=\alpha\cdot\bot(F)+\bot(G)$.

##### Induction step:

By the induction hypothesis $\Phi_{B,P}^{n}(\bot)$ is a linear function.
Therefore, $\Phi_{B,P}^{n+1}(\bot)=\Phi_{B,P}(\Phi_{B,P}^{n}(\bot))$ is also
linear by Lemma 7. ∎

###### Theorem 9 (Linearity of $\llbracket\cdot\rrbracket$).

The semantics transformer $\llbracket\cdot\rrbracket$ is linear, i.e. for any
cpGCL program P

$\llbracket P\rrbracket(\alpha F+G)=\alpha\cdot\llbracket
P\rrbracket(F)+\llbracket P\rrbracket(G).$

###### Proof.

By induction over the structure of $P$:

##### Case $P=\textnormal{{skip}}$:

$\displaystyle\llbracket P\rrbracket(\alpha F+G)$ $\displaystyle=\alpha F+G$
$\displaystyle=\alpha\llbracket P\rrbracket(F)+\llbracket P\rrbracket(G)$

##### Case $P=x_{i}\mathrel{\textnormal{$\mathtt{\coloneqq}$}}E$:

$\displaystyle\llbracket P\rrbracket(\alpha F+G)$ $\displaystyle=\llbracket
P\rrbracket\big{(}(\alpha[\lightning]_{F}+[\lightning]_{G})X_{\lightning}$
$\displaystyle\qquad+\sum_{\sigma\in\mathbb{N}^{k}}(\alpha[\sigma]_{F}+[\sigma]_{G})\mathbf{X}^{\sigma}\big{)}$
$\displaystyle=(\alpha[\lightning]_{F}+[\lightning]_{G})X_{\lightning}$
$\displaystyle\qquad+\sum_{\sigma\in\mathbb{N}^{k}}(\alpha[\sigma]_{F}+[\sigma]_{G})X_{1}^{\sigma_{1}}\cdots
X_{i}^{\mathrm{eval}_{\sigma}(E)}\cdots X_{k}^{\sigma_{k}}$
$\displaystyle=\alpha\cdot\left([\lightning]_{F}X_{\lightning}+\sum_{\sigma\in\mathbb{N}^{k}}[\sigma]_{F}X_{1}^{\sigma_{1}}\cdots
X_{i}^{\mathrm{eval}_{\sigma}(E)}\cdots X_{k}^{\sigma_{k}}\right)$
$\displaystyle\qquad+\left([\lightning]_{G}X_{\lightning}+\sum_{\sigma\in\mathbb{N}^{k}}[\sigma]_{G}X_{1}^{\sigma_{1}}\cdots
X_{i}^{\mathrm{eval}_{\sigma}(E)}\cdots X_{k}^{\sigma_{k}}\right)$
$\displaystyle=\alpha\cdot\llbracket P\rrbracket(F)+\llbracket P\rrbracket(G)$

##### Case $P=\textnormal{{observe}}\,\left(\,{B}\,\right)$:

$\displaystyle\llbracket P\rrbracket(\alpha F+G)$ $\displaystyle=\;$
$\displaystyle(\alpha[\lightning]_{F}+[\lightning]_{G}+\left|\langle{}\alpha
F+G{}\rangle_{\neg B}\right|)X_{\lightning}+\langle{}\alpha F+G{}\rangle_{B}$
$\displaystyle=\;$
$\displaystyle(\alpha[\lightning]_{F}+[\lightning]_{G}+\alpha\left|\langle{}F{}\rangle_{\neg
B}\right|+\left|\langle{}G{}\rangle_{\neg B}\right|)X_{\lightning}$ (Lin. of
$\langle{}\cdot{}\rangle_{B}$ (Lemma 6))
$\displaystyle\qquad+\alpha\langle{}F{}\rangle_{B}+\langle{}G{}\rangle$
$\displaystyle=\;$
$\displaystyle\alpha\left(([\lightning]_{F}+\left|\langle{}F{}\rangle_{\neg
B}\right|)X_{\lightning}+\langle{}F{}\rangle_{B}\right)$
$\displaystyle+\left(([\lightning]_{G}+\left|\langle{}G{}\rangle_{\neg
B}\right|)X_{\lightning}+\langle{}G{}\rangle_{B}\right)$ $\displaystyle=\;$
$\displaystyle\alpha\llbracket P\rrbracket(F)+\llbracket P\rrbracket(G)$

##### Case
$P=\left\\{\,{P_{1}}\,\right\\}\mathrel{\left[\,p\,\right]}\left\\{\,{P_{2}}\,\right\\}$:

$\displaystyle\llbracket P\rrbracket(\alpha F+G)$ $\displaystyle=\;$
$\displaystyle p\cdot\llbracket P_{1}\rrbracket(\alpha
F+G)+(1-p)\cdot\llbracket P_{2}\rrbracket(\alpha F+G)$ (I.H.)
$\displaystyle=\;$ $\displaystyle p\cdot(\alpha\llbracket
P_{1}\rrbracket(F)+\llbracket P_{1}\rrbracket(G))+(1-p)\cdot(\alpha\llbracket
P_{2}\rrbracket(F)+\llbracket P_{2}\rrbracket(G))$ $\displaystyle=\;$
$\displaystyle\alpha\left(p\cdot\llbracket
P_{1}\rrbracket(F)+(1-p)\cdot\llbracket P_{2}\rrbracket(F)\right)$
$\displaystyle\qquad+\left(p\cdot\llbracket
P_{1}\rrbracket(G)+(1-p)\cdot\llbracket P_{2}\rrbracket(G)\right)$
$\displaystyle=\;$ $\displaystyle\alpha\llbracket P\rrbracket(F)+\llbracket
P\rrbracket(G)$

##### Case
$P=\textnormal{{if}}\,\left(\,{B}\,\right)\,\left\\{\,{P_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{P_{2}}\,\right\\}$:

$\displaystyle\llbracket P\rrbracket(\alpha F+G)$ $\displaystyle=\;$
$\displaystyle(\alpha[\lightning]_{F}+[\lightning]_{G})X_{\lightning}+\llbracket
P_{1}\rrbracket(\langle{}\alpha F+G{}\rangle_{B})+\llbracket
P_{2}\rrbracket(\langle{}\alpha F+G{}\rangle_{\neg B})$ $\displaystyle=\;$
$\displaystyle(\alpha[\lightning]_{F}+[\lightning]_{G})X_{\lightning}+\llbracket
P_{1}\rrbracket(\alpha\langle{}F{}\rangle_{B}+\langle{}G{}\rangle_{B})$ (Lin.
of $\langle{}\cdot{}\rangle_{B}$ (Lemma 6)) $\displaystyle\qquad+\llbracket
P_{2}\rrbracket(\alpha\langle{}F{}\rangle_{\neg B}+\langle{}G{}\rangle_{\neg
B})$ $\displaystyle=\;$
$\displaystyle(\alpha[\lightning]_{F}+[\lightning]_{G})X_{\lightning}+\alpha\llbracket
P_{1}\rrbracket(\langle{}F{}\rangle_{B})+\llbracket
P_{1}\rrbracket(\langle{}G{}\rangle_{B})$ (I.H.)
$\displaystyle\qquad+\alpha\llbracket
P_{2}\rrbracket(\langle{}F{}\rangle_{\neg B})+\llbracket
P_{2}\rrbracket(\langle{}G{}\rangle_{\neg B})$ $\displaystyle=\;$
$\displaystyle\alpha\left([\lightning]_{F}X_{\lightning}+\llbracket
P_{1}\rrbracket(\langle{}F{}\rangle_{B})+\llbracket
P_{2}\rrbracket(\langle{}F{}\rangle_{\neg B}\right)$
$\displaystyle\qquad+\left([\lightning]_{G}X_{\lightning}+\llbracket
P_{1}\rrbracket(\langle{}G{}\rangle_{B})+\llbracket
P_{2}\rrbracket(\langle{}G{}\rangle_{\neg B}\right)$ $\displaystyle=\;$
$\displaystyle\alpha\llbracket P\rrbracket(F)+\llbracket P\rrbracket(G)$

##### Case $P=P_{1}\fatsemi P_{2}$:

$\displaystyle\llbracket P\rrbracket(\alpha F+G)$ $\displaystyle=\;$
$\displaystyle\llbracket P_{2}\rrbracket(\llbracket P_{1}\rrbracket(\alpha
F+G))$ (I.H.) $\displaystyle=\;$ $\displaystyle\llbracket
P_{2}\rrbracket(\alpha\llbracket P_{1}\rrbracket(F)+\llbracket
P_{1}\rrbracket(G))$ (I.H.) $\displaystyle=\;$ $\displaystyle\alpha\llbracket
P_{2}\rrbracket(\llbracket P_{1}\rrbracket(F))+\llbracket
P_{2}\rrbracket(\llbracket P_{1}\rrbracket(G))$ $\displaystyle=\;$
$\displaystyle\alpha\llbracket P\rrbracket(F)+\llbracket P\rrbracket(G)$

##### Case
$P=\textnormal{{while}}\left(\,{B}\,\right)\left\\{\,{P_{1}}\,\right\\}$:

$\displaystyle\llbracket P\rrbracket(\alpha F+G)$ $\displaystyle=\;$
$\displaystyle(\textup{lfp}\;\Phi_{B,P_{1}})(\alpha F+G)$ $\displaystyle=\;$
$\displaystyle\left(\sup\left\\{\Phi_{B,P_{1}}^{n}(\bot)\mid
n\in\mathbb{N}\right\\}\right)(\alpha F+G)$ $\displaystyle=\;$
$\displaystyle\sup\left\\{\Phi_{B,P_{1}}^{n}(\bot)(\alpha F+G)\mid
n\in\mathbb{N}\right\\}$ (Corollary 8, $\llbracket P_{1}\rrbracket$ lin. by
I.H.) $\displaystyle=\;$
$\displaystyle\sup\left\\{\alpha\cdot\Phi_{B,P_{1}}^{n}(\bot)(F)+\Phi_{B,P_{1}}^{n}(\bot)(G)\mid
n\in\mathbb{N}\right\\}$ $\displaystyle=\;$
$\displaystyle\alpha\cdot\sup\left\\{\Phi_{B,P_{1}}^{n}(\bot)(F)\mid
n\in\mathbb{N}\right\\}+\sup\left\\{\Phi_{B,P_{1}}^{n}(\bot)(G)\mid
n\in\mathbb{N}\right\\}$ $\displaystyle=\;$
$\displaystyle\alpha\cdot\left(\sup\left\\{\Phi_{B,P_{1}}^{n}(\bot)\mid
n\in\mathbb{N}\right\\}\right)(F)+\left(\sup\left\\{\Phi_{B,P_{1}}^{n}(\bot)\mid
n\in\mathbb{N}\right\\}\right)(G)$ $\displaystyle=\;$
$\displaystyle\alpha\cdot(\textup{lfp}\;\Phi_{B,P_{1}})(F)+(\textup{lfp}\;\Phi_{B,P_{1}})(G)$
$\displaystyle=\;$ $\displaystyle\alpha\llbracket P\rrbracket(F)+\llbracket
P\rrbracket(G)$

∎

###### Lemma 10 (Error Term Pass-Through).

For every program $P$ and every $F\in\textnormal{{eFPS}}$, the error term
$[\lightning]_{F}X_{\lightning}$ passes through the transformer unaffected,
i.e.

$\llbracket P\rrbracket(F)=\llbracket
P\rrbracket\left(\sum_{\sigma\in\mathbb{N}^{k}}[\sigma]_{F}\mathbf{X}^{\sigma}\right)+[\lightning]_{F}X_{\lightning}.$

###### Proof.

By linearity of $\llbracket P\rrbracket$, we get:

$\displaystyle\llbracket P\rrbracket(F)$ $\displaystyle=\llbracket
P\rrbracket\left(\sum_{\sigma\in\mathbb{N}^{k}}[\sigma]_{F}\mathbf{X}^{\sigma}+[\lightning]_{F}X_{\lightning}\right)$
$\displaystyle=\llbracket
P\rrbracket\left(\sum_{\sigma\in\mathbb{N}^{k}}[\sigma]_{F}\mathbf{X}^{\sigma}\right)+[\lightning]_{F}\cdot\llbracket
P\rrbracket(X_{\lightning})$

It therefore remains to be shown that $\llbracket
P\rrbracket(X_{\lightning})=X_{\lightning}$ by induction over the structure of
$P$:

##### Case $P=\textnormal{{skip}}$:

$\displaystyle\llbracket P\rrbracket(X_{\lightning})$
$\displaystyle=X_{\lightning}$

##### Case $P=x_{i}\mathrel{\textnormal{$\mathtt{\coloneqq}$}}E$:

$\displaystyle\llbracket P\rrbracket(X_{\lightning})$
$\displaystyle=X_{\lightning}+\sum_{\sigma\in\mathbb{N}^{k}}0\cdot
X_{1}^{\sigma_{1}}\cdots X_{i}^{\mathrm{eval}_{\sigma}(E)}\cdots
X_{k}^{\sigma_{k}}$ $\displaystyle=X_{\lightning}$

##### Case $P=\textnormal{{observe}}\,\left(\,{B}\,\right)$:

$\displaystyle\llbracket P\rrbracket(X_{\lightning})$
$\displaystyle=\left(1+\left|\langle{}X_{\lightning}{}\rangle_{\neg
B}\right|\right)X_{\lightning}+\langle{}X_{\lightning}{}\rangle_{B}$
$\displaystyle=X_{\lightning}$

##### Case
$P=\left\\{\,{P_{1}}\,\right\\}\mathrel{\left[\,p\,\right]}\left\\{\,{P_{2}}\,\right\\}$:

$\displaystyle\llbracket P\rrbracket(X_{\lightning})$
$\displaystyle=p\cdot\llbracket
P_{1}\rrbracket(X_{\lightning})+(1-p)\cdot\llbracket
P_{2}\rrbracket(X_{\lightning})$ (I.H. on $P_{1}$ and $P_{2}$)
$\displaystyle=p\cdot X_{\lightning}+(1-p)\cdot X_{\lightning}$
$\displaystyle=X_{\lightning}$

##### Case
$P=\textnormal{{if}}\,\left(\,{B}\,\right)\,\left\\{\,{P_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{P_{2}}\,\right\\}$:

$\displaystyle\llbracket P\rrbracket(F)$
$\displaystyle=X_{\lightning}+\llbracket
P_{1}\rrbracket(\langle{}X_{\lightning}{}\rangle_{B})+\llbracket
P_{2}\rrbracket(\langle{}X_{\lightning}{}\rangle_{\neg B})$
$\displaystyle=X_{\lightning}+\llbracket P_{1}\rrbracket(0)+\llbracket
P_{2}\rrbracket(0)$ $\displaystyle=X_{\lightning}$

##### Case $P=P_{1}\fatsemi P_{2}$:

$\displaystyle\llbracket P\rrbracket(X_{\lightning})$
$\displaystyle=\llbracket P_{2}\rrbracket(\llbracket
P_{1}\rrbracket(X_{\lightning}))$ (I.H. on $P_{1}$) $\displaystyle=\llbracket
P_{2}\rrbracket(X_{\lightning})$ (I.H. on $P_{2}$)
$\displaystyle=X_{\lightning}$

##### Case
$P=\textnormal{{while}}\left(\,{B}\,\right)\left\\{\,{P_{1}}\,\right\\}$:

We show that $\forall
n\in\mathbb{N}:\Phi_{B,P_{1}}^{n+1}(\bot)(X_{\lightning})=X_{\lightning}$:

$\displaystyle\Phi_{B,P_{1}}^{n+1}(\bot)(X_{\lightning})$
$\displaystyle=\Phi_{B,P_{1}}(\Phi_{B,P_{1}}^{n}(\bot))(X_{\lightning})$ (def.
$\Phi_{B,P_{1}}$)
$\displaystyle=X_{\lightning}+\langle{}X_{\lightning}{}\rangle_{\neg
B}+\Phi_{B,P_{1}}^{n}(\bot)(\llbracket
P_{1}\rrbracket(\langle{}X_{\lightning}{}\rangle_{B}))$
$\displaystyle=X_{\lightning}+\Phi_{B,P_{1}}^{n}(\bot)(0)$
($\Phi_{B,P_{1}}^{n}(\bot)(0)\leq\llbracket\textnormal{{while}}\left(\,{B}\,\right)\left\\{\,{P_{1}}\,\right\\}\rrbracket(0)=0$)
$\displaystyle=X_{\lightning}$

From this, it follows:

$\displaystyle\llbracket P\rrbracket(X_{\lightning})$
$\displaystyle=\sup\,\left\\{\Phi_{B,P_{1}}^{n}(\bot)(X_{\lightning})\mid
n\in\mathbb{N}\right\\}$ ($\forall
n\in\mathbb{N}:\Phi_{B,P_{1}}^{n+1}(\bot)(X_{\lightning})=X_{\lightning}$)
$\displaystyle=\sup\,\left\\{0,X_{\lightning}\right\\}$
$\displaystyle=X_{\lightning}$

∎

###### Lemma 11 (Alternative Representation).

$\displaystyle\llbracket\textnormal{{while}}\left(\,{B}\,\right)\left\\{\,{P}\,\right\\}\rrbracket(G)$
$\displaystyle=\sum_{i=0}^{\infty}\left([\lightning]_{\varphi_{B,P}^{i}(G)}X_{\lightning}+\langle{}\varphi_{B,P}^{i}(G){}\rangle_{\neg
B}\right)$
$\displaystyle\quad\text{where}\quad\varphi_{B,P}(G)\coloneqq\llbracket
P\rrbracket(\langle{}G{}\rangle_{B}).$

###### Proof.

First, we show by induction that for all $n\in\mathbb{N}$:

$\Phi_{B,P}^{n}(\bot)(G)=\sum_{i=0}^{n-1}\left([\lightning]_{\varphi_{B,P}^{i}(F)}X_{\lightning}+\langle{}\varphi_{B,P}^{i}(F){}\rangle_{\neg
B}\right).$

##### Base case:

$n=0$.

$\Phi_{B,P}^{0}(\bot)(G)=0=\sum_{i=0}^{-1}\left([\lightning]_{\varphi_{B,P}^{i}(G)}X_{\lightning}+\langle{}\varphi_{B,P}^{i}(G){}\rangle_{\neg
B}\right)$

##### Induction step:

$\displaystyle\Phi_{B,P}^{n+1}(\bot)(G)$
$\displaystyle=\Phi_{B,P}(\Phi_{B,P}^{n}(\bot))(G)$ (Def. $\Phi_{B,P}$)
$\displaystyle=[\lightning]_{G}X_{\lightning}+\langle{}G{}\rangle_{\neg
B}+\Phi_{B,P}^{n}(\bot)(\llbracket P\rrbracket(\langle{}G{}\rangle_{B}))$
(Def. $\varphi_{B,P}$)
$\displaystyle=[\lightning]_{G}X_{\lightning}+\langle{}G{}\rangle_{\neg
B}+\Phi_{B,P}^{n}(\bot)(\varphi_{B,P}(G))$
$\displaystyle=[\lightning]_{G}X_{\lightning}+\langle{}G{}\rangle_{\neg B}$
(I.H.)
$\displaystyle\quad+\sum_{i=0}^{n-1}\left([\lightning]_{\varphi_{B,P}^{i}(\varphi_{B,P}(G))}X_{\lightning}+\langle{}\varphi_{B,P}^{i}(\varphi_{B,P}(G)){}\rangle_{\neg
B}\right)$
$\displaystyle=[\lightning]_{\varphi_{B,P}^{0}(G)}X_{\lightning}+\langle{}\varphi_{B,P}^{0}(G){}\rangle_{\neg
B}$ ($\varphi_{B,P}^{0}(G)=G$, index shift)
$\displaystyle\quad+\sum_{i=1}^{n}[\lightning]_{\varphi_{B,P}^{i}(G)}X_{\lightning}+\langle{}\varphi_{B,P}^{i}(G){}\rangle_{\neg
B}$
$\displaystyle=\sum_{i=0}^{n}[\lightning]_{\varphi_{B,P}^{i}(G)}X_{\lightning}+\langle{}\varphi_{B,P}^{i}(G){}\rangle_{\neg
B}$

From this, it follows:

$\displaystyle\llbracket\textnormal{{while}}\left(\,{B}\,\right)\left\\{\,{P}\,\right\\}\rrbracket(G)$
$\displaystyle=\left(\sup_{n\in\mathbb{N}}\Phi_{B,P}^{n}(\bot)\right)(G)$
$\displaystyle=\sup\left\\{\Phi_{B,P}^{n}(\bot)(G)\mid
n\in\mathbb{N}\right\\}$
$\displaystyle=\sup_{n\in\mathbb{N}}\left\\{\sum_{i=0}^{n-1}[\lightning]_{\varphi_{B,P}^{i}(G)}X_{\lightning}+\langle{}\varphi_{B,P}^{i}(G){}\rangle_{\neg
B}\right\\}$
$\displaystyle=\sum_{i=0}^{\infty}[\lightning]_{\varphi_{B,P}^{i}(G)}X_{\lightning}+\langle{}\varphi_{B,P}^{i}(G){}\rangle_{\neg
B}$

∎

###### Lemma 12 (Infinite Applications of Linearity).

Let the linear and continuous function
$\psi\colon\textnormal{{eFPS}}\rightarrow\textnormal{{eFPS}}$. Further, let
$\alpha_{i}\in\mathbb{R}_{\geq 0}^{\infty}$ and $F_{i}\in\textnormal{{eFPS}}$
for all $i\in\mathbb{N}$. Then,

$\psi\left(\sum_{i\in\mathbb{N}}\alpha_{i}\cdot
F_{i}\right)=\sum_{i\in\mathbb{N}}\alpha_{i}\cdot\psi(F_{i}).$

###### Proof.

$\displaystyle\psi\left(\sum_{i\in\mathbb{N}}\alpha_{i}\cdot F_{i}\right)$
$\displaystyle=\psi\left(\sup\left\\{\sum_{i=0}^{n}\alpha_{i}\cdot F_{i}\mid
n\in\mathbb{N}\right\\}\right)$ (Cont. of $\psi$)
$\displaystyle=\sup\left\\{\psi\left(\sum_{i=0}^{n}\alpha_{i}\cdot
F_{i}\right)\mid n\in\mathbb{N}\right\\}$ (finitely many applications of
linearity)
$\displaystyle=\sup\left\\{\sum_{i=0}^{n}\alpha_{i}\cdot\psi(F_{i})\mid
n\in\mathbb{N}\right\\}$
$\displaystyle=\sum_{i\in\mathbb{N}}\alpha_{i}\cdot\psi(F_{i})$

∎

###  B.1. Coincidence to Operational Semantics

We refer to the operational semantics for cpGCL programs described in (Olmedo
et al., 2018). We show that the Markov chain $\mathcal{R}_{\sigma}\llbracket
P\rrbracket$ precisely reflects the unconditioned PGF semantics $\llbracket
P\rrbracket(\mathbf{{X}}^{\sigma})$ for any $p\in\textnormal{{cpGCL}}$ with
initial state $\sigma\in\mathbb{N}^{k}$. Lemma 14 shows that the probabilities
$\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle)$ for all
$\sigma^{\prime}$ and $\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\lightning)$ arising from the Markov chain correspond
to the coefficients of $\llbracket P\rrbracket(\mathbf{{X}}^{\sigma})$. It is
further shown that modifying these probabilities to the conditional
probabilities $\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle\mid\neg\diamondsuit\lightning)$
has the same effect as applying the normalization function norm, thus
concluding that the two semantics coincide (cf. Theorem 15).

###### Definition 13 (Markov Chain Semantics of cpGCL).

For any cpGCL program $P$ and any starting state $\sigma\in\mathbb{N}^{k}$,
the _operational Markov chain_ is

$\mathcal{R}_{\sigma}\llbracket P\rrbracket\ {}{}\triangleq{}{}\
\\!\left(\mathcal{S},\langle{}P,\sigma{}\rangle,\mathcal{P}\right),$

where:

  * •

$\langle{}P,\sigma{}\rangle$ is the starting state

  * •

the set of states $\mathcal{S}$ is the smallest set such that:

    * –

$\mathcal{S}$ contains the starting state $\langle{}P,\sigma{}\rangle$

    * –

if $s\in\mathcal{S}$ and $s$ has an outgoing transition to $s^{\prime}$
according to Fig. 4, then $s^{\prime}\in\mathcal{S}$

  * •

$\mathcal{P}\colon\mathcal{S}\times\mathcal{S}\rightarrow[0,1]$ is the
transition matrix with

    * –

$\mathcal{P}(s,s^{\prime})=p$ if $s\overset{p}{\rightarrow}s^{\prime}$ can be
derived according to Fig. 4

    * –

$\mathcal{P}(s,s^{\prime})=0$ otherwise

$\sigma\models B$ (skip)
$\langle{}\textnormal{{skip}},\sigma{}\rangle\longrightarrow\langle{}\downarrow,\sigma{}\rangle$
$\sigma\models B$ (asgn)
$\langle{}x\mathrel{\textnormal{$\mathtt{\coloneqq}$}}E,\sigma{}\rangle\longrightarrow\langle{}\downarrow,\sigma[x\leftarrow\mathrm{eval}_{\sigma}(E)]{}\rangle$
$\sigma\models B$ (obs-t)
$\langle{}\textnormal{{observe}}\,\left(\,{B}\,\right),\sigma{}\rangle\longrightarrow\langle{}\downarrow,\sigma{}\rangle$
$\sigma\not\models B$ (obs-f)
$\langle{}\textnormal{{observe}}\,\left(\,{B}\,\right),\sigma{}\rangle\longrightarrow\langle{}\lightning{}\rangle$
$\sigma\models B$ (seq-1)  $\langle{}\downarrow\fatsemi
Q,\sigma{}\rangle\longrightarrow\langle{}Q,\sigma{}\rangle$
$\langle{}P,\sigma{}\rangle\longrightarrow\langle{}\lightning{}\rangle$
(seq-2)  $\langle{}P\fatsemi
Q,\sigma{}\rangle\longrightarrow\langle{}\lightning{}\rangle$
$\langle{}P,\sigma{}\rangle\overset{p}{\longrightarrow}\langle{}P^{\prime},\sigma^{\prime}{}\rangle$
(seq-3)  $\langle{}P\fatsemi
Q,\sigma{}\rangle\overset{p}{\longrightarrow}\langle{}P^{\prime}\fatsemi
Q,\sigma^{\prime}{}\rangle$
$\sigma\models B$ (choice-l)
$\langle{}\left\\{\,{P}\,\right\\}\mathrel{\left[\,p\,\right]}\left\\{\,{Q}\,\right\\},\sigma{}\rangle\overset{p}{\longrightarrow}\langle{}P,\sigma{}\rangle$
$\sigma\models B$ (choice-r)
$\langle{}\left\\{\,{P}\,\right\\}\mathrel{\left[\,p\,\right]}\left\\{\,{Q}\,\right\\},\sigma{}\rangle\overset{1-p}{\longrightarrow}\langle{}Q,\sigma{}\rangle$
$\sigma\models B$ (if-t)
$\langle{}\textnormal{{if}}\,\left(\,{B}\,\right)\,\left\\{\,{P}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{Q}\,\right\\},\sigma{}\rangle\longrightarrow\langle{}P,\sigma{}\rangle$
$\sigma\not\models B$ (if-f)
$\langle{}\textnormal{{if}}\,\left(\,{B}\,\right)\,\left\\{\,{P}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{Q}\,\right\\},\sigma{}\rangle\longrightarrow\langle{}Q,\sigma{}\rangle$
$\sigma\models B$ (while-t)
$\langle{}\textnormal{{while}}\left(\,{B}\,\right)\left\\{\,{P}\,\right\\},\sigma{}\rangle\longrightarrow\langle{}P\fatsemi\textnormal{{while}}\left(\,{B}\,\right)\left\\{\,{P}\,\right\\},\sigma{}\rangle$
$\sigma\not\models B$ (while-f)
$\langle{}\textnormal{{while}}\left(\,{B}\,\right)\left\\{\,{P}\,\right\\},\sigma{}\rangle\longrightarrow\langle{}\downarrow,\sigma{}\rangle$
$\sigma\models B$ (terminal)
$\langle{}\downarrow,\sigma{}\rangle\longrightarrow\langle{}\mathnormal{sink}{}\rangle$
$\sigma\models B$ (undesired)
$\langle{}\lightning{}\rangle\longrightarrow\langle{}\mathnormal{sink}{}\rangle$
$\sigma\models B$ (sink)
$\langle{}\mathnormal{sink}{}\rangle\longrightarrow\langle{}\mathnormal{sink}{}\rangle$

Figure 4. Construction rules for the operational Markov chain.
$\sigma[x\leftarrow\mathrm{eval}_{\sigma}(E)]$ denotes the program state
$\sigma$ with the value of $x$ replaced by $\mathrm{eval}_{\sigma}(E)$.
Whenever a transition has no annotated weight above its arrow, it has a weight
of $1$.

###### Lemma 14.

For every $P\in\textnormal{{cpGCL}}$ and every two
$\sigma,\sigma^{\prime}\in\mathbb{N}^{k}$

  1. (1)

$\textup{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle)~{}=~{}[\sigma^{\prime}]_{\llbracket
P\rrbracket(\mathbf{{X}}^{\sigma})}$

  2. (2)

$\textup{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\lightning)~{}=~{}[\lightning]_{\llbracket
P\rrbracket(\mathbf{{X}}^{\sigma})}$

###### Proof.

We prove the statements (1) and (2) simultaneously by structural induction
over a cpGCL program $P$.

Case $P=\textnormal{{skip}}$: In this case, the Markov chain
$\mathcal{R}_{\sigma}\llbracket P\rrbracket$ looks as follows:

Prodigy
$\langle\textnormal{{skip}},\sigma\rangle$$\langle\downarrow,\sigma\rangle$$\langle\mathit{sink}\rangle$

Its PGF semantics yields:

$\displaystyle\llbracket
P\rrbracket(\mathbf{{X}}^{\sigma})~{}=~{}\mathbf{{X}}^{\sigma}$

Thus:

$\displaystyle\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle)$
$\displaystyle=\begin{cases}1,&\text{if}~{}\sigma^{\prime}=\sigma\\\
0,&\text{else}\end{cases}~{}=~{}[\sigma^{\prime}]_{\llbracket
P\rrbracket(\mathbf{{X}}^{\sigma})}$
$\displaystyle\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\lightning)$
$\displaystyle=0~{}=~{}[\lightning]_{\llbracket
P\rrbracket(\mathbf{{X}}^{\sigma})}$

Case $P=x_{i}\coloneq E$:

Prodigy $\langle
x_{i}\mathrel{\textnormal{$\mathtt{\coloneqq}$}}E,\sigma\rangle$$\langle\downarrow,\sigma[x_{i}\leftarrow\text{eval}_{\sigma}(E)]\rangle$$\langle\mathit{sink}\rangle$

Its PGF semantics yields:

$\displaystyle\llbracket P\rrbracket(\mathbf{{X}}^{\sigma})$
$\displaystyle=X_{1}^{\sigma_{1}}\cdots X_{i}^{\text{eval}_{\sigma}(E)}\cdots
X_{k}^{\sigma_{k}}$

Thus:

$\displaystyle\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle)$
$\displaystyle=\begin{cases}1,&\text{if}~{}\sigma^{\prime}=\sigma[x_{i}\leftarrow\text{eval}_{\sigma}(E)]\\\
0,&\text{else}\end{cases}$ $\displaystyle=~{}[\sigma^{\prime}]_{\llbracket
P\rrbracket(\mathbf{{X}}^{\sigma})}$
$\displaystyle\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\lightning)$
$\displaystyle=0~{}=~{}[\lightning]_{\llbracket
P\rrbracket(\mathbf{{X}}^{\sigma})}$

Case $P=\textnormal{{observe}}\,\left(\,{B}\,\right)$: We do a case
distinction whether $\sigma\models B$.

_Observe passed_ :

Prodigy
$\langle\textnormal{{observe}}\,\left(\,{B}\,\right),\sigma\rangle$$\langle\downarrow,\sigma\rangle$$\langle\mathit{sink}\rangle$

The PGF semantics yields:

$\displaystyle\llbracket P\rrbracket(\mathbf{{X}}^{\sigma})$
$\displaystyle=\langle\mathbf{{X}}^{\sigma}\rangle_{B}+\left(\left|\langle\mathbf{{X}}^{\sigma}\rangle_{\neg
B}\right|+[\lightning]_{\mathbf{{X}}^{\sigma}}\right)X_{\lightning}=\mathbf{{X}}^{\sigma}$

Thus:

$\displaystyle\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle)$
$\displaystyle=\begin{cases}1,&\text{if}~{}\sigma^{\prime}=\sigma\\\
0,&\text{else}\end{cases}=~{}[\sigma^{\prime}]_{\llbracket
P\rrbracket(\mathbf{{X}}^{\sigma})}$
$\displaystyle\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\lightning)$
$\displaystyle=0~{}=~{}[\lightning]_{\llbracket
P\rrbracket(\mathbf{{X}}^{\sigma})}$

_Observe failed_ :

Prodigy
$\langle\textnormal{{observe}}\,\left(\,{B}\,\right),\sigma\rangle$$\langle\lightning\rangle$$\langle\mathit{sink}\rangle$

The PGF semantics yields:

$\displaystyle\llbracket P\rrbracket(\mathbf{{X}}^{\sigma})$
$\displaystyle=\langle\mathbf{{X}}^{\sigma}\rangle_{B}+\left(\left|\langle\mathbf{{X}}^{\sigma}\rangle_{\neg
B}\right|+[\lightning]_{\mathbf{{X}}^{\sigma}}\right)X_{\lightning}=X_{\lightning}$

Thus:

$\displaystyle\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle)$
$\displaystyle=0~{}=~{}[\sigma^{\prime}]_{\llbracket
P\rrbracket(\mathbf{{X}}^{\sigma})}$
$\displaystyle\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\lightning)$
$\displaystyle=1~{}=~{}[\lightning]_{\llbracket
P\rrbracket(\mathbf{{X}}^{\sigma})}$

Case
$P=\left\\{\,{P_{1}}\,\right\\}\mathrel{\left[\,p\,\right]}\left\\{\,{P_{2}}\,\right\\}$:

Prodigy
$\langle\left\\{\,{P_{1}}\,\right\\}\mathrel{\left[\,p\,\right]}\left\\{\,{P_{2}}\,\right\\},\sigma\rangle$$\langle
P_{1},\sigma\rangle$$\langle P_{2},\sigma\rangle$$\ldots$$\ldots$$p$$1-p$

The PGF semantics yields:

$\displaystyle\llbracket P\rrbracket(\mathbf{{X}}^{\sigma})$
$\displaystyle=p\cdot\llbracket
P_{1}\rrbracket(\mathbf{{X}}^{\sigma})+(1-p)\cdot\llbracket
P_{2}\rrbracket(\mathbf{{X}}^{\sigma})$

Thus:

$\displaystyle\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle)$
$\displaystyle=p\cdot\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P_{1}\rrbracket}(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle)$
$\displaystyle\qquad+(1-p)\cdot\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P_{2}\rrbracket}(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle)$ (by
I.H.) $\displaystyle=p\cdot[\sigma^{\prime}]_{\llbracket
P_{1}\rrbracket(\mathbf{{X}}^{\sigma})}+(1-p)\cdot[\sigma^{\prime}]_{\llbracket
P_{2}\rrbracket(\mathbf{{X}}^{\sigma})}$
$\displaystyle=[\sigma^{\prime}]_{\llbracket
P\rrbracket(\mathbf{{X}}^{\sigma})}$
$\displaystyle\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\lightning)$
$\displaystyle=p\cdot\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P_{1}\rrbracket}(\diamondsuit\lightning)+(1-p)\cdot\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P_{2}\rrbracket}(\diamondsuit\lightning)$ (by I.H.)
$\displaystyle=p\cdot[\lightning]_{\llbracket
P_{1}\rrbracket(\mathbf{{X}}^{\sigma})}+(1-p)\cdot[\lightning]_{\llbracket
P_{2}\rrbracket(\mathbf{{X}}^{\sigma})}$
$\displaystyle=[\lightning]_{\llbracket P\rrbracket(\mathbf{{X}}^{\sigma})}$

Case
$P=\textnormal{{if}}\,\left(\,{B}\,\right)\,\left\\{\,{P_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{P_{2}}\,\right\\}$:
We do a case distinction on $\sigma\models B$.

_Condition is satisfied_ :

Prodigy
$\langle\textnormal{{if}}\,\left(\,{B}\,\right)\,\left\\{\,{P_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{P_{2}}\,\right\\},\sigma\rangle$$\langle
P_{1},\sigma\rangle$$\ldots$

The PGF semantics yields:

$\displaystyle\llbracket P\rrbracket(\mathbf{{X}}^{\sigma})$
$\displaystyle=\llbracket
P_{1}\rrbracket(\langle\mathbf{{X}}^{\sigma}\rangle_{B})+\llbracket
P_{2}\rrbracket(\langle\mathbf{{X}}^{\sigma}\rangle_{\neg
B})+[\lightning]_{\mathbf{{X}}^{\sigma}}X_{\lightning}~{}=~{}\llbracket
P_{1}\rrbracket(\mathbf{{X}}^{\sigma})$

Thus:

$\displaystyle\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle)$
$\displaystyle=\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P_{1}\rrbracket}(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle)$ (by
I.H.) $\displaystyle=[\sigma^{\prime}]_{\llbracket
P_{1}\rrbracket(\mathbf{{X}}^{\sigma})}$
$\displaystyle\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\lightning)$ $\displaystyle=[\lightning]_{\llbracket
P_{1}\rrbracket(\mathbf{{X}}^{\sigma})}$
$\displaystyle=[\lightning]_{\llbracket P\rrbracket(\mathbf{{X}}^{\sigma})}$

_Condition not satisfied_ :

Prodigy
$\langle\textnormal{{if}}\,\left(\,{B}\,\right)\,\left\\{\,{P_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{P_{2}}\,\right\\},\sigma\rangle$$\langle
P_{2},\sigma\rangle$$\ldots$

The PGF semantics yields:

$\displaystyle\llbracket P\rrbracket(\mathbf{{X}}^{\sigma})$
$\displaystyle=\llbracket
P_{1}\rrbracket(\langle\mathbf{{X}}^{\sigma}\rangle_{B})+\llbracket
P_{2}\rrbracket(\langle\mathbf{{X}}^{\sigma}\rangle_{\neg
B})+[\lightning]_{\mathbf{{X}}^{\sigma}}X_{\lightning}~{}=~{}\llbracket
P_{2}\rrbracket(\mathbf{{X}}^{\sigma})$

Thus:

$\displaystyle\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle)$
$\displaystyle=\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P_{2}\rrbracket}(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle)$ (by
I.H.) $\displaystyle=[\sigma^{\prime}]_{\llbracket
P_{2}\rrbracket(\mathbf{{X}}^{\sigma})}$
$\displaystyle\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\lightning)$ $\displaystyle=[\lightning]_{\llbracket
P_{2}\rrbracket(\mathbf{{X}}^{\sigma})}$
$\displaystyle=[\lightning]_{\llbracket P\rrbracket(\mathbf{{X}}^{\sigma})}$

Case $P={P_{1}}{\,\fatsemi}~{}{P_{2}}$:

Prodigy
$\langle{P_{1}}{\,\fatsemi}~{}{P_{2}},\sigma\rangle$$\langle\lightning\rangle$$\langle{\downarrow}{\,\fatsemi}~{}{P_{2}},\sigma^{\prime\prime}\rangle$$\ldots$$\langle
P_{2},\sigma^{\prime\prime}\rangle$$\ldots$

Case $P=\textnormal{{while}}\left(\,{B}\,\right)\left\\{\,{P_{1}}\,\right\\}$:

_Condition not fulfilled_ $(\sigma\not\models B)$:

Prodigy
$\langle\textnormal{{while}}\left(\,{B}\,\right)\left\\{\,{P_{1}}\,\right\\},\sigma\rangle$$\langle\downarrow,\sigma\rangle$$\langle\mathit{sink}\rangle$

For the PGF semantics, consider the following, for all $n\in\mathbb{N}$:

$\displaystyle\Phi_{B,P_{1}}^{n}(\bot)(\mathbf{{X}}^{\sigma})$
$\displaystyle=[\lightning]_{\mathbf{{X}}^{\sigma}}+\langle\mathbf{{X}}^{\sigma}\rangle_{\neg
B}+\Phi_{B,P_{1}}^{n}(\bot)(\llbracket
P_{1}\rrbracket(\langle\mathbf{{X}}^{\sigma}\rangle_{B}))$ ($\sigma\not\models
B$)
$\displaystyle=[\lightning]_{\mathbf{{X}}^{\sigma}}+\Phi_{B,P_{1}}^{n}(\bot)(\llbracket
P_{1}\rrbracket(\langle\mathbf{{X}}^{\sigma}\rangle_{B}))$
$\displaystyle=0+\mathbf{{X}}^{\sigma}+0$ $\displaystyle\llbracket
P\rrbracket(\mathbf{{X}}^{\sigma})$
$\displaystyle=\textup{lfp}\;\Phi_{B,P_{1}}(\mathbf{{X}}^{\sigma})$
$\displaystyle=\sup_{n\in\mathbb{N}}\left\\{\Phi_{B,P_{1}}^{n}(\bot)(\mathbf{{X}}^{\sigma})\mid
n\in\mathbb{N}\right\\}$ $\displaystyle=\mathbf{{X}}^{\sigma}$

Thus:

$\displaystyle\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle)$
$\displaystyle=\begin{cases}1,&\text{if}~{}\sigma^{\prime}=\sigma\\\
0,&\text{otherwise}\end{cases}\quad=\quad[\sigma^{\prime}]_{\llbracket
P\rrbracket(\mathbf{{X}}^{\sigma})}$
$\displaystyle\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\lightning)$
$\displaystyle=0\quad=[\lightning]_{\llbracket
P\rrbracket(\mathbf{{X}}^{\sigma})}$

_Condition is satisfied_ $(\sigma\models B)$:

At least one loop iteration is performed. In order for the program to
terminate in some state $\sigma^{\prime}$, some (non-zero) number of loop
iterations must be performed. The termination probability can therefore be
partitioned into the following infinite sum of probabilities:

$\displaystyle\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle)$
$\displaystyle=\sum_{n=1}^{\infty}\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit_{=n}\langle{}\downarrow,\sigma^{\prime}{}\rangle)$
$\displaystyle\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\lightning)$
$\displaystyle=\sum_{n=1}^{\infty}\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit_{=n}\langle{}\lightning{}\rangle)~{},$

where $\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit_{=n}\langle{}\downarrow,\sigma^{\prime}{}\rangle)$
denotes the probability to reach state
$\langle{}\downarrow,\sigma^{\prime}{}\rangle$ after _exactly_ $n$ loop
iterations and $\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit_{=n}\langle{}\lightning{}\rangle)$ denotes the
probability to reach state $\langle{}\lightning{}\rangle$ in exactly $n$ loop
iterations.

By Lemma 11, the PGF semantics can be represented as follows:

$\displaystyle\llbracket P\rrbracket(\mathbf{X}^{\sigma})$
$\displaystyle=\sum_{n=0}^{\infty}\left([\lightning]_{\varphi_{B,P_{1}}^{n}(\mathbf{X}^{\sigma})}X_{\lightning}+\langle{}\varphi_{B,P_{1}}^{n}(\mathbf{X}^{\sigma}){}\rangle_{\neg
B}\right),\quad\text{where}$
$\displaystyle\qquad\varphi_{B,P_{1}}(F)=\llbracket
P_{1}\rrbracket(\langle{}F{}\rangle_{B}).$ By the assumption that
$\sigma\models B$, the $0$-th term of this series must be $0$, and thus:
$\displaystyle\llbracket P\rrbracket(\mathbf{X}^{\sigma})$
$\displaystyle=\sum_{n=1}^{\infty}\left([\lightning]_{\varphi_{B,P_{1}}^{n}(\mathbf{X}^{\sigma})}X_{\lightning}+\langle{}\varphi_{B,P_{1}}^{n}(\mathbf{X}^{\sigma}){}\rangle_{\neg
B}\right)$

We can therefore restate the initial claims of Lemma 14 as the following
(stricter) conditions:

  1. 1.

For all $n\in\mathbb{N}_{>0}$:

$\qquad{\Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit_{=n}\langle{}\downarrow,\sigma^{\prime}{}\rangle)=[\sigma^{\prime}]_{\langle{}\varphi_{B,P_{1}}^{n}(\mathbf{X}^{\sigma}){}\rangle_{\neg
B}}$

  2. 2.

For all $n\in\mathbb{N}_{>0}$:

$\qquad{\Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit_{=n}\langle{}\lightning{}\rangle)=[\lightning]_{\varphi_{B,P_{1}}^{n}(\mathbf{X}^{\sigma})}$

For both parts, we make use of the following observation, which follows from
the linearity of $\varphi$ and the assumption $\sigma\models B$:

$\displaystyle\varphi_{B,P_{1}}^{n+1}(\mathbf{X}^{\sigma})$
$\displaystyle=\varphi_{B,P_{1}}^{n}\left(\varphi_{B,P_{1}}(\mathbf{X}^{\sigma})\right)$
$\displaystyle=\varphi_{B,P_{1}}^{n}\left(\sum_{\sigma^{\prime\prime}\in\mathbb{N}^{k}}[\sigma^{\prime\prime}]_{\llbracket
P_{1}\rrbracket(\mathbf{X}^{\sigma})}\mathbf{X}^{\sigma^{\prime\prime}}\right)$
(3)
$\displaystyle=\sum_{\sigma^{\prime\prime}\in\mathbb{N}^{k}}[\sigma^{\prime\prime}]_{\llbracket
P_{1}\rrbracket(\mathbf{X}^{\sigma})}\cdot\varphi_{B,P_{1}}^{n}(\mathbf{X}^{\sigma^{\prime\prime}})$

  1. 1.

First, note that a loop can never terminate in $\sigma^{\prime}$ if
$\sigma^{\prime}\models B$. Accordingly, the construction rules of the Markov
chain semantics (cf. Figure 4) contain the rule (while-f) as the only way of
reaching a terminating state from a loop, which is only applicable if
$\sigma^{\prime}\not\models B$. We therefore have (for all
$n\in\mathbb{N}^{k}_{>0}$):

${\Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit_{=n}\langle{}\downarrow,\sigma^{\prime}{}\rangle)=[\sigma^{\prime}]_{\langle{}\varphi_{B,P_{1}}^{n}(\mathbf{X}^{\sigma}){}\rangle_{\neg
B}}=0$

We show the case $\sigma^{\prime}\not\models B$ by induction:

##### Base case:

$n=1$.

$\displaystyle\quad{\Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit_{=1}\langle{}\downarrow,\sigma^{\prime}{}\rangle)$
$\displaystyle={\Pr}^{\mathcal{R}_{\sigma}\llbracket
P_{1}\rrbracket}(\diamondsuit\langle{}\downarrow,\sigma^{\prime}{}\rangle)$
(outer I.H.) $\displaystyle=[\sigma^{\prime}]_{\llbracket
P_{1}\rrbracket(\mathbf{X}^{\sigma})}$ ($\sigma^{\prime}\not\models B$)
$\displaystyle=[\sigma^{\prime}]_{\langle{}\llbracket
P_{1}\rrbracket(\mathbf{X}^{\sigma}){}\rangle_{\neg B}}$ ($\sigma\models B$)
$\displaystyle=[\sigma^{\prime}]_{\langle{}\llbracket
P_{1}\rrbracket(\langle{}\mathbf{X}^{\sigma}{}\rangle_{B}){}\rangle_{\neg B}}$
$\displaystyle=[\sigma^{\prime}]_{\langle{}\varphi_{B,P_{1}}(\mathbf{X}^{\sigma}){}\rangle_{\neg
B}}$

##### Induction step:

In order for the loop to terminate in $n+1$ iterations, the first execution of
the loop body must terminate in some state $\sigma^{\prime\prime}$, from which
the loop then terminates in $n$ iterations, i.e.:

$\displaystyle\quad{\Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit_{=n+1}\langle{}\downarrow,\sigma^{\prime}{}\rangle)$
$\displaystyle=\sum_{\sigma^{\prime\prime}\in\mathbb{N}^{K}}{\Pr}^{\mathcal{R}_{\sigma}\llbracket
P_{1}\rrbracket}(\diamondsuit\langle{}\downarrow,\sigma^{\prime\prime}{}\rangle\cdot{\Pr}^{\mathcal{R}_{\sigma^{\prime\prime}}\llbracket
P\rrbracket}(\diamondsuit_{=n}\langle{}\downarrow,\sigma^{\prime}{}\rangle)$
(outer I.H.)
$\displaystyle=\sum_{\sigma^{\prime\prime}\in\mathbb{N}^{k}}[\sigma^{\prime\prime}]_{\llbracket
P_{1}\rrbracket(\mathbf{X}^{\sigma})}\cdot{\Pr}^{\mathcal{R}_{\sigma^{\prime\prime}}\llbracket
P\rrbracket}(\diamondsuit_{=n}\langle{}\downarrow,\sigma^{\prime}{}\rangle)$
($0$ if $\sigma^{\prime\prime}\not\models B$)
$\displaystyle=\sum_{\sigma^{\prime\prime}\models
B}[\sigma^{\prime\prime}]_{\llbracket
P_{1}\rrbracket(\mathbf{X}^{\sigma})}\cdot{\Pr}^{\mathcal{R}_{\sigma^{\prime\prime}}\llbracket
P\rrbracket}(\diamondsuit_{=n}\langle{}\downarrow,\sigma^{\prime}{}\rangle)$
(inner I.H.) $\displaystyle=\sum_{\sigma^{\prime\prime}\models
B}[\sigma^{\prime\prime}]_{\llbracket
P_{1}\rrbracket(\mathbf{X}^{\sigma})}\cdot[\sigma^{\prime}]_{\langle{}\varphi_{B,P_{1}}^{n}(\mathbf{X}^{\sigma^{\prime\prime}}){}\rangle_{\neg
B}}$ ($0$ if $\sigma^{\prime\prime}\not\models B$)
$\displaystyle=\sum_{\sigma^{\prime\prime}\in\mathbb{N}^{k}}[\sigma^{\prime\prime}]_{\llbracket
P_{1}\rrbracket(\mathbf{X}^{\sigma})}\cdot[\sigma^{\prime}]_{\langle{}\varphi_{B,P_{1}}^{n}(\mathbf{X}^{\sigma^{\prime\prime}}){}\rangle_{\neg
B}}$ (Lin. of $[\sigma^{\prime}]$ and $\langle{}\cdot{}\rangle_{B}$)
$\displaystyle=\sum_{\sigma^{\prime\prime}\in\mathbb{N}^{k}}[\sigma^{\prime}]_{\langle{}[\sigma^{\prime\prime}]_{\llbracket
P_{1}\rrbracket(\mathbf{X}^{\sigma})}\cdot\varphi_{B,P_{1}}^{n}(\mathbf{X}^{\sigma^{\prime\prime}}){}\rangle_{\neg
B}}$ (Lin. of $[\sigma^{\prime}]$ and $\langle{}\cdot{}\rangle_{B}$)
$\displaystyle=[\sigma^{\prime}]_{\langle{}\sum_{\sigma^{\prime\prime}\in\mathbb{N}^{k}}[\sigma^{\prime\prime}]_{\llbracket
P_{1}\rrbracket(\mathbf{X}^{\sigma})}\cdot\varphi_{B,P_{1}}^{n}(\mathbf{X}^{\sigma^{\prime\prime}}){}\rangle_{\neg
B}}$ (by Equation 3)
$\displaystyle=[\sigma^{\prime}]_{\langle{}\varphi_{B,P_{1}}^{n+1}(\mathbf{X}^{\sigma}){}\rangle_{\neg
B}}$

  2. 2.

By induction:

##### Base case:

$n=1$.

$\displaystyle\quad{\Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit_{=1}\langle{}\lightning{}\rangle)$
$\displaystyle={\Pr}^{\mathcal{R}_{\sigma}\llbracket
P_{1}\rrbracket}(\diamondsuit\lightning)$ (outer I.H.)
$\displaystyle=[\lightning]_{\llbracket P_{1}\rrbracket(\mathbf{X}^{\sigma})}$
($\sigma\models B$) $\displaystyle=[\lightning]_{\llbracket
P_{1}\rrbracket(\langle{}\mathbf{X}^{\sigma}{}\rangle_{B})}$
$\displaystyle=[\lightning]_{\varphi_{B,P_{1}}(\mathbf{X}^{\sigma})}$

##### Induction step:

In order for the loop to reach $\langle{}\lightning{}\rangle$ in the
$(n+1)$-th iteration, the first execution of the loop body must terminate in
some state $\sigma^{\prime\prime}$, from where $\langle{}\lightning{}\rangle$
is then reached in the $n$-th iteration, i.e.:

$\displaystyle\quad{\Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit_{=n+1}\langle{}\lightning{}\rangle)$
$\displaystyle=\sum_{\sigma^{\prime\prime}\in\mathbb{N}^{k}}{\Pr}^{\mathcal{R}_{\sigma}\llbracket
P_{1}\rrbracket}(\diamondsuit\langle{}\downarrow,\sigma^{\prime\prime}{}\rangle\cdot{\Pr}^{\mathcal{R}_{\sigma^{\prime\prime}}\llbracket
P\rrbracket}(\diamondsuit_{=n}\langle{}\lightning{}\rangle)$ (outer I.H.)
$\displaystyle=\sum_{\sigma^{\prime\prime}\in\mathbb{N}^{k}}[\sigma^{\prime\prime}]_{\llbracket
P_{1}\rrbracket(\mathbf{X}^{\sigma})}\cdot{\Pr}^{\mathcal{R}_{\sigma^{\prime\prime}}\llbracket
P\rrbracket}(\diamondsuit_{=n}\langle{}\lightning{}\rangle)$ ($0$ if
$\sigma^{\prime\prime}\not\models B$)
$\displaystyle=\sum_{\sigma^{\prime\prime}\models
B}[\sigma^{\prime\prime}]_{\llbracket
P_{1}\rrbracket(\mathbf{X}^{\sigma})}\cdot{\Pr}^{\mathcal{R}_{\sigma^{\prime\prime}}\llbracket
P\rrbracket}(\diamondsuit_{=n}\langle{}\lightning{}\rangle)$ (inner I.H.)
$\displaystyle=\sum_{\sigma^{\prime\prime}\models
B}[\sigma^{\prime\prime}]_{\llbracket
P_{1}\rrbracket(\mathbf{X}^{\sigma})}\cdot[\lightning]_{\varphi_{B,P_{1}}^{n}(\mathbf{X}^{\sigma^{\prime\prime}})}$
($0$ if $\sigma^{\prime\prime}\not\models B$)
$\displaystyle=\sum_{\sigma^{\prime\prime}\in\mathbb{N}^{k}}[\sigma^{\prime\prime}]_{\llbracket
P_{1}\rrbracket(\mathbf{X}^{\sigma})}\cdot[\lightning]_{\varphi_{B,P_{1}}^{n}(\mathbf{X}^{\sigma^{\prime\prime}})}$
(Lin. of $[\lightning]$)
$\displaystyle=\sum_{\sigma^{\prime\prime}\in\mathbb{N}^{k}}[\lightning]_{[\sigma^{\prime\prime}]_{\llbracket
P_{1}\rrbracket(\mathbf{X}^{\sigma})}\cdot\varphi_{B,P_{1}}^{n}(\mathbf{X}^{\sigma^{\prime\prime}})}$
(Lin. of $[\lightning]$ and $\langle{}\cdot{}\rangle_{B}$)
$\displaystyle=[\lightning]_{\sum_{\sigma^{\prime\prime}\in\mathbb{N}^{k}}[\sigma^{\prime\prime}]_{\llbracket
P_{1}\rrbracket(\mathbf{X}^{\sigma})}\cdot\varphi_{B,P_{1}}^{n}(\mathbf{X}^{\sigma^{\prime\prime}})}$
(by Equation 3)
$\displaystyle=[\lightning]_{\varphi_{B,P_{1}}^{n+1}(\mathbf{X}^{\sigma})}$

∎

###### Theorem 15 (Operational Equivalence).

For every cpGCL program $p$ and every
$\sigma,\sigma^{\prime}\in\mathbb{N}^{k}$

$\displaystyle\text{Pr}^{\mathcal{R}_{\sigma}}\llbracket
P\rrbracket(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle\mid\neg\diamondsuit\lightning)~{}{}={}~{}[\sigma^{\prime}]_{\textit{norm}(\llbracket
P\rrbracket(\mathbf{{X}}^{\sigma}))}~{}.$

This includes the case of undefined semantics, i.e., the left-hand side is
undefined if and only if the right-hand side is undefined.

###### Proof.

$\displaystyle\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle\mid\neg\diamondsuit\lightning)$
$\displaystyle=\frac{\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle\wedge\neg\diamondsuit\lightning)}{\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\neg\diamondsuit\lightning)}$ (reaching
$\langle\downarrow,\sigma^{\prime}\rangle$ implies not reaching
$\langle\lightning\rangle$)
$\displaystyle=\frac{\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle)}{\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\neg\diamondsuit\lightning)}$
$\displaystyle=\frac{\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\langle\downarrow,\sigma^{\prime}\rangle)}{1-\text{Pr}^{\mathcal{R}_{\sigma}\llbracket
P\rrbracket}(\diamondsuit\lightning)}$ (cf. Lemma 14)
$\displaystyle=\frac{[\sigma^{\prime}]_{\llbracket
P\rrbracket(\mathbf{{X}}^{\sigma})}}{1-[\lightning]_{\llbracket
P\rrbracket(\mathbf{{X}}^{\sigma})}}$
$\displaystyle=[\sigma^{\prime}]_{\textit{norm}(\llbracket
P\rrbracket(\mathbf{{X}}^{\sigma}))}$

∎

##  Appendix C Reasoning about Loops

###### Definition 1 (Admissible eSOP-transformer).

A function $\psi\colon\textnormal{{eSOP}}\to\textnormal{{eSOP}}$ is called
_admissible_ if

  * •

$\psi$ is _continuous_ on eSOP.

  * •

$\psi$ is _linear_ in the following sense: For all $F,G\in\textnormal{{eSOP}}$
and $p\in[0,1]$

$pF+G\in\textnormal{{eSOP}}\quad\text{implies}\quad\psi(pF+G)~{}{}={}~{}p\psi(F)+\psi(G)~{}.$

  * •

$\psi$ is _homogeneous w.r.t. meta indeterminates_ , i.e., for all
$G\in\textnormal{{eSOP}}$ and $\tau\in\mathbb{N}^{l}$,

$\psi(G\mathbf{{U}}^{\tau})~{}{}={}~{}\psi(G)\mathbf{{U}}^{\tau}~{}.$

  * •

$\psi$ _preserves ePGF_ , i.e., $G\in\textnormal{{ePGF}}$ implies
$\psi(G)\in\textnormal{{ePGF}}$.

###### Theorem 2 (SOP Semantics).

Let $P$ be a loop-free cReDiP Program. Let
$G=\sum_{\sigma\in\mathbb{N}^{k}}G_{\sigma}\mathbf{{U}}^{\sigma}\in\textnormal{{eSOP}}$.
The eSOP semantics of $P$ is then given by:

$\llbracket P\rrbracket(G)=\sum_{\sigma\in\mathbb{N}^{k}}\llbracket
P\rrbracket(G_{\sigma})\cdot\mathbf{{U}}^{\sigma}$

###### Proof outline.

The proof of Theorem 5 proceeds along a similar line of reasoning as in (Chen
et al., 2022). First of all, we use Lemma 12 and obtain:

$\displaystyle\llbracket P\rrbracket(G)$
$\displaystyle=\sum_{\sigma\in\mathbb{N}^{k}}\llbracket
P\rrbracket(G_{\sigma}\mathbf{{U}}^{\sigma})$ (by eFPS arithmetic)
$\displaystyle=\sum_{\sigma\in\mathbb{N}^{k}}\llbracket
P\rrbracket\left(\sum_{\tau\in\mathbb{N}^{k}}[\tau]_{G_{\sigma}}\mathbf{{X}}^{\tau}\mathbf{{U}}^{\sigma}+[\lightning]_{G_{\sigma}}X_{\lightning}\mathbf{{U}}^{\sigma}\right)$
(by Lemma 12)
$\displaystyle=\sum_{\sigma\in\mathbb{N}^{k}}\sum_{\tau\in\mathbb{N}^{k}}\llbracket
P\rrbracket\left([\tau]_{G_{\sigma}}\mathbf{{X}}^{\tau}\mathbf{{U}}^{\sigma}+[\lightning]_{G_{\sigma}}X_{\lightning}\mathbf{{U}}^{\sigma}\right)$
(by Theorem 9)
$\displaystyle=\sum_{\sigma\in\mathbb{N}^{k}}\sum_{\tau\in\mathbb{N}^{k}}\llbracket
P\rrbracket\left([\tau]_{G_{\sigma}}\mathbf{{X}}^{\tau}\mathbf{{U}}^{\sigma}\right)+\llbracket
P\rrbracket\left([\lightning]_{G_{\sigma}}X_{\lightning}\mathbf{{U}}^{\sigma}\right)$
(by Lemma 4, Theorem 9)
$\displaystyle=\sum_{\sigma\in\mathbb{N}^{k}}\sum_{\tau\in\mathbb{N}^{k}}[\tau]_{G_{\sigma}}\cdot\llbracket
P\rrbracket\left(\mathbf{{X}}^{\tau}\mathbf{{U}}^{\sigma}\right)+[\lightning]_{G_{\sigma}}X_{\lightning}\mathbf{{U}}^{\sigma}$

Thus we need to show, that $\llbracket
P\rrbracket(\mathbf{{X}}^{\tau}\mathbf{{U}}^{\sigma})$ is homogeneous for all
$\tau,\sigma\in\mathbb{N}$. All loop-free cases but observe coincide with
ReDiP (Chen et al., 2022) on the distributions where the observe violation
probability is zero which is an immediate consequence of Lemma 4 and the
definition in Table 3.

To complete the proof, we show that
$\textnormal{{observe}}\,\left(\,{\textnormal{{false}}}\,\right)$ also has
this property by showing that its semantics is admissible. Recall the
$\textnormal{{observe}}\,\left(\,{\textnormal{{false}}}\,\right)$ semantics:
$G[\mathbf{{X}}/\mathbf{{1}},X_{\lightning}/1]\cdot X_{\lightning}$. Note that
the $\textnormal{{observe}}\,\left(\,{\textnormal{{false}}}\,\right)$
semantics is entirely based on the following elementary transformations, which
are admissible (by (Chen et al., 2022)):

  * •

Multiplication by a constant $G\in\textup{ePGF}\colon\lambda F.~{}G\cdot F$

  * •

Substitution of $X\in\mathbf{{X}}$ by a constant
$G\in\textup{ePGF}\colon\lambda F.~{}F[X/G]$.

Thus,
$\llbracket\textnormal{{observe}}\,\left(\,{\textnormal{{false}}}\,\right)\rrbracket\left(\mathbf{{X}}^{\tau}\mathbf{{U}}^{\sigma}\right)=\llbracket\textnormal{{observe}}\,\left(\,{\textnormal{{false}}}\,\right)\rrbracket\left(\mathbf{{X}}^{\tau}\right)\mathbf{{U}}^{\sigma}$
holds. Another, direct argument is as follows: It is important to understand
the second column of Table 3 correctly, especially for the
$\textnormal{{observe}}\,\left(\,{\textnormal{{false}}}\,\right)$ statement.
Here, $\mathbf{{X}}$ explicitly refers to the program variables occurring in
$P$, _not_ for the meta-indeterminates $\mathbf{{U}}$. In case we would also
substitute these values by 1, we would loose all information gathered by the
second order approach. Thus applying the semantics correctly, we get
$\llbracket\textnormal{{observe}}\,\left(\,{\textnormal{{false}}}\,\right)\rrbracket\left(\mathbf{{X}}^{\tau}\mathbf{{U}}^{\sigma}\right)=\mathbf{{1}}^{\tau}X_{\lightning}\mathbf{{U}}^{\sigma}=\llbracket\textnormal{{observe}}\,\left(\,{\textnormal{{false}}}\,\right)\rrbracket\left(\mathbf{{X}}^{\tau}\right)\mathbf{{U}}^{\sigma}$.
Combining that with the equation from above, we conclude

$\displaystyle\sum_{\sigma\in\mathbb{N}^{k}}\sum_{\tau\in\mathbb{N}^{k}}[\tau]_{G_{\sigma}}\cdot\llbracket
P\rrbracket\left(\mathbf{{X}}^{\tau}\mathbf{{U}}^{\sigma}\right)+[\lightning]_{G_{\sigma}}X_{\lightning}\mathbf{{U}}^{\sigma}$
$\displaystyle=\sum_{\sigma\in\mathbb{N}^{k}}\sum_{\tau\in\mathbb{N}^{k}}[\tau]_{G_{\sigma}}\cdot\llbracket
P\rrbracket\left(\mathbf{{X}}^{\tau}\right)\mathbf{{U}}^{\sigma}+[\lightning]_{G_{\sigma}}X_{\lightning}\mathbf{{U}}^{\sigma}$
(by Theorem 9)
$\displaystyle=\sum_{\sigma\in\mathbb{N}^{k}}\sum_{\tau\in\mathbb{N}^{k}}\llbracket
P\rrbracket\left([\tau]_{G_{\sigma}}\cdot\mathbf{{X}}^{\tau}\right)\mathbf{{U}}^{\sigma}+\llbracket
P\rrbracket\left([\lightning]_{G_{\sigma}}X_{\lightning}\right)\mathbf{{U}}^{\sigma}$
(by eFPS arithmetic)
$\displaystyle=\sum_{\sigma\in\mathbb{N}^{k}}\sum_{\tau\in\mathbb{N}^{k}}\left(\llbracket
P\rrbracket\left([\tau]_{G_{\sigma}}\cdot\mathbf{{X}}^{\tau}\right)+\llbracket
P\rrbracket\left([\lightning]_{G_{\sigma}}X_{\lightning}\right)\right)\mathbf{{U}}^{\sigma}$
(Theorem 9)
$\displaystyle=\sum_{\sigma\in\mathbb{N}^{k}}\sum_{\tau\in\mathbb{N}^{k}}\left(\llbracket
P\rrbracket\left([\tau]_{G_{\sigma}}\cdot\mathbf{{X}}^{\tau}+[\lightning]_{G_{\sigma}}X_{\lightning}\right)\right)\mathbf{{U}}^{\sigma}$
(by Def. of $G_{\sigma}$)
$\displaystyle=\sum_{\sigma\in\mathbb{N}^{k}}\llbracket
P\rrbracket\left(G_{\sigma}\right)\mathbf{{U}}^{\sigma}$

∎

##  Appendix D Parameter Synthesis

###### Theorem 1 (Decidability of Parameter Synthesis).

Let $W$ be a cReDiP while loop and $Q_{\mathbf{{p}}}$ be a loop-free cReDiP
program. It is decidable whether there exist parameter values $\mathbf{{p}}$
such that the instantiated template $Q_{\mathbf{{p}}}$ is an inductive
invariant, i.e.,
$\exists\mathbf{{p}}\in\mathbb{R}^{l}.~{}\forall\mathbf{{X}}\in\text{Vars}(W).~{}\quad\llbracket
W\rrbracket=\llbracket Q_{\mathbf{{p}}}\rrbracket$.

###### Proof.

Let $W$ and $Q_{\mathbf{{p}}}$ be given as described. Also, let
$g=(1-X_{1}U_{1})^{-1}\cdots(1-X_{k}U_{k})^{-1}\in\textnormal{{SOP}}$.

$\displaystyle\exists\mathbf{{p}}\in\mathbb{R}^{l}.~{}\forall\mathbf{{X}}.\quad\quad\llbracket
Q_{\mathbf{{p}}}\rrbracket=\llbracket\Phi_{B,P}(Q_{\mathbf{{p}}})\rrbracket$
(Lemma 6) $\displaystyle\Leftrightarrow~{}$
$\displaystyle\exists\mathbf{{p}}\in\mathbb{R}^{l}.~{}\forall\mathbf{{X}}.~{}\forall\mathbf{{U}}.\quad\llbracket
Q_{\mathbf{{p}}}\rrbracket(g)=\llbracket\Phi_{B,P}(Q_{\mathbf{{p}}})\rrbracket(g)$
(loop-free cReDiP preserves rational functions)
$\displaystyle\Leftrightarrow~{}$
$\displaystyle\exists\mathbf{{p}}\in\mathbb{R}^{l}.~{}\forall\mathbf{{X}}.~{}\forall\mathbf{{U}}.\quad\frac{F(\mathbf{{X}},X_{\lightning},\mathbf{{U}},\mathbf{{p}})}{H(\mathbf{{X}},X_{\lightning},\mathbf{{U}},\mathbf{{p}})}=\frac{\hat{F}(\mathbf{{X}},X_{\lightning},\mathbf{{U}},\mathbf{{p}})}{\hat{H}(\mathbf{{X}},X_{\lightning},\mathbf{{U}},\mathbf{{p}})}$
$\displaystyle\Leftrightarrow~{}$
$\displaystyle\exists\mathbf{{p}}\in\mathbb{R}^{l}.~{}\forall\mathbf{{X}}.~{}\forall\mathbf{{U}}.\quad
F(\mathbf{{X}},X_{\lightning},\mathbf{{U}},\mathbf{{p}})\hat{H}(\mathbf{{X}},X_{\lightning},\mathbf{{U}},\mathbf{{p}})=\hat{F}(\mathbf{{X}},X_{\lightning},\mathbf{{U}},\mathbf{{p}})H(\mathbf{{X}},X_{\lightning},\mathbf{{U}},\mathbf{{p}})$
$\displaystyle\Leftrightarrow~{}$
$\displaystyle\exists\mathbf{{p}}\in\mathbb{R}^{l}.~{}\forall\mathbf{{X}}.~{}\forall\mathbf{{U}}.\quad
F(\mathbf{{X}},\mathbf{{U}},\mathbf{{p}})\hat{H}(\mathbf{{X}},\mathbf{{U}},\mathbf{{p}})-\hat{F}(\mathbf{{X}},\mathbf{{U}},\mathbf{{p}})H(\mathbf{{X}},\mathbf{{U}},\mathbf{{p}})=0$

In the last step
$F(\mathbf{{X}},X_{\lightning},\mathbf{{U}},\mathbf{{p}})\hat{H}(\mathbf{{X}},X_{\lightning},\mathbf{{U}},\mathbf{{p}})$
and
$\hat{F}(\mathbf{{X}},X_{\lightning},\mathbf{{U}},\mathbf{{p}})H(\mathbf{{X}},X_{\lightning},\mathbf{{U}},\mathbf{{p}})$
are polynomials in
$\mathbb{R}[\mathbf{{p}}][\mathbf{{X}},X_{\lightning},\mathbf{{U}}]$. Using
the results about quantifier elimination in the theory of non-linear real
arithmetic (by Cylindrical Algebraic Decomposition (Caviness and Johnson,
2012)), we have a decision procedure of
$\mathcal{O}\left(2^{2^{\left|X\right|+\left|U\right|+1}}\right)$ worst-case
complexity to decide whether the formula can be satisfied. ∎

##  Appendix E Additional Examples

###### Example 1.

This example of two programs $I$ and $J$ shows the step-by-step computation of
the invariant and the modified invariant to proof the actual equivalence.

$\displaystyle I:\qquad$
$\displaystyle{{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}\\!\\!{\fatslash}\\!\\!{\fatslash}~{}~{}\vphantom{G^{\prime}}{(1-XU)^{-1}(1-YV)^{-1}}}}$
$\displaystyle\textnormal{{if}}\,\left(\,{y=1}\,\right)\,\\{$
$\displaystyle\qquad{{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}\\!\\!{\fatslash}\\!\\!{\fatslash}~{}~{}\vphantom{G^{\prime}}{(1-XU)^{-1}YV}}}$
$\displaystyle\qquad
x~{}+\\!={\textnormal{{iid}}\left(\mathtt{geom}\left(\nicefrac{{1}}{{2}}\right)+1,y\right)}\fatsemi$
$\displaystyle\qquad{{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}\\!\\!{\fatslash}\\!\\!{\fatslash}~{}~{}\vphantom{G^{\prime}}{(1-XU)^{-1}X(2-X)^{-1}YV}}}$
$\displaystyle\qquad y\mathrel{\textnormal{$\mathtt{\coloneqq}$}}0\fatsemi$
$\displaystyle\qquad{{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}\\!\\!{\fatslash}\\!\\!{\fatslash}~{}~{}\vphantom{G^{\prime}}{(1-XU)^{-1}X(2-X)^{-1}V}}}$
$\displaystyle\qquad\textnormal{{observe}}\,\left(\,{x<3}\,\right)$
$\displaystyle\qquad{{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}\\!\\!{\fatslash}\\!\\!{\fatslash}~{}~{}\vphantom{G^{\prime}}{(\nicefrac{{1}}{{2}}X+\nicefrac{{1}}{{4}}X^{2}+\nicefrac{{1}}{{4}}X_{\lightning})V}}}$
$\displaystyle\qquad\qquad{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}+\left((\nicefrac{{1}}{{2}}X^{2}+\nicefrac{{1}}{{2}}X_{\lightning})U+X_{\lightning}U^{2}(1-U)^{-1}\right)V}$
$\displaystyle\\}$
$\displaystyle{{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}\\!\\!{\fatslash}\\!\\!{\fatslash}~{}~{}\vphantom{G^{\prime}}{(1-XU)^{-1}(1-YV)^{-1}-(1-XU)^{-1}YV}}}$
$\displaystyle\qquad{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}+(\nicefrac{{1}}{{2}}X+\nicefrac{{1}}{{4}}X^{2}+\nicefrac{{1}}{{4}}X_{\lightning})V}$
$\displaystyle\qquad{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}+\left((\nicefrac{{1}}{{2}}X^{2}+\nicefrac{{1}}{{2}}X_{\lightning})U+X_{\lightning}U^{2}(1-U)^{-1}\right)V}$

We want to show that $\llbracket J\rrbracket(\hat{G})$ — where
$J=\textnormal{{if}}\,\left(\,{y=1}\,\right)\,\\{P\fatsemi
I\\}\,\textnormal{{else}}\,\\{\textnormal{{skip}}\\}$ — yields the same
result:

$\displaystyle J:\qquad$
$\displaystyle{{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}\\!\\!{\fatslash}\\!\\!{\fatslash}~{}~{}\vphantom{G^{\prime}}{(1-XU)^{-1}(1-YV)^{-1}}}}$
$\displaystyle\textnormal{{if}}\,\left(\,{y=1}\,\right)\,\\{$
$\displaystyle\qquad{{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}\\!\\!{\fatslash}\\!\\!{\fatslash}~{}~{}\vphantom{G^{\prime}}{(1-XU)^{-1}YV}}}$
$\displaystyle\qquad\left\\{\,{y\mathrel{\textnormal{$\mathtt{\coloneqq}$}}0}\,\right\\}\mathrel{\left[\,\nicefrac{{1}}{{2}}\,\right]}\left\\{\,{y\mathrel{\textnormal{$\mathtt{\coloneqq}$}}1}\,\right\\}\fatsemi$
$\displaystyle\qquad{{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}\\!\\!{\fatslash}\\!\\!{\fatslash}~{}~{}\vphantom{G^{\prime}}{\nicefrac{{1}}{{2}}(1-XU)^{-1}(Y+1)V}}}$
$\displaystyle\qquad x\mathrel{\textnormal{$\mathtt{\coloneqq}$}}x+1\fatsemi$
$\displaystyle\qquad{{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}\\!\\!{\fatslash}\\!\\!{\fatslash}~{}~{}\vphantom{G^{\prime}}{\nicefrac{{1}}{{2}}X(1-XU)^{-1}(Y+1)V}}}$
$\displaystyle\qquad\textnormal{{observe}}\,\left(\,{x<3}\,\right)\fatsemi$
$\displaystyle\qquad{{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}\\!\\!{\fatslash}\\!\\!{\fatslash}~{}~{}\vphantom{G^{\prime}}{\left(\nicefrac{{1}}{{2}}(X+X^{2}U)(Y+1)+X_{\lightning}U^{2}(1-U)^{-1}\right)V}}}$
$\displaystyle\qquad\textnormal{{if}}\,\left(\,{y=1}\,\right)\,\\{$
$\displaystyle\qquad\qquad{{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}\\!\\!{\fatslash}\\!\\!{\fatslash}~{}~{}\vphantom{G^{\prime}}{\nicefrac{{1}}{{2}}(X+X^{2}U)YV}}}$
$\displaystyle\qquad\qquad
x~{}+\\!={\textnormal{{iid}}\left(\mathtt{geom}\left(\nicefrac{{1}}{{2}}\right)+1,y\right)}\fatsemi$
$\displaystyle\qquad\qquad{{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}\\!\\!{\fatslash}\\!\\!{\fatslash}~{}~{}\vphantom{G^{\prime}}{\nicefrac{{1}}{{2}}(X^{2}+X^{3}U)(2-X)^{-1}YV}}}$
$\displaystyle\qquad\qquad
y\mathrel{\textnormal{$\mathtt{\coloneqq}$}}0\fatsemi$
$\displaystyle\qquad\qquad{{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}\\!\\!{\fatslash}\\!\\!{\fatslash}~{}~{}\vphantom{G^{\prime}}{\nicefrac{{1}}{{2}}(X^{2}+X^{3}U)(2-X)^{-1}V}}}$
$\displaystyle\qquad\qquad\textnormal{{observe}}\,\left(\,{x<3}\,\right)$
$\displaystyle\qquad\qquad{{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}\\!\\!{\fatslash}\\!\\!{\fatslash}~{}~{}\vphantom{G^{\prime}}{\nicefrac{{1}}{{2}}\left(\nicefrac{{1}}{{2}}X^{2}+\nicefrac{{1}}{{2}}X_{\lightning}+X\lightning
U\right)V}}}$ $\displaystyle\qquad\\}$
$\displaystyle\qquad{{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}\\!\\!{\fatslash}\\!\\!{\fatslash}~{}~{}\vphantom{G^{\prime}}{\left((\nicefrac{{1}}{{2}}X+\nicefrac{{1}}{{4}}X^{2}+\nicefrac{{1}}{{4}}X_{\lightning})+(\nicefrac{{1}}{{2}}X^{2}+\nicefrac{{1}}{{2}}X_{\lightning})U\right)V}}}$
$\displaystyle\qquad\qquad{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}+X_{\lightning}U^{2}(1-U)^{-1}V}$
$\displaystyle\\}$
$\displaystyle{{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}\\!\\!{\fatslash}\\!\\!{\fatslash}~{}~{}\vphantom{G^{\prime}}{(1-XU)^{-1}(1-YV)^{-1}-(1-XU)^{-1}YV}}}$
$\displaystyle\qquad{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}+\left((\nicefrac{{1}}{{2}}X+\nicefrac{{1}}{{4}}X^{2}+\nicefrac{{1}}{{4}}X_{\lightning})+(\nicefrac{{1}}{{2}}X^{2}+\nicefrac{{1}}{{2}}X_{\lightning})U\right)V}$
$\displaystyle\qquad{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}+X_{\lightning}U^{2}(1-U)^{-1}V}$