[FMFP] Big and small step semantics, equivalence theorem

2026-04-28 16:19:23 +02:00 · 2026-04-24 18:01:57 +02:00
parent bf5b0e1407
commit 68284b2461
18 changed files with 419 additions and 2 deletions
@@ -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'$,
@@ -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}
@@ -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.
@@ -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}
@@ -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')
+\]
@@ -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)
@@ -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.
@@ -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.