Functional Programming and Verification

Chair for Logic and Verification

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
  powTwoAdd 1 3
= fp aux 1 3
= aux (fp aux) 1 3
= (\x y -> x (x y)) ((fp aux) (1 - 1)) 3
= (y -> ((fp aux) (1 - 1)) (((fp aux) (1 - 1)) y)) 3
= (fp aux) (1 - 1) ((fp aux) (1 - 1) 3)
= aux (fp aux) (1 - 1) (aux (fp aux) (1 - 1) 3) -- sharing
= aux (fp aux) 0 (aux (fp aux) 0 3)  -- sharing
= (+) 1 ((+) 1 3)  -- sharing
= (+) 1 4 
= 5
mulPowTwo
  mulPowTwo 4 1
= fix (aux 4) 1
= x 1
= aux 4 x 1
= (\x -> x + x) (x (1 - 1))
= (x (1 - 1)) + (x (1 - 1))
= (aux 4 x (1 - 1)) + (aux 4 x (1 - 1)) -- sharing
= (aux 4 x 0) + (aux 4 x 0) -- sharing
= 4 + 4 -- sharing
= 8
superConst
  superConst 1 2
= fp aux 1 2
= aux (fp aux) 1 2
= (\x y -> x (x y)) ((fp aux) (1 - 1)) 2
= (\y -> ((fp aux) (1 - 1)) ((fp aux) (1 - 1) y)) 2
= ((fp aux) (1 - 1)) ((fp aux) (1 - 1) 2)
= (aux (fp aux) (1 - 1)) (aux (fp aux) (1 - 1) 2) -- sharing
= (aux (fp aux) 0) (aux (fp aux) 0 2) -- sharing
= (\x -> x) ((\x -> x) 2) -- sharing
= ((\x -> x) 2)
= 2

Observational Equivalence

  1. Wrong: Let xs = [1..] and p = head (rev (rev xs)). Then head (rev (rev xs)) diverges but head xs = 1.

  2. Wrong: Let xs = repeat False and p x = if x then x else x. Then p (and xs) = False but p (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
(\f -> \g -> g 1 . f 1) drop take evens  
(\g -> g 1 . drop 1) take evens
(take 1 . drop 1) evens
(\x -> take 1 (drop 1 x)) evens
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
(\f -> \g -> f 1 . g 1) take drop odds
(\g -> take 1 . g 1) drop odds
(take 1 . drop 1) odds
(\x -> take 1 (drop 1 x)) odds
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

Tail Recursion