Structural induction

Consider the following fairly obvious equation over a data structure (a list)

     length (list1 ++ list2) = length list1 + length list2          [EQ]

where ++ denotes list append in a language such as Haskell.

In order to prove this, we need some rules for length, and also for the append operation.

     length []     = 0              [LEN1]
     length (h:t)  = 1 + length t   [LEN2]

     [] ++ list    = list           [APP1]
     (h:t) ++ list = h: (t ++ list) [APP2]

Now, if we are to prove EQ, we consider two cases. We shall choose the base case to be when list1 is just the empty list, [].

First consider the LHS of EQ, with list1 set to []

     length ([] ++ list2) = length (list2) by APP1

Consider the RHS of EQ similarly

     length [] + length list2 = 0 + length list2 by LEN1
                              = length list2 - arithmetic

Thus when list1 is [], the LHS and the RHS of EQ are equal.

Now consider the case when list1 is a non empty list. We can denote this by (h:t), which means a head item followed by a list tail (which may itself be empty). We can also denote this by x:xs

In this case we again consider the LHS of EQ

      length ((x:xs) ++ list2) = length (x: (xs ++ list2)) by APP2
                              = 1 + length (xs ++ list2) by LEN2

and also the RHS

      length (x:xs) + length list2 = 1 + length xs + length list2 by LEN2

We need a rule similar to that used in mathematical induction, and structural induction suggests that we assume that if we have P(xs) => P(x:xs) for all x, xs then the proof requirements hold.

Thus we take P(xs) to be

      length xs ++ list2 = length xs ++ list2

hence it follows that P(x:xs) is true if P(xs) is, and this also holds in the example for EQ given here.

Once the principles of structural induction are understood, it can be easily applied to problems involving list structures, but it can also be extended to apply to many different types of data structures used in computer science.