mirror of
https://github.com/ProgramSnail/Lama.git
synced 2025-12-06 06:48:48 +00:00
169 lines
8 KiB
TeX
169 lines
8 KiB
TeX
\section{Structural Induction}
|
|
|
|
\begin{figure}
|
|
\begin{subfigure}{\textwidth}
|
|
\[
|
|
\begin{array}{rclr}
|
|
\sembr{n} & = & \lambda \sigma . n & \mbox{\scriptsize\rulename{[Const]}}\\
|
|
\sembr{x} & = & \lambda \sigma . \sigma x & \mbox{\scriptsize\rulename{[Var]}} \\
|
|
\sembr{A\otimes B} & = & \lambda \sigma . (\sembr{A}\sigma \oplus \sembr{B}\sigma) & \mbox{\scriptsize\rulename{[Binop]}}
|
|
\end{array}
|
|
\]
|
|
\caption{Denotational semantics for expressions}
|
|
\end{subfigure}
|
|
\vskip5mm
|
|
\begin{subfigure}{\textwidth}
|
|
\[\trans{c}{\epsilon}{c}\ruleno{Stop$_{SM}$}\]
|
|
\[\trule{\trans{\inbr{(x\oplus y)\llang{::}st, s}}{p}{c^\prime}}{\trans{\inbr{y\llang{::}x\llang{::}st, s}}{(\llang{BINOP $\;\otimes$})p}{c^\prime}}\ruleno{Binop$_{SM}$}\]
|
|
\[\trule{\trans{\inbr{z\llang{::}st, s}}{p}{c^\prime}}{\trans{\inbr{st, s}}{(\llang{CONST $\;z$})p}{c^\prime}}\ruleno{Const$_{SM}$}\]
|
|
\[\trule{\trans{\inbr{(s\;x)\llang{::}st, s}}{p}{c^\prime}}{\trans{\inbr{st, s}}{(\llang{LD $\;x$})p}{c^\prime}}\ruleno{LD$_{SM}$}\]
|
|
\caption{Big-step operational semantics for stack machine}
|
|
\end{subfigure}
|
|
\vskip5mm
|
|
\begin{subfigure}{\textwidth}
|
|
\[
|
|
\begin{array}{rclr}
|
|
\sembr{x}^{\mathscr E}_{comp}&=&\llang{[LD $\;x$]} & \mbox{\scriptsize\rulename{[Var$_{comp}$]}} \\
|
|
\sembr{n}^{\mathscr E}_{comp}&=&\llang{[CONST $\;n$]} & \mbox{\scriptsize\rulename{[Const$_{comp}$]}}\\
|
|
\sembr{A\otimes B}^{\mathscr E}_{comp}&=&\sembr{A}^{\mathscr E}_{comp}\llang{@}\sembr{B}^{\mathscr E}_{comp}\llang{@[BINOP $\otimes$]}) & \mbox{\scriptsize\rulename{[Binop$_{comp}$]}}
|
|
\end{array}
|
|
\]
|
|
\caption{Compilation}
|
|
\end{subfigure}
|
|
\caption{All relevant definitions}
|
|
\label{definitions}
|
|
\end{figure}
|
|
|
|
|
|
We have considered two languages (a language of expressions $\mathscr E$ and a language of stack machine programs $\mathscr P$), and a compiler from the former to the latter.
|
|
It can be formally proven, that the compiler is (fully) correct in the sense, given in the lecture 1. Due to the simplicity of the languages, the proof technique~---
|
|
\emph{structural induction}~--- is simple as well.
|
|
|
|
First, we collect all needed definitions in one place (see Fig.~\ref{definitions}). We simplified the description of stack machine semantics a little bit: first,
|
|
we dropped off all instructions, which cannot be generated by the expression compiler, and then, we removed the input and output streams from the stack machine
|
|
configurations, since they are never affected by the remaining instructions.
|
|
|
|
\begin{lemma}(Determinism)
|
|
Let $p$ be an arbitrary stack machine program, and let $c$, $c_1$ and $c_2$ be arbitrary configurations. Then
|
|
|
|
\[
|
|
\trans{c}{p}{c_1} \wedge \trans{c}{p}{c_2} \Rightarrow c_1= c_2
|
|
\]
|
|
\end{lemma}
|
|
\begin{proof}
|
|
Induction on the structure of $p$.
|
|
|
|
\textbf{Base case}. If $p=\epsilon$, then, by the rule \rulename{Stop$_{SM}$}, $c_1=c$ and $c_2=c$. Since no other rule can be
|
|
applied, we're done.
|
|
|
|
\textbf{Induction step}. If $p=\iota p^\prime$, then, by condition, we have
|
|
|
|
\[
|
|
\trule{\trans{c^\prime}{p^\prime}{c_1}}{\trans{c}{\iota p^\prime}{c_1}}
|
|
\]
|
|
|
|
and
|
|
|
|
\[
|
|
\trule{\trans{c^{\prime\prime}}{p^\prime}{c_2}}{\trans{c}{\iota p^\prime}{c_2}}
|
|
\]
|
|
|
|
where $c^\prime$ and $c^{\prime\prime}$ depend only on $c$ and $\iota$. By the case analysis on $\iota$ we conclude, that
|
|
$c^\prime=c^{\prime\prime}$. Since $p^\prime$ is shorter, than $p$, we can apply the induction hypothesis, which gives us
|
|
$c_1=c_2$.
|
|
\end{proof}
|
|
|
|
\FloatBarrier
|
|
|
|
\begin{lemma} (Compositionality)
|
|
Let $p=p_1p_2$ be an arbitrary stack machine program, subdivided into arbitrary subprograms $p_1$ and $p_2$. Then,
|
|
|
|
\[
|
|
\forall c_1, c_2:\;\trans{c_1}{p}{c_2}\;\Leftrightarrow\;\exists c^\prime:\; \trans{c_1}{p_1}{c^\prime} \wedge \trans{c^\prime}{p_2}{c_2}
|
|
\]
|
|
\end{lemma}
|
|
\begin{proof}
|
|
Induction on the structure of $p$.
|
|
|
|
\textbf{Base case}. The base case $p=\epsilon$ is trivial: use the rule \rulename{Stop$_{SM}$} and get $c^\prime=c_2=c_1$.
|
|
|
|
\textbf{Induction step}. When $p=\iota p^\prime$, then there are two cases:
|
|
|
|
\begin{itemize}
|
|
\item Either $p_1=\epsilon$, then $c^\prime=c_1$ trivially by the rule \rulename{Stop$_{SM}$}, and we're done.
|
|
\item Otherwise $p_1=\iota p_1^\prime$, and, thus, $p=\iota p_1^\prime p_2$. In order to prove the lemma, we need to prove two implications:
|
|
\begin{enumerate}
|
|
\item Let $\trans{c_1}{p=\iota p_1^\prime p_2}{c_2}$. Technically, we need here to consider three cases (one for each type of the instruction
|
|
$\iota$), but in all cases the outcome would be the same: we have the picture
|
|
|
|
\[
|
|
\trule{\trans{c^{\prime\prime}}{p_1^\prime p_2}{c_2}}{\trans{c_1}{p=\iota p_1^\prime p_2}{c_2}}
|
|
\]
|
|
|
|
where $c^{\prime\prime}$ depends only on $\iota$ and $c_1$. Since $p_1^\prime p_2$ is shorter, than $p$, we can apply the induction hypothesis, which gives us a
|
|
configuration $c^\prime$, such, that $\trans{c^{\prime\prime}}{p_1^\prime}{c^\prime}$ and $\trans{c^\prime}{p_2}{c_2}$. The observation $\trans{c_1}{\iota p_1^\prime}{c^\prime}$
|
|
concludes the proof (note, we implicitly use determinism here).
|
|
\item Let there exists $c^\prime$, such that $\trans{c_1}{\iota p_1^\prime}{c^\prime}$ and $\trans{c^\prime}{p_2}{c_2}$. From the first relation we have
|
|
|
|
\[
|
|
\trule{\trans{c^{\prime\prime}}{p_1^\prime}{c^\prime}}{\trans{c_1}{\iota p_1^\prime}{c^\prime}}
|
|
\]
|
|
|
|
where $c^{\prime\prime}$ depends only on $\iota$ and $c_1$. Since $p_1^\prime p_2$ is shorter, than $p$, we can apply the induction hypothesis, which
|
|
gives us $\trans{c^{\prime\prime}}{p_1^\prime p_2}{c_2}$, and, thus, $\trans{c_1}{\iota p_1^\prime p_2}{c_2}$ (again, we implicitly use determinism here).
|
|
\end{enumerate}
|
|
\end{itemize}
|
|
\end{proof}
|
|
|
|
\begin{theorem}(Correctness of compilation)
|
|
Let $e\in\mathscr E$ be arbitrary expression, $s$~--- arbitrary state, and $st$~--- arbitrary stack. Then
|
|
|
|
\[
|
|
\trans{\inbr{st, s}}{\sembr{e}^{\mathscr E}_{comp}}{\inbr{(\sembr{e}\,s)::st, s}}\; \mbox{iff} \; (\sembr{e}\,s)\; \mbox{is defined}
|
|
\]
|
|
\end{theorem}
|
|
\begin{proof}
|
|
Induction on the structure of $e$.
|
|
|
|
\textbf{Base case}. There are two subcases:
|
|
|
|
\begin{enumerate}
|
|
\item $e$ is a constant $z$. Then:
|
|
\begin{itemize}
|
|
\item $\sembr{e}\,s=z$ for each state $s$;
|
|
\item \mbox{$\sembr{e}^{\mathscr E}_{comp}=[\llang{CONST z}]$};
|
|
\item $\trans{\inbr{st, s}}{[\llang{CONST z}]}{\inbr{z::st, s}}$ for arbitrary $st$ and $s$.
|
|
\end{itemize}
|
|
|
|
This concludes the first base case.
|
|
|
|
\item $e$ is a variable $x$. Then:
|
|
\begin{itemize}
|
|
\item $\sembr{s}\,s=s\,x$ for each state $s$, such that $s\,x$ is defined;
|
|
\item \mbox{$\sembr{e}^{\mathscr E}_{comp}=[\llang{LD x}]$};
|
|
\item $\trans{\inbr{st, s}}{[\llang{CONST z}]}{\inbr{(s\,x)::st, s}}$ for arbitrary $st$ and arbitrary $s$, such that $s\, x$ is defined.
|
|
\end{itemize}
|
|
|
|
This concludes the second base case.
|
|
\end{enumerate}
|
|
|
|
\textbf{Induction step}. Let $e$ be $A\otimes B$. Then:
|
|
|
|
\begin{itemize}
|
|
\item $\sembr{A\otimes B}s=\sembr{A}s\oplus\sembr{B}s$ for each state $s$, such that both $\sembr{A}s$ and $\sembr{B}s$ are defined;
|
|
\item $\sembr{A\otimes B}^{\mathscr E}_{comp}=\sembr{A}^{\mathscr E}_{comp}\llang{@}\sembr{B}^{\mathscr E}_{comp}\llang{@[BINOP $\oplus$]}$;
|
|
\item by the inductive hypothesis, for arbitrary $st$ and $s$
|
|
|
|
\[
|
|
\trans{\inbr{st, s}}{\sembr{A}^{\mathscr E}_{comp}}{\inbr{(\sembr{A}s)::st, s}} \mbox{iff} \; (\sembr{A}\,s)\; \mbox{is defined}
|
|
\]
|
|
|
|
and
|
|
|
|
\[
|
|
\trans{\inbr{(\sembr{A}s)::st, s}}{\sembr{B}^{\mathscr E}_{comp}}{\inbr{(\sembr{B}s)::(\sembr{A}s)::st, s}} \mbox{iff} \; (\sembr{A}\,s) \;\mbox{and}\; (\sembr{A}\,s) \; \mbox{are defined}
|
|
\]
|
|
|
|
Taking into account the semantics of \llang{BINOP $\otimes$} and applying the compositionality lemma, the theorem follows.
|
|
\end{itemize}
|
|
\end{proof}
|