CS计算机代考程序代写 data structure Lambda Calculus chain Haskell algorithm Functional Programming SuSe19

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

16

37

19 21

25

2 12

Figure 1: Tree of type Tree 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) 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.

1

Functional Programming SuSe19
Solution – Exam 10.09.2019

37

21

19 16

25

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

2

Not enough participants
Add participant or get kth?

2

Functional Programming SuSe19
Solution – Exam 10.09.2019

get

1

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)

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.
Hints:
• The binomial coefficient

(
n
k

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

n

k

)
=

{
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

.

5

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

7

Functional Programming SuSe19
Solution – Exam 10.09.2019

b)

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

c)

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)

8

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.

9