diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.pdf b/semester4/fmfp/formal-methods-functional-programming-summary.pdf index 9cbfe37..cc1106e 100644 Binary files a/semester4/fmfp/formal-methods-functional-programming-summary.pdf and b/semester4/fmfp/formal-methods-functional-programming-summary.pdf differ diff --git a/semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/00_syntax.tex b/semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/00_syntax.tex index 63f0b4b..d201b36 100644 --- a/semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/00_syntax.tex +++ b/semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/00_syntax.tex @@ -7,7 +7,7 @@ We write $f^k$ (or $p^k$, for predicates) to indicate that it has \textit{arity} Constant functions have arity $0$, linear functions have arity $1$, thus, the arity of a given function (or predicate) is given by the number of parameters to uniquely describe it, minus one. -\inlinedefinition[Term] is the terms of first-order logic is smallest set, where (with $\cV$ again a set of variables) +\inlinedefinition[Term] is the terms of first-order logic and is the smallest set, where (with $\cV$ again a set of variables) \begin{enumerate} \item $x \in \textit{Term}$ if $x \in \cV$ \item $f^n(t_1, \ldots, t_n) \in \textit{Term}$ if $f^n \in \cF$ and $t_i \in \textit{Term}$, $\forall 1 \leq i \leq n$ (description of form of formulas) diff --git a/semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/01_semantics.tex b/semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/01_semantics.tex index b9c63c5..dd41fd9 100644 --- a/semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/01_semantics.tex +++ b/semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/01_semantics.tex @@ -1,5 +1,5 @@ \subsubsection{Semantics} -\inlinedefinition[Structure] is a pair $\cS = \langle U_\cS, I_\cS \rangle$, where $U_\cS$ is the universe and it is a non-empty set and $I_\cS$ is a mapping with +\inlinedefinition[Structure] is a pair $\cS = \langle U_\cS, I_\cS \rangle$, where $U_\cS$ is the universe (non-empty set) and $I_\cS$ is a mapping: \begin{enumerate} \item $I_\cS(p^n)$ is an $n$-ary relation on $U_\cS$ for $p^n \in \cP$ (short $p^\cS$) \item $I_\cS(f^n)$ is an $n$-ary (total) function on $U_\cS$ for $f^n \in \cF$ short ($f^\cS$) diff --git a/semester4/fmfp/parts/01_formal-reasoning/05_correctness/03_induction.tex b/semester4/fmfp/parts/01_formal-reasoning/05_correctness/03_induction.tex index 04f8e0e..f6b79dd 100644 --- a/semester4/fmfp/parts/01_formal-reasoning/05_correctness/03_induction.tex +++ b/semester4/fmfp/parts/01_formal-reasoning/05_correctness/03_induction.tex @@ -9,7 +9,7 @@ To prove $\forall n \in \N. P$ (with $n$ free in $P$), we do the following: \shade{blue}{Base case} We show that $P[n \mapsto 0]$ is correct -\shade{green}{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]$ +\shade{green}{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]$ is correct. 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. diff --git a/semester4/fmfp/parts/02_typing/01_mini-haskell/01_lambda-calculus.tex b/semester4/fmfp/parts/02_typing/01_mini-haskell/01_lambda-calculus.tex index 928dd44..d8d4ce6 100644 --- a/semester4/fmfp/parts/02_typing/01_mini-haskell/01_lambda-calculus.tex +++ b/semester4/fmfp/parts/02_typing/01_mini-haskell/01_lambda-calculus.tex @@ -1,6 +1,6 @@ \subsubsection{Lambda calculus} To prove that types are correct, the lambda calculus comes in handy. -It is based on the same concept as natural deduction trees +The proofs are again structured as derivation trees. \paragraph{Core rules for Lambda-Calculus} \[ diff --git a/semester4/fmfp/parts/02_typing/01_mini-haskell/03_type-inference.tex b/semester4/fmfp/parts/02_typing/01_mini-haskell/03_type-inference.tex index 337b5e4..4a2c489 100644 --- a/semester4/fmfp/parts/02_typing/01_mini-haskell/03_type-inference.tex +++ b/semester4/fmfp/parts/02_typing/01_mini-haskell/03_type-inference.tex @@ -7,7 +7,7 @@ Finally, apply constraints / unification to get possible types. \paragraph{Self application} This means that you apply a function to itself. -In Haskell, this is not typeable because there would need to be an infinite function type, but all \bi{Haskell types are finite} +In Haskell, this is not typeable because there would need to be an infinite function type, but all \bi{Haskell types are finite} \paragraph{Curry-Howard isomorphism}