diff --git a/README.md b/README.md index 9161167..516d8ac 100644 --- a/README.md +++ b/README.md @@ -37,9 +37,9 @@ If you find mistakes, please open an issue or fix them yourself and open a PR. - [Probability & Statistics Cheat-Sheet (DE)](./semester4/ps/ps-jh/probability-and-statistics-cheatsheet.pdf) Author: Janis Hutz - [Probability & Statistics Cheat-Sheet (TBD)](./semester4/ps/ps-rb/main.pdf) Author: Robin Bacher #### Other Courses -- [Formal Methods & Functional Programming Summary (EN)](./semester4/fmfp/formal-methods-functional-programming-summary.pdf) -- [Data Modelling & Databases Summary (EN)](./semester4/dmdb/data-modelling-databases-summary.pdf) -- [Computer Networks (EN)](./semester4/cn/computer-networks-summary.pdf) +- [Formal Methods & Functional Programming Summary (EN)](./semester4/fmfp/formal-methods-functional-programming-summary.pdf) Author: Janis Hutz +- [Data Modelling & Databases Summary (EN)](./semester4/dmdb/data-modelling-databases-summary.pdf) Author: Janis Hutz +- [Computer Networks (EN)](./semester4/cn/computer-networks-summary.pdf) Author: Not started yet ### Semester 6 #### Introduction to Machine Learning diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.pdf b/semester4/fmfp/formal-methods-functional-programming-summary.pdf index 70f51cf..0c714d2 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/formal-methods-functional-programming-summary.tex b/semester4/fmfp/formal-methods-functional-programming-summary.tex index ed58314..bda8be2 100644 --- a/semester4/fmfp/formal-methods-functional-programming-summary.tex +++ b/semester4/fmfp/formal-methods-functional-programming-summary.tex @@ -87,6 +87,17 @@ % \input{parts/02_typing/03_interpreter/} +\newsection +\section{Language Semantics} +\input{parts/03_language-semantics/00_imp/00_syntax.tex} +\input{parts/03_language-semantics/00_imp/01_semantics.tex} +\input{parts/03_language-semantics/00_imp/02_properties.tex} +\input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/00_transition-systems.tex} +\input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/01_semantics.tex} +% \input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/} +% \input{parts/03_language-semantics/01_operational-semantics/} +% \input{parts/03_language-semantics/} + \end{document} diff --git a/semester4/fmfp/parts/03_language-semantics/00_imp/00_syntax.tex b/semester4/fmfp/parts/03_language-semantics/00_imp/00_syntax.tex new file mode 100644 index 0000000..b52b7e6 --- /dev/null +++ b/semester4/fmfp/parts/03_language-semantics/00_imp/00_syntax.tex @@ -0,0 +1,37 @@ +\subsection{IMP Language} +\subsubsection{The syntax} +The allowed characters: +\begin{code}{haskell} + Letter = 'A' | . . . | 'Z' | 'a' | . . . | 'z' + Digit = '0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' +\end{code} + +And the allowed tokens: +\begin{code}{haskell} + Ident = Letter { Letter | Digit }* + Numeral = Digit | Numeral Digit + Var = Ident +\end{code} + +Arithmetic and Boolean statements could be defined in Haskell as follows +\begin{code}{haskell} + data Aexp = Bin Op Aexp Aexp | Var String | Num Integer + data Op = Add | Sub | Mul + data Bexp = Or Bexp Bexp | And Bexp Bexp | Not Bexp | Rel Rop Aexp Aexp + data Rop = Eq | Neq | Le | Leq | Ge | Geq +\end{code} + +Statements could be defined in Haskell as follows +\mint{haskell}+data Stm = Skip | Assign String Aexp | Seq Stm Stm | If Bexp Stm Stm | While Bexp Stm+ + +We use the following naming conventions for meta-variables: +\begin{tables}{ll}{Variable & Type} + $n$ & for numerals (\texttt{Numeral}) \\ + $x, y, z$ & for variables (\texttt{Var}) \\ + $e, e', e_1, e_2$ & for arithmetic expressions (\texttt{Aexp}) \\ + $b, b_1, b_2$ & for boolean expressions (\texttt{Bexp}) \\ + $s, s', s_1, s_2$ & for Statements (\texttt{Stm}) \\ +\end{tables} +Meta-variables stand for arbitrary program variables, whereas program variables are concrete variables in a program. + +To denote \bi{syntactic equality} of two variables or statements, we use $\equiv$ diff --git a/semester4/fmfp/parts/03_language-semantics/00_imp/01_semantics.tex b/semester4/fmfp/parts/03_language-semantics/00_imp/01_semantics.tex new file mode 100644 index 0000000..4bd2938 --- /dev/null +++ b/semester4/fmfp/parts/03_language-semantics/00_imp/01_semantics.tex @@ -0,0 +1,58 @@ +\subsubsection{The semantics} +\paragraph{Numerals} +The semantic function $\cN : \texttt{Numeral} \rightarrow \texttt{Val}$ maps a numeral $n$ to an integer value $\cN\llbracket n \rrbracket$, +with $x \in \{ 0, \ldots, 9 \}$: +\begin{align*} + \cN\llbracket x \rrbracket = x & & \cN\llbracket n x \rrbracket = \cN\llbracket n \rrbracket \cdot 10 + x +\end{align*} + + +\paragraph{States} +A state assigns a value to each program variable. It is a total function and is typically denoted by the meta-variable $\sigma$ +\[ + \sigma : \texttt{Var} \rightarrow \texttt{Val} +\] +To update states, we use the notation $\sigma[y \mapsto v]$, which is given by +\[ + (\sigma[y \mapsto v])(x) = \begin{cases} + v & \text{if } x \equiv y \\ + \sigma(x) & \text{if } x \not\equiv y + \end{cases} +\] +Two states $\sigma_1, \sigma_2 $ are equal if they are equal as functions: $\sigma_1 = \sigma_2 \Leftrightarrow \forall x. (\sigma_1(x) = \sigma_2(x))$ + + +\paragraph{Arithmetic Expressions} +$\cA : \texttt{Aexp} \rightarrow \texttt{State} \rightarrow \texttt{Val}$ maps an arithmetic expression $e$ and a state $\sigma$ to a value $\cA\llbracket e \rrbracket \sigma$, +given by: +\begin{align*} + \cA\llbracket x \rrbracket \sigma & = \sigma(x) \\ + \cA\llbracket n \rrbracket \sigma & = \cN\llbracket x \rrbracket \\ + \cA\llbracket e_1 \; \texttt{op} \; e_2 \rrbracket \sigma & = \cA\llbracket e_1 \rrbracket \sigma \; \overline{\texttt{op}} \; \cA\llbracket e_2 \rrbracket \sigma +\end{align*} +For $\texttt{op} \in \texttt{Op}$, $\overline{\texttt{op}}$ is the corresponding operation $\texttt{Val} \times \texttt{Val} \rightarrow \texttt{Val}$ + + +\paragraph{Boolean Expressions} +$\cB : \texttt{Bexp} \rightarrow \texttt{State} \rightarrow \texttt{Bool}$ maps boolean expression $b$ and a state $\sigma$ to a truth value $\cB\llbracket b \rrbracket \sigma$, +given by: +\[ + \cB\llbracket e_1 \; \texttt{op} \; e_2 \rrbracket \sigma = \begin{cases} + \texttt{tt} & \text{if } \cA\llbracket e_1 \rrbracket \sigma \; \overline{\texttt{op}} \; \cA\llbracket e_2 \rrbracket \sigma \\ + \texttt{ff} & \text{otherwise} + \end{cases} +\] +Thus, for the \texttt{op} \texttt{or}, we would have (analogous for \texttt{and}) +\[ + \cB\llbracket b_1 \; \texttt{or} \; b_2 \rrbracket \sigma = \begin{cases} + \texttt{tt} & \text{if } \cA\llbracket b_1 \rrbracket \sigma = \texttt{tt} \; \texttt{or} \; \cA\llbracket b_2 \rrbracket \sigma = \texttt{tt} \\ + \texttt{ff} & \text{otherwise} + \end{cases} +\] +\texttt{not} is defined as follows: +\[ + \cB\llbracket \texttt{not}\; b \rrbracket \sigma = \begin{cases} + \texttt{tt} & \text{if } \cA\llbracket b \rrbracket \sigma = \texttt{ff} \\ + \texttt{ff} & \text{otherwise} + \end{cases} +\] diff --git a/semester4/fmfp/parts/03_language-semantics/00_imp/02_properties.tex b/semester4/fmfp/parts/03_language-semantics/00_imp/02_properties.tex new file mode 100644 index 0000000..cf1f2f2 --- /dev/null +++ b/semester4/fmfp/parts/03_language-semantics/00_imp/02_properties.tex @@ -0,0 +1,81 @@ +\subsubsection{Properties of expression semantics} +Since we have recursive definitions for the semantics and syntax, we can use structural induction. + +\begin{recall}[]{Structural Induction} + For the data structure \texttt{Nat}, given by + \mint{haskell}+data Nat = Zero | Succ Nat+ + the structural induction derivation rule is given by + \[ + \begin{prooftree} + \hypo{\Gamma \vdash P(\texttt{Zero})} + \hypo{\Gamma, P(m) \vdash P(\texttt{Succ}\; m)} + \infer2[$m$ not free in $\Gamma$]{\Gamma \vdash \forall n \in \texttt{Nat}. P(n)} + \end{prooftree} + \] + Where we now write $P(m)$ instead of $P[n \mapsto m]$ and the second premise needs to be proven for all $m$ +\end{recall} + + +\paragraph{Inductive Definitions} +If we are to introduce a new arithmetic expression $-e$, we could do this in two ways. +For one, we could define $\cA\llbracket -e \rrbracket \sigma = 0 - \cA\llbracket e \rrbracket \sigma$. This \textit{is} an inductive definition because $e$ is a subterm of $-e$. + +If on the other hand we define $\cA\llbracket -e \rrbracket \sigma = \cA\llbracket 0 - e \rrbracket \sigma$, +it is \textit{not} an inductive definition because $0 - e$ is \textit{not} a subterm of $-e$ + + +\newpage +\paragraph{Free Variables} +For Arithmetic Expressions +\begin{align*} + FV(e_1 \; \texttt{op} \; e_2) & = FV(e_1) \cup FV(e_2) \\ + FV(n) & = \varnothing \\ + FV(x) & = \{ x \} +\end{align*} + +For Boolean Expressions +\begin{align*} + FV(b_1 \; \texttt{op} \; b_2) & = FV(b_1) \cup FV(b_2) \\ + FV(\texttt{not} b) & = FV(b) \\ + FV(b_1 \; \texttt{or} \; b_2) & = FV(b_1) \cup FV(b_2) \\ + FV(b_1 \; \texttt{and} \; b_2) & = FV(b_1) \cup FV(b_2) +\end{align*} + +And finally for Statements: +\begin{align*} + FV(\texttt{skip}) & = \varnothing \\ + FV(x := e) & = \{ x \} \cup FV(s_2) \\ + FV(s_1; s_2) & = FV(s_1) \cup FV(s_2) \\ + FV(\texttt{if}\; b\; \texttt{then} \; s_1 \; \texttt{else} \; s_2 \; \texttt{end}) & = FV(b) \cup FV(s_1) \cup FV(s_2) \\ + FV(\texttt{while}\; b\; \texttt{do} \; s \; \texttt{end}) & = FV(b) \cup FV(s) +\end{align*} + + +\paragraph{Substitution} +{\scriptsize We have already seen this kind of expression in the states, with this explanation it should make a lot more sense intuitively.} + +A substitution $f[x \mapsto e]$ replaces each free occurrence of variable $x$ in $f$ by $e$, where $f$ is any expression. + +Detailed rules for arithmetic expressions: +\begin{align*} + (e_1 \; \texttt{op} \; e_2)[x \mapsto e] & \equiv (e_1[x \mapsto e] \; \texttt{op} \; e_2[x \mapsto e]) \\ + n[x \mapsto e] & \equiv n \\ + y[x \mapsto e] & \equiv \begin{cases} + e & \text{if } x \equiv y \\ + y & \text{otherwise} + \end{cases} +\end{align*} + +The same for boolean expressions: +\begin{align*} + (e_1 \; \texttt{op} \; e_2)[x \mapsto e] & \equiv (e_1[x \mapsto e] \; \texttt{op} \; e_2[x \mapsto e]) \\ + (\texttt{not} \; b)[x \mapsto e] & \equiv \texttt{not} \; (b[x \mapsto e]) \\ + (b_1 \; \texttt{or} \; b_2)[x \mapsto e] & \equiv (b_1[x \mapsto e] \; \texttt{or} \; b_2[x \mapsto e]) \\ + (b_1 \; \texttt{and} \; b_2)[x \mapsto e] & \equiv (b_1[x \mapsto e] \; \texttt{and} \; b_2[x \mapsto e]) +\end{align*} + +\begin{lemma}[]{Substitution Lemma} + \[ + \cB\llbracket b[x \mapsto e] \rrbracket \Leftrightarrow \cB\llbracket b \rrbracket (\sigma[x \mapsto \cA\llbracket e \rrbracket \sigma]) + \] +\end{lemma} diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/00_transition-systems.tex b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/00_transition-systems.tex new file mode 100644 index 0000000..daf15e2 --- /dev/null +++ b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/00_transition-systems.tex @@ -0,0 +1,20 @@ +\newpage +\subsection{Operational Semantics} +\subsubsection{Transition Systems} +\inlinedefinition[Transition System] is a tuple $(\Gamma, T, \rightarrow)$, where $\Gamma$ is a set of \bi{configurations}, +$T$ is a set of terminal configurations, with $T \subseteq \Gamma$ and $\rightarrow$ is a transition relation, with $\rightarrow \; \subseteq \Gamma \times \Gamma$, +which describes how executions take place. Big-step transitions are of form $\langle s, \sigma \rangle \rightarrow \sigma'$, +e.g. $\langle \texttt{skip}, \sigma \rangle \rightarrow \sigma$ + +The transition relations are specified as rules of the form ($^*$ optional side-condition, $\varphi_i$ and $\psi$ transitions) +\[ + \begin{prooftree} + \hypo{\varphi_1} + \hypo{\dots} + \hypo{\varphi_n} + \infer3[(Name)$^*$]{\psi} + \end{prooftree} +\] +or spelled out, ``If $\varpi_1, \ldots, \varphi_n$ are transitions (and the \textit{side-condition} is true), then $\psi$ is a transition''. + +Herein, $\varphi_1, \ldots, \varphi_n$ are called \bi{premises} of the rule and $\psi$ is the \bi{conclusion}. A rule without premises is an \bi{axiom rule}. diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/01_semantics.tex b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/01_semantics.tex new file mode 100644 index 0000000..a331f1a --- /dev/null +++ b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/01_semantics.tex @@ -0,0 +1,54 @@ +\subsubsection{Big-Step Semantics of IMP} +\[ + \begin{prooftree} + \infer0[\textsc{Skip}$_{NS}$]{\langle \texttt{skip}, \sigma \rangle \rightarrow \sigma} + \end{prooftree} + \qquad + \begin{prooftree} + \infer0[\textsc{Ass}$_{NS}$]{\langle x := e, \sigma \rangle \rightarrow \sigma[x \mapsto \cA\llbracket e \rrbracket \sigma ]} + \end{prooftree} +\] + +\shade{gray}{Sequential Composition} $s;s'$ ($s$ is executed in state $\sigma$, then $s'$ in resulting $\sigma'$, resulting in $\sigma''$) +\[ + \begin{prooftree} + \hypo{\langle s, \sigma \rangle \rightarrow \sigma'} + \hypo{\langle s', \sigma' \rangle \rightarrow \sigma''} + \infer2[\textsc{Seq}$_{NS}$]{\langle s;s', \sigma \rangle \rightarrow \sigma''} + \end{prooftree} +\] + +\shade{gray}{Conditional Statements} $\texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}$ (If $b$ holds, execute $s$, otherwise execute $s'$) +\[ + \begin{prooftree} + \hypo{\langle s, \sigma \rangle \rightarrow \sigma'} + \infer1[\textsc{IfT}$_{NS}$]{\langle \texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow \sigma'} + \end{prooftree} + \qquad + \begin{prooftree} + \hypo{\langle s, \sigma \rangle \rightarrow \sigma'} + \infer1[\textsc{IfF}$_{NS}$]{\langle \texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow \sigma'} + \end{prooftree} +\] +Where the first rule applies if $\cB\llbracket b \rrbracket \sigma = \texttt{tt}$ + +\shade{gray}{Loop statements} $\texttt{while} \; b \; \texttt{do} \; s \; \texttt{end}$ (If $b$ holds, execute $s$ once, whole statement executed in resulting state $\sigma$) +\[ + \begin{prooftree} + \hypo{\langle s, \sigma \rangle \rightarrow \sigma'} + \hypo{\langle \texttt{while} \; b \; \texttt{do} \; s \; \texttt{end}, \sigma' \rangle \rightarrow \sigma''} + \infer2[\textsc{WhT}$_{NS}$]{\langle \texttt{while} \; b \; \texttt{do} \; s \; \texttt{end}, \sigma \rangle \rightarrow \sigma''} + \end{prooftree} + \qquad + \text{if } + \cB\llbracket b \rrbracket \sigma = \texttt{tt} +\] +If $b$ does not hold, the while statement does \textit{not} modify the state +\[ + \begin{prooftree} + \infer0[\textsc{WhF}$_{NS}$]{\langle \texttt{while} \; b \; \texttt{do} \; s \; \texttt{end}, \sigma \rangle \rightarrow \sigma} + \end{prooftree} + \qquad + \text{if } + \cB\llbracket b \rrbracket \sigma = \texttt{ff} +\] diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/02_equiv.tex b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/02_equiv.tex new file mode 100644 index 0000000..e69de29