@leo's

Here you have some functions were you can train your type inference skills. You might look up functions like map, +, <, ==, head, filter, elem, etc. if you don't know them by heart (but you should, you will be faster on the exam if you do). I will not publish solution for that. Use ":type" followed by a space and the function in ghci to get a result. I wish you good luck with the exam.

map ((+) 3) :: ?
(\x y -> x < y) :: ?
(\x -> x (<) + 1) :: ?
(\x z -> z (x z)) :: ?
(\x y -> x (\z -> y z)) :: ?
(\x -> x (==), 1) :: ?
filter (\x -> x elem) :: ?
map map :: ?
map.map :: ?
[\x a -> (a 1) x] :: ?
head.fst.head :: ?
map (+) [1,2,3,4] :: ?

A bit late, but here you get the solutions from week three.

Usage of List

Multiply all numbers from 1 to 100 by using a prelude function (and no recursion)

foldr (*) 1 [1..100]

Sum all odd numbers bellow 50. Use a prelude function and the haskell list in a clever way.

sum [1,3..49]

Generate the string "abcdefghijklmnopqrstuvwxyzabcdefghijklmnopqrstuvwxyz" (remember a string in haskell is just a list of chars)

['a'..'z'] ++ ['a'..'z']

List functions

sum :: (Num a) => [a] -> a
sum [] = 0
sum (x:xs) = x + (sum xs)

merge :: [a] -> [a] -> [a]    -- merge two list (in haskell (++))
merge [] ys = ys
merge (x:xs) ys = x : (merge xs ys)

nthElement :: [a] -> Int -> a -- give the n-th element of a list (in haskell (!!))
nthElement (x:xs) 0 = x       -- errors ignored
nthElement (x:xs) n+1 = nthElement xs n

List comprehension

Find all numbers bellow 1000 that are devidable by 3 or 5 with a list comprehension. 

[x | x <- [1..999], (mod x 3)==0 || (mod x 5)==0]

A Proof for the end

You can also do recursiv proofs over lists. Given the following programm:

map f [] = []                    (m.1)
map f (x:xs) = f x : map f xs    (m.2)
times2 x = 2*x                   (ti)
twice [] = []                    (tw.1)
twice (x:xs) = (2* x):(twice xs) (tw.2)

Prove "FORALL xs::[int]. twice xs = map times2 xs" with recursion.

FORALL xs::[int]. twice xs = map times2 xs
Let P(xs) = twice xs = map times2 xs. 
Show FORALL xs::[int]. P(xs) holds by induction over xs

Base case: P([])
twice [] = []               (tw.1)
         = map times2 []    (m1.rev)

Step case: Show FORALL x::int, xs::[int]. P(xs) => P(x:xs) (IH = P(xs))
Twice (x:xs) = (2 * x):(twice xs)         (tw.2)
             = (times2 x):(twice xs)      (ti.rev)
             = (times2 x):(map times2 xs) (IH)
             = map times2 (x:xs)          (tw.2.rev)

Here is the solution for the second week extra excercise. Download it form: leo.freeflux.net/files/fmfp/CA%20Solution.pdf

The "Listtatzelwurm" or "Listmonster" you might already know from the tutorial. It's from the site "learn you a haskell for greater good", if you need more help about list, the chapter with the Listmonster might be a help for you.

Let me give you some extra exercises for the current chapter. The solution will be online in around a week.

Usage of List

Multiply all numbers from 1 to 100 by using a prelude function (and no recursion)

Sum all odd numbers bellow 50. Use a prelude function and the haskell list in a clever way.

Generate the string "abcdefghijklmnopqrstuvwxyzabcdefghijklmnopqrstuvwxyz" (remember a string in haskell is just a ... of ...)

List functions

TA's usually just let you implement prelude functions to train list functions. So then, implement this functions recursiv:

sum :: (Num a) => [a] -> a
merge :: [a] -> [a] -> [a]    -- merge two list (in haskell (++))
nthElement :: [a] -> Int -> a -- give the n-th element of a list (in haskell (!!))

List comprehension

You already talked about list comprehension in the lecture. If you want to repeat it a bit, read the first chapter here http://www.haskell.org/haskellwiki/List_comprehension. Then find all numbers bellow 1000 that are devidable by 3 or 5 with a list comprehension. (When you sum this up you have already solved the first problem of project euler.)

A Proof for the end

You can also do recursiv proofs over lists. Given the following programm:

map f [] = []                    (m.1)
map f (x:xs) = f x : map f xs    (m.2)
times2 x = 2*x                   (ti)
twice [] = []                    (tw.1)
twice (x:xs) = (2* x):(twice xs) (tw.2)

Prove "FORALL xs::[int]. twice xs = map times2 xs" with recursion.

I just want to write down the proof that we did as an example in the last exercise session as you might want to use it as a reference for the current exercise sheet.

If we have the following haskell programm:

sum 0 = 0              --sum.1

sum n = n+sum (n-1)  --sum.2

And you want to prove forall n element of Nat. sum n = n*(n+1)/2 then we write the following proof:

Lemma: forall n element of Nat. sum n = n*(n+1)/2
Proof: We show forall n element of Nat. sum n = n*(n+1)/2 by induction. Let P(n) = sum n = n*(n+1)/2.

Base Case: Show P(0).

sum 0
= 0 -- sum.1
= 0*(0+1)/2 –- arith

Step Case: Let n element of Nat be arbitrary and assume that P(n) holds. Show P(n+1).

sum (n+1)
= (n+1) + sum ((n+1)-1) -- sum.2
= (n+1) + sum (n) -- arith
= (n+1) + n*(n+1)/2 -- P(n)
= 2*(n+1)/2 + n*(n+1)/2 --arith
= (n+2)*(n+1)/2 --arith
= (n+1)*((n+1)+1)/2 --arith

qed.

(The italic text of the proof might be used as a template for all recursiv proofs.)

For the second week I will give you an excercise sheet created by former FMFP TA Martin Schaub. You find the sheet here. I will put the solution for this sheet online during this week.

The Solution for the official excercise is already online at https://www1.ethz.ch/infsec/education/ss11/fmfp/fp_material_secured.

The master solution of the official excercise are online since quite some time on https://www1.ethz.ch/infsec/education/ss11/fmfp/fp_material_secured. Now I also put the solution for the first weeks extra exercises online.

The calculation in GHCi could look like:

Prelude> let x=31
Prelude> let y=11
Prelude> x+y
42
Prelude> x-y
20
Prelude> x*y
341
Prelude> div x y
2
Prelude> mod x y
9
Prelude> x^y
25408476896404831
Prelude> sqrt (fromIntegral x)
5.5677643628300215
Prelude> (fromIntegral x) ** 1/3
10.333333333333334

There are different methods to implement the n-th Factorial. Let me show you some examples. First with if, which is often considered as bad style.

fac n = if n==0 then 1 else n*(fac (n-1))

It's possible to implement it with pattern matching.

fac' 0 = 1
fac' n = n * (fac' (n-1)) 

Or with guards.

fac'' n = 
	| n==0 = 1
	| otherwise = n * (fac'' (n-1))

If this is all to easy for you. You might implement a endless list of factorials (this is beyond the course scope).

fac''' = 1:zipWith (*) fac''' [2..]

The proof for "kn(<k1,k2>), kn({s}k1) |- kn(s)" in ASCII-Art:

G := kn(<k1,k2>), kn({s}k1)

                    ------------------Ax
                     G |- kn(<k1,k2>)
----------------Ax  ------------------ Pair-EL
 G |- kn({s}k1)        G |- kn(k1)
------------------------------------ Enc-E
 G |- kn(s)