Functional Programming SS14
Solution – Exam (V3B) 20.08.2014
aaProf. Dr. J. Giesl F. Frohn
Exercise 1 (Quiz): (3 + 3 + 3 = 9 points)
a) Is \f -> (f True) (f 1) well typed in Haskell? Give the expression’s type or brie�y explain why it is
not well typed.
b) Prove or disprove: If a relation �⊆ A×A is con�uent, then every element of A has a normal form with
respect to �.
c) Are there monotonic functions which are not continuous? If so, give an example. Otherwise, give a brief
explanation.
Solution:
a) No, because the most general type schema for this Haskell expression is non-�at, but such type schemata
are not allowed in Haskell.
b) Counterexample: A = {a} with a � a. Obviously, the relation is con�uent and a does not have a normal
form w.r.t. �.
c) Yes, e.g., the function g : (Z⊥ → Z⊥)→ Z⊥ de�ned by
g(f) =
{
0, if f(x) 6= ⊥Z⊥ for all x ∈ Z
⊥Z⊥ , otherwise
is monotonic, but not continuous.
Exercise 2 (Programming in Haskell): (5 + 7 + 7 = 19 points)
We de�ne a polymorphic data structure Train to represent trains that can contain di�erent types of cargo.
data Train a
= Locomotive (Train a)
| Wagon a (Train a)
| Empty deriving Show
The data structure Cargo is used to represent di�erent types of cargo.
type Quantity = Int
type Weight = Int — in kg
data Cargo
= NoCargo
| Persons Quantity
| Goods Weight deriving Show
For example, aTrain is a valid expression of type Train Cargo.
aTrain = Locomotive (Wagon (Goods 100) (Wagon (Persons 10) (Wagon (Goods 200) Empty)))
Like aTrain, you can assume that every Train consists of a single Locomotive at its beginning followed by a
sequence of Wagons and Empty at its end.
The following function can be used to fold a Train.
1
Functional Programming SS14
Solution – Exam (V3B) 20.08.2014
fold :: (a -> b -> b) -> b -> Train a -> b
fold _ res Empty = res
fold f res (Locomotive t) = fold f res t
fold f res (Wagon c t) = f c (fold f res t)
So for a Train t, fold f res t removes the constructor Locomotive, replaces Wagon by f, and replaces Empty
by res.
In the following exercises, you are allowed to use prede�ned functions from the Haskell-Prelude.
a) Implement a function filterTrain together with its type declaration (filterTrain :: …). The
function filterTrain gets a predicate and an object of type Train a as input and returns an object of
type Train a that only contains those wagons from the given Train whose cargo satis�es the predicate.
For example, assume that the function areGoods is implemented as follows:
areGoods :: Cargo -> Bool
areGoods (Goods _) = True
areGoods _ = False
Then the expression filterTrain areGoods aTrain should be evaluated to
Locomotive (Wagon (Goods 100) (Wagon (Goods 200) Empty)).
b) Implement a function buildTrain :: [Cargo] -> Train Cargo. In the resulting Train, a single Wagon
must not contain more than 1000 kg of Goods. If the input list contains Goods that weigh more than
1000 kg, then these Goods must not be contained in the resulting train. Apart from this restriction, all
the Cargo given via the input list has to be contained. Moreover, the resulting Train has to consist of
a single Locomotive at its beginning, followed by a sequence of Wagons and Empty at its end. In your
solution, you should use the function filterTrain even if you could not solve the previous exercise part.
For example, buildTrain [Persons 10, Goods 2000, Goods 1000] should be evaluated to the ex-
pression Locomotive (Wagon (Persons 10) (Wagon (Goods 1000) Empty)).
c) Implement a function weight together with its type declaration which computes the weight of all Goods
in a train of type Train Cargo. For the de�nition of weight, use only one de�ning equation where the
right-hand side is a call to the function fold.
For example, weight aTrain should be evaluated to 300.
Solution:
a) filterTrain :: (a -> Bool) -> Train a -> Train a
filterTrain _ Empty = Empty
filterTrain p (Locomotive t) = Locomotive (filterTrain p t)
filterTrain p (Wagon c t) = if (p c) then (Wagon c t’) else t’
where t’ = filterTrain p t
b) buildTrain :: [Cargo] -> Train Cargo
buildTrain cargo = filterTrain (\c -> case c of
Goods x -> x <= 1000 _ -> True)
(Locomotive (foldr Wagon Empty cargo))
c) weight :: Train Cargo -> Int
weight = fold (\c res -> case c of
Goods x -> res + x
_ -> res)
0
2
Functional Programming SS14
Solution – Exam (V3B) 20.08.2014
Exercise 3 (List Comprehensions): (3 + 3 + 5 = 11 points)
a) Write a Haskell function divisors :: Int -> [Int] to compute the list of all proper divisors of a given
number x. Here, you can assume x ≥ 2. The result of divisors x includes 1, but not the number x
itself. So for example, divisors 6=[1,2,3]. Use only one de�ning equation where the right-hand side
is a list comprehension.
Hint: The function mod :: Int -> Int -> Int can be used to compute the modulo of two integers.
b) Write a Haskell expression in form of a list comprehension to compute all perfect numbers. A number
x with x ≥ 2 is perfect if and only if the sum of its proper divisors is equal to itself. For example, 6 is
perfect, since its proper divisors are 1, 2, and 3 and the sum of its proper divisors is 6. In your solution,
you should use the function divisors even if you were not able to solve the previous exercise part.
Hint: The function sum :: [Int] -> Int computes the sum of a list of integers.
c) Write a Haskell expression in form of a list comprehension to compute all semiperfect numbers. A number
x with x ≥ 2 is semiperfect if and only if the sum of all or some of its proper divisors is equal to itself.
For example, 12 is semiperfect: Its proper divisors are 1, 2, 3, 4, and 6 and the sum of 2, 4, and 6 is 12.
In your solution, you should use the function divisors even if you were not able to solve exercise part
(a). Moreover, you may use the function sum and the following functions:
• The function exists :: (a -> Bool) -> [a] -> Bool tests whether there is an element in the
given list that satis�es 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]]
Solution:
a) divisors :: Int -> [Int]
divisors x = [y|y<-[1..x-1], x `mod` y == 0]
b) perfect :: [Int]
perfect = [x|x<-[2..], sum (divisors x) == x]
c) semiperfect :: [Int]
semiperfect = [x|x<-[2..], exists (\s -> sum s == x) (subsequences (divisors x))]
Exercise 4 (Semantics): (10 + 10 + 6 + 3 = 29 points)
a) i) Let L[] = {[],[[]],[[[]]], . . . }, i.e., L[] contains all lists where m opening brackets are followed
by m closing brackets for an m ∈ N \ {0}. Let ≤nl⊆ L[] × L[] be the relation that compares the
nesting-level of two lists. More formally, if nl(x) is the nesting level of the list x and ≤⊂ N × N is
the usual less-or-equal relation, then
l ≤nl l′ ⇐⇒ nl(l) ≤ nl(l′)
So we have, e.g., []≤nl[[]] because the nesting level of [] is one and the nesting level of [[]] is
two.
1) Give an example for an in�nite chain in (L[],≤nl).
2) Prove or disprove: the partial order ≤nl is complete on L[].
3
Functional Programming SS14
Solution – Exam (V3B) 20.08.2014
ii) Let L0 be the set of all Haskell lists containing only zeros (so, e.g., [] ∈ L0 and [0, 0, 0] ∈ L0)
and let ≤len⊆ L0 × L0 be the relation that compares the length of two lists where all in�nite lists
are considered to have the same length. More formally, if len(x) is the length of the list x and
≤⊂ N ∪ {∞} × N ∪ {∞} is the usual less-or-equal relation, then
l ≤len l′ ⇐⇒ len(l) ≤ len(l′)
1) Give an example for an in�nite chain in (L0,≤len).
2) Prove or disprove: the partial order ≤len is complete on L0.
b) i) Consider the following Haskell function f:
f :: (Int, Int) -> Int
f (x, 0) = 1
f (x, y) = x * f (x, y – 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 for ff. You may use full Haskell for ff.
ii) Let φff be the semantics of the function ff. Give the de�nition of φ
n
ff(⊥) in closed form for any
n ∈ N, i.e., give a non-recursive de�nition of the function that results from applying φff n-times to
⊥.
iii) Give the de�nition of the least �xpoint of φff in closed form.
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
————————————-
data Train a
= L (Train a) — a Locomotive
| W a (Train a) — a Wagon
| E — an Empty Train
data Cargo
= NC — No Cargo
| P Int — n Persons ⊥
Z 2nd level
3rd level
1st level
S Z S (S ⊥)
S ⊥
Give a graphical representation of the �rst three levels of the domain for the type Train Cargo. The
third level contains the element W (P ⊥) ⊥, for example. Note that the domain for the type Train
Cargo also contains Trains with multiple locomotives, Trains without E at their ends, and so on. In
other words, the assumption from Exercise 2 (�Assume that every Train consists of a single Locomotive
at its beginning followed by a sequence of Wagons and Empty at its end.�) does not hold for this exercise.
d) Consider the de�nition for Nats from the previous exercise part, i.e., data Nats = Z | S Nats.
Moreover, consider the following Haskell function f’:
f’ :: Int -> Int -> Int
f’ x 0 = 1
f’ x y = x * f’ x (y – 1)
Write a function fNat :: Nats -> Nats -> Nats in Simple Haskell which, for natural numbers,
computes the same result as the function f’. That means, if n,m >= 0 and f’ n m = x, then we have
fNat (Sn Z) (Sm Z) = Sx Z. You can assume a prede�ned function mult :: Nats -> Nats -> Nats
4
Functional Programming SS14
Solution – Exam (V3B) 20.08.2014
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, argofconstr, and bot. You do not have to use the transformation rules from the lecture,
though.
Solution:
a) i) 1) {[], [[]], [[[]]], . . . }
2) Consider the chain above. Since it contains in�nitely many elements with increasing nesting
level, its upper bounds have to have in�nite nesting level. Since lists with in�nite nesting level
are not contained in L[], ≤n is not a cpo.
ii) 1) {[], [0], [0,0], . . . }
2) The relation ≤len is a cpo i� L0 has a least element w.r.t. ≤len and every ≤len-chain has a least
upper bound in L0. Obviously, the least element is the empty list []. Let C be a chain. If
C is �nite, then the longest list in C is the least upper bound. Otherwise, the in�nite list l∞
containing only zeros (as de�ned by zeros=0:zeros) is the least upper bound. Thus, ≤len is a
cpo.
b) i) ff :: ((Int, Int) -> Int) -> ((Int, Int) -> Int)
ff f (x, 0) = 1
ff f (x, y) = x * f (x, y – 1)
ii)
(φnff(⊥))(x, y) =
1 if y = 0 ∧ 0 < n
xy if 0 < y < n ∧ x 6= ⊥
⊥ otherwise
iii)
(lfp φff)(x, y) =
1 if y = 0
xy if 0 < y ∧ x 6= ⊥
⊥ otherwise
c)
L E
EL ⊥
⊥
L (L ⊥) W ⊥ E
W ⊥ ⊥
W (P ⊥) ⊥W ⊥ (L ⊥)L (W ⊥ ⊥) W NC ⊥W ⊥ (W ⊥ ⊥)
d) fNat = \x -> \y ->
if (isaZ y) then 1
else mult x (fNat x (argofS y))
5
Functional Programming SS14
Solution – Exam (V3B) 20.08.2014
Exercise 5 (Lambda Calculus): (4 + 8 = 12 points)
a) Reconsider the function f’ from the previous exercise:
f’ :: Int -> Int -> Int
f’ x 0 = 1
f’ x y = x * f’ x (y – 1)
Please implement this function in the Lambda Calculus, i.e., give a term f such that, for all x, y, z ∈ Z,
f’ x y == z if and only if f x y can be reduced to z 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 = λ add x y. if (y == 0) x (add (x+ 1) (y − 1))
and
δ = { if True→ λx y. x,
if False→ λx y. y,
fix→ λ f. f(fix f)}
∪ { x− y → z | x, y, z ∈ Z ∧ z = x− y}
∪ { x+ y → z | x, y, z ∈ Z ∧ z = x+ y}
∪ { x == x→ True | x ∈ Z}
∪ { x == y → False | x, y ∈ Z, x 6= y}
Please reduce fix t 0 0 by WHNO-reduction with the →βδ-relation. List all intermediate steps until
reaching weak head normal form, but please write �t� instead of
λ add x y. if (y == 0) x (add (x+ 1) (y − 1))
whenever possible.
Solution:
a) fix (λ f x y. if (y == 0) 1 (x ∗ (f x (y − 1))))
6
Functional Programming SS14
Solution – Exam (V3B) 20.08.2014
b)
fix t 0 0
→δ (λ f. (f (fix f))) t 0 0
→β t (fix t) 0 0
→β (λx y. if (y == 0) x ((fix t) (x+ 1) (y − 1))) 0 0
→β (λ y. if (y == 0) 0 ((fix t) (0 + 1) (y − 1))) 0
→β if (0 == 0) 0 ((fix t) (0 + 1) (0− 1))
→δ if True 0 ((fix t) (0 + 1) (0− 1))
→δ (λx y. x) 0 ((fix t) (0 + 1) (0− 1))
→β (λ y. 0) ((fix t) (0 + 1) (0− 1))
→β 0
Exercise 6 (Type Inference): (10 points)
Using the initial type assumption A0 := {x :: ∀a.a}, infer the type of the expression λf.f (f x) using the
algorithm W.
Solution:
W(A0, λf.f (f x))
W(A0 + {f :: b1}, f (f x))
W(A0 + {f :: b1}, f) = (id, b1)
W(A0 + {f :: b1}, f x)
W(A0 + {f :: b1}, f) = (id, b1)
W(A0 + {f :: b1}, x) = (id, b2)
mgu(b1, b2 → b3) = [b1/b2 → b3]
= ([b1/b2 → b3], b3)
mgu(b2 → b3, b3 → b4) = [b2/b3, b4/b3]
= ([b1/b3 → b3, b2/b3, b4/b3], b3)
= ([b1/b3 → b3, b2/b3, b4/b3], (b3 → b3)→ b3)
7