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)]
1
2
3
4
5
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.
1
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
2
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
3
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.
4
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)
6
Functional Programming SuSe19
Solution – Exam 12.08.2019
b)
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.
7
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).
8