\section{Structural Induction}

\hyperdef{recursive}{data}{
\subsection{Recursive Data Types}
}

\emph{Recursive data types} play a central role in programming.  From a
Mathematical point of view, recursive data types are what induction is
about.  Recursive data types are specified by \emph{recursive definitions}
that say how to build something from its parts.  These definitions have
two parts:
\begin{itemize}
\item \textbf{Base case(s)} that don't depend on anything else.
\item \textbf{Constructor case(s)} that depend on previous cases.
\end{itemize}

\hyperdef{paren}{string}{\subsection{Strings of Parentheses}}

Let $\prns$ be the set of all strings of parentheses.  For example,
the following two strings are in $\prns$:
\begin{equation}\label{2strings}
\mtt{())((((())}\quad \text{and}\quad \mtt{((())())()}
\end{equation}
Since we're just starting to study recursive data, just for practice we'll
formulate $\prns$ as a recursive data type,

\begin{definition}\label{prns-def}
The data type, $\prns$, of strings of parentheses is defined recursively:

\begin{itemize}

\item \textbf{Base case:} The \term{empty string}, $\emptystring$, is in
  $\prns$.

\item \textbf{Constructor case:} If $s \in \prns$, then
$s\mtt{)}$ and $s\mtt{(}$ are in $\prns$.

\end{itemize}

\end{definition}

Here we're writing $s\mtt{)}$ to indicate the string that is sequence of
parentheses (if any) in the string $s$, followed by a right parenthesis;
similarly for $s\mtt{(}$.


A string, $s \in \prns$, a called a \term{matched string} if its
parentheses ``match up'' in the usual way.  For example, the left hand
string above is not matched because its second right parenthesis does not
have a matching left parenthesis.  The string on the right is matched.

One precise way to determine if a string is matched is to start with 0 and
read the string from left to right, adding 1 to the count for each left
parenthesis and subtracting 1 from the count for each right parenthesis.
For example, here are the counts for the two strings above
\[\begin{array}{rrrrrrrrrrrrr}
& \mtt{(} & \mtt{)} & \mtt{)} & \mtt{(} & \mtt{(} & \mtt{(} & \mtt{(} &
\mtt{(} & \mtt{)} & \mtt{)} & \mtt{)} & \mtt{)}\\
0 & 1 & 0 & -1 & 0 & 1 & 2 & 3 & 4 & 3 & 2 & 1 & 0\\
\\
\\
& \mtt{(} & \mtt{(} & \mtt{(} & \mtt{)} & \mtt{)} & \mtt{(} & \mtt{)} &
\mtt{)} & \mtt{(} & \mtt{)}\\
0 & 1 & 2 & 3 & 2 & 1 & 2 & 1 & 0 & 1 & 0
\end{array}\]
A string has a \term{good count} if its running count never goes
negative and ends with 0.  So the second string above has a good count, but
the first one does not because its count went negative at the third step.
\begin{definition}\label{gc-def}
Let
\[
\GC \eqdef \set{ s \in \prns \suchthat s\ \text{has a good count}}.
\]
\end{definition}
The matched strings can now be characterized precisely as this set of
strings with good counts.  But it turns out to be really useful to
characterize the matched strings in another way as well, namely, as a
recursive data type:

\begin{definition}\label{RM-def}
Recursively define the set, $\RM$, of strings as follows:
\begin{itemize}

\item \textbf{Base case:} $\emptystring \in\RM$.

\item \textbf{Constructor case:} If $s,t \in\RM$, then
\[
\mtt{(}s\mtt{)}t \in\RM.
\]

\end{itemize}

\end{definition}


Here we're writing $\mtt{(}s\mtt{)}t$ to indicate the string that
starts with a left parenthesis, followed by the sequence of parentheses
(if any) in the string $s$, followed by a right parenthesis, and ending
with the sequence of parentheses in the string $t$.

Using this definition, we can see that $\emptystring \in\RM$ by the Base
case, so
\[
\mtt{(}\emptystring\mtt{)}\emptystring=\mtt{()}\in\RM
\]
by the Constructor case.  So now,
\begin{align*}
\mtt{(}\emptystring\mtt{)}\mtt{()} &= \mtt{()()} \in \RM
    & \text{(letting $s = \emptystring, t = \mtt{()}$)}\\
\mtt{(())}\emptystring & = \mtt{(())} \in \RM
    & \text{(letting $s = \mtt{()}, t = \emptystring$)}\\
&\ \ \mtt{(())()} \in \RM
    & \text{(letting $s = \mtt{()}, t = \mtt{()}$)}
\end{align*}
are also strings in $\RM$ by repeated applications of the Constructor
case.

\textbf{Quickie:} Verify that $\mtt{((())())()} \in \RM$.

It may not be obvious, but $\RM = \GC$.  We'll confirm this later.

\subsection{Arithmetic Expressions}
Expression evaluation is a key feature of programming languages, and
recognition of expressions as a recursive data type is a key to
understanding how they can be processed.

To illustrate this approach we'll work with a toy example: arithmetic
expressions like $3x^2 + 2x + 1$ involving only one variable, ``$x$.''
We'll refer to the data type of such expressions as $\aexp$.  Here is its
definition:

\begin{definition}\label{A}
The set, $\aexp$, of \emph{Arithmetic expressions} in the variable, $x$,
is defined recursively as follows:

\begin{itemize}
\item \textbf{Base cases:}

\begin{enumerate}

\item The variable, $x$, is in $\aexp$.

\item The arabic numeral, $\mtt{k}$, for any nonnegative integer, $k$, is
  in $\aexp$.

\end{enumerate}

\item \textbf{Constructor cases:} If $e,f \in \aexp$, then
\begin{enumerate}
\setcounter{enumi}{2}

\item $(e \sumsym f) \in \aexp$.  The expression $(e \sumsym f)$ is called a
  \term{sum}.  The \aexp's $e$ and $f$ are called the \term{components} of
  the sum; they're also called the \term{summands}.

\item $(e \prodsym f) \in \aexp$.  The expression $(e \prodsym f)$ is called a
  \term{product}.  The \aexp's $e$ and $f$ are called the
  \term{components} of the product; they're also called the
  \term{multiplier} and \term{multiplicand}.

\item $\minussym(e) \in \aexp$.  The expression $\minussym(e)$ is called a
  \term{negative}.
\end{enumerate}
\end{itemize}
\end{definition}

Notice that \aexp's are fully parenthesized, and exponents aren't allowed.
So the $\aexp$ version of the polynomial expression $3x^2 + 2x + 1$ would
officially be written as
\begin{equation}\label{fullparens}
((\mtt{3} \prodsym (x \prodsym x)) \sumsym ((\mtt{2} \prodsym x) \sumsym \mtt{1})).
\end{equation}
These parentheses and $\ast$'s clutter up examples, so we'll often use
simpler expressions like ``$3x^2 + 2x + 1$'' instead
of~\eqref{fullparens}.  But it's important to recognize that $3x^2 + 2x +
1$ is not an \aexp; it's an \emph{abbreviation} for an $\aexp$.

\subsection{The Nonnegative Integers}

The nonnegative integers can be understood as a recursive data type.
\begin{definition}\label{0succ}
The set, $\naturals$, is a data type defined recursivly as:
\begin{itemize}
\item $0 \in \naturals$.
\item If $n \in \naturals$, then the \emph{successor}, $n+1$, of $n$ is in
$\naturals$.
\end{itemize}

\end{definition}

\iffalse

 being represented as
a tagged datum.  To start, we might represent 0 as a length one sequence
consisting of the tag \texttt{zero}:
\begin{definition}
The nonnegative integers can be defined recursively as follows:

\begin{definition}\label{tagn}
\begin{itemize}
\item \textbf{Base case}  $\ang{\texttt{zero}}\in \naturals$.
\item \textbf{Constructor case} if $n \in \naturals$, then
      $\ang{\texttt{successor},n}\in \naturals$.
\end{itemize}

\end{definition}
\fi


\iffalse
\begin{example}
The set, $\List$, of \emph{pure lists} is defined recursively by:
\begin{enumerate}
\item The 0-tuple, $\nillist$, is in $\List$.
\item If $\ell_1$ and $\ell_2$ are in $\List$, then the pair $(\ell_1,
\ell_2)$ is in $\List$.
\end{enumerate}

In Lisp-like programming languages, the pairing operation is called
\texttt{cons} and the 0-tuple is called \texttt{nil}.

\end{example}
\fi

\subsection{Structural Induction on Recursive Data Types}

\hyperdef{struct}{induction}{Structural} induction is a method for proving
some property, $P$, of all the elements of a recursively-defined data
type.  The proof consists of two steps:
\begin{itemize}
\item Prove $P$ for the base cases of the definition. 
\item Prove $P$ for the constructor cases of the definition, assuming that it
  is true for the component data items.  
\end{itemize}

A very simple application of structural induction proves that the
recursively defined matched strings always have an equal number of left
and right parentheses.  To do this, define a predicate, $P$, on strings $s
\in \prns$:
\[
P(s) \eqdef\ \ s \text{ has an equal number of left and right parentheses}.
\]
\begin{proof}

  We'll prove that $P(s)$ holds for all $s \in\RM$ by structural induction
  on the definition that $s \in\RM$, using $P(s)$ as the induction
  hypothesis.

\textbf{Base case:} $P(\emptystring)$ holds because the empty string has zero
left and zero right parentheses.

\textbf{Constructor case:} For $r = \mtt{(}s\mtt{)}t$, we must show
that $P(r)$ holds, given that $P(s)$ and $P(t)$ holds.  So let $n_s$,
$n_t$ be, respectively, the number of left parentheses in $s$ and $t$.  So
the number of left parentheses in $r$ is $1+n_s+n_t$.

Now from the respective hypotheses $P(s)$ and $P(t)$, we know that the
number of right parentheses in $s$ is $n_s$, and likewise, the number of
right parentheses in $t$ is $n_t$.  So the number of right parentheses in
$r$ is $1+n_s+n_t$, which is the same as the number of left parentheses.
This proves $P(r)$.  We conclude by structural induction that $P(s)$ holds
for all $s \in\RM$.
\end{proof}

\begin{notesproblem}
\bparts
\ppart Give an easy proof using structural induction that every recursively
defined match string has a good count.  That is
\[
\RM \subseteq \GC.
\]
\ppart Conversely, prove by induction on the length of strings that the
every string with a good count has a recursive definition, that is,
\[
\GC \subseteq \RM.
\]

\eparts
\end{notesproblem}

By the way, you should notice that ordinary induction is simply the
special case of structural induction on the recursive
Definition~\ref{0succ} of $\naturals$!

\subsection{Functions on Recursively-defined Data Types}

Functions on recursively-defined data types can be defined recursively
using the same cases as the data type definition.  Namely, to define a
function, $f$, on a recursive data type, define the value of $f$ for the
base cases of the data type definition, and then define the value of $f$
in each constructor case in terms of the values of $f$ on the component
data items.

\iffalse

For example, some basic functions on strings have simple recursive
definitions based on a recursive definition of strings as a tagged datum:

\begin{definition}\label{A*}
The set, $A^*$, of strings over a set, $A$, called the \emph{alphabet},
is defined recursively as follows:
\begin{itemize}
\item \textbf{Base case:} $\ang{\texttt{emptystring}} \in A^*$.

\item \textbf{Constructor case:} if $s \in A^*$ and $a \in A$, then
$\ang{\texttt{successor-string},s,a}\in A^*$.

\end{itemize}
\end{definition}
Here, of course, $\ang{\texttt{emptystring}}$ is a tagged representation
of the emptystring, $\emptystring$, and
\[
\ang{\texttt{successor-string}, s, a}
\]
is a tagged representation of the string, $sa$, equal to the string $s$,
followed by the character, $a$.

Now we give a recursive definition of the \emph{length} of a string.
\begin{definition}
The \emph{length}, $\lnth{s}$, of a string, $s$, is defined recursively by
the rules:
\begin{itemize}
\item $\lnth{\emptystring} \eqdef 0$
\item $\lnth{sa} \eqdef 1+\lnth{s}$.
\end{itemize}
\end{definition}

\begin{definition}
The \emph{concatenation}, $st$, of strings $s$ and $t$ over an alphabet,
$A$, is defined recursively on $t$ by the rules:
\begin{itemize}
\item $s\emptystring \eqdef s$.
\item $s(ta) \eqdef (st)a$ for $a \in A$.
\end{itemize}
\end{definition}
\fi

For example, from the recursive definition of the set, $\RM$, of strings of
matched parentheses, we define:
\begin{definition}
The \emph{depth}, $d(s)$, of a string, $s \in\RM$, is defined
recursively by the rules:
\begin{itemize}
\item $d(\emptystring) \eqdef 0.$
\item $d(\mtt{(}s\mtt{)}t)
    \eqdef \max \set{d(s) + 1, d(t)}$
\end{itemize}
\end{definition}

\textbox{\textbf{Warning:} When a recursive definition of a data type
allows the same element to be constructed in more than one way, the
definition is said to be \emph{ambiguous}.  A function defined recursively
from an ambiguous definition of a data type will not be well-defined
unless the values specified for the different ways of constructing the
element agree.}

We were careful to choose an \emph{un}ambiguous definition of $\RM$ to
ensure that functions defined recursively on the definition would always
be well-defined.  As an example of the trouble an ambiguous definition can
cause, let's consider yet another definition of the matched strings.

\iffalse Recursive definitions of tagged data types, where the tag
uniquely determines the rule used to construct an element, are guaranteed
to be unambiguous.
\fi

\begin{example}\label{M}
  Define the set, $M \subseteq \prns$ recursively as follows:
\begin{itemize}

\item \textbf{Base case:} $\emptystring \in M$,

\item \textbf{Constructor cases:} if $s,t \in M$, then
the strings $\mtt{(}s\mtt{)}$ and $st$ are also in $M$.
\end{itemize}
\end{example}

\begin{notesproblem}
Give an easy proof by structural induction that $M =\RM$.
\end{notesproblem}

Since $M = \RM$, and the definition of $M$ seems more straightforward, why
didn't we use it?  Because the definition of $M$ is ambiguous, while the
trickier definition of $\RM$ is unambiguous.  Does this ambiguity matter?
Yes it does.  For suppose we defined
\begin{align*}
  f(\emptystring)        & \eqdef 1,\\
  f(\ \mtt{(}s\mtt{)}\ ) & \eqdef 1+ f(s),\\
  f(st)                  & \eqdef (f(s)+1) \cdot (f(t)+1)
                            & \text{for } st\neq \emptystring.
\end{align*}

Let $a$ be the string $\mtt{(())} \in M$ built by two successive
applications of the first $M$ constructor starting with $\emptystring$.  Next
let $b \eqdef aa$ and $c \eqdef bb$, each built by successive applications
of the second $M$ constructor starting with $a$.

Alternatively, we can build $ba$ from the second constructor with $s=b$
and $t=a$, and then get to $c$ using the second constructor with $s=ba$
and $t=a$.

Now by these rules, $f(a) = 2$, and $f(b) = (2+1)(2+1)=9$.  This means
that $f(c) = f(bb)= (9+1)(9+1)=100$.

But also $f(ba) = (9+1)(2+1) = 27$, so that $f(c) = f(ba\,a) = (27 +1)
(2+1) = 84$.

The outcome is that $f(c)$ is defined to be both 100 and 84, which shows
that the rules defining $f$ are inconsistent.

On the other hand, structural induction remains a sound proof method even
for ambiguous recursive definitions, which is why it was easy to prove
that $M=\RM$.

\subsection{Recursive Functions on Nonnegative Integers}

Definition~\ref{0succ} of the nonnegative integers as a recursive data
type justifies the familiar recursive definitions of functions on the
nonnegative integers.  Here are some examples.

\begin{description}
\item[The Factorial function.] This function is often written ``$n!$.''
You will see a lot of it later in the term.  Here we'll use the notation
$\text{fac}(n)$:
\begin{itemize}
\item $\text{fac}(0) \eqdef 1$.
\item $\text{fac}(n+1) \eqdef (n+1)\cdot \text{fac}(n)$ for $n \ge 0$.
\end{itemize}

\item[The Fibonacci numbers.]  Fibonacci numbers arose out of an effort 800
  years ago to model population growth.  They have a continuing fan club of
  people captivated by their extraordinary properties.  The $n$th Fibonacci
  number, $\text{fib}$, can be defined recursively by:
\begin{align*}
\text{fib}(0) &\eqdef 0,\\ 
\text{fib}(1) &\eqdef 1,\\ 
\text{fib}(n) &\eqdef \text{fib}(n-1) + \text{fib}(n-2) &\mbox{for $n \geq 2$.} 
\end{align*}
Here the recursive step starts at $n=2$ with base cases for 0 and 1.  This
is needed since the recursion relies on two previous values.

\iffalse
What is $\text{fib}(4)$?  Well, $\text{fib}(2) =
\text{fib}(1)+\text{fib}(0) = 1$, $\text{fib}(3) =
\text{fib}(2)+\text{fib}(1) = 2$, so $\text{fib}(4) = 3$.  The sequence
starts out $0, 1, 1, 2, 3, 5, 8, 13, 21,\dots$.
\fi

\item[Sum-notation.]  Let ``$S(n)$'' abbreviate the expression
``$\sum_{i=1}^n f(i)$.''  We can recursively define $S(n)$ with the rules
  \begin{itemize}
  \item $S(0) \eqdef 0$.
  \item $S(n+1) \eqdef  f(n+1) + S(n)$ for $n\geq 0$.
  \end{itemize}

\iffalse
\item[Simultaneous recursive definitions:]
  You can define several things at the same time, in terms of each
  other.  For example, we may define two functions $f$ and $g$ from
  $\naturals$ to $\naturals$, recursively, by:
  \begin{itemize}
  \item
    $f(0) \eqdef 1$,
  \item
    $g(0) \eqdef 1$,
  \item
    $f(n+1) \eqdef f(n) + g(n)$, for $n \geq 0$,
  \item
    $g(n+1) \eqdef f(n) \times g(n)$, for $n \geq 0$.
  \end{itemize}
\fi

\end{description}

\iffalse

\begin{optional}

We can use the recursive definition of a function to establish its
properties by structural induction.

As an illustration, we'll prove a cute identity involving Fibonacci
numbers.  Fibonacci numbers provide lots of fun for mathematicians because
they satisfy many such identities.
\begin{proposition}
  $\forall n \geq 0 (\Sigma_{i=0}^n F_i^2 = F_n F_{n+1})$.
\end{proposition}

Example: $n = 4$:
\[
0^2 + 1^2 + 1^2 + 2^2 + 3^2 = 15 = 3 \cdot 5.
\]
Let's try a proof by (standard, not strong) induction.  The theorem
statement suggests trying it with $P(n)$ defined as:
\[
\sum_{i=0}^n F_i^2 = F_n F_{n+1}.
\]

\textbf{Base case} ($n=0$). 
$\Sigma_{i=0}^0 F_i^2 \eqdef (F_0)^2 = 0 = F_0 F_1$ because
$F_0 \eqdef 0$.

\textbf{Inductive step} ($n\geq 0$).  Now we stare at the gap between
$P(n)$ and $P(n+1)$.  $P(n+1)$ is given by a summation that's obtained
from that for $P(n)$ by adding one term; this suggests that, once again,
we subtract.  The difference is just the term $F_{n+1}^2$.  Now, we are
assuming that the original $P(n)$ summation totals $F_n F_{n+1}$ and want
to show that the new $P(n+1)$ summation totals $F_{n+1} F_{n+2}$.  So we
would {\em like\/} the difference to be
\[
F_{n+1} F_{n+2} - F_n F_{n+1}.
\]

So, the actual difference is $F_{n+1}^2$ and the difference we want is
$F_{n+1} F_{n+2} - F_n F_{n+1}$.  Are these the same?  We want to check
that:
\[
F_{n+1}^2 = F_{n+1} F_{n+2} - F_n F_{n+1}.
\]
But this is true, because it is really the Fibonacci definition in
disguise: to see this, divide by $F_{n+1}$.

\end{optional}
\fi

\subsubsection{Ill-formed Function Definitions}

There are some \hyperdef{ill}{formed}{blunders} to watch out for when
defining functions recursively.  Below are some function specifications
that resemble good definitions of functions on the nonnegative integers,
but they aren't.

\begin{eqnarray}\label{f1}
f_1(n)\eqdef 2+f_1(n-1).
\end{eqnarray}
This ``definition'' has no base case.  If some function, $f_1$,
satisfied~(\ref{f1}), so would a function obtained by adding a constant to
the value of $f_1$.  So equation~(\ref{f1}) does not uniquely define
an $f_1$.

\begin{eqnarray}\label{f2}
f_2(n) \eqdef
\begin{cases}
 0, & \text{if $n=0$},\\
 f_2(n+1) &  \text{otherwise}.
\end{cases}
\end{eqnarray}
This ``definition'' has a base case, but still doesn't uniquely determine
$f_2$.  Any function that is 0 at 0 and constant everywhere else would
satisfy the specification, so~\eqref{f2} also does not uniquely define
anything.

In a typical programming language, evaluation of $f_2(1)$ would begin with
a recursive call of $f_2(2)$, which would lead to a recursive call of
$f_2(3)$, \dots with recursive calls continuing without end.  This
``operational'' approach interprets~\eqref{f2} as defining a
\emph{partial} function, $f_2$, that is undefined everywhere but 0.

\begin{eqnarray}\label{f3}
f_3(n) \eqdef \begin{cases}
  0, &  \text{if $n$ is divisible by 2,}\\
  1, &  \text{if $n$ is divisible by 3,}\\
  2, & \text{otherwise.}
 \end{cases}
\end{eqnarray}
This ``definition'' is inconsistent: it requires $f_3(6) = 0$ and $f_3(6)
=1$, so~(\ref{f3}) doesn't define anything.

\subsubsection{A Mysterious Function}
Mathematicians have been wondering about this function specification for a
while:
\begin{eqnarray}\label{f5}
f_4(n) \eqdef\begin{cases}
 1, & \text{if $n\le 1$},\\
 f_4(n/2) &  \text{if $n>1$ is even},\\
 f_4(3n+1)& \text{if $n>1$ is odd}.
\end{cases}
\end{eqnarray}
For example, $f_4(3)=1$ because
\[
f_4(3)\eqdef f_4(10)\eqdef f_4(5)\eqdef f_4(16)\eqdef f_4(8)\eqdef
f_4(4)\eqdef f_4(2)\eqdef f_4(1)\eqdef 1.
\]
The constant function equal to 1 will satisfy~\eqref{f5}, but it's not
known if another function does too.  The problem is that the third case
specifies $f_4(n)$ in terms of $f_4$ at arguments larger than $n$, and so
cannot be justified by induction on $\naturals$.  It's known that any
$f_4$ satisfying~\eqref{f5} equals 1 for all $n$ up to over a billion.

\textbf{Quick exercise:} Why does the constant function 1
satisfy~\eqref{f5}?

\iffalse

\section{Tagged data}

Labelling a recursively defined data item with a tag that uniquely
determines the rule used to construct it is a standard approach to avoiding
unambiguous recursive definitions in programming.

For example, arithmetic expressions like
\begin{equation}\label{ax}
-(a(x\cdot x)+ bx) + 1
\end{equation}
are another important example of a recursive data type.  We could define
them as parenthesized strings with symbols for arithmetic operators and
names for variables and constants, but a tagged representation is more
useful:

\begin{definition}\label{A}
The set, $\aexp$, of \emph{Arithmetic expressions} over a set of
\emph{variables}, $V$, is defined recursively as follows:
\begin{itemize}
\item \textbf{Base cases:}
\begin{enumerate}
\item If $n \in \integers$, then $\ang{\texttt{int}, n} \in \aexp$.
\item If $v \in V$, then $\ang{\texttt{var}, v} \in \aexp$.
\end{enumerate}
\item \textbf{Constructor cases:} if $e,e' \in \aexp$, then
\begin{enumerate}
\item $\ang{\texttt{sum}, e, e'} \in \aexp$,
\item $\ang{\texttt{prod}, e, e'} \in \aexp$, and
\item $\ang{\texttt{minus}, e} \in \aexp$.
\end{enumerate}
\end{itemize}
\end{definition}

So the $\aexp$ corresponding to formula~\ref{ax} would be:
\begin{equation}\label{axtag}
\begin{array}{rll}
\left< \right. \texttt{sum}, 
         & \left< \right. \texttt{minus},\ \ \left< \right. \texttt{sum},
               & \ang{\texttt{prod},\ \ \ang{\texttt{var},\ a},
                                     \ang{\texttt{prod},\ \
                                            \ang{\texttt{var},\ x},\
                                            \ang{\texttt{var},\ x}}},\\
                               && \left. \left. \ang{\texttt{prod},\ \
                                       \ang{\texttt{var},\ b},\
                                       \ang{\texttt{var},\ x}}
                                   \right> \right>,\\
         & \left. \left. \ang{\texttt{int},\ 1} \right> \right>
\end{array}
\end{equation}
Now the expression~\ref{ax} is certainly a lot more humanly intelligible
than~\ref{axtag}, but is in fact the preferred representation in
programming.

the parse tree of Figure~\ref{fig:parse} is

uses the \emph{parse trees} of the expressions,
rather than strings.  Figure~\ref{fig:parse} shows a
parse tree for expression~\eqref{ax}.

\begin{figure}[htbp]
\centering \includegraphics[height=4.5in]{figures/parsetree.pdf}
\caption{Parse tree for $-(a(x\cdot x)+ bx) + 1$.}
\label{fig:parse}
\end{figure}


Such a tree would be represented by pairs or triples that begin with a
\emph{tag} equal to the label of the top node of the parse tree.  We'll
call these tagged data items $\aexp$'s.  
\fi


\subsection{Evaluation and Substitution with Aexp's}

\subsubsection{Evaluating Aexp's}

Since the only variable in an \aexp\ is $x$, the value of an \aexp\ is
determined by the value of $x$.  For example, if the value of $x$ is 3,
then the value of $3x^2 + 2x + 1$ is obviously 34.  In general, given any
$\aexp$, $e$, and an integer value, $n$, for the variable, $x$, we can
evaluate $e$ to finds its value, $\meval(e,n)$.  It's easy, and useful, to
specify this evaluation process with a recursive definition.

\begin{definition}\label{meval-def}
  The \term{evaluation function}, $\meval: \aexp \times \integers \to
  \integers$, is defined recursively on expressions, $e \in \aexp$, as
  follows.  Let $n$ be any integer.

\begin{itemize}
\item \textbf{Base cases:}

\begin{enumerate}

\item\label{eval-var} Case[$e$ is $x$]
\[
\meval(x, n) \eqdef n.
\]
(The value of the variable, $x$, is given to be $n$.)

\item\label{eval-const} Case[$e$ is $\mtt{k}$]
\[
\meval(\mtt{k}, n) \eqdef k.
\]
(The value of the numeral $\mtt{k}$ is the integer $k$, no matter what
value $x$ has.)

\end{enumerate}

\item \textbf{Constructor cases:}

\begin{enumerate}
\setcounter{enumi}{2}

\item\label{eval-sum} Case[$e$ is $(e_1 \sumsym e_2)$]
\[
\meval((e_1 \sumsym e_2),n) \eqdef
  \meval(e_1,n)+\meval(e_2,n).
\]

\item\label{eval-prod} Case[$e$ is $(e_1 \prodsym e_2)$]
\[
\meval((e_1 \prodsym e_2),n) \eqdef \meval(e_1,n) \cdot \meval(e_2,n).
\]

\item\label{eval-minus} Case[$e$ is $\minussym(e_1)$]
\[
\meval(\minussym(e_1),n) \eqdef - \meval(e_1,n).
\]
\end{enumerate}

\end{itemize}

\end{definition}

For example, here's how the recursive definition of $\meval$ would arrive at
the value of $3+x^2$ when $x$ is 2:
\begin{align*}
\meval((\mtt{3} \sumsym (x \prodsym x)),2)
 & = \meval(\mtt{3},2) + \meval((x \prodsym x),2)
                  & \text{(by~Def~\ref{meval-def}.\ref{eval-sum})}\\
 & = 3 + \meval((x \prodsym x),2) & \text{(by~Def~\ref{meval-def}.\ref{eval-const})}\\
 & = 3 + (\meval(x,2) \cdot \meval(x,2)) & \text{(by~Def~\ref{meval-def}.\ref{eval-prod})}\\
 & = 3 + (2 \cdot 2) & \text{(by~Def~\ref{meval-def}.\ref{eval-var})}\\
 & = 3 + 4 = 7.
\end{align*}

\subsubsection{Substituting into Aexp's}
Substituting expressions for variables is a standard, important
operation.  For example the result of substituting the expression $3x$ for $x$
in the $(x(x-1))$ would be $(3x(3x-1)$.  We'll use the general
notation $\msubst{f}{e}$ for the the result of substituting an $\aexp$, $f$,
for each of the $x$'s in an $\aexp$, $e$.  For instance,
\[
\msubst{3x}{x(x-1)} = 3x(3x-1).
\]

This substitution function has a simple recursive definition:

\begin{definition}\label{subst-def}
  The \term{substitution function} from $\aexp \times \aexp$ to \aexp\ is
  defined recursively on expressions, $e \in \aexp$, as follows.  Let $f$
  be any $\aexp$.

\begin{itemize}
\item \textbf{Base cases:}

\begin{enumerate}

\item\label{subst-var} Case[$e$ is $x$]
\[
\msubst{f}{x} \eqdef f.
\]
(The result of substituting $f$ for the variable, $x$, is just $f$.)

\item\label{subst-const} Case[$e$ is $\mtt{k}$]
\[
\msubst{f}{\mtt{k}} \eqdef \mtt{k}.
\]
(The numeral, $\mtt{k}$, has no $x$'s in it to substitute for.)

\end{enumerate}

\item \textbf{Constructor cases:}

\begin{enumerate}
\setcounter{enumi}{2}
\item\label{subst-sum} Case[$e$ is $(e_1 \sumsym e_2)$]
\[
\msubst{f}{(e_1 \sumsym e_2)}) \eqdef  (\msubst{f}{e_1} \sumsym
\msubst{f}{e_2}).
\]

\item\label{subst-prod} Case[$e$ is $(e_1 \prodsym e_2)$]
\[
\msubst{f}{(e_1 \prodsym e_2)}) \eqdef  (\msubst{f}{e_1} \prodsym
\msubst{f}{e_2}).
\]

\item\label{subst-minus} Case[$e$ is $\minussym(e_1)$]
\[
\msubst{f}{\minussym(e_1)} \eqdef \minussym (\msubst{f}{e_1}).
\]

\end{enumerate}
\end{itemize}
\end{definition}

Here's how the recursive definition of the substitution function would find
the result of substituting $3x$ for $x$ in the $x(x-1)$:
\begin{align*}
\msubst{3x}{(x(x-1))} & =
\msubst{3x}{(x \prodsym (x \sumsym \minussym(1)))} & \text{(unabbreviating)}\\
 & = (\msubst{3x}{x} \prodsym \msubst{3x}{(x \sumsym \minussym(1))})
         & \text{(by~Def~\ref{subst-def}~\ref{subst-prod})}\\
 & = (3x \prodsym \msubst{3x}{(x \sumsym \minussym(1))})
         & \text{(by~Def~\ref{subst-def}~\ref{subst-var})}\\
 & = (3x \prodsym (\msubst{3x}{x} \sumsym \msubst{3x}{\minussym(1)}))
         & \text{(by~Def~\ref{subst-def}~\ref{subst-sum})}\\
 & = (3x \prodsym (3x \sumsym \minussym (\msubst{3x}{1})))
         & \text{(by~Def~\ref{subst-def}~\ref{subst-var} \&~\ref{subst-minus})}\\
 & = (3x \prodsym (3x \sumsym \minussym (1)))
         & \text{(by~Def~\ref{subst-def}~\ref{subst-const})}\\
 & = 3x(3x-1) & \text{(abbreviation)}
\end{align*}

Now suppose we have to find the value of $\msubst{3x}{(x(x-1))}$ when $x =
2$.  There are two approaches.

First, we could actually do the substitution above to get $3x(3x-1)$, and
then we could evaluate $3x(3x-1)$ when $x =2$, that is, we could
recursively calculate $\meval(3x(3x-1),2)$ to get the final value 30.  In
programming jargon, this would be called evaluation using the
\emph{Substitution Model}.  Tracing through the steps in the evaluation,
we find that the Substitution Model requires two substitutions for
occurrences of $x$ and 5 integer operations: 3 integer multiplications, 1
integer addition, and 1 integer negative operation.  Note that in this
Substitution Model the multiplication $3 \cdot 2$ was performed twice to
get the value of 6 for each of the two occurrences of $3x$.

The other approach is called evaluation using the \emph{Environment
  Model}.  Namely, we evaluate $3x$ when $x = 2$ using just 1
multiplication to get the value 6.  Then we evaluate $x(x-1)$ when $x$ has
this value 6 to arrive at the value $6\cdot 5=30$.  So the Environment
Model requires 2 variable lookups and only 4 integer operations: 1
multiplication to find the value of $3x$, another multiplication to find
the value $6 \cdot 5$, along with 1 integer addition and 1 integer
negative operation.

So the Environment Model approach of calculating
\[
\meval(x(x-1), \meval(3x,2))
\]
instead of the Substitution Model approach of calculating
\[
\meval(\msubst{3x}{x(x-1)},2)
\]
is faster.  But how do we know that these final values reached by these
two approaches always agree?  We can prove this easily by structural
induction on the definitions of the two approaches.  More precisely, what
we want to prove is

\begin{theorem}\label{environments}
For all expressions $e,f \in \aexp$ and $n \in \integers$,
\begin{equation}\label{eval-subst}
\meval(\msubst{f}{e},n) = \meval(e, \meval(f,n)).
\end{equation}
\end{theorem}

\begin{proof}
The proof is by structural induction on $e$.\footnote{This is an example
of why it's useful to notify the reader what the induction variable is
---in this case it isn't $n$.}

\textbf{Base cases:}
\begin{itemize}

\item Case[$e$ is $x$]

  The left hand side of equation~\eqref{eval-subst} equals $\meval(f,n)$
  by this base case in Definition~\ref{subst-def} of the substitution
  function, and the right hand side also equals $\meval(f,n)$ by this base
  case in Definition~\ref{meval-def} of $\meval$.


\item Case[$e$ is $\mtt{k}$].

  The left hand side of equation~\eqref{eval-subst} equals $\mtt{k}$ by
  this base case in Definitions~\ref{subst-def} and~\ref{meval-def} of
  the substitution and evaluation functions.  Likewise, the right hand
  side equals $\mtt{k}$ by two applications of this base case in the
  Definition~\ref{meval-def} of $\meval$.

\end{itemize}

\textbf{Constructor cases}:
\begin{itemize}

\item Case[$e$ is $(e_1 \sumsym e_2)$]

  By the structural induction hypothesis~\eqref{eval-subst}, we may assume
  that for all $f \in \aexp$ and $n \in \integers$,

\begin{equation}\label{ln4.hyp}
\meval(\msubst{f}{e_i},n)  =  \meval(e_i, \meval(f,n))
\end{equation}
for $i= 1,2$.  We wish to prove that

\begin{equation}\label{s+}
\meval(\msubst{f}{(e_1\sumsym e_2)},n)  =  \meval((e_1 \sumsym e_2), \meval(f,n))
\end{equation}

But the left hand side of~(\ref{s+}) equals
\[
\meval(\, (\msubst{f}{e_1} \sumsym \msubst{f}{e_2}),\ n)
\]
by Definition~\ref{subst-def}.\ref{subst-sum} of substitution into a sum
expression.  But this equals
\[
\meval(\msubst{f}{e_1},n) + \meval(\msubst{f}{e_2},n)
\]
by Definition~\ref{meval-def}.\ref{eval-sum} of $\meval$ for a sum expression.  By
induction hypothesis~\eqref{ln4.hyp}, this in turn equals
\[
\meval(e_1,\meval(f,n)) + \meval(e_2,\meval(f,n)).
\]
Finally, this last expression equals the right hand side of~(\ref{s+}) by
Definition~\ref{meval-def}.\ref{eval-sum} of $\meval$ for a sum
expression.  This proves~(\ref{s+}) in this case.

\item $e$ is $(e_1 \prodsym e_2)$.  Similar.

\item $e$ is $-(e_1)$.  Even easier.

\end{itemize}

This covers all the constructor cases, and so completes the proof by
structural induction.

\end{proof}


\iffalse
\subsection{A String Theorem}

Here is a more complex proof, illustrating a combination of structural
induction and strengthening the hypothesis.

\begin{theorem}
  In a string of $0$s and $1$s, the number of occurrences of the pattern
  $01$ is less than or equal to the number of occurrences of $10$, plus
  one.
\end{theorem}

Let's try to prove this by structural induction.  First we must
define $P(s)$.  Let's write $\ms{num}(pat,s)$ as the number of
occurrences of the pattern string pat in s.  Now our inductive
hypothesis is
\[
P(s): \ms{num}(01,s) \leq \ms{num}(10,s) + 1. 
\]
If you try to prove this by structural induction, you will get
stuck.
Why? 
Consider what happens when you add $1$ at the end.  
This could increase the number of $01$s without increasing the number of
$10$s. 

So, to prove by structural induction on strings, let's strengthen the
hypothesis by adding another clause.  If a string ends in $0$ then
the number of $01$s is less than or equal to the number of $10$s.
That solves the problem by weakening what we have to show when the
string ends in $1$.  But maybe it causes another problem somewhere
else.  Let's give it a try:

Redefine $P(s) \eqdef$
\begin{eqnarray*}
\ms{num}(01,s) & \leq & \ms{num}(10,s) + 1, \text{ and}\\
\leftenq{\text{If $s$ ends in $0$ then}}\\
\ms{num}(01,s) & \leq  &\ms{num}(10,s).
\end{eqnarray*} 
 
This means that, for each inductive step have two things to show.

\structuredproof{

  Prove: $\forall s \in S \; (P(s))$ \\
  1. (Base) $P(\emptystring)$ 
  \reason{No patterns of either kind.} \\
  2. (Inductive step) $\forall s \in S \; (P(s) \implies P(s 0))$ \\
  1. Fix $s$. \\
  2. Assume $P(s)$. \\
  3. $P(s 0)$ \\
  1. $\ms{num}(01,s0) \leq \ms{num}(10,s0) + 1$. 
  \reason{???} \\
  2. If $s 0$ ends in $0$ then $\ms{num}(01,s0) \leq
  \ms{num}(10,s0)$. \noreason \\
  \reason{???} \\
  3. QED
  \reason{Conjunction} \\
  4. QED 
  \reason{Implication, UG} \\
  3. (Inductive step) $\forall s \in S \; (P(s) \implies P(s 1))$ \\
  1. Fix $s$. \\
  2. Assume $P(s)$. \\
  3. $P(s 1)$ \\
  1. $\ms{num}(01,s1) \leq \ms{num}(10,s1) + 1$. 
  \reason{???} \\
  2. If $s 1$ ends in $0$ then $\ms{num}(01,s1) \leq
  \ms{num}(10,s1)$.\noreason \\
  \reason{???} \\
  3. QED
  \reason{Conjunction} \\
  4. QED 
  \reason{Implication, UG} \\
  4. QED
  \reason{Structural induction on strings.}\\
}

First let's consider $s1$. This is the case that looks dangerous,
because it might increase the number of $01$s.  We have to prove two
statements.  The second is easy, because the new string doesn't end in
$0$.  We say it's ``vacuously true''.

The first statement now takes some work. 
We might be adding to the number of $01$s.  
However, if we do, the previous string must have ended with $0$. 
Then the inductive hypothesis says that the previous string had to
satisfy the stronger inequality in the second statement. 
Adding one to the LHS of the stronger inequality yields the weaker
inequality we want.

The following proof fragment considers cases based on whether $s$ ends
in $0$ or not.  If not, it might end in $1$, or might be empty (don't
forget this possibility).

\begin{proof}
  3. $P(s 1)$ \\
  1. $\ms{num}(01,s1) \leq \ms{num}(10,s1) + 1$. \\
  1. If $s$ ends in $0$ then $\ms{num}(01,s1) \leq\ms{num}(10,s1) + 1$. \\
  1. Assume $s$ ends in $0$. \\
  2. $\ms{num}(01,s) \leq \ms{num}(10,s)$ 
  Inductive hypothesis (3.2), part 2. \\
  3. $\ms{num}(01,s1) = \ms{num}(01,s) + 1$ 
  Adding one more $01$. \\
  4. $\ms{num}(10,s1) = \ms{num}(10,s)$ \\
  5. $\ms{num}(01,s1) \leq\ms{num}(10,s1) + 1$. 
  Algebra (combining 3.3.1.1.2, ...3, and ...4) \\
  QED 
  Implication \\
  2. If $s$ ends in $1$ then $\ms{num}(01,s1)\leq\ms{num}(10,s1) + 1$. \\
  Inductive hypothesis, part 1; no new $01$s. \\
  3. If $s = \emptystring$ then $\ms{num}(01,s1) \leq\ms{num}(10,s1)+ 1$. \\
  $s1$ is just $1$, which has no $01$s. \\
  4. QED 
  Cases \\
  2. If $s 1$ ends in $0$ then $\ms{num}(01,s1) \leq \ms{num}(10,s1)$. \\
  Vacuously true, because $s1$ doesn't end in $0$. \\
  3. QED
  Conjunction \\
\end{proof}
Of course, you could also expand the step for $s$ ending in $1$ into a
careful series of inequalities.

Now consider $s0$.  We hope that what we did to make the $s1$ case
work doesn't mess up the $s0$ case.  But we have to check.

The first statement is easy.  It follows from the first statement of
the inductive hypothesis for $s$, because we are not increasing the
number of $01$s.  But now the second statement takes more work.  The
difficulty is that the new string ends in $0$, which means that we
have to show the stronger inequality in the second statement.  But to
do this, we might only have the weaker inequality for the previous
string.  The argument again depends on what the previous string $s$
ended with.  So again, we consider cases, based on whether $s$ ends in
$0$ or $1$, or is empty.  If $s$ ends in $0$ we rely on the second
statement of the inductive hypothesis for $s$ (with the stronger
inequality), whereas if $s$ ends in $1$ we rely on the first statement
(with the weaker inequality).  In this case, we have to ``turn the
weaker inequality into the stronger inequality''.

\structuredproof[38ex]{
  3. $P(s 0)$ \\
  1. $\ms{num}(01,s0) \leq \ms{num}(10,s0) + 1$.
  \reason{Induct. hypothesis, part 1; no new $01$s.} \\
  2. If $s 0$ ends in $0$ then $\ms{num}(01,s0) \leq\ms{num}(10,s0)$. \\
  1. $\ms{num}(01,s0) \leq \ms{num}(10,s0)$. \\
  1. If $s$ ends in $0$ then $\ms{num}(01,s0)
  \leq\ms{num}(10,s0)$. \noreason \\
  \reason{Induct. hypothesis, part 2; no new $01$s} \\
  2. If $s$ ends in $1$ then $\ms{num}(01,s0)
  \leq\ms{num}(10,s0)$. \noreason \\ 
  1. Assume $s$ ends in $1$. \\
  2. $\ms{num}(01,s) \leq \ms{num}(10,s) + 1$. 
  \reason{Inductive hypothesis, part 1} \\
  3. $\ms{num}(01,s0) = \ms{num}(01,s)$ \\
  4. $\ms{num}(10,s0) = \ms{num}(10,s) + 1$ 
  \reason{Exactly one new occurrence of $10$.} \\
  5. $\ms{num}(01,s0) \leq \ms{num}(10,s0)$ 
  \reason{Algebra} \\
  6. QED
  \reason{Implication} \\
  3. If $s = \emptystring$ then $\ms{num}(01,s0) \leq
  \ms{num}(10,s0)$. \noreason \\ 
  
\reason{$s0$ is just $1$, which has no $01$s or $10$s.} \\
  4. QED 
  \reason{Cases} \\
  2. QED
  \reason{Propositional reasoning (truth table)} \\
  3. QED 
  \reason{Conjunction}\\
}

If you actually write out all these cases in the proof, you will
notice that some facts are stated repeatedly, e.g., that when you add
a $0$ to the end of a string you are not increasing the number of
$01$s.  To avoid having to state these facts several times, you can
move them earlier in the proof.
\fi


\iffalse

\begin{example*}
\begin{definition}\label{E}
Define a set, $E$, recursively as follows:
\begin{itemize}
\item \textbf{Base case:} $0 \in E$,\label{0E}
\item \textbf{Constructor cases:} if $n \in E$, then
\begin{enumerate}
\item $n+2 \in E$, when $n\geq 0$;\label{+2E}
\item $-n \in E$, when $n > 0$.\label{-E}
\end{enumerate}
\end{itemize}

\end{definition}
\end{example*}

Using this definition, we can see that $0 \in E$ by the Base case, so $0 +
2 = 2 \in E$ by Constructor case~\ref{+2E}., and so $2+2 =4 \in E$, $4+2 =
6 \in E$, \dots, and in fact any nonnegative even number is in $E$ by
successive application of case~\ref{+2E}.  Also, by case~\ref{-E}.,
$-2,-4,-6,\dots \in E$.  So clearly all the even integers are in $E$.

Is anything else in $E$?  The definition doesn't say so explicitly, but an
implicit condition on a recursive definition is that the only way things
get into $E$ is as a consequence of the Base and Constructor cases.  In
other words, $E$ will be exactly the set of even integers.

A very simple application of structural induction proves that the set $E$
given by Definition~\ref{E} is exactly the set of even numbers.  We already
explained why all the even numbers are in $E$.  So what's left is to show
that:

\begin{lemma*}
Every number in the set $E$ in Definition~\ref{E} is even.
\begin{proof}
The proof is by structural induction on $n \in E$.  The induction
hypothesis is 
\[
Q(n) \eqdef \text{$n$ is even}.
\]

\textbf{Base case}: $Q(0)$ holds since 0 is even.

\textbf{Constructor cases}: assuming $n \in E$ and $Q(n)$ holds, prove
that
\begin{itemize}

\item $Q(n+2)$ holds.  This is immediate, since adding 2 to an even number
  gives an even number.

\item $Q(-n)$ holds.  This is also immediate, since $n$ is even iff $-n$ is
even.

\end{itemize}

This completes the proof of the Constructor cases, and we conclude by
structural induction at $Q(n)$ holds for all $n \in E$.
\end{proof}

\end{lemma*}


defining the set, $E$, of even numbers as in Definitions~\ref{E}, but
without the conditions~\ref{+2E}.\ and~\ref{-E}.\ that restrict application of
the rules.  Namely,

\begin{definition}\label{Eamb}
Define a set, $E'$, recursively as follows:
\begin{itemize}
\item \textbf{Base case:} $0 \in E'$,\label{0Eamb}
\item \textbf{Constructor cases:} if $n \in E'$, then
\begin{enumerate}
\item $n+2 \in E'$, \label{+2Eamb}
\item $-n \in E'$.\label{-Eamb}
\end{enumerate}
\end{itemize}
\end{definition}

Now Definition~\ref{Eamb} is perfectly legitimate, and we could us it to
prove by structural induction that $E'$ also is the set of even integers,
that is, $E'= E$.  But Definition~\ref{Eamb} is ambiguous.  For example,
$0\in E'$ by the base case, but also $0=-0 \in E'$ by applying constructor
case~\ref{-Eamb} to the base case.  This begins to matter when we try to
define a function, $s$, from $E'$ to nonnegative integers based on
Definition~\ref{Eamb}:
\begin{align*}
  s(0) & \eqdef 1,\\
s(n+2) & \eqdef 1+ s(n),\\
 s(-n) & \eqdef 1+ s(n).
\end{align*}
So $s(0) \eqdef 1$ by the base case of this definition, and also $s(0)=
s(-0) \eqdef 1+s(0) = 1 + 1 = 2$ by the second constructor case, which
shows that these rules are inconsistent.

On the other hand, using the unambiguous Definition~\ref{E} of $E$,
essentially the same definition of $S$ works just fine.  Namely, define
\begin{align*}
  s(0) & \eqdef 1,\\
  s(n+2) & \eqdef 1+ s(n), & \text{ for } n \geq 0\\
  s(-n) & \eqdef 1+ s(n) & \text{ for } n > 0.
\end{align*}
Now $s(n)$ is unambiguously defined, and in fact is precisely the (unique)
number of steps required to construct $n \in E$ according to the
unambiguous Definition~\ref{E} of $E$.
\fi

\endinput