\documentclass[11pt,fleqn]{article}

\usepackage{amsmath}
\usepackage{latexsym}
% \usepackage{code}

\input{cs221-style}

% \newcommand{\typ}[2]{\ensuremath{\Gamma \vdash #1 : \, #2}}
\newcommand{\Ok}[2]{\ensuremath{#1 \vdash #2 ~\, \mathsf{ok}}}
\newcommand{\OkG}[1]{\ensuremath{\Gamma \vdash #1 ~\, \mathsf{ok}}}
\newcommand{\num}{\ensuremath{\mathtt{num}}}
\newcommand{\plus}{\ensuremath{\mathtt{plus}}}
\newcommand{\Times}{\ensuremath{\mathtt{times}}}
\newcommand{\Let}{\ensuremath{\mathtt{let}}}
\newcommand{\Trans}[2]{#1 \, \mapsto \, #2}


\begin{document}
\handout{1}{Oct 25, 2005}{Rule Induction Example}
This handout provides a detailed examination of Rule Induction for the
particular rule set defining the small-step dynamic semantics for
the simple language Arith+Let (see Section 1). It gives a full
presentation of the Induction Principle for this rule set, and then
a detailed (even pedantic) sample inductive proof based on the
Induction Principle.
\section{Small-step dynamic semantics for Arith with Let}
\vspace{-1.5ex}
\begin{center}
  \begin{tabular}{p{3.0in}@{}p{3.0in}}
    \begin{displaymath}
     \inferl{AD_1}{\Trans{\plus(\num[m],\num[n])}{\num[p]}}
	{(p = m + n)}
    \end{displaymath}
  &
    \begin{displaymath}
     \inferl{AD_2}{\Trans{\Times(\num[m],\num[n])}{\num[p]}}
	{(p = m \times n)}
    \end{displaymath}
  \\
    \multicolumn{2}{p{5.0in}}{
    \begin{displaymath}
      \inferl{AD_3}{\Trans{\Let(\num[n],\,x.e_2)}{\{\num[p]/x\}e_2}}
	{\strut}
    \end{displaymath}}
  \\
    \begin{displaymath}
      \inferl{AD_4}{\Trans{\plus(e_1,e_2)}{\plus(e'_1,e_2)}}
	{\Trans{e_1}{e'_1}}
    \end{displaymath}
  &
    \begin{displaymath}
      \inferl{AD_5}{\Trans{\plus(\num[n],e_2)}{\plus(\num[n],e'_2)}}
	{\Trans{e_2}{e'_2}}
    \end{displaymath}
  \\
    \begin{displaymath}
      \inferl{AD_6}{\Trans{\Times(e_1,e_2)}{\Times(e'_1,e_2)}}
	{\Trans{e_1}{e'_1}}
    \end{displaymath}
  &
    \begin{displaymath}
      \inferl{AD_7}{\Trans{\Times(\num[n],e_2)}{\Times(\num[n],e'_2)}}
	{\Trans{e_2}{e'_2}}
    \end{displaymath}
  \\
    \multicolumn{2}{p{6.0in}}{
    \begin{displaymath}
      \inferl{AD_8}{\Trans{\Let(e_1,\,x.e_2)}{\Let(e'_1,\,x.e_2)}}
	{\Trans{e_1}{e'_1}}
    \end{displaymath}}
  \end{tabular}
\end{center}

\section{Induction Principle for Dynamic Sematics Rules}

The Induction Principle for the transition relation $\mapsto$ defined
by rules $AD_1$ through $AD_8$ allows us to prove general statements
of the form
\begin{equation}
IConc: \quad \forall e, e' . \, \Trans{e}{e'} \Rightarrow P(e,e')
\end{equation}
where $P$ is some binary property on expressions. For instance, to
prove the following proposition stating that the transition relation
is deterministic:
\begin{equation}
\forall e_1, e_2, e_3 . \; \Trans{e_1}{e_2} ~\&~ \Trans{e_1}{e_3}
\;\Rightarrow\; e_2 = e_3
\end{equation}
we could define the property $P$ as follows:
\begin{equation}
P(e,e') \; \Leftrightarrow \; \forall e''.\,\Trans{e}{e''}
\;\Rightarrow\; e'' = e'
\end{equation}
The Induction Principle is the implication
\begin{equation}
IC_1 \, \& \, IC_2 \,\&\, \ldots \, \& \, IC_8 \; \Rightarrow \; IConc
\end{equation}
where each $IC_i$ is an \emph{induction clause} for the corresponding
inference rule $AD_i$, as described below.

\paragraph{Instruction Rules:} The induction clauses for the three
\emph{instruction} rules are simple because they do not introduce induction hypotheses.
\paragraph{Rule $AD_1$}
\begin{equation}
IC_1: \quad \forall e,e' . \, \mbox{if}~ \Trans{e}{e'}~\mbox{by}~AD_1,~\mbox{then}~ P(e,e')
\end{equation}
or equivalently
\begin{equation}
IC_1: \quad \forall m,n . \, P(\plus(\num[m],\num[n]), \num[m + n])
\end{equation}
\paragraph{Rule $AD_2$}
\begin{equation}
IC_2: \quad \forall e,e' . \, \mbox{if}~ \Trans{e}{e'}~\mbox{by}~AD_2,~\mbox{then}~ P(e,e')
\end{equation}
or equivalently
\begin{equation}
IC_2: \quad \forall m,n . \, P(\Times(\num[m],\num[n]), \num[m \times n])
\end{equation}
\paragraph{Rule $AD_3$}
\begin{equation}
IC_3: \quad \forall e,e' . \, \mbox{if}~ \Trans{e}{e'}~\mbox{by}~AD_2,~\mbox{then}~ P(e,e')
\end{equation}
or equivalently
\begin{equation}
IC_3: \quad \forall n,e . \, P(\Let(\num[n],\,x.e), \{\num[n]/x\}e)
\end{equation}
\pagebreak
\paragraph{Search Rules:} The induction clauses for the \emph{search} rules are more
complicated, and involve induction hypotheses (which are underlined here).
\paragraph{Rule $AD_4$}
\begin{eqnarray}
\lefteqn{IC_4: \quad \forall e,e' . \, \mbox{if}~
\Trans{e}{e'}~\mbox{by}~AD_4,~\mbox{so that for some}~ e_1,
e_2, ~\mbox{and}~ e'_1,} \hspace{4em} \nonumber \\
& & e = \plus(e_1,e_2) ~\mbox{and}~ e' = \plus(e'_1,e_2)
~\mbox{and}~ \Trans{e_1}{e'_1}, \nonumber \\
& & \mbox{then}~ \underline{P(e_1,e'_1)} ~\Rightarrow~ P(e,e')
\end{eqnarray}
or equivalently
\begin{equation}
IC_4: \quad \forall e_1,e'_1,e_2 . ~ \Trans{e_1}{e'_1} \;\&\;
\underline{P(e_1,e'_1)} ~\Rightarrow ~ P(\plus(e_1,e_2), \plus(e'_1,e_2))
\end{equation}

\paragraph{Rule $AD_5$}
\begin{eqnarray}
\lefteqn{IC_5: \quad \forall e,e' . \, \mbox{if}~
\Trans{e}{e'}~\mbox{by}~AD_5,~\mbox{so that for some}~ n,
e_2, ~\mbox{and}~ e'_2,} \hspace{4em} \nonumber \\
& & e = \plus(\num[n],e_2) ~\mbox{and}~ e' = \plus(\num[n],e'_2)
~\mbox{and}~ \Trans{e_2}{e'_2}, \nonumber \\ 
& & \mbox{then}~ \underline{P(e_2,e'_2)} ~\Rightarrow~ P(e,e')
\end{eqnarray}
or equivalently
\begin{equation}
IC_5: \quad \forall n,e_2,e'_2 . ~ \Trans{e_2}{e'_2} \;\&\;
\underline{P(e_2,e'_2)} ~\Rightarrow ~P(\plus(\num[n],e_2), \plus(\num[n],e'_2))
\end{equation}

\paragraph{Rule $AD_6$} $IC_6$ is similar to $IC_4$ with $\Times$
substituted for $\plus$.

\paragraph{Rule $AD_7$} $IC_7$ is similar to $IC_5$ with $\Times$
substituted for $\plus$.

\paragraph{Rule $AD_8$} 
\begin{eqnarray}
\lefteqn{IC_8: \quad \forall e,e' . \, \mbox{if}~
\Trans{e}{e'}~\mbox{by}~AD_8,~\mbox{so that for some}~x, e_1,
e_2, ~\mbox{and}~ e'_1,} \hspace{4em} \nonumber \\
& & e = \Let(e_1,x.e_2) ~\mbox{and}~ e' = \Let(e'_1,x.e_2)
~\mbox{and}~ \Trans{e_1}{e'_1}, \nonumber \\
& & \mbox{then}~ \underline{P(e_1,e'_1)} ~\Rightarrow~ P(e,e')
\end{eqnarray}
or equivalently
\begin{equation}
IC_8: \quad \forall x,e_1,e'_1,e_2 . ~ \Trans{e_1}{e'_1} \;\&\;
\underline{P(e_1,e'_1)} ~\Rightarrow ~P(\Let(e_1,x.e_2), \Let(e'_1,x.e_2))
\end{equation}

\section{Example Proof}
Now let's use this induction principle for Arith+Let to do a
representative proof by Rule Induction over the rule set $AD_1$
through $AD_8$ defining the small step transition relation $\mapsto$.

\noindent
\textbf{Proposition:} 
$\forall e_1, e_2, e_3 . \; \Trans{e_1}{e_2} ~\&~ \Trans{e_1}{e_3}
\;\Rightarrow\; e_2 = e_3$

\noindent
\textbf{Proof:} We recast the statement of the proposition so that it
has the form of the conclusion of our Induction Principle (1), using
the property $P$ defined in (3). So our goal is to use the induction
principle to prove
\begin{equation}
\forall e, e' . \, \Trans{e}{e'} \Rightarrow (\forall
e''.\,\Trans{e}{e''} \;\Rightarrow\; e'' = e')
\end{equation}
The proof proceeds by cases, one case for each rule, or more precisely
for each inductive clause $IC_1$ through $IC_8$. Having proved each 
inductive clause, we can apply the Inductive Principle (4) to prove
the conclusion.

\noindent
\textbf{Case} $IC_1$. Assume that $e$ is such that
\begin{equation}\label{IC1}
\Trans{\plus(\num[m],\num[n])}{e}
\end{equation}
Only rules $AD_1$ or $AD_4$ or $AD_5$ could possibly derive (\ref{IC1}) because
only their conclusions match the form of the source expression
$\plus(\num[m],\num[n])$. But $AD_4$ cannot be used to derive
(\ref{IC1}) since $\num[m]$ is final, and similarly $AD_5$ cannot
be used because $\num[n]$ is final.

\noindent
Thus (\ref{IC1}) can only be derived by rule $AD_1$.
It follows that $e$ must be $\num[m + n]$.

\noindent
\textbf{Case} $IC_2$. The proof is similar to that of $IC_1$, replacing
$\plus$ with $\Times$ and $+$ with $\times$.

\noindent
\textbf{Case} $IC_3$. Assume that
\begin{equation}\label{IC1}
\Trans{\Let(\num[n],x.e_2)}{e}
\end{equation}
Only rules $AD_3$ or $AD_8$ could possibly apply because
only their conclusions match the form of the source expression
$\Let(\num[n],x.e_2)$. But $AD_8$ cannot be used to derive
(\ref{IC1}) since $\num[n]$ is final.

\noindent
Thus (\ref{IC1}) can only be derived by rule $AD_3$.
It follows that $e$ must be $\{\num{n}/x\}e_2$.

\noindent
\textbf{Case} $IC_4$. Assume that
\begin{equation}\label{IC4}
\Trans{\plus(e_1,e_2)}{\plus(e'_1,e_2)}
\end{equation}
by rule $AD_4$, implying that $\Trans{e_1}{e'_1}$. We can assume the
Induction Hypothesis $P(e_1,e'_1)$, \textit{i.e.}
\begin{equation}\label{IH4}
\forall e''.\,\Trans{e_1}{e''} \;\Rightarrow\; e'' = e'_1
\end{equation}
Now suppose that $e'$ is such that
\begin{equation}\label{hyp4}
\Trans{\plus(e_1,e_2)}{e'}
\end{equation}
Then (\ref{hyp4}) must be derived using either $AD_1$, $AD_4$, or
$AD_5$. But $AD_1$ and $AD_5$ are not possible because $e_1$ is not
final ($\Trans{e_1}{e'_1}$) and so
$e_1$ cannot be of the form $\num[n]$. Hence (\ref{hyp4}) must be
derived using $AD_4$, implying that there is an expression $e''_1$
such that $e' = \plus(e''_1,e_2)$ and $\Trans{e_1}{e''_1}$. But then
the Induction Hypothesis (\ref{IH4}) implies that $e''_1 = e'_1$,
which in turn implies that $e' = \plus(e'_1,e_2)$.

\noindent
\textbf{Case} $IC_5$. Assume that
\begin{equation}\label{IC5}
\Trans{\plus(\num[n],e_2)}{\plus(\num[n],e'_2)}
\end{equation}
by rule $AD_5$, implying that $\Trans{e_2}{e'_2}$. We can assume the
Induction Hypothesis $P(e_2,e'_2)$, \textit{i.e.}
\begin{equation}\label{IH5}
\forall e''.\,\Trans{e_2}{e''} \;\Rightarrow\; e'' = e'_2
\end{equation}
Now suppose that $e'$ is such that
\begin{equation}\label{hyp5}
\Trans{\plus(\num[n],e_2)}{e'}
\end{equation}
Then (\ref{hyp5}) must be derived using either $AD_1$, $AD_4$, or
$AD_5$. But $AD_1$ is not possible because $e_2$ is not
final ($\Trans{e_2}{e'_2}$) and so is
not of the form $\num[n]$, and $AD_4$ is not possible because
$\num[n]$ \emph{is} final.
Hence (\ref{hyp5}) must be
derived using $AD_5$, implying that there is an expression $e''_2$
such that $e' = \plus(\num[n],e''_2)$ and $\Trans{e_2}{e''_2}$. But then
the Induction Hypothesis (\ref{IH5}) implies that $e''_2 = e'_2$,
which in turn implies that $e' = \plus(\num[n],e'_2)$.

\noindent
\textbf{Case} $IC_6$. The proof is similar to that of $IC_4$, replacing
$\plus$ with $\Times$ and $+$ with $\times$.

\noindent
\textbf{Case} $IC_7$. The proof is similar to that of $IC_5$, replacing
$\plus$ with $\Times$ and $+$ with $\times$.

\noindent
\textbf{Case} $IC_8$. Assume that
\begin{equation}\label{IC8}
\Trans{\Let(e_1,x.e_2)}{\Let(e'_1,x.e_2)}
\end{equation}
by rule $AD_8$, implying that $\Trans{e_1}{e'_1}$. We can assume the
Induction Hypothesis $P(e_1,e'_1)$, \textit{i.e.}
\begin{equation}\label{IH8}
\forall e''.\,\Trans{e_1}{e''} \;\Rightarrow\; e'' = e'_1
\end{equation}
Now suppose that $e'$ is such that
\begin{equation}\label{hyp8}
\Trans{\Let(e_1,x.e_2)}{e'}
\end{equation}
Then (\ref{hyp8}) must be derived using either $AD_3$ or
$AD_8$. But $AD_1$ is not possible because $e_1$ is not
final ($\Trans{e_1}{e'_1}$) and so is not of the form $\num[n]$.
Hence (\ref{hyp8}) must be
derived using $AD_8$, implying that there is an expression $e''_1$
such that $e' = \Let(e''_1,x.e_2)$ and $\Trans{e_1}{e''_1}$. But then
the Induction Hypothesis (\ref{IH8}) implies that $e''_1 = e'_1$,
which in turn implies that $e' = \plus(e'_1,e_2)$.

\noindent
\textit{QED}

\section{A More Informal Proof}
Lets now look at a more conventional, semi-formal way of presenting
the same proof (roughly comparable to the style of proof found in
Harper's text and the research literature). In such a proof, the
the Induction Principle is assumed but not made explicit, and
sometimes the induction hypothesis for an inductive case is also not
stated explicitly, but instead is refered to by the phrase ``by induction''.
We'll just give a couple representative cases for this proof.

\noindent
\textbf{Proof:} We proceed by rule induction on the hypothesis
$\Trans{e_1}{e_2}$.

\noindent
\textbf{Case:} $\Trans{e_1}{e_2}$ by Rule $AD_1$.
Then
\begin{eqnarray}
e_1 & = & \plus(\num[m],\num[n]) \quad \mbox{and} \\
e_2 & = & \num[m+n]
\end{eqnarray}
If $\Trans{e_1}{e'}$ for some expression $e'$, this must be derived
using a Rule matching $e_1$. But the only such rule is $AD_1$, because
the fact that $\num[m]$ and $\num[n]$ are final rules out $AD_4$ and $AD_5$.
But if $\Trans{e_1}{e'}$ by rule $AD_1$, it is clear that $e' =
\num[m+n]$, and hence $e' = e_2$.

\noindent
\textbf{Case:} $\Trans{e_1}{e_2}$ by Rule $AD_4$.
Then
\begin{eqnarray}
e_1 & = & \plus(e_{1,1},e_{1,2}) \quad \mbox{and} \\
e_2 & = & \plus(e'_{1,1},e_{1,2})
\end{eqnarray}
where
\begin{equation}\label{e11trans}
\Trans{e_{1,1}}{e'_{1,1}}
\end{equation}
Suppose that for some $e'$,
\begin{equation}\label{e1trans2}
\Trans{e_1}{e'}
\end{equation}
Since $e_{1,1}$ cannot be a number expression because of
(\ref{e11trans}), the only rule that could derive (\ref{e1trans2}) is
$AD_4$, which implies that $e' = \plus(e'_1,e_{1,2})$ for some $e'_1$
such that $\Trans{e_{1,1}}{e'_1}$. But \emph{by induction}, $e'_{1,1}$
is the unique expression such that (\ref{e11trans}) holds, and
therefore we must have $e'_1 = e'_{1,1}$, and hence $e' = e_2$.

\section{Appendix: Static Semantics for Arith with Let}
Just for completeness, we include the static semantics for Arith with
Let. 

\noindent
The judgement $\OkG{e}$ expresses the fact that $e$ is well-formed
with free variables contained in the set $\Gamma$.
\vspace{-1.5ex}
\begin{center}
  \begin{tabular}{p{2.5in}@{}p{2.5in}}
    \begin{displaymath}
     \inferl{AS_1}{\OkG{x}}{(x \in \Gamma)}
    \end{displaymath}
  &
    \begin{displaymath}
      \inferl{AS_2}{\OkG{\num[n]}}{(n \ge 0)}
    \end{displaymath}
  \\
    \begin{displaymath}
      \inferl{AS_3}{\OkG{\plus(e_1,e_2)}}
	{\OkG{e_1} \qquad \OkG{e_2}}
    \end{displaymath}
  &
    \begin{displaymath}
      \inferl{AS_4}{\OkG{\times(e_1,e_2)}}
	{\OkG{e_1} \qquad \OkG{e_2}}
    \end{displaymath}
  \\
    \multicolumn{2}{p{5.0in}}{
    \begin{displaymath}
      \inferl{AS_5}{\OkG{\Let(e_1,\,x.e_2)}}
	{\OkG{e_1} \qquad \Ok{\Gamma \cup \{x\}}{e_2} \qquad
	(x \not\in \Gamma)}
    \end{displaymath}}
  \end{tabular}
\end{center}


\end{document}
