\usetikzlibrary{external,shapes.symbols,automata,positioning,arrows.meta,decorations.pathmorphing,datavisualization.formats.functions,patterns}

\usetikzlibrary{external,shapes.symbols,calc,automata,positioning,arrows.meta,decorations.pathmorphing,datavisualization.formats.functions,patterns}

% TeX root = ../main.tex
\centering
\begin{tikzpicture}[
        shorten >=1pt,
        >={Stealth[round]},
        node distance=2cm,
        semithick,
        on grid,
        auto,
        initial text=,
        initial above,
    ]
    \draw[helplines] (-3,1) grid (3,-7);
    \node[state,initial]    (l0)                            {$l_0$};
    \node[state]            (li1)   [below left = of l0]    {$l_{i_1}$};
    \node[state]            (lin)   [below right = of l0]   {$l_{i_n}$};
    \node[state]            (li1')  [below = of li1]        {$l_{i_1}'$};
    \node[state]            (lin')  [below = of lin]        {$l_{i_n}'$};
    \node[state]            (lo1)   [below = of li1']       {$l_{o_1}$};
    \node[state]            (lom)   [below = of lin']       {$l_{o_m}$};
    \node[state]            (lo1')  [below = of lo1]        {$l_{o_1}'$};
    \node[state]            (lom')  [below = of lom]        {$l_{o_m}'$};
    \node (center)[below=4.2cm of l0] {};
    \draw[color=gray] (center) ellipse [x radius=3cm,y radius=3cm];
    \path[->]   (li1)     edge    node      {$t_{i_1}$}  (li1')
                (lin)     edge    node      {$t_{i_n}$}  (lin')
                (lo1)     edge    node      {$t_{o_1}$}  (lo1')
                (lom)     edge    node      {$t_{o_m}$}  (lom');
    %todo: squigilly line 
    \draw[->,decorate,decoration={snake,pre length=5pt,post length=10pt}] (l0) -- (li1);
    \draw[->,decorate,decoration={snake,pre length=5pt,post length=10pt}] (l0) -- (lin);
\end{tikzpicture}

\begin{comment}
    cfr --
\end{comment}

\subsection{SCCs}
\begin{figure}
    \input{figures/ch4_scc1}
    \caption{Visualization of partial evaluation for a single SCC}
\end{figure}

    For any assignment $s\in\Sigma$, non-probabilistic update $\eta: \PV
    \rightarrow \Z[\V \union D]$, and values $k_i \in

    For any assignment $s,s'\in\Sigma$, and probabilistic update $\eta: \PV
    \rightarrow \Z[\V \union D]$ holds $s'(x_i) = k_i \in
    \text{supp}([\eta(x_i)](s))$ implies $s'\models \tilde{\eta}()$
    and values $k_i \in

\begin{definition}[Equivalent \glspl{pip}]
    Let $\Prog_1,\Prog_2$ be \glspl{pip} with $\Prog_1 = (\PV, \Loc_1, \GT_1,
    l_0)$, $\Prog_2 = (\PV, \Loc_2, \GT_2, l_0)$ and their respective
    probability spaces $(\runs_1, \F_1, \PrSs^1)$ and $(\runs_2, \F_2,
    \PrSs^2)$. Besides $\T_1$ and $\T_2$ denote the set of transitions of
    $\Prog_1$ and $\Prog_2$; $\fpath_1$ and $\fpath_2$ the set of finite paths,
    etc. 
    The two programs are equivalent if the two random variables $\Rt_{\Prog_1}$
    and $\Rt_{\Prog_2}$ have the same probability distributions $\mu_1$ and
    $\mu_2$ with $\mu_1(k) = \mu_2(k)$ for all $k\in\overline{\N}$.
\end{definition}
\begin{theorem}
    If $\Prog_1$ and $\Prog_2$ are equivalent then:
    \begin{enumerate}
        \item A total runtime-complexity bound for the $\Prog_1$ is a total
            runtime complexity bound for $\Prog_2$ and vice-versa. 
        \item $\Prog_1$ and $\Prog_2$ have the same expected runtime-complexity. 
    \end{enumerate}
    \proof{
        Let $\RB_P$ 
    }
\end{theorem}
\begin{rem}
    The probability distribution doesn't care about the underlying probability
    space making it the perfect tool to compare the semantics of two different
    \glspl{pip}.
\end{rem}
We will show the partial evaluation $\Prog'$ is equivalent to the original
\gls{pip} $\Prog$. In a first step we will show that for every admissible finite
prefix in $\Prog$ there exists an admissible finite prefix in $\Prog'$ with the
same probability and intermediate states and vice versa. This in turn will be
expanded for all admissible runs and finally we will show that this proves an
equal probability distribution of the total runtime complexity. 
\subsection{Induction}
Given an admissible run $f^*= c_0c_1\dots \in \runs$ of the original program
$\Prog$ with $c_i = (l_i,s_i,t_i)$ for all $i = 0,1,\dots$ and a scheduler
$\scheduler$ for the very same program. 
\textbf{Induction hypothesis.} We can find an arbitrarily long prefix
$f'_n=c'_0c'_1\cdots{}c_n \in \fpath'$ of length $n \in \N$ and scheduler
$\scheduler'_n$ such that:
\begin{enumerate}
    \item $\prSs(c_0\dots{}c_n) = \prSns'(c'_0\dots{}c'_n)$
    \item  $c'_i = (\langle l_i, \varphi_i\rangle,s_i,t'_i)$ for some
        $\varphi_i \in \C$, $t'_i \in \T'$, and $i = 1, \dots, n$ \label{itm:location_in_version}
    \item $s_i \models \varphi_i$ \label{itm:si_models_phi}
\end{enumerate}
Items \ref{itm:location_in_version} and \ref{itm:si_models_phi} are only
required for the induction, but are unimportant for the final result. 
\textbf{Induction start n=0.}
Since $f^*$ is an admissible run, $c_0 = (l_0, s_0,t_\text{in})$. Set
$f'_0=(\langle l_0,\textit{true}\rangle,s_0,t_\text{in})$. $\langle l_0,
\textit{true}$ is a location in $\Prog'$ since it is added at first by the
evaluation algorithm. $s_0 \models \textit{true}$ trivially. $\prSs(c_0) =
\prSs'(c'_0) = 1$ since both $c_0$ and $c'_0$ are valid starting configurations
in $\Prog$ and $\Prog'$ respectively.
\textbf{Induction step.} 
Assume the induction hypothesis holds for $n$ we will construct a prefix of
length $n+1$ for that the hypothesis equally holds. 
Since the run is admissible, so is its prefix $f_i = c_0c_1\dots{}c_nc_{n+1}$
and by definition \todo{ref}
\begin{equation*}
    \prSs(f) = \prSs(c_0) \cdot \prod_{i=1,\dots,n+1} \prSs(c_{i-1} \rightarrow
    c_i) > 0
\end{equation*}
Let $\scheduler(c_n) = (g_{n+1},\tilde{s}_n)$, by definition \todo{ref}
\begin{equation*}
    \prSs(c_n \rightarrow c_{n+1}) = p \cdot
    \prod_{x\in\PV}[\eta(x)](\tilde{s}_n)(s_{n+1}(x)) \cdot \prod_{u\in\V\backslash\PV}
    \delta_{\tilde{s}_n(u),s_n(u)} > 0
\end{equation*}
Since $f'_n$ is an admissible path, $\langle l_n, \varphi_n \rangle$ is a valid
location (version) in $\Prog'$, every version is unfolded by the evaluation
algorithm immediately after being added to the new program in (\todo{ref}). As
$g_i$ is selected by the scheduler, $g_{n+1}$ is a general transition with
$l_{g_{n+1}} = l_n$. As such $g_{n+1}$ is unfolded by the algorithm in
(\todo{ref}) and so is the transition $t_{n+1}$ as part of unfolding of the
general transition $g_{n+1}$.
With $g'_{n+1}=\text{unfold*}(\varphi_n, g_{i+1})$, define the next
$\scheduler'_{n+1}$ as 
\begin{equation*}
    \scheduler'_{n+1}(c) = \begin{cases}
        (g'_{n+1}, \tilde{s}_n) & \text{if } c = c'_n \\
        \scheduler'_n & \text{otherwise}
    \end{cases}
\end{equation*}
Select $t'_{n+1} = \text{unfold*}(\varphi_n, t_{n+1}) \in g'_{n+1}$
Recall definition (\todo{ref}), by construction $t'_{n+1}=(\langle l_n,
\varphi\rangle,p,\tau_i,\eta,\langle l_{n+1}, \varphi_{n+1}\rangle)$
for some formula $\varphi_{n+1}$.
\begin{equation*}
    \prSnns(c'_n \rightarrow c'_{n+1}) = p \cdot
    \prod_{x\in\PV}[\eta(x)](\tilde{s'}_n)(s'_{n+1}(x)) \cdot \prod_{u\in\V\backslash\PV}
    \delta_{\tilde{s}(u),s(u)} > 0
\end{equation*}
By lemma (\todo{ref}) $s_{n+1} \models \varphi_{n+1}$, fulfilling (3) of the
induction hypothesis. We fulfill (2) of the induction hypothesis, by
constructing $c'_{n+1} = (\langle l_{n+1}, \varphi_n\rangle, s_{n+1},
t'_{n+1})$. By setting $s'_{n+1} = s_{n+1}$ we get $\prSnns(c'_n\rightarrow
c'_{n+1})= \prSs(c_n \rightarrow c_{n+1})$ and with the induction hypothesis
\begin{equation*}
    \prSs(f_n) = \prSnns(f'_nc'_{n+1})
\end{equation*}
and fulfill (1) of the induction hypothesis.

\begin{figure}[h]
    \centering
    \begin{subcaptionblock}[t]{0.45\textwidth}
        \centering
        \input{figures/ch4_scc_prog}
        \caption{The original program}
    \end{subcaptionblock}
    \begin{subcaptionblock}[t]{0.45\textwidth}
        \centering
        \input{figures/ch4_scc_lift}
        \caption{Copy and lift}
    \end{subcaptionblock}
    \begin{subcaptionblock}[t]{0.45\textwidth}
        \centering
        \input{figures/ch4_scc_remove}
        \caption{Remove SCC}
    \end{subcaptionblock}
    \begin{subcaptionblock}[t]{0.45\textwidth}
        \centering
        \input{figures/ch4_scc_evaluate}
        \caption{Evaluate entry transitions}
    \end{subcaptionblock}
    \caption{Visualization of partial evaluation for a single
    SCC\label{fig:evaluate_scc}}
\end{figure}
\begin{algorithm}
    \caption{$evaluate_{SCC}(P, A)$}
    \KwData{ A PIP $P$, a \gls{scc} $A\subset\T$ }
    \KwResult{A Graph $G$}
    $\Tin \leftarrow \Tin(A)$\;
    $\Tout \leftarrow \Tout(A)$\;
    \SetKwFunction{FEvaluate}{evaluate}
    \SetKwProg{Fn}{Function}{:}{end}
    \Fn{\FEvaluate{$G$, $v$, $t$}}{
        $N = \unfold^*(v)$\;
        \For{$t = (v, \tau, \eta, p, v') \in N $}{
            \uIf {$(l_v, \tau, \eta,p, l_{v'}) \in \Tout$}{
                $G \leftarrow G + (v, \tau, \eta, p, \langle v_{l'},
                \textit{true}\rangle)$\;
            }
            \uElseIf {$v' \not\in G$}{
                $G \leftarrow G + t$\;
                $G \leftarrow evaluate(P, G, v')$\;
            }
            \Else {
                $G \leftarrow G + t$\;
            }
        }
        \Return {$G$}
    }
    $G \leftarrow \text{lift}(P - A - \Tin - \Tout)$\;

    \For{$t_i = (l_\text{i}, \_, \_ ,\_, l_\text{i}') \in \Tin $}{
        $ G \leftarrow \text{evaluate}(P, G, \langle l_i, \textit{true}\rangle,
        t_i)$\;
    }
    \Return {$G$}\;
\end{algorithm}

\newcommand{\D}[0]{\mathcal{D}} % variable distributions 

\newcommand{\prSns}[0]{\textit{pr}_{\scheduler'_n, s_0}}
\newcommand{\prSnns}[0]{\textit{pr}_{\scheduler'_{n+1}, s_0}}

\section{Preliminaries}\label{sec:preliminaries}
\subsection{Constraints}\label{ssec:constraints}

This thesis uses a lot of notation. For ease of reading, the reader is provided
with this overview of commonly encountered symbols and their usage.
\begin{center}
    \begin{tabular}{|l|l|}
        \hline
        Symbols & Usage \\ 
        \hline
        $a,i,j,l,k,m,n$ & integer values \\
        $e$ & polynomial expressions \\
        $s$ & assignments \\
        $p$ & probability \\
        $x,y,z$ & program variables \\
        $D$ & distributions \\
        $d$ & temporary variable replacing a distribution \\
        $\psi, $ & constraints \\
        $\varphi, $ & formulas\\
        $l$ & locations \\
        $t$ & transitions \\
        $g$ & general transitions \\
        $\tau$ & guards of transitions \\
        $u$ & non-probabilistic update functions\\
        $\eta$ & probabilistic update functions\\
        $\vartheta$ & probabilistic polynomial.\\
        $\mu$ & probability distributions \\
        $f$ & finite prefixes \\
        $\scheduler$ & scheduler \\
        $\B$ & set of bounds \\
        $\C$ & set of constraints \\
        $\D$ & set of distributions \\
        $\G$ & set of graphs \\
        $\GT$ & set of general transitions \\
        $\Lin$ & set of linear constraints\\
        $\PV$ & set of program variables \\
        $\T$ & set of transitions \\
        $\TV$ & set of temporary variables \\
        $\V$ & set of variables \\
        \hline
    \end{tabular}
\end{center}
Let $\overline{\N} = \N \union \{\infty\}$. Let $[\cdot\backslash{}\cdot]$
denote the syntactical substitution where one symbols is replaced by
another. For example $(x<y)[x\backslash{}1] = (1 < y)$. 
For $n \in \N$ consecutive substitutions they also denoted using a shortened
notation. For example $[x_i\backslash{}y_i] =
[x_0\backslash{}y_0]\dots[x_n\backslash{}y_n]\dots$ for some $i = 0,\dots, n$. 
\section{Constraints}\label{sec:constraints}

    non-strict inequality constraints} is defined as the set $\Lin^{\leq}$:
    \begin{align}
        \Lin^{\leq}=\set{a_0 + \sum_{i=1}^{n} a_i v_i \leq 0}{a_i \in \R}
    \end{align}

    non-strict inequality constraints} is defined as the set
    \begin{align*}
        \Lin^{\leq}=\set{a_0 + \sum_{i=1}^{n} a_i v_i \leq 0}{a_i \in \R}.
    \end{align*}

    defined as the set $\Lin^{<}$:
    \begin{align}
        \Lin^{<}:=\set{a_0 + \sum_{i=1}^{n} a_i v_i < 0}{a_i \in \R}
    \end{align}

    defined as the set
    \begin{align*}
        \Lin^{<}=\set{a_0 + \sum_{i=1}^{n} a_i v_i < 0}{a_i \in \R}.
    \end{align*}
    The union of strict and non-strict linear constraints is called
    \textit{mixed linear inequality} constraints denoted as $\Lin = \Lin^{\leq}
    \union \Lin^{<}$.
    The set of \textit{non-strict polynomial inequality} constraints is defined
    as the set 
    \begin{equation*}
        \C^{\leq} = \set{e \leq 0}{e \in \Z[\V]},
    \end{equation*}
    whereas the set of \textit{strict polynomial inequality} constraints is
    defined as the set 
    \begin{equation*}
        \C^< = \set{e < 0}{e \in \Z[\V]},
    \end{equation*}
    and the set of \textit{mixed polynomial inequality} constraints is the set
    $\C = \C^{\leq} \union \C^{<}$. 

The union of strict and non-strict linear constraints is called \textit{mixed}
linear constraints denoted as $\Lin := \Lin^{\leq} \union \Lin^{<}$.

\begin{rem}
    Strict and non-strict linear constraints are a subset of their polynomial
    counterpart. For the most part we will just refer to \enquote{constraints}
    when the exact type of constraint is unimportant.
\end{rem}

    <, =)$, a constraint $\psi \in \Lin$ is \textit{satisfiable} in when
    $\mathfrak{A} \models \psi$. We say a (total) variable assignment $\beta: \V

    <, =)$, a constraint $\psi \in \C$ is \textit{satisfiable} in when
    $\mathfrak{A} \models \psi$. We say a variable assignment $\beta: \V

A set of constraints $C \subseteq \Lin$ is satisfiable, when their conjunction is
satisfiable and we write $\mathfrak{A} \models C$ instead of $\mathfrak{A}
\models \LAnd_{\psi_i \in C} \psi_i$. In addition whenever the structure is evident
from context, we write $\models \psi$ and $\beta \models \psi$ instead of
$\mathfrak{A} \models \psi$ and $(\mathfrak{A}, \beta) \models \psi$ respectively. 

A set of constraints $C \subseteq \Lin$ is satisfiable, when their conjunction
is satisfiable and we write $\mathfrak{A} \models C$ instead of $\mathfrak{A}
\models \LAnd_{\psi_i \in C} \psi_i$. In addition whenever the structure is
evident from context, we write $\models \psi$ and $\beta \models \psi$ instead
of $\mathfrak{A} \models \psi$ and $(\mathfrak{A}, \beta) \models \psi$
respectively. 

The following properties hold. Hence, conjunctions and sets of constraints can
be used interchangeably.
\begin{align}
    \llbracket \psi_1 \Land \psi_2 \rrbracket = \llbracket \psi_1 \rrbracket \intersect
    \llbracket \psi_2 \rrbracket \\

Let $\varphi_1,\varphi_2 \in \C$ and $C \subseteq \C$, the following properties
hold. Hence, conjunctions and sets of constraints can be used interchangeably.
\begin{align*}
    \llbracket \psi_1 \Land \psi_2 \rrbracket = \llbracket \psi_1 \rrbracket
    \intersect \llbracket \psi_2 \rrbracket \\

\end{align}

\end{align*}

Note that the constraints are restricted to (strict) inequality against zero. In

Note that the constraints are restricted to inequalities against zero. In

\begin{align}

\begin{align*}

\end{align}

\end{align*}

        Assume $\varphi_1$ entails $\varphi_2$. Let $\sigma \models \varphi_1$ be

        Assume $\varphi_1$ entails $\varphi_2$. Let $\beta \models \varphi_1$ be

        $\sigma \models \varphi_2$ and in turn $\sigma \not\models

        $\beta \models \varphi_2$ and in turn $\beta \not\models

researched. The theories relevant for this thesis the are quantifier-free linear
integer arithmetic (usually called \texttt{QF\_LIA}) and quantifier-free
polynomial integer arithmetic (\texttt{QF\_PIA}). 

researched. The theories relevant for this thesis the are the quantifier-free
linear integer arithmetic (usually called \texttt{QF\_LIA}) and the
quantifier-free polynomial integer arithmetic (\texttt{QF\_PIA}). 

\section{Updates}
An update assigns a value to variable after the update using the values of
variables before the update. Constraints and assignments have no notion of time,
whereas for updates there exists a \textit{before} and an \textit{after}. 
In this section we will only consider integer arithmetic, although using real
arithmetic works analogously. 
Let $\Z[\V]$ be the set of integer polynomials over variables $\V$ and $\Sigma =
\set{s : A \rightarrow \Z}{A \subseteq \V}$ be the set of integer assignments.
For an integer polynomial $f\in\Z[\V]$ and a full assignment $s \in \Sigma$ we
write $f(s)$ for the value that is found by fully evaluating the polynomial
$f[x_i\backslash{}s(x_i)]$. \todo{restrict to full assignments?}

\begin{definition}[(Non-probabilistic) polynomial update\label{def:update}]
    An update is described by an update function $u : A \rightarrow \Z[\V]$ that
    maps every updated variable to a polynomial expression over $\V$. The value
    of a variable $x\in A$ \textit{after} the update is determined by $u(x)(s)$
\end{definition}
For an update described by the update function $u : A \rightarrow \Z[\V]$ and a
full assignment $s : \V \rightarrow \Z$, we write $u(s) : A \rightarrow \Z$ for
the partial assignment found by assigning every updated variable to it's value
after the update. 
\begin{equation}
    u(s)(x) = \begin{cases} 
        u(x)(s) & \text{if } x \in A \\
        \text{undefined} & \text{otherwise}
    \end{cases}
\end{equation}
Let $\varphi \in \C$ we write $u(\varphi)$ to denote the constraint 
\begin{equation}
    u(\varphi)(s) = \LAnd_{x_i\in A} x'_i = 
\end{equation}
\begin{lemma}[Update constraints]
    Let $s \in \Sigma$. If 
\end{lemma}

\begin{definition}[Total worst-case runtime complexity \label{def:wc_rt_complexity}]
    For a \gls{pip} $\Prog$, the overall worst-case runtime complexity $\Rt_\Prog :
    \runs \rightarrow \overline{\N}$ is defined as the \textit{random variable}
    \begin{equation}
        \Rt_\Prog(\vartheta)= \sum_{g\in\GT}\Rt(g)(\vartheta)
    \end{equation}
\end{definition}
The following holds for any $\vartheta = (\_,t_0,\_)(\_,t_1,\_)\dots \in \runs$:
\begin{align}
    \Rt_P(\vartheta) &= \sum_{g\in\GT}\Rt(g)(\vartheta) & \text{by Definition
    \ref{def:wc_rt_complexity}} \\
    &= \sum_{g\in\GT} |\set{i}{t_i \in g}| & \text{by Definition \ref{def:past}}
    \\
    &= | \set{i}{t_i \in g, g\in\GT} & \text{for all } g \neq g', g\intersect{}g' = \emptyset 
\end{align}
\begin{rem}
    $t_\bot \in g_\bot \not\in \GT$, hence terminating runs have a finite
    overall runtime complexity.
\end{rem}
The worst-case total runtime complexity, for an initial state $s_0\in\Sigma$ and
all scheduler $\scheduler$, is the supremum over all admissible runs:
\begin{align}
    \sup \set{\Rt_\Prog (\vartheta)}{\vartheta \in \runs, \PrSs(\vartheta) > 0}
\end{align}
The expected total runtime complexity is the expected value of the random
variable $\ESs(\Rt_\Prog)$