@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)

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.)

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)

For the first week I got you some simple extra exercises. Most of them were already covered in the lecture or in the tutorial. But probably it might be helpful to repeat it by your own.

Start GHCi and define y and x by typing "let x= 31" and "let y=11". So now do some math with this directly in the GHCi-Console.

• Add x and y
• Subtract y from x
• Multiply x and y
• Divide 3 by 5
• Divide x by y in such a way that you get the next lower Integer
• Find the modulo of x divided by y
• Get x to the power of y
• Get the square root of x
• Get the cube root of 27 (Hint: If you need help, look how the square root is defined in prelude)

Define the function for the n-th Factorial. You might try the different methods in haskell to get such a function.

Prove kn(<k1,k2>), kn({s}k1) |- kn(s) with the knowledge derivation rules in http://people.inf.ethz.ch/meiersi/teaching/fmfp10/tut-sheet1.pdf (that should be now really easy for you). Solve the knowledge proofs in this file without looking at the solution.

I will put up some solution for this some when next week.

Hi dear Student, you found the website to Leo's Functional Programming Tutorial. I will publish here extra exercises and stuff from the tutorial.

"So now! How to start!" I think this is a good start:

• Download and install the haskell platform from http://hackage.haskell.org/platform/ (If you are a Linux user you might install it with your package manager)
• Download and print out the first exercise sheet from the course homepage http://www.infsec.ethz.ch/education/ss11/fmfp/
• Hand in the solution per mail to leob ät student point ethz point ch (or in my shelf on the other side of the room CNB F101)

"I want more!" Here you go:

• learn haskell in 10 minutes (very short tutorial)
• try haskell online (a very short online tutorial, that covers a bit more then you had in lecture so far)
• You might learn a bit more with the book "Real World Haskell"
• Take a look at the course link page.
• There are more books in the computer science library. (Although the course material covers everything you need for the course/exam. And books cover usually more on the haskell site, but less on the formal proves side.)

"Ok, that's all boring! Give me more!" Ok, if you really wish:

• Try to solve the exercise in more than one way! Usually you can solve every problem in haskell in three to four different ways.
• The project euler gives you quite a lot of problems. Haskell is a good programming language to solve them. But they are hard and it might be highly addictive.

So I wish you all the best with the course! And feedback is always appreciated.