CS计算机代考程序代写 data structure Lambda Calculus chain Haskell algorithm Solution2014-08-20-V3B.pdf

Solution2014-08-20-V3B.pdf

Solution2014-09-15-V3B.pdf

Solution2016-08-17.pdf

Solution2016-09-19.pdf

Solution2019-08-12 (1).pdf

Solution2019-09-10 (1).pdf

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.

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)

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[].

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

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

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

Functional Programming SS14
Solution – Exam (V3B) 20.08.2014

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)

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

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]]

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)

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 ⊥

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

⊥ : (⊥ : ⊥)⊥ : []

[] ⊥ : ⊥

⊥

Empty : ⊥(Node ⊥ ⊥ ⊥) : ⊥

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

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

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)

Functional Programming SS16
Solution – Exam 17.08.2016

aaProf. Dr. J. Giesl D. Korzeniewski

Exercise 1 (Programming in Haskell): (6 + 6 + 7 + 16 = 35 points)

We de�ne a polymorphic data structure Warehouse to represent a warehouse that can contain goods.

data Warehouse a

= Corridor (Warehouse a) (Warehouse a)

| Shelf [a] deriving Show

The data structure Goods is used to represent di�erent types of goods.

data Goods

= NoGoods | Box | Barrel deriving (Show, Eq)

For example, aWarehouse is a valid expression of type Warehouse Goods.

aWarehouse = Corridor (Shelf [Box, Box]) (Corridor (Shelf [Barrel, NoGoods]) (Shelf [Box]))

The following function can be used to fold a Warehouse:

fold :: (a -> a -> a) -> a -> Warehouse a -> a

fold f res (Shelf xs) = foldr f res xs

fold f res (Corridor left right) = f (fold f res left) (fold f res right)

In the following exercises, you are allowed to use the functions given above, functions implemented in preceding
parts of the exercise, and prede�ned functions from the Haskell-Prelude. Moreover, you are always allowed to
implement additional auxiliary functions.

a) Implement a function buildWarehouse :: [a] -> Int -> Warehouse a that gets a list and a number
indicating how many items may be stored in one shelf. The function should return a warehouse containing
all items in the input list, distributed on the minimal number of shelves possible while respecting the
limit given by the second input.

If the input list is the empty list, Shelf [] should be returned. If the integer argument is less than 1
the function may behave arbitrarily.

For example buildWarehouse [Box, Box, Barrel, NoGoods, Box] 2 should result in a warehouse
with 3 shelves which together contain all elements from the list. A possible result would be aWarehouse,
as de�ned above.

b) Implement a function mapWarehouse together with its type declaration (mapWarehouse :: …). The
function mapWarehouse gets a unary function and a Warehouse, and applies the function to every element
stored in the lists of the Shelf objects of the Warehouse. For example, the expression
mapWarehouse (\x -> if x == Box then NoGoods else x) returns a function that replaces all Boxes
in a Warehouse by NoGoods.

c) Implement a function inventory :: Warehouse Goods -> (Int, Int) that returns a tuple containing
the number of Boxes and Barrels in the input Warehouse. For example inventory aWarehouse should
yield (3, 1).

Hints:

You may use fold given above and mapWarehouse from the previous task (even if you have not solved
the previous task).

d) In this part of the exercise, you should implement a program that controls a forklift. The goal of the
forklift is to store Goods in a Warehouse. Goods can only be placed in free spaces indicated by NoGoods
or stacked on top of a shelf.

Implement a function storeGoods :: Warehouse Goods -> Goods -> IO (). Its input is a Warehouse
that contains Goods. It processes the Warehouse as follows:

Functional Programming SS16
Solution – Exam 17.08.2016

For a Corridor, it prints “Do you want to turn left or right? (l|r)”. If the user answers “l”,
it proceeds with the �rst argument of the Corridor, if the answer is “r” it continues with the second
argument of Corridor, otherwise an error message “Incorrect input” is printed and the question is
repeated.

Once a Shelf is encountered the user is asked “How high do you want to raise the fork?” and an
integer k is read. The program then distinguishes the following cases:

• The number k is less than 0: An error message “Your forklift fell over” is printed.
• The number k is a position of the list in the Shelf: (Here an object Shelf [x_0, …, x_n] has
positions 0, . . . , n and the object at position i is x_i.) If the list contains NoGoods at position
k, the message “Inserted the ” is printed where is replaced by Box or Barrel
depending on the input, otherwise the message “No room in the shelf” is printed.

• The number k is at least the length of the list: The message “Stacked on top of the shelf” is
printed.

Afterwards the program terminates.

A successful run might look as follows:

*Main> storeGoods (Corridor (Shelf [Barrel, NoGoods, Box]) (Shelf [Box])) Barrel

Do you want to turn left or right? (l|r) l

How high do you want to raise the fork? 1

Inserted the Barrel

In the following run, the goods are stacked on top of a shelf:

*Main> storeGoods (Corridor (Shelf [Barrel, NoGoods, Box]) (Shelf [Box])) Barrel

Do you want to turn left or right? (l|r) y

Incorrect input

Do you want to turn left or right? (l|r) r

How high do you want to raise the fork? 42

Stacked on top of the shelf

Hints:

You should use the function getChar :: IO Char to read a character input from the user. Moreover,
you may assume there is a function getInt :: IO Int that reads an integer from the command line.
To print a String, you should use the function putStr :: String -> IO () or the function putStrLn
:: String -> IO (), if the output should end with a line break. You should use the function
show :: Goods -> String to convert a Goods object to a String. To save space, you may also assume
that the following additional declarations exist in your program:

leftRight, incorrect, howHigh, fellOver, noRoom, stacked :: String

leftRight = “Do you want to turn left or right? (l|r) ”

incorrect = “Incorrect input”

howHigh = “How high do you want to raise the fork? ”

fellOver = “Your forklift fell over”

noRoom = “No room in the shelf”

stacked = “Stacked on top of the shelf”

Solution:

a) buildWarehouse :: [a] -> Int -> Warehouse a
buildWarehouse [] _ = Shelf []

buildWarehouse xs max | length xs <= max = Shelf xs | otherwise = Corridor (Shelf (take max xs)) (buildWarehouse (drop max xs) max) 2 Functional Programming SS16 Solution - Exam 17.08.2016 b) mapWarehouse :: (a -> b) -> Warehouse a -> Warehouse b
mapWarehouse f (Shelf xs) = Shelf (map f xs)

mapWarehouse f (Corridor left right) =

Corridor (mapWarehouse f left) (mapWarehouse f right)

c) inventory :: Warehouse Goods -> (Int, Int)
inventory w =

fold (\(x, y) (x’, y’) -> (x+x’, y+y’)) (0, 0) (mapWarehouse invHelper w)

where invHelper Box = (1, 0)

invHelper Barrel = (0, 1)

invHelper _ = (0, 0)

d) storeGoods :: Warehouse Goods -> Goods -> IO ()
storeGoods (Corridor left right) g = do

putStr leftRight

input <- getChar putStrLn "" case input of 'l' -> storeGoods left g

‘r’ -> storeGoods right g

_ -> do

putStrLn incorrect

storeGoods (Corridor left right) g

storeGoods (Shelf xs) g = do

putStr howHigh

input <- getInt case () of _ | input < 0 -> putStrLn fellOver

| input < (length xs) -> if (xs !! input) == NoGoods

then putStrLn (“Inserted the “++(show g))

else putStrLn noRoom

| otherwise -> putStrLn stacked

Exercise 2 (Semantics): (17 + 16 + 9 = 42 points)

a) i) Let D1, D2, and D3 be domains with complete orders v1, v2, and v3, respectively. Let g : D1 → D2
and f : D2 → D3 be strict and monotonic functions. Here, we say that g is strict on a (possibly
non-�at) domain D1 if and only if g(⊥D1) = ⊥D2 . As usual, f ◦ g is the composition of f and g
(i.e., (f ◦ g)(x) = f(g(x))). Prove or disprove whether f ◦ g is:
1) strict

2) monotonic

ii) Let Σ = {a, . . . , z}, let Σ∗ be the set of all �nite words over the alphabet Σ, and let ≤lex denote
the usual lexicographic order on Σ∗ (which corresponds to the order of words in a lexicon). So, for
example abc ≤lex abcd and xyz ≤lex xzz.
Prove or disprove each of the following statements:

1) There is an in�nite chain in (Σ∗,≤lex).
2) The order ≤lex is complete on Σ∗.
3) The order ≤lex is con�uent.

b) i) Consider the following Haskell function f:

f :: (Int, Int) -> Int

f (x, 0) = 0

f (x, y) = (x * y) + f (x, y – 1)

Functional Programming SS16
Solution – Exam 17.08.2016

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
⊥. Here, you should assume that Int can represent all integers, so no over�ow can occur.

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 Warehouse a

= Corridor

(Warehouse a)

| Shelf [a]

data Goods

= NoGoods | Box | Barrel ⊥

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 Warehouse Goods.
You may abbreviate the constructors to the �rst two letters (i.e., you may write Co instead of Corridor).

Solution:

a) i) 1)

(f ◦ g)(⊥D1) = f(g(⊥D1)) Def. of ◦
= f(⊥D2) g is strict
= ⊥D3 f is strict

Thus f ◦ g is strict.
2) Let d1, d

′
1 ∈ D1 such that d1 vD1 d′1. Because g is monotonic, we have that g(d1) vD2 g(d′1).

Because f is monotonic, we also have f(g(d1)) vD3 f(g(d′1)). Therefore, (f ◦ g)(d1) vD3 (f ◦
g)(d′1). So, f ◦ g is monotonic.

ii) 1) C = {z, zz, zzz, . . . } is an in�nite chain.
2) The relation ≤lex is not a cpo. A relation ≤lex is a cpo i� Σ∗ has a least element w.r.t. ≤lex and

every ≤lex-chain has a least upper bound in Σ∗. Obviously, the least element is the empty word
�. Consider C = {z, zz, zzz, . . . }. For every word w ∈ Σ∗ of length n ∈ N we have w ≤lex zn+1,
w 6= zn+1 and zn+1 ∈ Σ∗. Because Σ∗ contains only �nite words, this implies that the chain C
has no least upper bound in Σ∗.

3) The relation ≤lex is con�uent. If u ≤lex v, u ≤lex w and n is the maximum of the lengths of
v and w, then we have v ≤lex zn and w ≤lex zn. This su�ces since ≤lex is transitive and thus
≤∗lex=≤lex.

Functional Programming SS16
Solution – Exam 17.08.2016

b) i) ff :: ((Int, Int) -> Int) -> ((Int, Int) -> Int)
ff f (x, 0) = 0

ff f (x, y) = (x * y) + f (x, y – 1)

ii)

(φnff(⊥))(x, y) =




0 if y = 0 ∧ 0 < n x·y·(y+1) 2 if 0 < y < n ∧ x 6= ⊥ ⊥ otherwise iii) (lfp φff)(x, y) =   0 if y = 0 x·y·(y+1) 2 if 0 < y ∧ x 6= ⊥ ⊥ otherwise c) Co ⊥ (Co ⊥ ⊥) Co (Sh ⊥) ⊥ Sh ⊥ Sh (⊥ : ⊥) ⊥ Co ⊥ ⊥ Sh [ ]Co (Co ⊥ ⊥) ⊥ Co ⊥ (Sh ⊥) Exercise 3 (Lambda Calculus): (5 + 14 + 6 = 25 points) a) Consider the following variant of the function from Exercise 2b: f' :: Int -> Int -> Int

f’ x 0 = 0

f’ x y = (x * y) + f’ x (y – 1)

Please implement this function in the lambda calculus, i.e., give a lambda term q such that, for all
x, y, z ∈ Z, f’ x y == z if and only if q 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 = λ g x y. if (x == 1) Nil (Cons y (g (x− 1) (y ∗ x)))

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 ∗ y → z | x, y, z ∈ Z ∧ z = x · y}
∪ { x == x→ True | x ∈ Z}
∪ { x == y → False | x, y ∈ Z, x 6= y}

Functional Programming SS16
Solution – Exam 17.08.2016

Please reduce fix t 3 1 by WHNO-reduction with the →βδ-relation. List all intermediate steps until
reaching weak head normal form, but please write �t� instead of

λ g x y. if (x == 1) Nil (Cons y (g (x− 1) (y ∗ x)))

whenever possible.

c) Consider the representation of natural numbers in the pure lambda calculus presented in the lecture, i.e.,
n ∈ N is represented by the term λ f x. fn x. Give a pure lambda term for multiplication, i.e., a term
mult such that mult(λ f x. fn x)(λ f x. fm x) can be reduced to λ f x. fn·m x.

Explain your solution shortly. You may give a reduction sequence as explanation.

Solution:

a) fix (λ f x y. if (y == 0) 0 ((x ∗ y) + (f x (y − 1))))

fix t 3 1

→δ (λ f. (f (fix f))) t 3 1

→β t (fix t) 3 1

→β (λx y. if (x == 1) Nil (Cons y ((fix t) (x− 1) (y ∗ x)))) 3 1

→β (λ y. if (3 == 1) Nil (Cons y ((fix t) (3− 1) (y ∗ 3)))) 1

→β if (3 == 1) Nil (Cons 1 ((fix t) (3− 1) (1 ∗ 3)))

→δ if False Nil (Cons 1 ((fix t) (3− 1) (1 ∗ 3)))

→δ (λx y. y) Nil (Cons 1 ((fix t) (3− 1) (1 ∗ 3)))

→β (λ y. y) (Cons 1 ((fix t) (3− 1) (1 ∗ 3)))

→β Cons 1 ((fix t) (3− 1) (1 ∗ 3))

mult = λn m f. n (m f) or

mult = λn m f.m (n f)

The representation of m applies the function f m times to some x: (m f). This is applied n times to
some x by supplying it as the function to the representation of n. This results in n ·m applications of f
to some x, which represents n ·m.

Functional Programming SS16
Solution – Exam 17.08.2016

mult(λ f x. fn x)(λ f x. fm x)

→β(λm f. (λ f x. fn x) (m f))(λ f x. fm x)

→βλ f. (λ f x. fn x) ((λ f x. fm x) f)

→βλ f. (λ f x. fn x) (λx. fm x)

→βλ f. (λx. (λx. fm x)n x)

=λ f.
(
λx.

(
(λx. fm x)

(
. . . ((λx. fm x) x)

)))
→∗βλ f. (λx. f

m·n x)

=λ f x. fm·n x

Exercise 4 (Type Inference): (18 points)

Using the initial type assumption A0 := {h :: ∀a.a}, infer the type of the expression λx.h (xh) using the
algorithm W.

Solution:

W(A0, λx.h (xh))
W(A0 + {x :: b1}, h (xh))

W(A0 + {x :: b1}, h) = (id, b2)
W(A0 + {x :: b1}, x h)

W(A0 + {x :: b1}, x) = (id, b1)
W(A0 + {x :: b1}, h) = (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)

Functional Programming SS16
Solution – Exam 19.09.2016

aaProf. Dr. J. Giesl D. Korzeniewski

Exercise 1 (Programming in Haskell): (7 + 7 + 5 + 18 = 37 points)

We de�ne a polymorphic data structure Maze to represent a maze (i.e., a labyrinth) that can contain treasures
and traps. The data structure Discovery is used to represent traps and treasures.

data Maze a data Discovery

= Intersection (Maze a) (Maze a) = Trap String

| Corridor a (Maze a) | Treasure

| DeadEnd a

| Exit

For example, aMaze is a valid expression of type Maze Discovery.

aMaze = Intersection (Corridor (Trap “a trap door”) (DeadEnd Treasure))

(Intersection (DeadEnd Treasure) Exit)

a) Implement a function buildMaze :: Int -> Maze Int that gets a random seed as input.

The call (buildMaze seed) for an integer seed should create a maze according to the following rules:

• with probability 1
5
the function returns Exit

• with probability 1
5
the function returns a DeadEnd with a random number as argument

• with probability 1
5
the function returns a Corridor with a random number and a random submaze

• with probability 2
5
the function returns an Intersection with two random submazes, which di�er

with high probability (i.e., they are constructed from di�erent seeds)

Hints:

• You are given a function rand :: Int -> Int which creates a new uniformly distributed (pseudo)
random number from an input number, the seed. Already a small di�erence in the seed creates very
di�erent results (i.e., the sequence produced by consecutive calls (rand seed) and (rand (seed+1))
is reasonably random). Also using a previous random number as new seed produces reasonably ran-
dom sequences.

For each decision during the generation, for each number inserted into the maze, and for each
submaze a new random number should be used. So for any integer seed never use (rand seed)
twice in a computation.

• To get a result with a certain probability, you should generate a (pseudo) random number and
perform an appropriate case analysis depending on the value of this random number.

b) Implement a function mapMaze which gets a function and a maze as input. It should return a maze,
where the function is applied to each element stored in the maze. For example, if it gets a function
even :: Int -> Bool and a maze of type Maze Int, it should return a maze where we have True at
each position where there was an even number in the input maze.

Also give a reasonable type declaration for the function!

c) Implement a function populateMaze :: Maze Int -> Maze Discovery which takes a maze as returned
by buildMaze from part a) and returns a maze �lled with di�erent Discoveries which depend on the
numbers that were in the maze before. The function should replace even numbers with
(Trap “a trap door”) and odd numbers by a Treasure.

Hints:

You may use mapMaze from the previous task (even if you have not solved the previous task).

d) In this part of the exercise, you should implement a small game where you control an adventurer who
explores a Maze Discovery.

Functional Programming SS16
Solution – Exam 19.09.2016

1) Implement a function react :: Discovery -> Int -> IO Int that handles the reaction to a
Discovery. It gets a Discovery and the number of already collected treasures as input. For traps
it should output a message indicating that a trap was reached including the String of the trap and
that all treasures were lost. So the result in this case is 0, wrapped in the IO monad. For treasures,
it should print that a treasure was found and the new number of treasures collected. The result in
this case is the input number incremented by one, wrapped in the IO monad.

Hints:

• To print a String, you should use the function putStr :: String -> IO () or the function
putStrLn :: String -> IO (), if the output should end with a line break.

2) Implement a function exploreMaze :: Maze Discovery -> [Maze Discovery] -> Int -> IO ().
This function is the main loop of the game. The �rst input parameter is the maze in front of the
adventurer, the second parameter is the current path of Intersections back to the starting point,
and the third parameter is the number of already collected treasures.
At an Intersection the user gets asked for input, the possibilities are l for left, r for right, or b for
back. Depending on the input, the exploration should continue at the �rst (left) or second (right)
argument of the Intersection, or for input b at the �rst Intersection in the list of exploreMaze’s
second input parameter.
At a Corridor or DeadEnd, �rst react should be called and after that, the exploration continues either
at the following maze or, in case of a DeadEnd, at the �rst Intersection in the list of exploreMaze’s
second input parameter.
At an Exit, the user gets a message which indicates that the adventurer escaped the maze and prints
the number of treasures collected.
During the main loop you should always update the current path back to the starting point if you
move out of an Intersection and the function react from 1) can help you to update the current
number of treasures.
We assume that one can also escape the maze via the entrance. So, whenever the adventurer should
go back, either because of a DeadEnd or the user input b, but the list in the second input parameter
is empty, the function should behave as if an Exit was encountered.

A run might look as follows:

*Main> exploreMaze aMaze [] 0

Go left, right, or back? (l|r|b) l

You reached a trap door and lost your treasures!

You found another treasure! You now have 1 treasures.

Go left, right, or back? (l|r|b) l

You reached a trap door and lost your treasures!

You found another treasure! You now have 1 treasures.

Go left, right, or back? (l|r|b) r

Go left, right, or back? (l|r|b) l

You found another treasure! You now have 2 treasures.

Go left, right, or back? (l|r|b) b

Go left, right, or back? (l|r|b) r

You escaped the maze with 2 treasures.

Hints:

• You should use the function getChar :: IO Char to read a character input from the user.
• You do not have to handle wrong user input correctly, i.e., you may assume that the user will only
supply valid input.

• You do not have to pay attention to output formating (spaces, line breaks).
• You do not have do modify the maze, e.g, if treasures are found they are not removed but may be
collected multiple times.

Functional Programming SS16
Solution – Exam 19.09.2016

Solution:

a) buildMaze :: Int -> Maze Int
buildMaze seed | m5 == 0 = Exit

| m5 == 1 = DeadEnd (rand (seed+1))

| m5 == 2 = Corridor (rand (seed+1)) (buildMaze (seed+2))

| otherwise = Intersection (buildMaze (seed+1)) (buildMaze (seed+2))

where m5 = (rand seed) `mod` 5

b) mapMaze :: (a -> b) -> Maze a -> Maze b
mapMaze f (Intersection left right) = Intersection (mapMaze f left) (mapMaze f right)

mapMaze f (Corridor a maze) = Corridor (f a) (mapMaze f maze)

mapMaze f (DeadEnd a) = DeadEnd (f a)

mapMaze _ _ = Exit

c) populateMaze :: Maze Int -> Maze Discovery
populateMaze maze = mapMaze populate maze

where populate x | even x = Trap “a trap door”

| otherwise = Treasure

d) 1) react :: Discovery -> Int -> IO Int
react (Trap s) t = do

putStrLn (“You reached “++s++” and lost your treasures!”)

return 0

react Treasure t = do

putStrLn (“You found another treasure! You now have “++(show t)++” treasures.”)

return (t+1)

2) exploreMaze :: Maze Discovery -> [Maze Discovery] -> Int -> IO ()
exploreMaze (Intersection left right) ms t = do

putStr “Go left, right, or back? (l|r|b) ”

input <- getChar putStrLn "" case input of 'l' -> exploreMaze left ((Intersection left right):ms) t

‘r’ -> exploreMaze right ((Intersection left right):ms) t

‘b’ -> exploreMaze (head’ ms) (tail ms) t

where head’ [] = Exit

head’ (x:xs) = x

exploreMaze (Corridor a m) ms t = do

new_t <- react a t exploreMaze m ms new_t exploreMaze (DeadEnd a) ms t = do new_t <- react a t exploreMaze (head' ms) (tail ms) new_t where head' [] = Exit head' (x:xs) = x exploreMaze Exit _ t = do putStrLn ("You escaped the maze with "++(show t)++" treasures.") 3 Functional Programming SS16 Solution - Exam 19.09.2016 Exercise 2 (Semantics): (17 + 12 + 9 = 38 points) a) i) Prove or disprove continuity for each of the functions f, g : (Z⊥ → Z⊥)→ Z⊥ f(h) = { 0 if h(0) = 0 ⊥ otherwise g(h) = { 0 if h(x) = 0 holds for all x ∈ Z⊥ ⊥ otherwise If you want to make use of the fact that computable functions are continuous, give an implementation of the function and an argument for the correctness of the implementation. ii) Let L denote the set of all Haskell lists of type [Int]. For example [1, 3, 5, 5, 2], [1, 2, 3, 2, 1], and the in�nite list [3, 6, 9, 12, . . . ] are contained in L. Let ` ∈ L. We de�ne s : L→ N∪{∞} where s(`) is the length of the longest pre�x of ` that is sorted in ascending order. For example s([1, 3, 5, 5, 2]) = 3, s([4, 3, 1]) = 1, and s([3, 6, 9, 12, . . . ]) =∞ Let ≤sort ⊂ L×L be the partial order de�ned as `1 ≤sort `2 if and only if s(`1) < s(`2) or `1 = `2. Here, we have n <∞ for every n ∈ N, but ∞ ≮∞. Prove or disprove each of the following statements: 1) There is an in�nite chain in (L,≤sort). 2) The order ≤sort is complete on L. 3) The order ≤sort is con�uent. b) i) Consider the following Haskell function f: f :: (Int, Int) -> Int

f (x, 0) = x

f (x, y) = y * f (x, y – 1)

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
⊥. Here, you should assume that Int can represent all integers, so no over�ow can occur.

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 Maze a

= C a (Maze a)

| D a

| E

data Discovery

= Tp String | Ts

⊥

Z 2nd level

3rd level

1st level

S Z S (S ⊥)

S ⊥

Functional Programming SS16
Solution – Exam 19.09.2016

Give a graphical representation of the �rst three levels of the domain for the type Maze Discovery.

Solution:

a) i) The function f is continuous. Let C = {hi | i ∈ N} ⊂ Z⊥ → Z⊥ be a chain. Either there is an i
such that hi(0) = 0, then also for all j > i, hj(0) = 0 and thus (tC)(0) = 0. Hence, f(tC) = 0
and tf(C) = t{⊥, 0} = 0. Otherwise for all i we have hi(0) 6= 0 and thus (tC)(0) 6= 0. Hence,
f(tC) = ⊥ and tf(C) = t{⊥} = ⊥.
The function g is not continuous. Let C ′ = {h′i | i ∈ N} where h

′
i(x) = 0 i� x < i or x = ⊥, else h′i(x) = ⊥. For all hi ∈ C ′, g(hi) = ⊥ but tC ′ is the constant function 0, so g(tC ′) = 0 6= tg(C ′) = t{⊥} = ⊥. ii) 1) C = {[1, 2, 1, 1, . . . ], [1, 2, 3, 1, 1, . . . ], [1, 2, 3, 4, 1, 1, . . . ], . . . } is an in�nite chain. 2) The relation ≤sort is not a cpo. A relation ≤sort is a cpo i� L has a least element w.r.t. ≤sort and every ≤sort-chain has a least upper bound in L. Obviously, the least element is the empty list [ ]. Consider C, de�ned as above. Obviously every sorted, in�nite list is an upper bound. But as sorted, in�nite lists are incomparable w.r.t. ≤sort, there is no least upper bound. 3) The relation ≤sort is not con�uent. We have [ ] ≤sort [1, 2, 3, . . . ] and [ ] ≤sort [2, 4, 6, . . . ], but all in�nite, sorted lists are incomparable. Thus, there is no q such that [1, 2, 3, . . . ] ≤sort q and [2, 4, 6, . . . ] ≤sort q. b) i) ff :: ((Int, Int) -> Int) -> ((Int, Int) -> Int)
ff f (x, 0) = x

ff f (x, y) = y * f (x, y – 1)

ii)

(φnff(⊥))(x, y) =

{
y! · x if 0 ≤ y < n ∧ x 6= ⊥ ⊥ otherwise iii) (lfp φff)(x, y) = { y! · x if 0 < y ∧ x 6= ⊥ ⊥ otherwise c) C Ts ⊥ D (Tp ⊥) C ⊥ ⊥ C (Tp ⊥) ⊥ ⊥ E D TsC ⊥ EC ⊥ (D ⊥)C ⊥ (C ⊥ ⊥) D ⊥ Exercise 3 (Lambda Calculus): (9 + 10 + 6 = 25 points) a) Consider the following Haskell function: 5 Functional Programming SS16 Solution - Exam 19.09.2016 len :: List a -> Int

len Nil = 0

len (Cons x xs) = 1 + len xs

Here Cons and Nil are the list constructors as de�ned in the lecture.

Please give an equivalent function in simple Haskell. Here, you can of course use prede�ned functions
like isa_Nil, argof_Cons, and sel_n_k. Additionally, implement the function in the lambda calculus,
i.e., give a lambda term q such that, for all lists list and y ∈ Z, y is the length of list if and only
if len list 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 (+).

You do not have to use the transformation algorithms presented in the lecture. It is su�cient to just
give an equivalent simple program and an equivalent lambda term.

b) Let
t = λ g x y. if (x ∗ y == 0) y (g x (y + x))

and

δ = { if True→ λx y. x,
if False→ λx y. y,
fix→ λ f. f(fix f)}

Please reduce fix t 3 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 y. if (x ∗ y == 0) y (g x (y + x))

whenever possible.

c) Consider λx.x a b as a representation of pairs of values (a, b) in pure lambda calculus.

Give a de�nition for a pure lambda term apply which applies a given term f to both elements of a
pair, i.e., apply f (λx.x a b) →∗β λx.x (f a), (f b)) should hold. You may use the shorthand notations
True = λx y.x and False = λx y.y in your solution.

Explain your solution shortly!

Solution:

a) len = \xs -> if (isa_Nil xs) then 0 else
(if (isa_Cons xs) then (1 + sel_2_2 (argof_Cons xs) else bot)

fix (λ f xs. if (isaNil xs) 0 (if (isaCons xs) (1 + f (sel2,2 (argofCons xs))) (bot))

Alternatively:

len = \xs -> if (isa_Nil xs) then 0 else

(1 + sel_2_2 (argof_Cons xs))

Functional Programming SS16
Solution – Exam 19.09.2016

fix (λ f xs. if (isaNil xs) 0 (1 + f (sel2,2 (argofCons xs))))

fix t 3 0

→δ (λ f. (f (fix f))) t 3 0

→β t (fix t) 3 0

→β (λx y. if (x ∗ y == 0) y ((fix t) x (y + x))) 3 0

→β (λ y. if (3 ∗ y == 0) y ((fix t) 3 (y + 3))) 0

→β if (3 ∗ 0 == 0) 0 ((fix t) 3 (0 + 3))

→δ if (0 == 0) 0 ((fix t) 3 (0 + 3))

→δ if True 0 ((fix t) 3 (0 + 3))

→δ (λx y. x) 0 ((fix t) 3 (0 + 3))

→β (λ y. 0) ((fix t) 3 (0 + 3))

→β 0

apply = λ f p. λ x. x (f (p True)) (f (p False))

Using True and False we can select the �rst and second element of the pair respectively. Inside the
template for a new pair the function f is applied to each element of the pair individually.

Exercise 4 (Type Inference): (20 points)

Using the initial type assumption A0 := {f :: ∀a.(a→ List a)}, infer the type of the expression f (λx.f x)
using the algorithm W.
Indicate the computed most general type or explain the problem the algorithm encounters if the expression is
not well typed.

Solution:

W(A0, f (λx.f x))
W(A0, f) = (id, b1 → List b1)
W(A0, λx.f x)

W(A0 + {x :: b2}, f x)
W(A0 + {x :: b2}, f) = (id, b3 → List b3)
W(A0 + {x :: b2}, x) = (id, b2)

mgu(b3 → List b3, b2 → b4) = [b2/b3, b4/List b3]
= ([b2/b3, b4/List b3], List b3)

= ([b2/b3, b4/List b3], b3 → List b3)

Functional Programming SS16
Solution – Exam 19.09.2016

mgu(b1 → List b1, (b3 → List b3)→ b5) = [b1/(b3 → List b3), b5/List (b3 → List b3)]
([b2/b3, b4/List b3, b1/(b3 → List b3), b5/List (b3 → List b3)], List(b3 → List b3))

Functional Programming SuSe19
Solution – Exam 12.08.2019

aaProf. Dr. J. Giesl M. Hark

Exercise 1 (Programming in Haskell): (6 + 9 + 9 + 14 = 38 points)
We use the following data structure Graph a to represent undirected graphs in Haskell by a list of edges, where
the nodes are labeled by values of type a.

data Graph a = Edges [(a,a)]

So the edges are represented as pairs of type (a,a). For example, the graph from Fig. 1 can be represented
by:

gExmp :: Graph Int
gExmp = Edges [(1,2),(1,4),(1,5),(2,3),(2,4),(3,4),(4,5),(4,6)]

Figure 1: Graph of type Graph Int

In each of the following exercises you can use functions from the Haskell Prelude and from previous exercises
even if you did not implement them. Moreover, you can always implement auxiliary functions.

a) Write a Haskell–function neighbors and also give its type declaration. Its first argument is a graph
g::Graph a for a type a from the type class Eq, and its second argument is an element v::a. The call
neighbors g v then results in the list of nodes directly connected by an edge to v in g. For example,
neighbors gExmp 2 == [1,3,4]. The order of the resulting list is irrelevant and it does not matter if
the list contains duplicates.

b) Consider the following function which computes a list of all values stored in a graph.

nodes :: Eq a => Graph a -> [a]
nodes (Edges es) = removeDuplicates (concat (map (\(x,y)->[x,y]) es))

where
removeDuplicates = foldr (\x ys -> x:(filter (x /=) ys)) []

Hence, nodes gExmp results in [1,2,4,5,3,6].
Write a Haskell–function existsPath and also give its type declaration. Its first argument is a graph
g::Graph a for a type a from the type class Eq, and its second and third argument are nodes v::a and
w::a. The call existsPath g v w results in True if and only if there is a path connecting v and w in g.
There is a path from v to w of at most length n if and only if v == w or there is a neighbor u of v and a
path of at most length n-1 from u to w. For example, existsPath gExmp 6 3 == True.
Note that a path from v to w exists if and only if there exists a path from v to w of at most length
(nodes g).

Hints:
• You may use the function nodes.
• The function elem::Eq a => a -> [a] -> Bool checks membership in a list, i.e., elem x xs ==
True if and only if x occurs in xs.

Functional Programming SuSe19
Solution – Exam 12.08.2019

c) Write a Haskell–function isConnected and also give its type declaration. Its only argument is g::Graph
a for a type a from the type class Eq. It returns True if and only if for every two elements v and w of
nodes g, we have existsPath g v w == True. For example, isConnected gExmp == True.

Hints:
• You may again use the function nodes from part b) of the exercise.
• List comprehensions are particularly suitable to compute all pairs (v,w) of (distinct) elements of
nodes g.

• The function and::[Bool] -> Bool conjuncts all elements in the input, e.g., and [True, True,
True] == True but and [True, False, True] == False.

d) Implement a function railNetwork::Graph String -> IO (). This function simulates a network of
railway connections as a Graph String between cities. The user can either add a connection to the
network or check if there exists a connection between two cities.

Furthermore, the following data declaration is given.

data NetworkInput = Track (String, String) | Connection (String, String) | Exit

When railNetwork g is called, it asks the user for an input. If the input is

• “Track:Start;End” then an edge from Start to End is added to g and the function railNetwork
calls itself on the transformed graph again.

• “Connection:Start;End” then the user is informed whether there is a path from Start to End in
g. The function railNetwork then calls itself again with the same argument.

• something else, then the program terminates.

In this exercise, you can assume that there is a function parseNetworkInput::String -> NetworkInput
that translates a String into a NetworkInput, i.e., parseNetworkInput “Track:Start;End” == Track
(“Start”, “End”), parseNetworkInput “Connection:Start;End” == Connection (“Start”, “End”),
and parseNetworkInput s == Exit for all other strings s.

An example run should look as follows. Here, inputs of the user are written in italics.

*Main> railNetwork (Edges [])
Enter track or check connection

Track:Berlin;Wolfsburg

Track added
Enter track or check connection

Track:Wolfsburg;Cologne

Track added
Enter track or check connection

Connection:Cologne;Berlin

There is a connection from Cologne to Berlin
Enter track or check connection

Connection:Cologne;Munich

This connection does not exist
Enter track or check connection

Stop

Functional Programming SuSe19
Solution – Exam 12.08.2019

*Main>

Hints:
• The function putStrLn::String -> IO() prints a string and performs a line break.
• The function getLine::IO String reads a string from the keyboard.

Solution:

import Data.Char

data NetworkInput = Track (String , String) | Connection (String , String) | Exit

trim :: String -> String
trim = f . f

where f = reverse . dropWhile isSpace

parseNetworkInput :: String -> NetworkInput
parseNetworkInput input | lhs == “Track” = Track ((trim (drop 1 start)),

(trim (drop 1 end)))
| lhs == “Connection” = Connection ((trim (drop 1 start)),

(trim (drop 1 end)))
| otherwise = Exit

where
(lhs , rhs) = span (/= ’:’) (trim input)
(start , end) = span (/= ’;’) (trim rhs)

data Graph a = Edges [(a,a)]

nodes:: Eq a => Graph a -> [a]
nodes (Edges es) = removeDuplicates (concat (map (\(x,y)->[x,y]) es))

where
removeDuplicates = foldr (\x ys -> x:( filter (x /=) ys)) []

a) neighbors :: Eq a => Graph a -> a -> [a]
neighbors (Edges es) v = [n | (n, m) <- es, m == v] ++ [m | (n, m) <- es , n == v] b) existsPath :: Eq a => Graph a -> a -> a -> Bool
existsPath (Edges es) x y = existsPathHelp (length (nodes (Edges es))) (Edges es) x y

where
existsPathHelp 0 _ x y = (x == y)
existsPathHelp n (Edges es) x y = let neigh = neighbors (Edges es) y in

(elem x neigh) || (( filter (existsPathHelp (n-1) (Edges es) x) neigh) /= [])

c) isConnected :: Eq a => Graph a -> Bool
isConnected g = let vertices = nodes g in

and [( existsPath g v w)| v <- vertices , w <- vertices , v /= w] d) railNetwork :: Graph String -> IO ()
railNetwork (Edges tracks) = do

putStrLn “Enter track or check connection”
input <- getLine case (parseNetworkInput input) of Track (start , end) -> do
putStrLn “Track added”
railNetwork (Edges ((start ,end): tracks ))

Connection (start , end) -> do
if (existsPath (Edges tracks) start end) then

Functional Programming SuSe19
Solution – Exam 12.08.2019

putStrLn (“There is a connection from ” ++ start ++ ” to ” ++ end)
else putStrLn “This connection does not exist”

railNetwork (Edges tracks)
Exit -> return ()

Exercise 2 (Semantics): ((9 + 11) + (5 + 7 + 4) + 7 = 43 points)
a) i) Let D be a domain and v a complete partial order on D. Let f : D → D be a continuous function w.r.t. v

and Fix(f) ⊆ D its set of fixpoints. Let v|Fix(f) be the restriction of v to Fix(f), i.e., for every x, y ∈ Fix(f)
let x v|Fix(f) y hold iff x v y. Prove that v|Fix(f) is complete on Fix(f).

ii) Let D be a domain, v a complete partial order on D, and f : D → D a continuous function w.r.t. v. By i),
f has a least fixpoint lfp f . Prove the following claim.

If d ∈ D with f(d) v d then lfp f v d.

Hints:
• Use the characterization of the least fixpoint from the Fixpoint Theorem and perform an induction

proof.

b) i) Consider the following Haskell function f:
f :: (Int, Int, Int) -> Int
f (x, y, 0) = 1
f (x, y, n) = x * f(x, y, n-1) + y * f(x, y, n-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 fixpoint 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 definition of φmff(⊥) in closed form for any m ∈ N,
i.e., give a non-recursive definition of the function that results from applying φff m-times to ⊥. Here, you
should assume that Int can represent all integers, so no overflow can occur.

iii) Give the definition of the least fixpoint of φff in closed form.

c) Consider the data type declarations on the left and, as an example, the graphical representation of the first four
levels of the domain for Nats on the right:

data Nats = Z | S Nats

———————–

data EncapsuledList a
= L [a]

S (S (S ⊥))S (S Z)

⊥

4th level

Z 2nd level

3rd level

1st level

S Z S (S ⊥)

S ⊥

Give a graphical representation of the first four levels of the domain for the type EncapsuledList Bool.

Functional Programming SuSe19
Solution – Exam 12.08.2019

Solution:

a) i) • By the Fixpoint Theorem, lfp f exists, i.e., Fix(f) has a smallest element w.r.t. v|Fix(f).
• Let S ⊆ Fix(f) be a chain. Then f(S) = {f(s) | s ∈ S} = {s | s ∈ S} = S as S only consists of fixpoints.

As v is complete on D, lub S ∈ D exists. As f is continuous we have f(lub S) = lub f(S) = lub S,
i.e., lub S ∈ Fix(f). So, every chain has a least upper bound. This completes the proof.

ii) By the Fixpoint Theorem we have lfp f = lub {fn(⊥) | n ∈ N}. We will show by induction that fn(⊥) v d
for any n ∈ N. Then, d is an upper bound on the set {fn(⊥) | n ∈ N}, hence, lfp f = lub {fn(⊥) | n ∈ N} v d
as it is the least upper bound.
I.B. We have ⊥ v d by definition.
I.H. Assume fn(⊥) v d for some fixed n ∈ N.
I.S. We have

f
n+1

(⊥) =f(fn(⊥))
vf(d) v d. (By continuity ⇒ monotonicity, I.H and assumption.)

b) i) ff :: ((Int, Int, Int) -> Int) -> ((Int, Int, Int) -> Int)
ff g (x, y, 0) = 1
ff g (x, y, n) = x * g(x, y, n-1) + y * g(x, y, n-1)

ii) φ0ff(⊥) = ⊥

φ1ff(⊥)(x, y, n) =

{
1, n = 0

⊥, otherwise

φ2ff(⊥)(x, y, n) =



1, n = 0

(x+ y)n, 0 < n < 2 ∧ x, y 6= ⊥ ⊥, otherwise φmff(⊥)(x, y, n) =   1, n = 0 ∧m > 0
(x+ y)n, 0 < n < m ∧ x, y 6= ⊥ ⊥, otherwise iii) lfp φff(x, y, n) =   1, n = 0 (x+ y)n, 0 < n ∧ x, y 6= ⊥ ⊥, otherwise L (⊥ : ⊥) L ⊥ ⊥ L [] L (True : ⊥)L (⊥ : (⊥ : ⊥)) L (False : ⊥) L (⊥ : []) 5 Functional Programming SuSe19 Solution - Exam 12.08.2019 Exercise 3 (Lambda Calculus): ((5 + 5) + 8 + 6 = 24 points) a) Consider the following function computing the difference of two natural numbers (if the first argument is not smaller than the second). Here, natural numbers are represented by the data structure Nats defined by data Nats = Z | S Nats. minus :: Nats -> Nats -> Nats
minus x Z = x
minus (S x) (S y) = minus x y

i) Please give an equivalent function in simple Haskell.
ii) Implement the function minus in the lambda calculus, i.e., give a lambda term q such that, for all natural

numbers m,n the term q (Sm Z) (Sn Z) can be reduced to{
Sm−n Z, if m ≥ n
bot, otherwise

via WHNO-reduction with the →βδ-relation and the set of rules δ as introduced in the lecture to implement
Haskell.

Hints:
• You can use infix notation for predefined functions like (&&) in both simple Haskell and the lambda calculus.
• You do not have to use the transformation algorithms presented in the lecture. It is sufficient to just give

an equivalent simple program and an equivalent lambda term.

b) Let
t = λ g n. if (n <= 0) 1 (g n) and δ = { if True→ λx y. x, if False→ λx y. y, fix→ λ f. f(fix f)} ∪ { x <= y → True | x ≤ y ∈ Z} ∪ { x <= y → False | x > y ∈ Z}

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 n. if (n <= 0) 1 (g n) whenever possible. c) Consider the representation of natural numbers in the pure lambda calculus presented in the lecture (i.e., n ∈ N is represented by the term n = λ f x. fn x) and the representation of Booleans (i.e., True = λ x y.x and False = λ x y.y). Give a pure lambda term for the function isZero, such that isZero(λ f x. fn x) can be reduced to False if n > 0 and to True if n = 0.
Explain your solution shortly. You may give a reduction sequence as explanation.
Hints:
• A function λ x.t where x does not occur as a free variable in the term t is a constant function. Then

applying λ x.t to a term multiple times still evaluates to t.

Solution:

a) i) minus = \x -> \y ->
if (isa_Z y) then x

else if (isa_S x) && (isa_S y) then minus (argof_S x) (argof_S y)
else bot

ii)
fix (λ g x y.if (isa_Z y) x (if ((isa_S x) && (isa_S y)) (g (argof_S x) (argof_S y))) bot)

Functional Programming SuSe19
Solution – Exam 12.08.2019

fix t 0

→δ (λ f. (f (fix f))) t 0

→β t (fix t) 0

→β (λ n. if (n <= 0) 1 ((fix t) n)) 0 →β if (0 <= 0) 1 ((fix t) 0) →δ if True 1 ((fix t) 0) →δ (λ x y.x) 1 ((fix t) 0) →β (λ y.1) ((fix t) 0) →β 1 c) isZero = λn.n (λz.False) True The representation of n applies the function f n times to some x. If n = 0 then the first argument is simply ignored, i.e., it can be reduced to True. If n > 0 then the constant function λz.False is applied n–times to True
which results in False.

isZero 0

→β 0 (λz.False) True

→∗β True

isZero n

→β n (λz.False) True

= (λf x.f
n
x) (λz.False) True

→∗β (λz.False)
n True

→∗β False (Hint)

Exercise 4 (Type Inference): (15 points)
Using the initial type assumption A0 := {f :: ∀a.a→ Int, g :: ∀a.a→ a→ a}, infer the type of the expression λy.g (f y)
using the algorithm W.
Hints:
• When writing W(A, t) = (θ, t), you do not have to give the full substitution θ, but it is enough to give the parts

of θ that concern the free variables in the type schemas of A.

Functional Programming SuSe19
Solution – Exam 12.08.2019

Solution:

W(A0, λy.g (f y))
W(A0 + {y :: b1}, g (f y))

W(A0 + {y :: b1}, g)
= (id, b2 → b2 → b2)
W(A0 + {y :: b1}, f y)

W(A0 + {y :: b1}, f)
= (id, b3 → Int)
W(A0 + {y :: b1}, y)
= (id, b1)
mgu (b3 → Int, b1 → b4)
= [b3/b1, b4/Int]

= (id, Int)
mgu (b2 → b2 → b2, Int→ b5)
= [b2/Int, b5/Int→ Int]

(id, Int→ Int)
(id, b1 → (Int→ Int))

Under the type assumption A0 the most general type of λy.g (f y) is b→ (Int→ Int).

Functional Programming SuSe19
Solution – Exam 10.09.2019

aaProf. Dr. J. Giesl M. Hark

Exercise 1 (Programming in Haskell): (5 + 12 + 9 + 14 = 40 points)
We use the following data structure Tree a to represent binary trees in Haskell.

data Tree a = E | N a (Tree a) (Tree a)

For example, the tree from Fig. 1 can be represented by:

exTree :: Tree Int
exTree = N 16 (N 37 (N 19 E E) (N 21 E E)) (N 25 (N 2 E E) (N 12 E E))

19 21

2 12

Figure 1: Tree of type Tree Int

a) Declare Tree a as an instance of the type class Ord whenever a is an instance of Ord. In this instance
declaration, you should provide an implementation of the function <= to compare two trees. For two non-empty trees t1 and t2, we have t1 <= t2 if and only if the value of t1’s root node is smaller or equal to the value of t2’s root node. For example, (exTree <= N 19 E E) == True but (N 19 E E <= exTree) == False, as (19 <= 16) == False. Furthermore, (t <= E) == True for any t::Tree a but (E <= t) == True if and only if t == E. Hints: • You can assume that Tree a is an instance of Eq whenever a is an instance of Eq. b) A heap is a binary tree in which a value stored at a node is greater or equal to all values stored in its children. For example, the tree in Fig. 1 is not a heap, as (16 >= 37) == False. However, the subtree
of the tree in Fig. 1 with root 25 is a heap, as (25 >= 2) == True and (25 >= 12) == True. Note that
the root node of a heap contains the maximal value stored in the heap. The empty tree E is also a heap.

Write a Haskell–function heapify and also give its type declaration. Its only argument is an element
t::Tree a for a type a of the type class Ord. The call heapify t for some t::Tree a results in a tree
h::Tree a which stores exactly the same values as t but is also a heap. If a value is stored n times in
t, then it is also stored n times in heapify t.

For a tree N v l r, your implementation should check if v is greater or equal to the values stored in l
and r, respectively. If yes, the result is N v lh rh, where lh is l transformed into a heap and rh is r
transformed into a heap. If no, then swap v and the maximal value of the tree. Afterwards, call heapify
on the subtree where v was swapped to in order to ensure that the result is a heap.

For example, heapify exTree results in the tree in Fig. 2.

c) For the following exercise, assume that there is a function deleteRoot::Ord a => Tree a -> Tree a.
For a given heap h with h /= E, the call deleteRoot h results in a heap storing exactly the same values
as h without its root node. Again, if a value is stored n times in h without its root node, then the value
is also stored n times in deleteRoot h. Furthermore, assume that there is a function insert::a ->
Tree a -> Tree a that inserts a value into a tree.

Functional Programming SuSe19
Solution – Exam 10.09.2019

19 16

2 12

Figure 2: Heapified version of Fig. 1

Write a Haskell–function heapsort and also give its type declaration. Its only argument is a list xs::[a]
for a type a of the type class Ord. The function heapsort sorts xs in decreasing order by first transforming
it into a heap. Then, it extracts the maximal value of the heap by using deleteRoot and adds this value
to the resulting list. This is repeated until the heap is empty.

Hints:
• You can use the functions heapify, insert, and foldr to transform a list into a heap.

d) Implement a function participants::[(String, String)] -> IO (). This function simulates an in-
teractive system for managing participants encoded as pairs (surname, first_name).

When participants xs is called, it asks the user for an input. If the input is

• “get”, then the user can enter a value k::Int and gets the kth name when sorting the participants
w.r.t. surnames in decreasing order. Participants with the same surnames are sorted by their first
names. The first participant has the index 0. If there are less than k+1 participants, an error
message is prompted. Then participants calls itself again with the same argument.

• “add”, then the user enters first the surname and then the first name of the participant to be added.
Then participants prompts a success message and calls itself again with the list resulting from
xs when adding the entered participant.

• In any other case the program terminates.

An example run should look as follows. Here, inputs of the user are written in italics.

*Main> participants []
Add participant or get kth?

add

Giesl

Juergen

Added participant
Add participant or get kth?

add

Mueller

Julia

Added participant
Add participant or get kth?

get

Not enough participants
Add participant or get kth?

Functional Programming SuSe19
Solution – Exam 10.09.2019

get

Giesl, Juergen
Add participant or get kth?

Stop

*Main>

Hints:
• The function putStrLn::String -> IO() prints a string and performs a line break.
• The function getLine::IO String reads a string from the keyboard.
• You can assume that there is a function getInt::IO Int that reads an integer from the keyboard.
• You can use the indexing operator (!!)::[a] -> Int -> a. Here, xs!!k gives the kth element of

the list xs whenever k is between 0 and (length xs)-1.

• You can use the function heapsort to sort the list of participants in decreasing order. The reason
is that for two pairs (s1,s2),(t1,t2)::(String,String) we have (s1,s2) <= (t1,t2) iff s1 <= t1 or s1 == t1 and s2 <= t2. Strings are compared as usual by <=. Solution: data Tree a = E | N a (Tree a) (Tree a) deriving Show instance Eq a => Eq (Tree a) where
(==) E E = True
(==) (N v1 l1 r1) (N v2 l2 r2) = v1 == v2
(==) _ _ = False

–Help
insert :: Ord a => a -> Tree a -> Tree a
insert x E = N x E E
insert x (N v l r) | x < v = N v (insert x l) r | otherwise = N v l (insert x r) deleteLeaf :: Tree a -> (a, Tree a)
deleteLeaf (N v E E) = (v, E)
deleteLeaf (N v (N v1 l1 r1) r) = let (v3, l3) = deleteLeaf (N v1 l1 r1) in (v3, (N v l3 r))
deleteLeaf (N v E (N v2 l2 r2)) = let (v4, r4) = deleteLeaf (N v2 l2 r2) in (v4, (N v E r4))

deleteRoot :: Ord a => Tree a -> Tree a
deleteRoot (N v E E) = E
deleteRoot (N v l r) = let (x, N w l1 r1) = deleteLeaf (N v l r) in (heapify (N x l1 r1))

getInt :: IO Int
getInt = do

x <- getLine return (read x :: Int) a) instance Ord a => Ord (Tree a) where
(<=) _ E = True (<=) (N v1 l1 r1) (N v2 l2 r2) = v1 <= v2 (<=) _ _ = False 3 Functional Programming SuSe19 Solution - Exam 10.09.2019 b) heapify :: Ord a => Tree a -> Tree a
heapify E = E
heapify (N v E E) = N v E E
heapify (N v l E) = let (N v1 l1 r1) = lh in

if (v >= v1) then (N v lh E) else N v1 (heapify (N v l1 r1)) E
where lh = (heapify l)

heapify (N v E r) = let (N v2 l2 r2) = rh in
if (v >= v2) then (N v E rh) else N v2 E (heapify (N v l2 r2))

where rh = (heapify r)
heapify (N v l r) | ((N v l r) >= lh) && ((N v l r) >= rh) = N v lh rh

| lh >= rh = let (N v1 l1 r1) = lh in N v1 (heapify (N v l1 r1)) rh
| lh < rh = let (N v2 l2 r2) = rh in N v2 lh (heapify (N v l2 r2)) where (lh , rh) = (( heapify l), (heapify r)) c) heapsort :: Ord a => [a] -> [a]
heapsort xs = toList (heapify (foldr insert E xs)) where

toList E = []
toList (N v l r) = v:toList(deleteRoot (N v l r))

d) participants :: [(String , String )] -> IO ()
participants xs = do

putStrLn “Add participant or get kth?”
x <- getLine if (x == "get") then do k <- getInt if (k < 0 || k >= (length xs))

then do
putStrLn “Not enough participants”
participants xs

else
let (sur , first) = (heapsort xs) !! k in do

putStrLn (sur ++ “, ” ++ first)
participants xs

else if (x == “add”) then
do

sur <- getLine first <- getLine putStrLn "Added participant" participants ((sur , first) : xs) else return () Exercise 2 (Semantics): ((10 + 7) + (5 + 7 + 4) + 7 = 40 points) a) i) Prove the following generalization of the Fixpoint Theorem. Let D be a domain, v a complete partial order on D, f : D → D a continuous function w.r.t. v, and d ∈ D. If d v f(d) then p∗ = t{fn(d) | n ∈ N} satisfies the following: • The element p∗ is a fixpoint of f . • For every fixpoint p of f with d v p we have p∗ v p. Hints: • You do not have to show that t{fn(d) | n ∈ N} exists, i.e., that {fn(d) | n ∈ N} is indeed a chain. ii) Let D be a domain, v a complete partial order on D, and f : D → D a continuous function w.r.t. v. By the Fixpoint Theorem, f has a least fixpoint lfp f . Disprove the following claim by giving a counterexample: If d ∈ D with d v f(d) then d v lfp f. Hints: 4 Functional Programming SuSe19 Solution - Exam 10.09.2019 • You also have to show that your counterexample meets the requirements, i.e., that the chosen order is complete, that your function f is continuous, and that your chosen d ∈ D satisfies d v f(d). • You may use that any flat domain with the order x v y iff x = y ∨ x = ⊥ is complete. • On flat domains, continuity and monotonicity are equivalent. b) i) Consider the following Haskell function f: f :: (Int, Int) -> Int
f (n, 0) = 1
f (0, k) = 0
f (n, k) = f(n-1, k) + f(n-1, k-1)

(
n
k

)
for n ∈ N, k ∈ Z is defined as follows:(

)
=

{
n!

k!·(n−k)! , 0 ≤ k ≤ n
0, k < 0 or k > n

• For n ∈ N, k ∈ Z we have
(
n+1
k

)
=
(
n
k

)
+
(
n
k−1

)
.

iii) Give the definition of the least fixpoint of φff in closed form.
c) Consider the data type declarations on the left and, as an example, the graphical representation of the first three

levels of the domain for Nats on the right:

data Nats = Z | S Nats

———————–

data Tree a = E | N a (Tree a) (Tree a)

data Unit = U ()

⊥

Z 2nd level

3rd level

1st level

S Z S (S ⊥)

S ⊥

Give a graphical representation of the first three levels of the domain for the type Tree Unit.

Solution:

a) i) 1. p∗ is a fixpoint of f :
We have

f(p
∗
)

=f(t{fn(d) | n ∈ N})
=t{f(fn(d)) | n ∈ N} (Continuity)

=t{fn+1(d) | n ∈ N}

=t
(
{fn+1(d) | n ∈ N} ∪ {d}

)
(d v f(d))

=t{fn(d) | n ∈ N}
=p
∗
.

Functional Programming SuSe19
Solution – Exam 10.09.2019

So, t{fn(d) | n ∈ N} is a fixpoint of f .
2. p∗ v p for all fixpoints p with p v d:

Take any fixpoint p, such that d v p. We will show that for every n ∈ N we have fn(d) v p by using
induction on n.

(I.B.) f0(d) = d v p by assumption.
(I.H.) Assume that for a fixed n ∈ N we have fn(d) v p.
(I.S.)

f
n+1

(d) =f(f
n
(d))

vf(p) (I.H. and continuity ⇒ monotonicity)
=p. (as p is a fixpoint of f)

But this means that p is an upper bound of {fn(d) | n ∈ N}, so we must have p∗ = t{fn(d) | n ∈ N} v p
as p∗ is the least upper bound. This concludes the proof.

ii) Take Z⊥ with the order x v y iff x = y∨x = ⊥. By the hint, this is a complete order. The identity function
idZ⊥ : Z⊥ → Z⊥, x 7→ x is continuous as it is monotonic and Z⊥ is flat:

x v y ⇒ idZ⊥(x) = x v y = idZ⊥(y).

Alternatively, for any chain S ⊆ Z⊥ we have idZ⊥(S) = S, i.e., idZ⊥(tS) = tS = t idZ⊥(S).
Furthermore, 2 v 2 = idZ⊥(2). However, idZ⊥(⊥) = ⊥. So, the least fixpoint is ⊥ but 2 6v ⊥.

b) i) ff :: ((Int, Int) -> Int) -> ((Int, Int) -> Int)
ff g (n, 0) = 1
ff g (0, k) = 0
ff g (n, k) = g(n-1, k) + g(n-1, k-1)

ii) φ0ff(⊥) = ⊥

φ1ff(⊥)(n, k) =



1, k = 0

0, n = 0 ∧ k 6∈ {0,⊥}
⊥, otherwise



1, k = 0 ∧ n 6∈ N(
n
k

)
, 0 ≤ n < 1 ∧ k 6= ⊥ ⊥, otherwise φ2ff(⊥)(n, k) =   1, k = 0 0, n = 0 ∧ k 6∈ {0,⊥} 1, n = k = 1 0, n = 1 ∧ k 6∈ {0, 1,⊥} ⊥, otherwise =   1, k = 0 ∧ n 6∈ N( n k ) , 0 ≤ n < 2 ∧ k 6= ⊥ ⊥, otherwise φmff(⊥)(n, k) =   1, k = 0 ∧ n 6∈ N ∧m > 0(
n
k

)
, 0 ≤ n < m ∧ k 6= ⊥ ⊥, otherwise iii) lfp φff(n, k) =   1, k = 0 ∧ n 6∈ N( n k ) , 0 ≤ n ∧ k 6= ⊥ ⊥, otherwise c) E N ⊥ ⊥ ⊥ N ⊥ (N ⊥ ⊥ ⊥) ⊥ ⊥ N ⊥ ⊥ EN (U ⊥) ⊥ ⊥ N ⊥ E ⊥ N ⊥ ⊥ (N ⊥ ⊥ ⊥) 6 Functional Programming SuSe19 Solution - Exam 10.09.2019 Exercise 3 (Lambda Calculus): ((4 + 4) + 8 + 6 = 22 points) a) Consider the following function that determines whether the first list is shorter or as long as than the second. Here, lists are represented by the data structure List a defined by data List a = N | C a (List a). cp :: List a -> List a -> Bool
cp N ys = True
cp (C x xs) N = False
cp (C x xs) (C y ys) = cp xs ys

i) Please give an equivalent function in simple Haskell.
ii) Implement the function cp in the lambda calculus, i.e., give a lambda term q such that, for all lists l1, l2 the

term q l1 l2 can be reduced to True if and only if l1 is at most as long as l2, and to False otherwise.

Hints:
• You do not have to use the transformation algorithms presented in the lecture. It is sufficient to just give

an equivalent simple program and an equivalent lambda term.
• You can use infix notation for predefined functions like (&&) in both simple Haskell and the lambda calculus.

b) Let
t = λ g n. if (n == 0) (λz.True) (λz.g 0)

and

δ = { if True→ λx y. x,
if False→ λx y. y,
fix→ λ f. f(fix f)}

∪ { x == y → True | x, y ∈ Z, x = y}
∪ { x == y → False | x, y ∈ Z, x 6= y}

Please reduce fix t 1 by WHNO-reduction with the→βδ-relation. List all intermediate steps until reaching weak
head normal form, but please write “t” instead of

λ g n. if (n == 0) (λz.True) (λz.g 0)

whenever possible.

c) Consider the representation of natural numbers in the pure lambda calculus presented in the lecture (i.e., n ∈ N
is represented by the term n = λ f x. fn x). Give a pure lambda term for the function minus, such that for

m,n ∈ N the expression minus m n can be reduced to

{
m− n, if n ≤ m
0, otherwise.

Explain your solution shortly. You may give a reduction sequence as explanation.
Hints:

• You can assume that there is a pure lambda term pred such that pred n can be reduced to

{
n− 1, if n > 0
0, if n = 0.

Solution:

a) i) cp = \xs -> \ys ->
if (isa_N xs) then True

else if (isa_C xs) && (isa_N ys) then False
else if (isa_C xs) && (isa_C ys)

then cp (sel_2,2 (argof_C xs)) (sel_2,2 (argof_C ys))
else bot

ii)

fix (λ g xs ys.if (isa_N xs) True (if (isa_C xs && isa_N ys) False

(if (isa_C xs && isa_C ys) (g (sel_2,2 (argof_C xs)) (sel_2,2 (argof_C xs))) bot)))

Functional Programming SuSe19
Solution – Exam 10.09.2019

fix t 1

→δ (λ f. (f (fix f))) t 1

→β t (fix t) 1

→β (λ n. if (n == 0) (λz.True) (λz.fix t 0)) 1

→β if (1 == 0) (λz.True) (λz.fix t 0)

→δ if False (λz.True) (λz.fix t 0)

→δ (λ x y.y) (λz.True) (λz.fix t 0)

→β (λ y.y) (λz.fix t 0)

→β λz.fix t 0

minus = λ m n.n pred m

The representation of n applies a function g n–times to some x. If g = pred then this results in subtracting 1
exactly n times from m and in 0 if m 6≥ n.

minus m n

→β (λ n.n pred m) n

→β n pred m

→β (λx.predn x) m

→β predn m

→∗β

{
m− n, if n ≤ m
0, otherwise

Exercise 4 (Type Inference): (18 points)
Using the initial type assumptionA0 := {f :: ∀a.a→ a, g :: ∀a.Bool→ a→ a}, infer the type of the expression λx.g (f x) x
using the algorithm W.
Hints:
• When writing W(A, t) = (θ, t), you do not have to give the full substitution θ, but it is enough to give the parts

of θ that concern the free variables in the type schemas of A.

Solution:

W(A0, λx.g (f x) x)
W(A0 + {x :: b1}, g (f x) x)

Functional Programming SuSe19
Solution – Exam 10.09.2019

W(A0 + {x :: b1}, g (f x))
W(A0 + {x :: b1}, g)
= (id, Bool→ b2 → b2)
W(A0 + {x :: b1}, f x)

W(A0 + {x :: b1}, f)
= (id, b3 → b3)
W(A0 + {x :: b1}, x)
= (id, b1)
mgu (b3 → b3, b1 → b4) = [b3/b1, b4/b1]

= (id, b1)
mgu (Bool→ b2 → b2, b1 → b5) = [b1/Bool, b5/(b2 → b2)]

= ([b1/Bool], b2 → b2)
W(A0 + {x :: Bool}, x)
= (id, Bool)
mgu (b2 → b2, Bool→ b6) = [b2/Bool, b6/Bool]

= ([b1/Bool], Bool)
= (id, Bool→ Bool)

Under the type assumption A0 the most general type of λx.g (f x) x is Bool→ Bool.

Related Posts