\section{Preliminaries} 

\newcommand{\PV}[0]{\mathcal{V}} % Program variables

\newcommand{\PV}[0]{\mathcal{PV}} % Program variables
\newcommand{\TV}[0]{\mathcal{TV}} % Program variables
\newcommand{\C}[0]{\mathcal{C}} % Set of Constraints

\subsection{Constraints, Polyhedra, Projections}
Koat2 can work on integer programs with polynomial integer
arithmetic.\cite{Brockschmidt16} To represent states and invariants in such a
program, one needs polynomial constraints. As an extended concept Koat uses
Boxes and we will use Polyhedra for the partial evaluation. Since those concepts
are closely related we will introduce them together. 
Let $\PV$ be a set of program variables and $\TV$ be a set of temporary
variables. Together they form the set of variables $\V := \PV \union \TV$. 
Let $(\N, +, \cdot, 0, 1, <)$ be the structure of 
The set of constraints $\C$ is defined as the minimal as $\{c = e < 0 | e \in
\Z[\V]\}$. That is the set of all constraints over integer polynomials less than
zero.

\begin{definition}[Linear Constraints] 
    Let $V$ be a fixed set of integer
    Variables $\{x_1, x_2, \dots, n\} $. A linear constraint is defined as $\psi
    = a_0 + a_1 x_1 + \dots + a_n x_n \diamond 0$ where $a_i \in \mathbb{N}$ are
    integer coefficients, $x_i \in V$ are variables and $\diamond \in \{>, <, 
    \geq, \leq, =\}$. \end{definition}

Note that all constraint $e_1 \diamond e_2$ with the operators $\diamond
\in >, <, \leq, \geq$ can be transformed into an equivalent constraint $e' < 0
\in \C$:
\begin{align*}
    e_1 \geq e_2 &\equiv e_2 - e_1 - 1 < 0 \\
    e_1 \leq e_2 &\equiv e_1 - e_2 < 0
\end{align*}
and so on. Koat2 internaly represents all constraints in the simplified form, 
and one can assume that all constraints are given in the simplified form. 
However, for better readability we will use the general form in the examples. 
Given a variable assignment $\sigma: \PV \mapsto \Z$ for the program variables
we say $\sigma$ satisfies the constraint $c \in \C$ when the constraint holds
with every variable $v \in \V$ being replaced by it's assigned value $\sigma(v)$
or more formally:
and we say a constraint is satisfiable if there exists a variable assignment
that satisfies the constraint. 
For a set of constraints $C \subset \C$ we say that it is satisfied by the
assignment, if and only if the assignmnet satisfies every constraint contained
in the set. 

\begin{definition}[Assignment] 
    An assignment $\sigma : V \mapsto \mathbb{Z}$ assigns an integer value to
    each variable in $V$. $\sigma$ is a solution for a linear constraint $\psi$
\end{definition} \

\todo{existentially quantify variables}

\section{Random Variables and distributions.}
Since we are talking about probabilistic programs, we will need tools to
represent probabilities throughout the program.

- struktur = universum + signatur + interpretation der signatur
in unserem fall:
  - universum = integer
  - signatur = (+, *, 0, 1, <)
  - interpretation wie erwartet

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. 

wir arbeiten auf quantoren freie 
wir definieren constraints 
wir erlauben ausschließlich FO(\tau) formeln der form von constraints
- $FO(\tau)$ formeln
- Atom $
- constraints als quantoren freie Formeln auffassen.
- existentieller abschluss: existentielle quantifizierung aller Variablesn
Notation: $\models$
Finding a variable assignment
\subsection{Probability}
Since we are talking about probabilistic programs, we will need tools to
represent probabilities throughout the program. For example 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. 

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}[Measure]
    A set function $\mu$ on a $\sigma$-field $\F$ in $\Omega$ is a probability
    measure if it satisfies the following conditions:
    \begin{enumerate}
        \item $\mu(A)\in [0,1]$ for $A \in \F$
        \item $\mu(\emptyset) = 0$
        \item if $A_1, A_2, ...$ is a disjoint sequence of $\F$-sets then 
            \begin{equation*}
                \mu\left(\Union_{k=1}^\infty A_k \right) = \sum_{k=1}^\infty
                \mu(A_k)
            \end{equation*}
        \item $\mu(\Omega) = 1$
    \end{enumerate}
\end{definition}
\cite{alma991005910089706448}
For random program variables in this thesis, $\Omega$ will be the set of
integers and $\mathcal{F}$ the maximal $\sigma$-field in $\Omega$, the powerset
$2^\Omega$. However since the program variables are chosen at random, a
specific path over a given program can also be considered a random event in the
probability space and hence be considered as a ransom variable. In this case
$\Omega$ is the set of all runs $\mathcal{Runs}$. The exact definition will be
introduced later on in \Sref{}.
The general concept of random variables is not to be confused with program
variables (that can take random values). Random variables assign a probability
to an event of a probability space. 

    A random variable assignes a probability 

    A random variable on a probability space $(\Omega, \F, \P)$ is a 

\begin{definition}[Linear Constraints] 
    Let $V$ be a fixed set of integer
    Variables $\{x_1, x_2, \dots, n\} $. A linear constraint is defined as $\psi
    = a_0 + a_1 x_1 + \dots + a_n x_n \diamond 0$ where $a_i \in \mathbb{N}$ are
    integer coefficients, $x_i \in V$ are variables and $\diamond \in \{>, <, 
    \geq, \leq, =\}$. \end{definition}
\begin{definition}[Assignment] 
    An assignment $\sigma : V \mapsto \mathbb{Z}$ assigns an integer value to
    each variable in $V$. $\sigma$ is a solution for a linear constraint $\psi$
\end{definition} \