\documentstyle[fuzz]{article}
%\documentstyle[12pt]{article}

\input{./handout}

\begin{document}

\handout{7}{27 September 1995}{Structural Induction}


\section{Introduction}

We often find ourselves in the situation of wanting to prove something
of the form:
\[ \forall x: S @ P(x) \]
That is, we want to prove that all elements of some set $S$ have the
property $P$. If all of the elements of $S$ are defined by some
regular structural rules, induction is frequently the proof technique
of choice.

Examples of sets that can be defined by structural rules include:
\begin{itemize}\itemsep -2pt
\item {\bf natural numbers}: starting with the element $0$, each element
is the successor of some other element in the set.
\item {\bf sequences}: starting with the empty sequence, $<>$, each
element is built up by appending an element to an existing list.
\item {\bf parse trees}: starting with the ``terminal'' nodes of a grammar, each
parse true is a structure defined by one of a ``non-terminal''
productions of the grammar.
\end{itemize}
In the first of these examples, the proof technique is typically
referred to as ``natural induction''.  In the others, it is typically
referred to as ``structural induction''.

In these notes we will illustrate the use of structural induction
over binary trees. Other forms of structural induction work similarly.
Here is how we will proceed.  First, we provide a ``structural''
definition of trees: this determines the rules that allow us to define
all trees of interest. Next, we define what we mean by ``size'' of a
tree. Then we will propose a small theorem about calculating the size;
this is what we will then prove.

\section{Definition of Binary Trees}

There are many ways to model binary trees using sets and functions. For
this example we will use a definition that relies on some Z
notation for describing recursive data structures. The details of the
syntax are not terribly important at this point, but you should
understand the basic idea about building up trees from other trees.

Here is the definition:
\begin{zed}
    TREE ::= leaf | node \ldata TREE \cross TREE\rdata 
\end{zed}
It says that a tree is either a leaf or is made up of two subtrees glued
together with node. Usually we would associate some data with the leaf
and/or nodes, but for present purposes this simple definition will
suffice.

Here are some examples of the kind of structures that we can build up
using this definition:

\[
    leaf\\
    node(leaf, leaf)\\
    node(node(leaf, leaf), leaf)\\
    node(leaf, node(node(leaf, leaf), leaf))
\]

\section{Definition of Size}

There are also many ways that we might define the size of a
tree. Some definitions would count just the leaves, others just the
nodes. Here we will count both. 

Informally, we could say that the size of a single leaf is 1, while
the size of a tree built out of two subtrees, say $t_1$ and $t_2$, is
the sum of the sizes of the two subtrees plus 1 (for the joining node).

The basic idea of this definition is that we define the size of a tree
inductively over the structure, saying how the size of a given tree is
calculated from sizes its parts. Putting this more formally in the notation of
{\em Software Engineering Mathematics}, we would define a function by
first declaring its type (in this case $size: TREE \fun \nat$), and
then saying how it is defined in each of the two cases.

\begin{axdef}
    size: TREE \fun \nat
\where
    \forall t_1, t_2: TREE @\\
\t1	size (leaf) = 1 \land \\
\t1	size (node (t_1,t_2)) = 1 + size(t_1) + size(t_2)
\end{axdef}

\noindent {\em [Note: I am doing things a little differently than what I tried
to do in class. Here I am simply asserting that this is the definition
of $size$; in class I tried to prove something {\em about\/} this
definition.]}

In a similar way, we might make other definitions about trees. Here
are two useful ones:

\begin{axdef}
    leaves: TREE \fun \nat \\
    nodes: TREE \fun \nat
\where
    \forall t_1, t_2: TREE @ 
\also
\t1	leaves (leaf) = 1 \land \\
\t1	leaves (node (t_1,t_2)) = leaves(t_1) + leaves(t_2) \land
\also
\t1	nodes (leaf) = 0 \land \\
\t1	nodes (node(t_1,t_2)) = 1 + nodes(t_1) + nodes(t_2)
\end{axdef}


\section{Proving a Theorem by Structural Induction}

Based on what we've said about our definitions, there is a pretty
obvious connection between the three definitions give above. That is,
we would expect the size of a tree to be the sum of the leaves and the
nodes. We can make this precise as follows:

\newtheorem{theorem}{Theorem}
\begin{theorem}
$\forall t:TREE @ size(t) = leaves(t) + nodes(t)$.
\end{theorem}

We will prove this by structural induction. As with natural deduction
there are two cases: a base case for leaves, and an induction case for
composite trees. Here is how it goes:

\noindent{\bf Proof:}
Let t: TREE. \\
{\bf Base Case:} Assume t is a leaf. \\
\begin{argue}
\t1	    size(t) \\
\t1	    = & assumption \\
\t1	    size(leaf) \\
\t1	    = & definition of $size$ \\
\t1	    1 \\
\t1	    = & arithmetic \\
\t1	    1 + 0 \\
\t1	    = & definition $leaves$ \\
\t1	    leaves(t) + 0 \\
\t1	    = & definition $nodes$\\
\t1	    leaves(t) + nodes(t)
\end{argue}
{\bf Induction Case:} Assume that $t = node(t_1,t_2))$ and that the
theorem hold for all trees $t':TREE$ such that $size(t') < size(t)$. \\
\begin{argue}
\t1	size(t) \\
\t1	= & assumption\\
\t1	size(node(t_1,t_2)))\\
\t1	= &  definition of $size$ \\
\t1	1 + size(t_1) + size(t_2) \\
\t1	= & induction hypothesis (applied to $t_1$ and $t_1$) \\
\t1	1 + (leaves(t_1) + nodes(t_1)) + (leaves(t_2) + nodes(t_2)) \\
\t1	= & commutative and associative properties of $+$ \\
\t1	(leaves(t_1) + leaves(t_2)) + (1 + nodes(t_1) + nodes(t_2)) \\
\t1	= & definition of $leaves$\\
\t1	leaves(node(t_1, t_2)) + (1 + nodes(t_1) + nodes(t_2)) \\
\t1	= & definition of $nodes$\\
\t1	leaves(node(t_1, t_2)) + nodes(node(t_1, t_2)) \\
\t1	= & definition of $t$ \\
\t1	leaves(t) + nodes(t)
\end{argue}

\section{Exercises for the Reader}

\begin{enumerate}
\item Show that $\forall t: TREE @ leaves(t) = nodes(t) + 1$.
\item Define a $mirror$ function that flips a tree over. Then show
that $\forall t: TREE @ size(mirror(t)) = size(t)$.
\end{enumerate}
\end{document}