Assignment 10

Home

Program Verification

Related Reading:  Chapter 10 in the Omnibus, Chapter 11 in SOE.

Due:  Midnight Sunday April 20, 2008

  1. Do problem 11.2 in SOE, but only for the following laws:

    map (f . g) = map f . map g
    (xs ++ ys) ++ zs = xs ++ (ys ++ zs)
    reverse (reverse xs) = xs

     
  2. Do problem 11.5 in SOE.

 

Solution to problem 11.5

"Consider this definition of the factorial function:

> fac1 :: Integer -> Integer
> fac1 0 = 1
> fac1 n = n * fac1 (n-1)

and this alternative definition:

> fac2 :: Integer -> Integer
> fac2 n = fac' n 1
> where fac' 0 x = x
> fac' n x = fac' (n-1) (n*x)

Prove that fac1 n = fac2 n for all non-negative integers n."

Solution:

Base case (n=0):

fac1 0 => 1 => fac' 0 1 => fac2 0

Induction step:

fac1 (n+1)
=> (n+1) * fac1 n     -- unfold fac1
=> (n+1) * fac2 n     -- ind hyp
=> (n+1) * fac' n 1     -- unfold fac2
=> fac' n (n+1)     -- Lemma 1
=> fac' (n+1) 1     -- fold fac'
fac2 (n+1)     -- fold fac2

Lemma 1: (n+1) * fac' n 1 = fac' n (n+1)

To prove Lemma 1 it is easier to first prove a more general lemma:

Lemma 2: a * fac' n x = fac' n (a*x)

Indeed, Lemma 1 follows immediately from Lemma 2.

Proof of Lemma 2:

Base case (n=0):

a * fac' 0 x => a * x => fac' 0 (a*x)

Induction step (n=n+1):

a * fac' (n+1) x
=> a * fac' n ((n+1)*x)     -- unfold fac'
=> fac' n (a*((n+1)*x))     -- ind hyp
=> fac' n ((n+1)*(a*x))     -- associativity & commutativity
fac' (n+1) (a*x)     -- fold fac'