[FMFP] Correctness

semester4/fmfp/parts/01_formal-reasoning/05_correctness/00_intro.tex

@@ -0,0 +1,4 @@
+\newsection
+\subsection{Correctness}
+For many programs, termination is an important aspect when talking about correctness,
+as is, of course, that the return value is ``correct''.

semester4/fmfp/parts/01_formal-reasoning/05_correctness/01_termination.tex

@@ -0,0 +1,15 @@
+\subsubsection{Termination}
+\inlinetheorem For a function $f$ is defined in terms of other functions $g_1, \ldots, g_k$, for all of which we have $g_i \neq f$ and each $g_i$ terminates, then so does $f$.
+
+\inlinelemma Sufficient condition for termination: The arguments are smaller along a \bi{well-founded} order on the function's domain
+
+\inlinedefinition[Well-Founded Order] An order $>$ on a set $S$ is \bi{well-founded} if and only if there is no infinite decreasing chain $x_1 > x_2 > \ldots$ for $x_i \in S$ 
+An example of such an order is $>$ on $\N$, denoted $>_\N$. Counter example: $>_\Z$ (not bounded from below)
+
+
+\inlinelemma Let $R \subseteq S \times S$ be a relation on $S$. Let $s_0, s_i \in S$ and $i \geq 1$.
+Then $s_0 \; R^i \; s_i$ if and only if $s_1, \ldots s_{i - 1} \in S$ such that $s_0 \; R \; s_1 \R \ldots R \; s_{i - 1} \; R \; s_i$
+
+\inlinedefinition $R^+ \equiv \bigcup_{n \geq 1} R^n$, where $R^n \equiv R \circ R^{n - 1}$ for $n \geq 2$ and $R^1 \equiv R$
+
+\inlinetheorem If $>$ is a well-founded order on $S$, then $>^+$ is also well-founded on $S$

semester4/fmfp/parts/01_formal-reasoning/05_correctness/02_behaviour.tex

@@ -0,0 +1,44 @@
+\subsubsection{Correctness - Behaviour}
+We denote that two functions \texttt{fac} and \texttt{fac2} compute the same function usually as
+\[
+    \forall n \in \N. \texttt{fac } n = \texttt{fac2 } (n, 1)
+\]
+The two functions are given as follows:
+\begin{multicols}{2}
+    \begin{code}{haskell}
+        fac :: Int -> Int
+        fac 0 = 1
+        fac n = n * fac (n - 1)
+    \end{code}
+    \begin{code}{haskell}
+        fac2 :: (Int, Int) -> Int
+        fac2 (0, a) = a
+        fac2 (n, a) = fac2 (n - 1, n * a)
+    \end{code}
+\end{multicols}
+An important fact to consider is that testing, while useful to find errors can't replace a formal proof to show that a function is correct!
+
+These proofs are based on a simple idea: \bi{functions are equations} and thus, we can reason about them through equational reasoning, or more generally,
+proofs in first-order logic with equality.
+
+Often, especially in Haskell programs, we have cases depending on values. Logically, to prove such a function, we also use case distinction, also referred to as reasoning by cases.
+
+\inlineexample Consider the Haskell function below \rmvspace
+\begin{code}{haskell}
+    maxi :: Int -> Int -> Int
+    maxi n m
+        | n >= m    = n
+        | otherwise = m
+\end{code}
+To prove that it is correct, we can use reasoning by cases:
+
+We have $n \geq m \lor \neg(n \geq m)$.
+
+We then show that the function is correct for both cases (i.e. LHS and RHS of OR):
+\begin{enumerate}[label=C\arabic*]
+    \item $n \geq m$: Then $\texttt{maxi } n \ m = n$ and $n \geq n$
+    \item $\neg(n \geq m)$: Then $\texttt{maxi } n \ m = m$. But $m > n$, so we have $\texttt{maxi } n\ m \geq n$
+\end{enumerate}
+In this proof we used the \textbf{TND} and \textbf{$\lor$-E} (here also called \bi{Case Split}) rules.
+
+So what we have to show, given $Q \lor R$ for any proposition $P$ with case split is that \bi{(1)} $P$ follows from $Q$ and \bi{(2)} $P$ follows from $R$

semester4/fmfp/parts/01_formal-reasoning/05_correctness/03_induction.tex

@@ -0,0 +1,15 @@
+\subsubsection{Induction}
+To prove recursive formulas, or more precisely formulated, a formula $P$ (with free variable $n$) for all $n \in \N$.
+
+A proof by cases is not possible, as there are infinitely many cases (one for each input).
+Thus: We can use induction to prove recursive formulas or functions.
+
+\paragraph{The schema}
+To prove $\forall n \in \N. P$ (with $n$ free in $P$), we do the following:
+
+\bi{Base case}: We show that $P[n \mapsto 0]$ is correct
+
+\bi{Step case}: For an arbitrary $m$ not free in $P$, we show that $P[n \mapsto m + 1]$ is correct under the assumption that $P[n \mapsto m]$
+
+For \bi{well-founded} domains, we have to adjust the induction hypothesis slightly: We assume $\forall l \in \N. l < m \rightarrow P[n \mapsto l]$
+and then prove $P[n \mapsto m]$ under our assumption.