Functional Programming SS14
Solution – Exam (V3B) 15.09.2014
aaProf. Dr. J. Giesl F. Frohn
Exercise 1 (Quiz): (3 + 3 + 3 = 9 points)
a) Give a type declaration for f such that (f True) (f 1) is well typed in Haskell or explain why such a
type declaration cannot exist.
b) Prove or disprove: If �⊆ A×A is con�uent, then each a ∈ A has at most one normal form w.r.t. �.
c) What is the connection between monotonicity, continuity, and computability?
Solution:
a) f :: a -> b -> Bool
b) Let q1 and q2 be �-normal forms of t. Thent �∗ q1 and t �∗ q2. By con�uence of �, there must be a q
such that q1 �∗ q and q2 �∗ q. Since q1 and q2 are normal forms, we get q1 = q = q2.
c) Every computable function is continuous and every continuous function is monotonic.
Exercise 2 (Programming in Haskell): (6 + 7 + 7 = 20 points)
We de�ne a polymorphic data structure Tree e for binary trees whose nodes store values of type e.
data Tree e = Node e (Tree e) (Tree e) | Empty
The data structure Forest e is used to represent lists of trees.
type Forest e = [Tree e]
Furthermore, we de�ne the following data structure:
data Animal = Squirrel | None
For example, aForest is a valid expression of type Forest Animal.
aForest = [Node Squirrel Empty (Node Squirrel Empty Empty), Node None Empty Empty]
In this exercise, you may use full Haskell and prede�ned functions from the Haskell Prelude.
a) Implement a function hunt together with its type declaration that removes all Squirrels from a Forest
Animal, i.e., each occurrence of a Squirrel should be replaced by None.
For example, hunt aForest should be evaluated to [Node None Empty (Node None Empty Empty),
Node None Empty Empty].
b) Implement a function fold :: (e -> res -> res -> res) -> res -> Tree e -> res to fold a Tree.
The �rst argument of fold is the function that is used to combine the value of the current Node with
the subresults obtained for the two direct subtrees of the current Node. The second argument of fold is
the start value, i.e., the initial subresult. The third argument is the Tree that has to be folded. So for
a Tree t, fold f x t replaces the constructor Node by f and the constructor Empty by x.
As an example, consider the following function:
count :: Animal -> Int -> Int -> Int
count Squirrel x y = x + y + 1
count None x y = x + y
1
Functional Programming SS14
Solution – Exam (V3B) 15.09.2014
Then fold count 0 (Node Squirrel Empty (Node Squirrel Empty Empty)) should evaluate to 2,
i.e., this application of fold counts all Squirrels in a Tree.
c) Implement a function isInhabited together with its type declaration which gets a Forest Animal as
input and returns True if and only if there is a Tree in the Forest that contains a Squirrel. For the
de�nition of isInhabited, use only one de�ning equation where the right-hand side contains a call to
the function fold. Of course, you may (and have to) use the function fold even if you were not able to
solve exercise part (b). Moreover, you may use the function count from exercise part (b).
Note that the function fold operates on a Tree, whereas the function isInhabited operates on a Forest!
Solution:
a) hunt :: Forest Animal -> Forest Animal
hunt forest = map f forest where
f Empty = Empty
f (Node _ l r) = Node None (f l) (f r)
b) fold :: (e -> res -> res -> res) -> res -> Tree e -> res
fold f x Empty = x
fold f x (Node v l r) = f v (fold f x l) (fold f x r)
c) isInhabited :: Forest Animal -> Bool
isInhabited xs = sum (fold count 0 xs) > 0
Exercise 3 (List Comprehensions): (4 + 7 = 11 points)
In this exercise, you can assume that there exists a function divisors :: Int -> [Int] where, for any
natural number x ≥ 2, divisors x computes the list of all its proper divisors (including 1, but excluding x).
So for example, divisors 6 = [1,2,3].
a) Write a Haskell expression in form of a list comprehension to compute all amicable pairs of numbers. A
pair of natural numbers (x, y) with x > y ≥ 2 is amicable if and only if the sum of the proper divisors of
x is equal to y and the sum of the proper divisors of y is equal to x. For example, (284, 220) is amicable:
• The proper divisors of 284 are 1, 2, 4, 71, and 142 and their sum is 220.
• The proper divisors of 220 are 1, 2, 4, 5, 10, 11, 20, 22, 44, 55, and 110 and their sum is 284.
In other words, give a list comprehension for a list that only contains amicable pairs of numbers and, for
every amicable pair of numbers p, there is an n ∈ N such that the nth element of the list is p.
Hint: The function sum :: [Int] -> Int computes the sum of a list of integers.
b) Write a Haskell expression in form of a list comprehension to compute all practical numbers. A natural
number x ≥ 2 is practical if and only if each smaller number y ∈ {1, . . . , x − 1} is equal to the sum of
some of x’s proper divisors. For example, 6 is practical: Its proper divisors are 1, 2, and 3 and we have
4 = 3 + 1 and 5 = 3 + 2.
In your solution, you may use the function sum and the following functions:
• The function any :: (a -> Bool) -> [a] -> Bool tests whether there is an element in the given
list that satis�es the given predicate.
• The function all :: (a -> Bool) -> [a] -> Bool tests whether all elements in the given list
satisfy the given predicate.
• The function subsequences [a] -> [[a]] computes all subsequences of the given list. For exam-
ple, we have:
subsequences [1,2,3] = [[],[1],[2],[1,2],[3],[1,3],[2,3],[1,2,3]]
2
Functional Programming SS14
Solution – Exam (V3B) 15.09.2014
Solution:
a) [(x,y) | x<-[3..], y<-[2..x-1], sum (divisors x) == y, sum (divisors y) == x] b) [x | x<-[2..], all (\y -> any (\s -> sum s == y) (subsequences (divisors x))) [2..x-1]]
Exercise 4 (Semantics): (12 + 7 + 5 + 4 = 28 points)
a) i) Let N∞ be the set of all in�nite sequences of natural numbers (e.g., [0, 0, 2, 2, 4, 4, . . . ] ∈ N∞) and let
≤p⊆ N∞ × N∞ be the relation that compares in�nite sequences of natural numbers by their pre�x
sums. The nth pre�x sum pn(s) for some n ∈ N of a sequence s ∈ N∞ is the sum of the �rst n
elements of s. We have s ≤p s′ if and only if s = s′ or there is an n ∈ N such that pn(s) < pn(s′)
and pm(s) = pm(s
′) for all m ∈ {0, . . . , n− 1}.
1) Prove that ≤p is transitive.
2) Give an example for an in�nite chain in (N∞,≤p).
3) Prove or disprove: The partial order ≤p is complete on N∞.
ii) Prove or disprove: The partial order ≤ is complete on N. Here, ≤ is the usual "less than or equal"
relation.
b) i) Consider the following Haskell function f:
f :: Int -> Int
f 0 = 1
f x = x * x * f (x – 1)
Please give the Haskell declaration for the higher-order function ff corresponding to f, i.e., the
higher-order function ff such that the least �xpoint of ff is f. In addition to the function declaration,
please also give the type declaration of ff. You may use full Haskell for ff.
ii) Let φff be the semantics of the function ff. Give the least �xpoint of φff in closed form, i.e., give
a non-recursive de�nition of the least �xpoint of φff.
Hint: For natural numbers x, the factorial function can be de�ned as follows:
x! =
{
1 if x = 0
x · (x− 1)! if x > 0
c) Consider the data type declarations on the left and, as an example, the graphical representation of the
�rst three levels of the domain for Nats on the right:
data Nats = Z | S Nats
————————————-
type Forest e = [Tree e]
data Tree e =
Node e (Tree e) (Tree e)
| Empty
⊥
Z 2nd level
3rd level
1st level
S Z S (S ⊥)
S ⊥
3
Functional Programming SS14
Solution – Exam (V3B) 15.09.2014
Give a graphical representation of the �rst three levels of the domain for the type Forest Int. The
third level contains the element Empty:⊥, for example.
d) Reconsider the de�nition for Nats from the previous exercise part, i.e., data Nats = Z | S Nats. More-
over, reconsider the function f:
f :: Int -> Int
f 0 = 1
f x = x * x * f (x – 1)
Write a function fNat :: Nats -> Nats in Simple Haskell which, for natural numbers, computes the
same result as the function f. That means, if n >= 0 and f n = x, then we have fNat (Sn Z) = Sx Z.
You can assume that there exists a prede�ned function mult :: Nats -> Nats -> Nats to multiply two
natural numbers. However, there is no prede�ned function to subtract natural numbers of type Nats.
Your solution should use the functions de�ned in the transformation from the lecture such as isaconstr
and argofconstr. You do not have to use the transformation rules from the lecture, though.
Solution:
a) i) 1) Let x ≤p y ≤p z. If x = y or y = z, we are done. Otherwise, there is an n ∈ N such
that pn(x) < pn(y) and pm(x) = pm(y) for all m ∈ {1, . . . , n − 1} and an n′ ∈ N such that
pn′(y) < pn′(z) and pm(y) = pm(z) for all m ∈ {1, . . . , n′ − 1}. Let n′′ = min(n, n′). Then
pn′′(x) < pn′′(z) and pm(x) ≤ pm(z) for all m ∈ {1, . . . , n′′ − 1} and thus x ≤p z.
2) {[0, 0, 0, . . . ], [1, 0, 0, . . . ], [2, 0, 0, . . . ], . . . }
3) Consider the chain above. Its least upper bound is [∞, 0, 0, . . . ] /∈ N∞. Thus, ≤p is not a cpo on
N∞.
ii) Consider the chain N. Its least upper bound is ∞ /∈ N. Thus, ≤ is not complete on N.
b) i) ff :: (Int -> Int) -> (Int -> Int)
ff f 0 = 1
ff f x = x * x * f (x – 1)
ii)
(lfp φff)(x) =
{
(x!)2 if 0 ≤ x
⊥ otherwise
c)
⊥ : (⊥ : ⊥)⊥ : []
[] ⊥ : ⊥
⊥
Empty : ⊥(Node ⊥ ⊥ ⊥) : ⊥
4
Functional Programming SS14
Solution – Exam (V3B) 15.09.2014
d) fNat = \x ->
if (isaZ x) then 1
else mult x (mult x (fNat (argofS x)))
Exercise 5 (Lambda Calculus): (4 + 8 = 12 points)
a) Reconsider the function f from the previous exercise:
f :: Int -> Int
f 0 = 1
f x = x * x * f (x – 1)
Please implement this function in the Lambda Calculus, i.e., give a term t such that, for all x, y ∈ Z,
f x == y if and only if t x can be reduced to y via WHNO-reduction with the →βδ-relation and the set
of rules δ as introduced in the lecture to implement Haskell. You can use in�x notation for prede�ned
functions like (==), (∗) or (−).
b) Let t = λg x.if (x == 0) x (g x) and
δ = { if True→ λx y. x,
if False→ λx y. y,
fix→ λ f. f(fix f)}
∪ { x == x→ True | x ∈ Z}
∪ { x == y → False | x, y ∈ Z, x 6= y}
Please reduce fix t 0 by WHNO-reduction with the →βδ-relation. List all intermediate steps until
reaching weak head normal form, but please write �t� instead of λg x.if (x == 0) x (g x) whenever
possible.
Solution:
a) fix (λf x.if (x == 0) 1 (x ∗ x ∗ (f (x− 1))))
b)
fix t 0
→δ (λ f. (f (fix f))) t 0
→β t (fix t) 0
→β (λx. if (x == 0) x (fix t x)) 0
→β if (0 == 0) 0 (fix t 0)
→δ if True 0 (fix t 0)
→δ (λx y. x) 0 (fix t 0)
→β (λ y. 0) (fix t 0)
→β 0
5
Functional Programming SS14
Solution – Exam (V3B) 15.09.2014
Exercise 6 (Type Inference): (10 points)
Using the initial type assumption A0 := {x :: ∀a.a, g :: ∀a.a}, infer the type of the expression λf.g (f x) using
the algorithm W.
Solution:
W(A0, λf.g (f x))
W(A0 + {f :: b1}, g (f x))
W(A0 + {f :: b1}, g) = (id, b2)
W(A0 + {f :: b1}, f x)
W(A0 + {f :: b1}, f) = (id, b1)
W(A0 + {f :: b1}, x) = (id, b3)
mgu(b1, b3 → b4) = [b1/b3 → b4]
= ([b1/b3 → b4], b4)
mgu(b2, b4 → b5) = [b2/b4 → b5]
= ([b1/b3 → b4, b2/b4 → b5], b5)
= ([b1/b3 → b4, b2/b4 → b5], (b3 → b4)→ b5)
6