CSci 555: Functional Programming
Spring Semester 2000

Assignment #4
Due Thursday, 30 March, 8:00 A.M.

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 following properties 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.

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)

    (++) :: [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

UP to CSCI 555 assignments document?