\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}
