eth-janishutz/eth-summaries
1
0
Fork 0
mirror of https://github.com/janishutz/eth-summaries.git synced 2026-04-28 16:19:23 +02:00
Code Issues Packages Projects Releases Wiki Activity

[FMFP] IMP intro, start of operational semantics

Browse Source
This commit is contained in:
Janis Hutz
2026-04-24 12:00:28 +02:00
parent 86152fc82e
commit bf5b0e1407
9 changed files with 264 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files
semester4/fmfp/parts/03_language-semantics/00_imp/00_syntax.tex
+37
View File
@@ -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$
semester4/fmfp/parts/03_language-semantics/00_imp/01_semantics.tex
+58
View File
@@ -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}
\]
semester4/fmfp/parts/03_language-semantics/00_imp/02_properties.tex
+81
View File
@@ -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}
semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/00_transition-systems.tex
+20
View File
@@ -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}.
semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/01_semantics.tex
+54
View File
@@ -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}
\]
semester4/fmfp/parts/03_language-semantics/01_operational-semantics/02_equiv.tex
View File