Exam
Date of first exam: 26.02.2021, 17.00-19.00
Date of retake exam: 31.03.2021
Date exam test run on artemis: 19.02.2021, 08.30-19.00
The exam will take place online on artemis. You will receive exercises, solve them on your own at home, and then submit the solutions online. You must work on the exam on your own. The exam is open book, but you must not, in any way, get support by someone else (in person, chat, forum, discussion group, etc.). Doing so is classified as cheating (“Unterschleif”) and leads to consequences as mentioned in the APSO (“Allgemeine Prüfungs- und Studienordnung”). In particular, the exam will be marked as failed (w. cheating), and you will only be allowed trying to pass the module in one final exam attempt (before being exmatriculated) (cf. APSO §24 (5)).
The exam submission will be checked for plagiarism. If you happen to copy code, for example, from a book or website, you must cite the reference. Do this by adding a reference to the source using a comment at the relevant places, e.g. -- adapted from http://learnyouahaskell.com/zippers
. Failing to cite in an appropriate manner is classified as plagiarism.
If we have reasons to doubt that you solved the exercises on your own, we may schedule an additional oral exam at short notice. Failing the oral exam means failing the whole exam with the consequences explained in the first paragraph under “cheating”.
We expect you to hand in compiling Haskell code. Non-compiling code will be graded but can result in significant point deductions. The exam will neither require nor allow the usage of any packages outside the base and QuickCheck package.
You will not receive any feedback when you submit your solutions. Check your submission for compilation errors on your local machine.
Proofs must be written in a simple text file, pasted to the artemis editor, and structured in a format as practised during the past semester (lecture or cyp-like). Those proofs do not need to compile against cyp but must contain the central ingredients (proof rules, justifications, inductive hypotheses, etc.).
In case of an unexpected breakdown of artemis - and only in such an case - you have to hand in your exam via e-mail to fpv@in.tum.de. Again, late submissions will not be accepted.
If you think the instructions of an exercise are wrong, you can send an e-mail to fpv@in.tum.de. If it turns out that the instructions must be changed, we will send an e-mail to all participants and also announce it in the FPV-announcements stream on Zulip. Other questions about the exercises will not be answered during the exam.
If you encounter technical problems, you can also send an e-mail to fpv@in.tum.de.
First Exam
Grading
Grade | Min Points | Max Points |
---|---|---|
1 | 36.5 | 40 |
1.3 | 34.5 | 36.49 |
1.7 | 32 | 34.49 |
2 | 29.5 | 31.99 |
2.3 | 27 | 29.49 |
2.7 | 25 | 26.99 |
3 | 22.5 | 24.99 |
3.3 | 20 | 22.49 |
3.7 | 17.5 | 19.99 |
4 | 15 | 17.49 |
4.3 | 13 | 14.99 |
4.7 | 10.5 | 12.99 |
5 | 0 | 10.49 |
Solutions
Path to Success
Sharing is Caring
powTwoAdd
mulPowTwo
superConst
Observational Equivalence
Wrong: Let
xs = [1..]
andp = head (rev (rev xs))
. Thenhead (rev (rev xs))
diverges buthead xs = 1
.Wrong: Let
xs = repeat False
andp x = if x then x else x
. Thenp (and xs) = False
butp (and' xs)
diverges.
InputOutput
QuickCheck
Proof 1
f2 a xs = f1 (+) a xs
Lemma f2 a xs = f1 (+) a xs
Proof by induction on xs
Base case:
To show: f2 a [] = f1 (+) a []
f2 a []
(by def) = a
(by def) = f1 (+) a []
Induction step:
To show: f2 a (x:xs) = f1 (+) a (x:xs)
IH: f2 a xs = f1 (+) a xs
f2 a (x:xs)
(by def) = f2 (a+x) xs
(by IH) = f1 (+) (a+x) xs
f1 (+) a (x:xs)
(by def) = f1 (+) (a+x) xs
map2 g a xs = map (g a) xs
Lemma map2 g a xs = map (g a) xs
Proof by induction on xs
Base case:
To show: map2 g a [] = map (g a) []
map2 g a []
(by def) = []
(by def) = map (g a) []
Induction step:
To show: map2 g a (x:xs) = map (g a) (x:xs)
IH: map2 g a xs = map (g a) xs
map2 g a (x:xs)
(by def) = g a x : map2 g a xs
(by IH) = g a x : map (g a) xs
map (g a) (x : xs)
(by def) = g a x : map (g a) xs
f2 xs a = f1 (*) a xs
Lemma f2 xs a = f1 (*) a xs
Proof by induction on xs
Base case:
To show: f2 [] a = f1 (*) a []
f2 [] a
(by def) = a
(by def) = f1 (*) a []
Induction step:
To show: f2 (x:xs) a = f1 (*) a (x:xs)
IH: f2 xs a = f1 (*) a xs
f2 (x : xs) a
(by def) = x * f2 xs a
(by IH) = x * f1 (*) a xs
f1 (*) a (x:xs)
(by def) = x * f1 (*) a xs
zipp xs xs = map d xs
Lemma zipp xs xs = map d xs
Proof by induction on xs
Base case:
To show: zipp [] [] = map d []
zipp [] []
(by def) = []
(by def) = map d []
Induction step:
To show: zipp (x:xs) (x:xs) = map d (x:xs)
IH: zipp xs xs = map d xs
zipp (x:xs) (x:xs)
(by def) = (x+x) : zipp xs xs
(by IH) = (x+x) : map d xs
map d (x:xs)
(by def) = d x : map d xs
(by def) = (x+x) : map d xs
Proof 2
fl z (reverse xs) = fl z xs (1)
Lemma app: fl z (xs ++ [y]) = fl (z + y) xs
Proof by induction on xs
Base case:
To show: fl z ([] ++ [y]) = fl (z + y) []
fl z ([] ++ [y])
(by def) = fl z [y]
(by def) = fl (z + y) []
(by def) = z + y
(by def) = fl (z + y) []
Induction step:
To show: fl z ((x:xs) ++ [y]) = fl (z + y) (x:xs)
IH: fl z (xs ++ [y]) = fl (z + y) xs
fl z ((x:xs) ++ [y])
(by def) = fl z (x : (xs ++ [y]))
(by def) = fl (z+x) (xs ++ [y])
(by IH) = fl (z+x+y) xs
fl (z+y) (x:xs)
(by def) = fl (z+y+x) xs
= fl (z+x+y) xs
Lemma fl z (reverse xs) = fl z xs
Proof by induction on xs
Base case:
To show: fl z (reverse []) = fl z []
fl z (reverse [])
(by def) = fl z []
Induction step:
To show: fl z (reverse (x:xs)) = fl z (x:xs)
IH: fl z (reverse xs) = fl z xs
fl z (reverse (x:xs))
(by def) = fl z (reverse xs ++ [x])
(by app) = fl (z+x) (reverse xs)
(by IH) = fl (z+x) xs
(by def) = fl z (x:xs)
fl (reverse xs) z = fl xs
Lemma app: fl (xs ++ [y]) z = fl xs (y * z)
Proof by induction on xs
Base case:
To show: fl ([] ++ [y]) z = fl [] (y*z)
fl ([] ++ [y]) z
(by def) = fl [y] z
(by def) = fl [] (y*z)
(by def) = y*z
(by def) = fl [] (y*z)
Induction step:
To show: fl ((x:xs) ++ [y]) z = fl (x:xs) (y * z)
IH: fl (xs ++ [y]) z = fl xs (y * z)
fl ((x:xs) ++ [y]) z
(by def) = fl (x : (xs ++ [y])) z
(by def) = fl (xs ++ [y]) (x*z)
(by IH) = fl xs (y*x*z)
fl (x:xs) (y*z)
(by def) = fl xs (x*y*z)
= fl xs (y*x*z)
Lemma fl (reverse xs) z = fl xs
Proof by induction on xs
Base case:
To show: fl (reverse []) z = fl [] z
fl (reverse []) z
(by def) = fl [] z
Induction step:
To show: fl (reverse (x:xs)) z = fl (x:xs) z
IH: fl (reverse xs) z = fl xs z
fl (reverse (x:xs)) z
(by def) = fl (reverse xs ++ [x]) z
(by app) = fl (reverse xs) (x * z)
(by IH) = fl xs (x * z)
(by def) = fl (x:xs) z
fr z (reverse xs) = fr z xs
Lemma app: fr z (xs ++ [y]) = y + fr z xs
Proof by induction on xs
Base case:
To show: fr z ([] ++ [y]) = y + fr z []
fr z ([] ++ [y])
(by def) = fr z [y]
(by def) = y + fr z []
Induction step:
To show: fr z ((x:xs) ++ [y]) = y + fr z (x:xs)
IH: fr z (xs ++ [y]) = y + fr z xs
fr z ((x:xs) ++ [y])
(by def) = fr z (x : (xs ++ [y]))
(by def) = x + fr z (xs ++ [y])
(by IH) = x + y + fr z xs
y + fr z (x:xs)
(by def) = y + x + fr z xs
= x + y + fr z xs
Lemma fr z (reverse xs) = fr z xs
Proof by induction on xs
Base case:
To show: fr z (reverse []) = fr z []
fr z (reverse [])
(by def) = fr z []
Induction step:
To show: fr z (reverse (x:xs)) = fr z (x:xs)
IH: fr z (reverse xs) = fr z xs
fr z (reverse (x:xs))
(by def) = fr z (reverse xs ++ [x])
(by app) = x + fr z (reverse xs)
(by IH) = x + fr z xs
(by def) = fr z (x:xs)
fr (reverse xs) z = fr xs z
Lemma app: fr (xs ++ [y]) z = fr xs z * y
Proof by induction on xs
Base case:
To show: fr ([] ++ [y]) z = fr [] z * y
fr ([] ++ [y]) z
(by def) = fr [y] z
(by def) = fr [] z * y
Induction step:
To show: fr ((x:xs) ++ [y]) z = fr (x:xs) z * y
IH: fr (xs ++ [y]) z = fr xs z * y
fr ((x:xs) ++ [y]) z
(by def) = fr (x # (xs ++ [y])) z
(by def) = fr (xs ++ [y]) z * x
(by IH) = fr xs z * y * x
fr (x:xs) z * y
(by def) = fr xs z * x * y
= fr xs z * y * x
Lemma fr (reverse xs) z = fr xs z
Proof by induction on xs
Base case:
To show: fr (reverse []) z = fr [] z
fr (reverse []) z
(by def) = fr [] z
Induction step:
To show: fr (reverse (x:xs)) z = fr (x:xs) z
IH: fr (reverse xs) z = fr xs z
fr (reverse (x:xs)) z
(by def) = fr (reverse xs ++ [x]) z
(by app) = fr (reverse xs) z * x
(by IH) = fr xs z * x
(by def) = fr (x:xs) z
Shapes
Pairings
Second Exam
Grading
Grade | Min Points | Max Points |
---|---|---|
1 | 37.5 | 40 |
1.3 | 35.5 | 37.49 |
1.7 | 33 | 35.49 |
2 | 30.5 | 32.99 |
2.3 | 28 | 30.49 |
2.7 | 26 | 27.99 |
3 | 23.5 | 25.99 |
3.3 | 21 | 23.49 |
3.7 | 18.5 | 20.99 |
4 | 16 | 18.49 |
4.3 | 14 | 15.99 |
4.7 | 11.5 | 13.99 |
5 | 0 | 11.49 |
Solutions
Different Implementations
Retake Proof 1
h a u = g (+) a u
Lemma h a u = g (+) a u
Proof by induction on u
Base case:
To show: h a N = g (+) a N
h a N
(by def) = a
(by def) = g (+) a N
Induction step:
To show: h a (C u x) = g (+) a (C u x)
IH: h a u = g (+) a u
h a (C u x)
(by def) = h (a+x) u
(by IH) = g (+) (a+x) u
g (+) a (C u x)
(by def) = g (+) (a+x) u
g u a = h (*) a u
Lemma g u a = h (*) a u
Proof by induction on u
Base case:
To show: g D a = h (*) a D
g D a
(by def) = a
(by def) = h (*) a D
Induction step:
To show: g (E u x) a = h (*) a (E u x)
IH: g u a = h (*) a u
g (E u x) a
(by def) = x * g u a
(by IH) = x * h (*) a u
h (*) a (E u x)
(by def) = x * h (*) a u
m2 g a t = m (g a) t
Lemma m2 g a t = m (g a) t
Proof by induction on t
Base case:
To show: m2 g a A = m (g a) A
m2 g a A
(by def) = A
(by def) = m (g a) A
Induction step:
To show: m2 g a (B t x) = m (g a) (B t x)
IH: m2 g a t = m (g a) t
m2 g a (B t x)
(by def) = B (m2 g a t) (g a x)
(by IH) = B (m (g a) t) (g a x)
m (g a) (B t x)
(by def) = B (m (g a) t) (g a x)
tt t t = m v t
Lemma tt t t = m v t
Proof by induction on t
Base case:
To show: tt A A = m v A
tt A A
(by def) = A
(by def) = m v A
Induction step:
To show: tt (U t x) (U t x) = m v (U t x)
IH: tt t t = m v t
tt (U t x) (U t x)
(by def) = U (tt t t) (x+x)
(by IH) = U (m v t) (x+x)
m v (U t x)
(by def) = U (m v t) (v x)
(by def) = U (m v t) (x+x)
Retake Proof 2
f m = g m (1)
Lemma f m = g m
Proof by f-induction on m
Case 1
To show: f Nothing = g Nothing
f Nothing
(by def) = []
(by def) = g Nothing
Case 2
To show: f (Just []) = g (Just [])
f (Just [])
(by def) = []
(by def) = g (Just [])
Case 3
To show: f (Just (x:xs)) = g (Just (x:xs))
IH: f(Just xs) = g(Just xs)
f (Just(x:xs))
(by def) = x : f (Just xs)
(by IH) = x : g (Just xs)
(by def) = x : xs
g (Just(x:xs))
(by def) = x : xs
f m = g m (2)
Lemma f m = g m
Proof by f-induction on m
Case 1
To show: f Nothing = g Nothing
f Nothing
(by def) = Zero
(by def) = g Nothing
Case 2
To show: f (Just Zero) = g (Just Zero)
f (Just Zero)
(by def) = Zero
(by def) = g (Just Zero)
Case 3
To show: f (Just(Suc n)) = g (Just(Suc n))
IH: f (Just n) = g (Just n)
f (Just(Suc n))
(by def) = Suc (f (Just n))
(by IH) = Suc(g (Just n))
(by def) = Suc n
g (Just(Suc n))
(by def) = Suc n
f m = g m (3)
Lemma f m = g m
Proof by f-induction on m
Case 1
To show: f Nothing = g Nothing
f Nothing
(by def) = Zero
(by def) = g Nothing
Case 2
To show: f (Just Zero) = g (Just Zero)
f (Just Zero)
(by def) = Suc Zero
(by def) = g (Just Zero)
Case 3
To show: f (Just(Suc n)) = g (Just(Suc n))
IH: f(Just n) = g(Just n)
f (Just(Suc n))
(by def) = Suc (f (Just n))
(by IH) = Suc(g (Just n))
(by def) = Suc(Suc n)
g (Just(Suc n))
(by def) = Suc(Suc n)
Retake InputOutput
Types, Tests, Abstractions
Evaluation
Evaluation 1
-> \g -> g 1 . f 1) drop take evens
(\f -> g 1 . drop 1) take evens
(\g take 1 . drop 1) evens
(-> take 1 (drop 1 x)) evens
(\x take 1 (drop 1 evens)
take 1 (drop 1 (0 : map (+2) evens))
take 1 (drop (1-1) (map (+2) evens))
take 1 (drop 0 (map (+2) evens))
take 1 (map (+2) evens)
take 1 (map (+2) (0 : map (+2) evens))
take 1 ((0 + 2) : map (+2) (map (+2) evens))
0+2) : take 0 ((0 + 2) : map (+2) (map (+2) evens))
(0+2) : []
(2 : []
take 1 (f 0)
take 1 (f 0 ++ [0])
take 1 (f 0 ++ [0] ++ [0])
...
take can never determine whether it’s second argument is a Nil or a Cons, therefore no progress can be made
Evaluation 2
-> \g -> f 1 . g 1) take drop odds
(\f -> take 1 . g 1) drop odds
(\g take 1 . drop 1) odds
(-> take 1 (drop 1 x)) odds
(\x take 1 (drop 1 odds)
take 1 (drop 1 (1 : map (+2) odds))
take 1 (drop (1-1) (map (+2) odds))
take 1 (drop 0 (map (+2) odds))
take 1 (map (+2) odds)
take 1 (map (+2) (1 : map (+2) odds))
take 1 ((1 + 2) : map (+2) (map (+2) odds))
1+2) : take 0 (map (+2) (map (+2) odds))
(1+2) : []
(3 : []
head (f 0)
head (f 0 ++ [0])
head (f 0 ++ [0] ++ [0])
...
head can never determine whether it’s argument is a Nil or a Cons, therefore no progress can be made