\section{Induction in Computer Science}

Induction is a powerful and widely applicable proof technique, which is why
we've devoted an entire chapter to it.  Strong induction and its special
case of ordinary induction are applicable to any kind of thing with
nonnegative integer sizes --which is a awful lot of things, including all
step-by-step computational processes.

\iffalse
Ordinary induction is specially helpful in the study of computation.  Why?
Well, ordinary induction on nonnegative integers is a ``one step at a
time'' proof method.  Computations also evolve ``one step at a time.''
\fi

Structural induction then goes beyond natural number counting by offering a
a simple, natural approach to proving things about recursive computation
and recursive data types.  This makes it a technique every Computer
Scientist should embrace.

\iffalse
In many cases a nonnegative integer size can be defined for a recursively
defined datum, such as the length of a string, or the number of operations
in an $\aexp$.  It is then possible to prove properties of data by ordinary
induction on their size.  But this approach often produces more cumbersome
proofs than structural induction.

In fact, structural induction is theoretically more powerful than ordinary
induction.  However, it's only more powerful when it comes to reasoning
about infinite data types ---like infinite trees, for example ---so this
greater power doesn't matter in practice.  What does matter is that for
recursively defined data types, structural induction is a simple and
natural approach.
\fi

\endinput
