diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.pdf b/semester4/fmfp/formal-methods-functional-programming-summary.pdf index 0c714d2..9a0f62f 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 bda8be2..908fb68 100644 --- a/semester4/fmfp/formal-methods-functional-programming-summary.tex +++ b/semester4/fmfp/formal-methods-functional-programming-summary.tex @@ -4,10 +4,24 @@ \usepackage{lmodern} \usepackage{ebproof} +\usepackage{overarrows} + +\NewOverArrowCommand{\overrightharpoon}{% + end=\rightharpoonup +} \ebproofset{separation=2.5em} \setFontType{sans} \multicolsep 5pt plus 2pt minus 2pt +\setcounter{secnumdepth}{5} +\makeatletter +\renewcommand\subparagraph{% + \@startsection{subparagraph}{5}{0mm}% + {-.5\baselineskip}% + {.25\baselineskip}% + {\normalfont\normalsize\bfseries}} +\makeatother + \setup{Formal Methods \& Functional Programming} \begin{document} @@ -94,7 +108,22 @@ \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/02_instantiations.tex} +\input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/03_termination.tex} +\input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/04_semantic-equivalence.tex} +\input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/05_unfolding-loops.tex} +\input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/06_deterministic-semantics.tex} +\input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/07_extensions-of-imp.tex} % \input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/} +\input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/00_structural-operational-semantics.tex} +\input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/01_rules.tex} +\input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/02_multi-step-derivation-seq.tex} +\input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/03_termintation.tex} +\input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/04_proofs.tex} +\input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/05_semantic-equivalence.tex} +\input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/06_extensions.tex} +% \input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/} +\input{parts/03_language-semantics/01_operational-semantics/02_equiv.tex} % \input{parts/03_language-semantics/01_operational-semantics/} % \input{parts/03_language-semantics/} 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 index daf15e2..d2f2939 100644 --- 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 @@ -1,6 +1,10 @@ \newpage \subsection{Operational Semantics} -\subsubsection{Transition Systems} +Big-step semantics describe how the \bi{overall} results of the execution are obtained and use Natural semantics rules. +Small-step semantics describe how the individual steps of the computations take place and use Structural Operational Semantics (SOS) + +\subsubsection{Big-Step Semantics} +\paragraph{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'$, 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 index a331f1a..72b9a64 100644 --- 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 @@ -1,4 +1,4 @@ -\subsubsection{Big-Step Semantics of IMP} +\paragraph{Big-Step Semantics of IMP} \[ \begin{prooftree} \infer0[\textsc{Skip}$_{NS}$]{\langle \texttt{skip}, \sigma \rangle \rightarrow \sigma} diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/02_instantiations.tex b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/02_instantiations.tex new file mode 100644 index 0000000..5b6968d --- /dev/null +++ b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/02_instantiations.tex @@ -0,0 +1,17 @@ +\paragraph{Rule Schemes and Instantiations} +Each inference rule is actually a rule scheme, where the meta-variables are placeholders for statements, states, etc. +Each rule scheme describes infinitely many \bi{rule instances}. + +A rule is \bi{instantiated} when all meta-variables are replaced with syntactic elements +Assignment rule scheme vs. instance +\[ + \begin{prooftree} + \infer0[\textsc{Ass}$_{NS}$]{\langle x := e, \sigma \rangle \rightarrow \sigma[x \mapsto \cA\llbracket e \rrbracket \sigma]} + \end{prooftree} + \qquad + \begin{prooftree} + \infer0[\textsc{Ass}$_{NS}$]{\langle v := v + 1, \sigma_\text{zero} \rangle \rightarrow \sigma[v \mapsto \cA\llbracket v + 1 \rrbracket \sigma_\text{zero}]} + \end{prooftree} +\] + +The \bi{rule instances} can be combined to derive a transition $\langle s, \sigma \rangle \rightarrow \sigma'$ and we get a derivation tree. diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/03_termination.tex b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/03_termination.tex new file mode 100644 index 0000000..b19f018 --- /dev/null +++ b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/03_termination.tex @@ -0,0 +1,9 @@ +\newpage +\paragraph{Termination} +\begin{definition}[]{Termination} + The execution of a statement $s$ in a state $\sigma$ + \begin{itemize} + \item \bi{terminates successfully} if and only if there exists a state $\sigma'$ such that $\vdash \langle s, \sigma \rangle \rightarrow \sigma'$ + \item \bi{fails to terminate} if and only if there is no state $\sigma'$ such that $\vdash \langle s, \sigma \rangle \rightarrow \sigma'$ + \end{itemize} +\end{definition} diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/04_semantic-equivalence.tex b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/04_semantic-equivalence.tex new file mode 100644 index 0000000..74be2b1 --- /dev/null +++ b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/04_semantic-equivalence.tex @@ -0,0 +1,5 @@ +\paragraph{Semantic equivalence} +\inlinedefinition Two statements $s_1$ and $s_2$ are \bi{semantically equivalent}, denoted $s_1 \simeq s_2$, if and only if +\[ + \forall \sigma, \sigma' . (\vdash \langle s_1, \sigma \rangle \rightarrow \sigma' \Longleftrightarrow \; \vdash \langle s_2, \sigma \rangle \rightarrow \sigma') +\] diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/05_unfolding-loops.tex b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/05_unfolding-loops.tex new file mode 100644 index 0000000..17dc900 --- /dev/null +++ b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/05_unfolding-loops.tex @@ -0,0 +1,45 @@ +\paragraph{Unfolding loops} +In languages like \texttt{C} (and by extension \texttt{C++}) and \texttt{Java}, unfolding a loop leads to non-equivalent code: + +\begin{multicols}{2} + \begin{code}{c} + int i = 0; + while ( i < 2 ) { + + + while ( i < 1 ) + if ( i == 0 ) break; + + i++; + } + printf( "i = %d", i ); + \end{code} + Prints \shade{gray}{\texttt{i = 2}} + \begin{code}{c} + int i = 0; + while ( i < 2 ) { + if ( i == 0 ) { + if ( i == 0 ) break; + while ( i < 1 ) + if ( i == 0 ) break; + } + i++; + } + printf( "i = %d", i ); + \end{code} + Prints \shade{gray}{\texttt{i = 0}} +\end{multicols} + +In IMP however, this kind of action leads to equivalence: +\[ + \forall b, s.(\texttt{while b do s end} \; \simeq \; \texttt{if b then s; while b do s end end}) +\] +So what we have to prove is this: +\[ + \forall b, s, \sigma, \sigma'.(\vdash \langle \texttt{while b do s end}, \sigma \rangle \; \simeq \; + \vdash \langle \texttt{if b then s; while b do s end end}, \sigma \rangle \rightarrow \sigma') +\] + +A proof idea is to show equivalence by proving the implication in both directions. For each of them, we show that there is a derivation tree. + +\inlineproof available in the lecture slides for Formal Methods, Slides 78 - 80 (Slide Deck 3, pages 23 - 25) diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/06_deterministic-semantics.tex b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/06_deterministic-semantics.tex new file mode 100644 index 0000000..1e348a0 --- /dev/null +++ b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/06_deterministic-semantics.tex @@ -0,0 +1,17 @@ +\paragraph{Deterministic Semantics} +\inlinelemma The big-step semantics of IMP is deterministic + +\inlineproof We need to show $\forall s, \sigma, \sigma', \sigma''. + (\vdash \langle s, \delta \rangle \rightarrow \sigma' \land \vdash \langle s, \sigma \rangle \rightarrow \sigma'' \implies \sigma' = \sigma'')$ + +The full proof for this is available on the slides for Formal Methods, pages 82 - 91 (Slide Deck 3, pages 27 - 40) + +In there, \bi{Induction on Derivation Trees} is used. +Similar like other induction proofs, we show that a property $P(T)$ holds for all derivation trees $T$, +we prove that $P(T)$ holds for an arbitrary derivation tree $T$ under the assumption (the induction hypothesis) that $P(T')$ holds for all sub-trees $T'$ of $T$ + +This kind of induction is a special case of \bi{well-founded (Noetherian) induction}. +We define $T' \sqsubset T$ (with $T, T'$ derivation trees) to mean that $T'$ is a proper sub-tree of $T$. +$\sqsubset$ is a well-founded ordering, because derivation trees are finite and we call $T'$ a \bi{sub-derivation} of $T$ if $T' \sqsubset T$. +Typically, \textit{case distinction} is used on the rule applied at the root of $T$ because that provides more information about the structure of the derivation, +such as telling us about sub-derivation to which the induction hypothesis applies. diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/07_extensions-of-imp.tex b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/07_extensions-of-imp.tex new file mode 100644 index 0000000..ccd3948 --- /dev/null +++ b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/07_extensions-of-imp.tex @@ -0,0 +1,73 @@ +\newpage +\paragraph{Extensions of IMP} +\subparagraph{Local Variable Declarations} +\label{sec:big-step-local-var} +A statement \texttt{var x := e in s end} declares a local variable that is visible in the sub-statement of the declaration, \texttt{s}. + +Here, the Expression $e$ is evaluated in the initial state, then $s$ is executed in a state in which $x$ has the value of $e$ and after the execution, +the original value of $x$ is restored. + +The corresponding Big-step semantics rule is: +\[ + \begin{prooftree} + \hypo{\langle s, \sigma[x \mapsto \cA \llbracket e \rrbracket \sigma] \rangle \rightarrow \sigma' } + \infer1[\textsc{Loc}$_{NS}$]{\langle \texttt{var x := e in s end}, \sigma \rangle \rightarrow \sigma'[x \mapsto \sigma(x)]} + \end{prooftree} +\] + + +\subparagraph{Procedure Declaration and Calls} +\[ + \texttt{procedure p(}x_1, \ldots, x_n; y_1, \ldots, y_m \texttt{) begin s end} +\] +Here, the $x_i$ are the \bi{value} parameters and the $y_j$ are the \bi{variable} parameters. The latter can be used to assign values back to the procedure caller (return values). + +In a \bi{procedure declaration} the \bi{formal} parameter names $x_i$ and $y_j$ must be pairwise distinct and the only free variables in $s$. + +For the \bi{procedure call} $p(e_1, \ldots, e_n; z_1, \ldots, z_m)$, the \bi{actual} variable parameters must be pairwise distinct. + +The corresponding Big-step semantics rule is: +\[ + \begin{prooftree} + \hypo{\langle s, \sigma_\text{zero}[\overrightharpoon{x_i} \mapsto \overrightharpoon{\cA \llbracket e_i \rrbracket \sigma}] + [\overrightharpoon{y_j} \mapsto \overrightharpoon{\sigma(z_j)}] \rangle \rightarrow \sigma'} + \infer1[\textsc{Call}$_{NS}$]{\langle p(\overrightharpoon{e_i}; \overrightharpoon{z_j}), \sigma \rangle + \rightarrow \sigma[\overrightharpoon{z_j} \mapsto \overrightharpoon{\sigma'(y_j)}]} + \end{prooftree} +\] +where the notation $\sigma[\overrightharpoon{x_i} \mapsto \overrightharpoon{v_i}]$ is an abbreviation of $\sigma[x_1 \mapsto v_1]\ldots[x_n \mapsto v_n]$ + + +\subparagraph{Non-determinism} +For a statement $s \bigbox s'$, either $s$ or $s'$ is non-deterministically chosen to be executed. + +\inlineexample In the statement \texttt{x := 1 $\bigbox$ (x := 2; x := x + 2)}, we either get $x = 1$ or $x = 4$ +(either the statement on the left or right of the box is evaluated) + +The corresponding rules are: +\[ + \begin{prooftree} + \hypo{\langle s, \sigma \rangle \rightarrow \sigma'} + \infer1[\textsc{ND1}$_{NS}$]{\langle s \bigbox s', \sigma \rangle \rightarrow \sigma'} + \end{prooftree} + \qquad + \begin{prooftree} + \hypo{\langle s', \sigma \rangle \rightarrow \sigma'} + \infer1[\textsc{ND2}$_{NS}$]{\langle s \bigbox s', \sigma \rangle \rightarrow \sigma'} + \end{prooftree} +\] +An important note on non-terminating branches, we will not ``see'' them, because big-step semantics can't encompass that concept. + + +\subparagraph{Parallelism} +In a statement \texttt{s par s'}, both $s$ and $s'$ are executed, but their execution can be \bi{interleaved}. + +\inlineexample \texttt{x := 1 par (x := 2; x := x + 2)} could result in: +\begin{multicols}{2} + \begin{itemize} + \item $4$: first \texttt{x:=1}, then \texttt{x:=2} and finally \texttt{x:=x+2} + \item $1$: first \texttt{x:=2}, then \texttt{x:=x+2} and finally \texttt{x:=1} + \item $3$: first \texttt{x:=2}, then \texttt{x:=1} and finally \texttt{x:=x+2} + \end{itemize} +\end{multicols} +In Big-step semantics however, there are no rules for this, because it can only define atomic steps. diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/00_structural-operational-semantics.tex b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/00_structural-operational-semantics.tex new file mode 100644 index 0000000..c2547cd --- /dev/null +++ b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/00_structural-operational-semantics.tex @@ -0,0 +1,17 @@ +\newpage +\subsubsection{Small-Step semantics} +\paragraph{Structural Operational Semantics (SOS)} +Expressing each individual steps of execution allows one to express the \bi{order of execution} of these steps, +thus allowing us to describe properties of non-terminating programs and parallelization. + +$\gamma$ is used as the meta-variable for terminal and non-terminal configurations. +For the transitions, we denote the relation $\rightarrow_1$, which can have two forms: +\begin{itemize} + \item $\langle s, \sigma \rangle \rightarrow_1 \langle s', \sigma' \rangle$ is for any non-complete computation, + where the next computation is expressed by the intermediate configuration $\langle s', \sigma' \rangle$ + \item $\langle s, \sigma \rangle \rightarrow_1 \sigma'$ is the final execution that reaches a terminal state. +\end{itemize} + +Finally, a transition $\langle s, \sigma \rangle \rightarrow_1 \gamma$ describes the \bi{first step} of the execution of $s$ in state $\sigma$. + +A non-terminal configuration $\langle s, \sigma \rangle$ is \bi{stuck}, if there does not exist a configuration $\gamma$ such that $\langle s, \sigma \rangle \rightarrow_1 \gamma$. diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/01_rules.tex b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/01_rules.tex new file mode 100644 index 0000000..23c68d8 --- /dev/null +++ b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/01_rules.tex @@ -0,0 +1,56 @@ +\subparagraph{The rules} +\[ + \begin{prooftree} + \infer0[\textsc{Skip}$_{SOS}$]{\langle \texttt{skip}, \sigma \rangle \rightarrow_1 \sigma} + \end{prooftree} + \qquad + \begin{prooftree} + \infer0[\textsc{Ass}$_{SOS}$]{\langle x := e, \sigma \rangle \rightarrow_1 \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''$). +Then, either $s$ executes completely in one step (\textsc{Seq1}), or does not (\textsc{Seq2}). +\[ + \begin{prooftree} + \hypo{\langle s, \sigma \rangle \rightarrow_1 \sigma'} + \infer1[\textsc{Seq1}$_{SOS}$]{\langle s;s', \sigma \rangle \rightarrow_1 \langle s', \sigma' \rangle} + \end{prooftree} + \qquad + \begin{prooftree} + \hypo{\langle s', \sigma' \rangle \rightarrow_1 \langle s'', \sigma' \rangle} + \infer1[\textsc{Seq2}$_{SOS}$]{\langle s;s', \sigma \rangle \rightarrow_1 \langle s'';s', \sigma' \rangle} + \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} + \infer0[\textsc{IfT}$_{SOS}$]{\langle \texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow_1 \langle s', \sigma' \rangle} + \end{prooftree} + \qquad + \begin{prooftree} + \infer0[\textsc{IfF}$_{SOS}$]{\langle \texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow_1 \langle s', \sigma' \rangle} + \end{prooftree} +\] +Where the first rule applies if $\cB\llbracket b \rrbracket \sigma = \texttt{tt}$. Below a further two rules for the true case: +\[ + \begin{prooftree} + \hypo{\langle s, \sigma \rangle \rightarrow_1 \sigma'} + \infer1[\textsc{IfT1}$_{SOS}$]{\langle \texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow_1 \sigma'} + \end{prooftree} + \qquad + \begin{prooftree} + \hypo{\langle s, \sigma \rangle \rightarrow_1 \langle s'', \sigma' \rangle} + \infer1[\textsc{IfT2}$_{SOS}$]{\langle \texttt{if}\;b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow_1 \langle s''', \sigma' \rangle} + \end{prooftree} +\] + + +\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} + \infer0[\textsc{While}$_{SOS}$]{\langle \texttt{while} \; b \; \texttt{do} \; s \; \texttt{end}, \sigma \rangle \rightarrow_1 + \langle \texttt{if} \; b \; \texttt{then} \; s; \; \texttt{while} \; b \; \texttt{do} \; s \; \texttt{end else skip end}, \sigma \rangle} + \end{prooftree} +\] diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/02_multi-step-derivation-seq.tex b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/02_multi-step-derivation-seq.tex new file mode 100644 index 0000000..e68a9d6 --- /dev/null +++ b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/02_multi-step-derivation-seq.tex @@ -0,0 +1,22 @@ +\paragraph{Multi-Step Execution} +We use the definitions we have to define a \bi{$k$-step execution}, denoted $\gamma \rightarrow_1^k \gamma'$. +Of course, this means intuitively that there is an execution of exactly $k$ steps from $\gamma$ to $\gamma'$. + +We define the relation inductively over $k$: +\begin{itemize} + \item $\gamma \rightarrow_1^0 \gamma'$ if and only if $\gamma = \gamma'$ + \item $\gamma \rightarrow_1^k \gamma'$ if and only if there exists $\gamma''$ such that both $\vdash \gamma \rightarrow_1$ and $\gamma'' \rightarrow_1^{k - 1} \gamma'$ +\end{itemize} +Resulting from this, $\gamma \rightarrow_1^{k_1 + k_2} \gamma'$ if and only if $\exists \gamma'' . \gamma \rightarrow_1^{k_1} \gamma'' \land \gamma'' \rightarrow_1^{k_2} \gamma'$ + +We write $\gamma \rightarrow_1^* \gamma'$ to signify that there is an execution from $\gamma$ to $\gamma'$ in some finite number of steps, or more formally: +\[ + \exists k. \gamma \rightarrow_1^k \gamma' +\] + + +\paragraph{Derivation Sequences} +\inlinedefinition A \bi{derivation sequence} is a non-empty sequence of configurations $\gamma_0, \ldots$, for which $\gamma_i \rightarrow_1^1 \gamma_{i + 1}$ for each $0 \leq i$, +such that $i + 1$ is in the range of the sequence. If the sequence is finite, then the last configuration in the sequence is either a terminal or stuck configuration. + +The \bi{length} of the derivation sequence is the number of transitions (thus number of states minus one!) diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/03_termintation.tex b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/03_termintation.tex new file mode 100644 index 0000000..2f8890d --- /dev/null +++ b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/03_termintation.tex @@ -0,0 +1,10 @@ +\paragraph{Termination} +\inlinetheorem The execution of a statement $s$ in a state $\sigma$ +\begin{itemize} + \item \bi{terminates} if and only if there is a finite derivation sequence starting with $\langle s, \sigma \rangle$ + \item \bi{runs forever} if and only if there is an infinite derivation sequence starting with $\langle s, \sigma \rangle$ +\end{itemize} + +\inlinetheorem The execution of statement $s$ in state $\sigma$ \bi{terminates} successfully, if and only if $\exists \sigma'. \langle s, \sigma \rangle \rightarrow^*_1 \sigma'$ + +Of note is that these are properties of \bi{configurations} and not just statements. diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/04_proofs.tex b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/04_proofs.tex new file mode 100644 index 0000000..9938843 --- /dev/null +++ b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/04_proofs.tex @@ -0,0 +1,6 @@ +\paragraph{Proving properties of Derivation Sequences} +For reasoning about finite derivation sequences, we commonly reason about a multi-step execution $\gamma \rightarrow_1^k \gamma'$ +by \bi{strong induction on the number of steps $k$}, where we define $P(k) \equiv$ ``for all executions of length k, our property holds'' and we prove $P(k)$ for arbitrary $k$ +with the \bi{induction hypothesis} $\forall k' < k. P(k')$ holds + +After the setup, it \textit{often} proceeds by case distinction on the $0$ step and the other steps diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/05_semantic-equivalence.tex b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/05_semantic-equivalence.tex new file mode 100644 index 0000000..de234d4 --- /dev/null +++ b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/05_semantic-equivalence.tex @@ -0,0 +1,16 @@ +\paragraph{Semantic Equivalence and Determinism} +\inlinedefinition Under the small-step semantics, two statements $s_1$ and $s_2$ are \bi{semantically equivalent} if for all states $\sigma$ both: +\begin{itemize} + \item for all stuck or terminal configurations $\gamma$ we have $\langle s_1, \sigma \rangle \rightarrow_1^* \gamma$ if and only if + $\langle s_2, \sigma \rangle \rightarrow_1^* \gamma$, and + \item there is and infinite derivation sequence starting in $\langle s_1, \sigma \rangle$ if and only if there is one starting in $\langle s_2, \sigma \rangle$ +\end{itemize} + +\inlinelemma The small-step semantics of IMP is \bi{deterministic}. That is: +\[ + \forall s, \sigma, \gamma, \gamma'. \vdash \langle s, \sigma \rangle \rightarrow_1 \gamma + \land \vdash \langle s, \gamma \rangle \rightarrow_1 \gamma' + \implies \gamma = \gamma' +\] + +\inlinecorollary There is exactly one derivation sequence starting in configuration $\langle s, \sigma \rangle$ diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/06_extensions.tex b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/06_extensions.tex new file mode 100644 index 0000000..2361acb --- /dev/null +++ b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/06_extensions.tex @@ -0,0 +1,67 @@ +\paragraph{Extensions of IMP} + +\subparagraph{Local Variable Declarations} +As already partially established in Section \ref{sec:big-step-local-var}, the steps to define a local variable are (for \texttt{var x:=e in s end}): +\begin{multicols}{3} + \begin{enumerate} + \item Assign $e$ to $x$ + \item Execute $s$ (possibly many steps) + \item Restore the initial value of $x$ + \end{enumerate} +\end{multicols} + +Since we need to somehow inject he restore instruction into the statements $s$, we extend the \texttt{Stm} category with a \texttt{restore} statement, +defined as \texttt{restore (Var, Val)}. + +With that, we can define the rules: +\[ + \begin{prooftree} + \infer0[\textsc{Loc}$_{SOS}$]{\langle \texttt{var x:= e in s end}, \sigma \rangle \rightarrow_1 \langle \texttt{s;restore }(x, \sigma(x)), + \sigma[x \mapsto \cA \llbracket e \rrbracket \sigma] \rangle} + \end{prooftree} +\] +\[ + \begin{prooftree} + \infer0[\textsc{Ret}$_{SOS}$]{\langle \texttt{restore }(x, \sigma(x)), \sigma \rangle \rightarrow_1 \sigma[x \mapsto v]} + \end{prooftree} +\] + +Of course, we could also just model execution stacks, as most languages do. + + +\subparagraph{Non-determinism} +The rules here are analogous to the ones from the big-step rules +\[ + \begin{prooftree} + \infer0[\textsc{ND1}$_{SOS}$]{\langle s \bigbox s', \sigma \rangle \rightarrow_1 \langle s, \sigma \rangle} + \end{prooftree} + \qquad + \begin{prooftree} + \infer0[\textsc{ND2}$_{SOS}$]{\langle s \bigbox s', \sigma \rangle \rightarrow_1 \langle s, \sigma' \rangle} + \end{prooftree} +\] + + +\subparagraph{Parallelism} +\[ + \begin{prooftree} + \hypo{\langle s, \sigma \rangle \rightarrow_1 \langle s'', \sigma' \rangle} + \infer1[\textsc{Par1}$_{SOS}$]{\langle s \texttt{ par } s', \sigma \rangle \rightarrow_1 \langle s'' \texttt{ par } s', \sigma' \rangle} + \end{prooftree} + \qquad + \begin{prooftree} + \hypo{\langle s, \sigma \rangle \rightarrow_1 \sigma'} + \infer1[\textsc{Par2}$_{SOS}$]{\langle s \texttt{ par } s', \sigma \rangle \rightarrow_1 \langle s', \sigma' \rangle} + \end{prooftree} +\] +\[ + \begin{prooftree} + \hypo{\langle s', \sigma \rangle \rightarrow_1 \langle s'', \sigma' \rangle} + \infer1[\textsc{Par3}$_{SOS}$]{\langle s \texttt{ par } s', \sigma \rangle \rightarrow_1 \langle s \texttt{ par } s'', \sigma' \rangle} + \end{prooftree} + \qquad + \begin{prooftree} + \hypo{\langle s', \sigma \rangle \rightarrow_1 \sigma'} + \infer1[\textsc{Par4}$_{SOS}$]{\langle s \texttt{ par } s', \sigma \rangle \rightarrow_1 \langle s, \sigma' \rangle} + \end{prooftree} +\] 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 index e69de29..8b62f7a 100644 --- 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 @@ -0,0 +1,24 @@ +\newpage +\subsubsection{Equivalence} +\begin{theorem}[]{Equivalence Theorem} + For every statement $s$ of IMP, we have + \[ + \vdash \langle s, \sigma \rangle \rightarrow \sigma' \Leftrightarrow \langle s, \sigma \rangle \rightarrow_1^* \sigma' + \] + {\scriptsize If the execution of $s$ from some state terminates successfully in one of the semantics, than so will it in the other. + The execution fails to terminate in the big-step semantics if and only if it either gets stuck, or runs forever in the small-step semantics} +\end{theorem} + + +\inlinelemma[Equivalence Lemma 1] For every statement $s$ of IMP and states $\sigma$ and $\sigma'$ we have: +\[ + \vdash \langle s, \sigma \rangle \rightarrow \sigma' \implies \langle s, \sigma \rangle \rightarrow_1^* \sigma' +\] +{\scriptsize If the execution of $s$ from $\sigma$ terminates successfully in the big-step semantics, so will it in the small-step semantics (in the same state, too!)} + + +\inlinelemma[Equivalence Lemma 2] For every statement $s$ of IMP and states $\sigma$ and $\sigma'$ and $k \in \N$, we have: +\[ + \langle s, \sigma \rangle \rightarrow_1^k \sigma' \implies \vdash \langle s, \sigma \rangle \rightarrow \sigma' +\] +{\scriptsize If the execution of $s$ from $\sigma$ terminates successfully in the small-step semantics, so will it in the big-step semantics (in the same state, too!)}