%
% Acronyms
\usepackage{glossaries}

\usepackage{todonotes}

\newcommand{\V}[0]{\mathcal{V}} % Variables
\newcommand{\PV}[0]{\mathcal{V}} % Program variables
\newcommand{\F}[0]{\mathcal{F}} % Program variables
\newcommand{\Z}[0]{\mathbb{Z}} % whole numbers, integers
\newcommand{\GT}[0]{GT} % General transitions
\newcommand{\with}[0]{\text{ with }}
\newcommand{\union}[0]{\cup}
\newcommand{\Union}[0]{\bigcup}
\newcommand{\intersect}[0]{\cap}
\newcommand{\Intersect}[0]{\bigcap}

\section{Random Variables and distributions.}
Since we are talking about probabilistic programs, we will need tools to
represent probabilities throughout the program.
A variable in a probabilistic program can take a random value. That means that
the value assigned to a variable is not deterministic but chosen at random
from a given distribution. However, other uses of random variables will arise in
this thesis and we will introduce the concept of random variables in a
generalized manner. 
The field of probability and random variables is well studied. We will only
introduce the core concepts needed to understand this thesis and follow the
definitions from \cite{alma991005910089706448}. For additional information we
will refere to the literature. 
\begin{definition}[Probability space]
    A probability space is a triple $(\Omega,\F,P)$. Where the
    following holds: 
    \begin{enumerate}
        \item $\Omega$ is a non-empty set of all possible outcomes and $\omega
            \in \Omega$ denotes an arbitrary possible outcome.
        \item $\F$ is the set of events that contains $\Omega$, is
            closed under complement, intersection and countable unions. Such a
            set is also called $\sigma$-field or $\sigma$-algebra.
            \begin{enumerate}
                \item $\Omega \in \F$ 
                \item For $A\subseteq\Omega$, if $A\in\F$ then so is
                    its complement $A^c\in\F$.
                \item For $A,B \subseteq \Omega$, if $A, B \in \F$,
                    then so is $A \cup B \in \F$.
                \item For $ A_1, A_2, \dots,A_n \subseteq \Omega$, if $A_i \in
                    \F$, then so is their union $\Union\limits_{i=1}^n
                    A_i \in \F$.
            \end{enumerate}
        \item $P$ assignes a probability to every event and satisfies the
            following conditions:
            \begin{enumerate}
                \item $0 \leq P(A) \leq 1$ for $A \in \F$,
                \item $P(\emptyset) = 0$, and $P(\Omega) = 1$,
                \item $ $\todo{invariance of permutation.}
            \end{enumerate}
    \end{enumerate}
            \todo{Refere to a definition of a $\sigma$-algebra.}
\end{definition}

For random program variables in this thesis, $\Omega$ will almost certainly be
the set of integers and $\mathcal{F}$ the maximal $\sigma$-field in $\Omega$,
the powerset $2^\Omega$. Other values of $\Omega$ are possible like the set
of all runs in a program, that can also be taken as outcomes of a random
sampling.
\begin{definition}[Random variable]
    A random variable assignes a probability 
\end{definition}
A discrete bounded probability distribution gives a probability to every
possible integer and can be seen as a function $q: \Z \mapsto [0,1]$ where all 
values of $q$ add up to $1$, that is $\sum_{x\in\Z} q(x) = 1$.
Common operations can be defined over probability distributions as well, which
will be very handy in probabilistic integer programs. Given two probability
distributions $p$, and $q$, the following operations are defined:
\begin{equation*}
    p \diamond q (x) = \sum_{\substack{i,j \in \Z \\ i \diamond j = x}} p(i)
    \cdot q(i) \hspace{1cm} \with \diamond \in \{+, \cdot\}
\end{equation*}
\todo{more operators?}
In the context of this thesis the discrete bounded distributions will be used to
describe the possible values of a variable. They can be used as if they were
non-probabilistic values, for exymple and 
It can be used inside the 
A note non-probabilistic (fixed) value $k$ is equivalent to a distribution which
assignes the probability $1$ to this fixed value $k$ and $0$ to every other
value.
program itself during assignments when setting a new value to a variable or 
during analysis to describe the possible values of the variables at a certain
configuration. 
\[
    p_k(x) = \begin{cases} 
        1, & x = k \\
        0, & \text{otherwise}
    \end{cases}
\]
The resulting 

\begin{comment}
    The syntax and semantics of probabilistic programs has been extensively
    studied:
    - [Supermartingales,
    2017](https://arxiv.org/pdf/1709.04037.pdf#cite.Billingsley%3Abook)
    - [Probabilistic Koat2, 2021](https://arxiv.org/pdf/2010.06367.pdf)
\end{comment}

    \newcommand{\V}[0]{\mathcal{V}} % Variables
    \newcommand{\PV}[0]{\mathcal{V}} % Program variables
    \newcommand{\Z}[0]{\mathbb{Z}} % whole numbers, integers
    \newcommand{\GT}[0]{GT} % General transitions

                \item an update function $η : \PV \mapsto \Z[\V] \cup D$, mapping every 
                    program variable to a polynomial or a bounded distribution 
                    function. All $t \in g$ must share the same start location 
                    $l$, guard $τ$. 

                \item an update function $η : \PV \mapsto \Z[\V] \cup D$,
                    mapping every program variable to a polynomial or a bounded
                    distribution function. All $t \in g$ must share the same
                    start location $l$, guard $τ$. 

% TODO: examples
\subsection{Semantics}
A configuration is a tuple of a location and a variable assignment $(l, \sigma)$
that stands for a specific state of a running program. Given a starting 
assignment for the program variables (the input to the program), the program 
is evaluated starting from the start location $l_0$. 
An execution path of a program is a sequence of configurations, where the first
configuration is the starting configuration. Note that at this point it is 
unclear what a valid 

% TODO: examples

One can take two vies to the evaluation of 
Let's define the semantics of propabilistic integer programs. We will take two
views onto the semantics of integer programs. First the intuitive one and second
a more formal definition. 
\todo{introduce variables, assignments, constraints, polyhedron}
The curent configuration is represented as a tuple $(l_0, c_0)$. 
An execution path is a sequence of configurations. 
\subsection{Runtime}
\begin{comment}
    for a transition:
    - constant cost
    - most simple case cost = 1 for every transition
    - combining transitions and adding costs
    - costs depending on variables
    for a prefix:
    - finite sequence of configurations
    - runtime = sum of all costs over all steps in the prefix
    - probability = product over all transition probabilities in the prefix
    - legal prefix = non-zero probability
    for a path:
    - infinite sequence of configurations
    - runtime = runtime of the largest non-zero probability prefix
    - pro
    legal paths = paths with a non-zero 
    for a program:
    - supremum over runtime of all paths
\end{comment}
\begin{definition}[Runtime of a run]
\end{definition}
\begin{definition}[Worst-case runtime of a Program]
\end{definition}
\begin{definition}[Expected runtime of a Program]
\end{definition}

\cite{https://raw.githubusercontent.com/TermCOMP/TPDB/master/xml/xtc.xsd}

% \cite{https://raw.githubusercontent.com/TermCOMP/TPDB/master/xml/xtc.xsd}

\subsection{SCC}
\begin{definition}[SCC]

\end{definition}

Transform a program into an equivalent program. \todo{define equivalence of
programs}