Month: August 2013

Structural induction

Structural induction is a generalization of mathematical induction.

To see how, consider the definition of naturals (which mathematical induction is based on):

Inductive nat : Set :=
  | O => nat
  | S => nat -> nat.

So, generally what we do is prove the base case P(O), and then prove the recursive step P(S (S n)) by assuming P(n).

Structural induction can be applied more generally, say lists.

Inductive natlist : Set :=
  | nil  => natlist
  | cons => nat -> natlist -> natlist.

In this case we prove the base case P(nil), and then prove the recursive step P(l') by assuming P(l), where l' = cons(x, l).

So as an example, let’s try to prove that map(id) = id.

First, let’s look at the definitions for map and id:

map _ []     = []
map f (x:xs) = f x : map f xs
id x         = x

We use induction on x.

Base case: map(id, []) = [] = id([])

Inductive step: Assume that map(id, xs) = id(xs), and prove that map(id, (x:xs)) = id(x:xs).

map(id, (x:xs)) = id(x) : map(id, xs) = I.H. = id(x) : id(xs) = x : xs = id(x : xs).

Eta-reduction: map(id) = id.

Q.E.D.

Prime check

Here is a tiny proof, when doing primality test, why it is enough to check divisors only up to sqrt(n) instead of n:

Let n divide q.

If n < sqrt(q) < q
then n < sqrt(q) < q/n < q

q/n < q is trivial

sqrt(q) < q/n
1/sqrt(q) < 1/n

sqrt(q) > n

Alternatively

If sqrt(q) < n < q
then q/n < sqrt(q) < n < q

sqrt(q) < n
sqrt(q) > q/n

Implementation of the algorithm in Haskell:

primetest :: Int -> Bool
primetest x = primetest' x $ (ceiling.sqrt.fromIntegral) x
  where
  primetest' 1 _ = False
  primetest' x 1 = True
  primetest' x y = if x `mod` y == 0 then False else primetest' x (y - 1)

The part where I do (ceiling.sqrt.fromIntegral) may look magical, but what it does is:
1. Convert x from integer to something that sqrt accepts
2. Calculate the sqrt of it
3. Convert it back to integer