# Lecture 4 - Structural Induction and Tail Recursion

Simple induction on the natural numbers can get us reasonably far when it comes to proving theorems, but in this class we are also interested in proving theorems on SML code, not just for mathematical propositions. In such cases, we would like to be able to induct on the structure of data, which leads us to a phenomenon known as structural induction, a more powerful, more general form of induction.

We saw how we could employ structural induction to induct on the structure of a
list, by proving a base case and inductive case, using the principle of
structural induction for lists. This is similar to the principle of simple
induction for natural numbers, which involves a base case and inductive step of
$n$ and $n+1$, but instead operates on SML lists in the cases of `[]`

and
`x::xs`

.

We then introduced the concept of tail recursion, which concerns
recursive functions which perform a recursive call, as the last thing that they
do. We saw that these have implications for efficiency benefits, because by not
needing to remember to do things after the recursive call, we avoid needing to use
excess memory, and we applied this knowledge to write the tail-recursive version
of the `length`

function, in `tlength`

.