CSci 555: Functional Programming
Fall Semester 2010

Assignment #4
Due Friday, 19 November


This is an individual assignment, which you must complete in accordance with the instructions given in the Professional Conduct and Assignments sections of the Syllabus .

Prove any six of the first seven properties given below using the definitions given at the end. You may use earlier properties in proofs of later ones. You also may, of course, use well-known properties of arithmetic, but please state the properties that you uses as justifications for steps.

Graduate students prove property 8 below.

  1. Prove for all finite lists xs and ys that
    sumlist (xs ++ ys) = sumlist xs + sumlist ys

  2. Prove for all finite lists xs and ys that
    sumlist (xs ++ ys) = sumlist (ys ++ xs)

  3. Prove for all finite lists xs that
    length (double xs) = length xs

  4. Prove for all natural numbers n that
    fac n = fac2 n

  5. Prove for all finite lists xs and ys and all predicates p of the proper type that
    filter p (xs ++ ys) = filter p xs ++ filter p ys

  6. Prove for all finite lists xs and all predicates p and q of the proper types that
    filter p (filter q xs) = filter q (filter p xs)

  7. Prove for all finite lists of lists xss and all functions f of the appropriate type that
    map f (concat xss) = concat (map (map f) xss)

  8. Prove for all Nat values x and y, addNat x y = addNat y x.

    (++) :: [a] -> [a] -> [a]
    [] ++ ys     = ys                        -- append.1
    (x:xs) ++ ys = x:(xs ++ ys)              -- append.2

    length :: [a] -> Int
    length []      = 0                       -- length.1
    length (_:xs)  = 1 + length xs           -- length.2

    concat :: [[a]] -> [a]
    concat []       = []                     -- concat.1
    concat (xs:xss) = xs ++ concat xss       -- concat.2

    map :: (a -> b) -> [a] -> [b]
    map f []     = []                        -- map.1
    map f (x:xs) = f x : map f xs            -- map.2


    filter :: (a -> Bool) -> [a] -> [a]
    filter p []     = []                     -- filter.1
    filter p (x:xs)
        | p x       = x : filter p xs        -- filter.2
	| otherwise = filter p xs            -- filter.3

    (.) :: (b -> c) -> (a -> b) -> (a -> c)
    (f . g) x = f (g x)                      -- composition

    sumlist :: [Int] -> Int
    sumlist []     = 0                       -- sumlist.1
    sumlist (x:xs) = x + sumlist xs          -- sumlist.2

    double :: [Int] -> [Int]
    double []      = []                      -- double.1
    double (x:xs)  = (2*x):double xs         -- double.2

    fac :: Int -> Int
    fac 0         = 1                        -- fac.1
    fac n | n > 0 = n * fac (n-1)            -- fac.2

    fac2 :: Int -> Int
    fac2 n | n >= 0 = facAux n 1             -- fac2.1
        where 
            facAux 0 p = p                   -- fac2.2
            facAux n p = facAux (n-1) (n*p)  -- fac2.3

    data Nat = Zero | Succ Nat

    addNat :: Nat -> Nat -> Nat
    addNat Zero     y    = y
    addNat x        Zero = x
    addNat (Succ x) y    = addNat x (Succ y)


UP to CSCI 555 assignments document?


Copyright © 2010, H. Conrad Cunningham
Last modified: Thu, 11 Nov 2010