[FMFP] Exam notes for FP almost complete

semester4/fmfp/parts/01_induction-proofs/00_intro.tex

@@ -1,6 +1,7 @@
 To prove recursive formulas, or more precisely formulated, a formula $P$ (with free variable $n$) for all $n \in \N$,
-we have can use weak or strong induction.
-Weak induction may be a \textit{slightly} misleading term, because it isn't necessarily weaker than strong induction.
+we can use weak or strong induction.
+Weak induction may be a \textit{slightly} misleading term, because it isn't necessarily weaker than strong induction,
+for mathematical induction, for structural induction, there is a difference.
 
 This section has been moved to the very start of the theory part, even though many of the topics mentioned have not been covered in the summary yet,
 such that all the induction proofs can be covered in the same place.

semester4/fmfp/parts/01_induction-proofs/02_structural-induction.tex

@@ -1,7 +1,7 @@
 \subsection{Structural Induction}
 In this subsection, we present structural induction over lists.
 The same concept also applies similarly to trees and more.
-Weak Structural Induction on treees is presented in the subsequent subsection.
+Weak Structural Induction on trees is presented in the subsequent subsection.
 
 For both, we only provide the natural deduction rules, as the proofs proceed analogously to the ones for mathematical induction.
 
@@ -25,3 +25,8 @@ For both, we only provide the natural deduction rules, as the proofs proceed ana
         \infer1[$xs$ not free in $\Gamma$, $ys$ not free in $P(xs)$]{\Gamma \vdash \forall xs . P(xs)}
     \end{prooftree}
 \end{align*}
+
+
+\subsubsection{Generalizing expressions}
+Sometimes, an expression can be hard to proof straight away because there is a constant in it.
+In that case, replace that constant, making sure to update both sides of the expression to reflect the change.

semester4/fmfp/parts/01_induction-proofs/05_workflow.tex

@@ -0,0 +1,12 @@
+\subsection{Workflow}
+{\scriptsize the notes in this section may seem a bit over the top,
+    but in the exercise sessions it was mentioned repeatedly that they will heavily deduct points for not following the scheme.
+    One example that was named is that in some exams out of 36 points for a proof, 9 were awarded for simply following the expected structure}
+\begin{enumerate}
+    \item Determine the exact expression to proof (possibly generalizing it, and if so, state something like ``Consider the generalized statement'')
+    \item Then, start the proof by stating something along the lines of ``We prove $\forall n \in \N P$ by weak mathematical induction on $n$''.
+    \item Depending on the proof type, proceed with base cases, or case analysis. \hl{Important}: State ``Let $m$ be arbitrary'' for free variables,
+          and if there are extra variables introduced by the application (e.g. a \texttt{Leaf} type has value $x$ in it), state ``Fix $x$ and we show $P[t \mapsto \texttt{Leaf} x]$''
+    \item Then, do the step case (if applicable). \hl{Important}: State ``Let $n$ be arbitrary'', or in the case of structural induction, there may be arguments for the type,
+          such as for \texttt{Tree}, then state ``Let \texttt{l::Tree} and \texttt{r::Tree} be arbitrary''.
+\end{enumerate}

semester4/fmfp/parts/03_typing/01_mini-haskell/00_syntax.tex

@@ -1,4 +1,5 @@
 \subsection{Mini-Haskell}
+\label{sec:mini-haskell}
 This is a stripped down version of Haskell, used here to explore the type system Haskell uses
 
 \subsubsection{Syntax}

semester4/fmfp/parts/06_exercises/01_fp/03_type-inference.tex

@@ -1,4 +1,13 @@
 \subsubsection{Type Inference}
+\begin{examdetails}
+    There typically is one such task. They provide the inference rules
+\end{examdetails}
+The proof trees are again drawn up bottom up, applying rules from the outside in.
 \begin{enumerate}
-    \item 
+    \item Create a proof tree using the typing rules.
+    \item During the proof, keep track of what the applications of rules tell us about types in a list.
+    \item After reaching leafs in the prooftree, resolve the types by inserting the now known types into the types you kept in the list.
 \end{enumerate}
+Remember that not all expressions are typeable, so if you end up getting an invalid tree or a conflict of types, this is very much possible.
+
+To prove that the type of an expression is correct, we can simply draw up a type derivation tree, using the typing rules from Section~\ref{sec:mini-haskell}.

semester4/fmfp/parts/06_exercises/02_fm/00_imp.tex

@@ -0,0 +1 @@
+\subsubsection{IMP}

semester4/fmfp/parts/06_exercises/02_fm/01_operational-semantics.tex

@@ -0,0 +1,5 @@
+\subsubsection{Operational Semantics}
+\paragraph{Big Step Semantics}
+
+
+\paragraph{Small Step Semantics}

semester4/fmfp/parts/06_exercises/02_fm/02_axiomatic-semantics.tex

@@ -0,0 +1 @@
+\subsubsection{Axiomatic Semantics}

semester4/fmfp/parts/06_exercises/02_fm/03_modelling.tex

@@ -0,0 +1 @@
+\subsubsection{Modelling}

semester4/fmfp/parts/06_exercises/02_fm/04_ltl.tex

@@ -0,0 +1 @@
+\subsubsection{Linear Time Properties (LTL)}