06.11.2014
IA014   Advanced Functional Programming        Duration: 60 minutes
Name: Room: Coordinates:
Sf}l&&1/         l_L      "J    L"      I                           U(ZO         l_L      'J    L"      J_l    L1"      J_l    L"      'J    C J_l    L1"      '_l    L"      J_l          SCO'PG         C      J_l    l_L      '_l    L" JJ
Do not write anything here! Write down your personal identification number (uco) only. When doing so, follow the digit templates please. D IE3H5E1B3
fixed point combinators Question 1
In the lecture, you have seen a proof that Y := Xf.(Xx.f(x x)) (Xx.f(x x)) is a 10 points
fixed point combinator. Prove that
D := Xf.(Xxy.f {x x y)) (Xxy.f {x x y)) {dragon)
(where D stands for „Dragon") is also a fixed point combinator.
Do not write anything here! Write your solution on this side of a sheet only.
06.11.2014
IA014   Advanced Functional Programming        Duration: 60 minutes
Name: Room: Coordinates:
2
Sf}l&&1/ l_L      'J    ^H^A U(ZO l_L      'J    L"      J_l    L1"      J_l    L"      'J    C      J_l    L1"      '_l    L"      J_l SCO'PG C      J_l    l_L      '_l    L" JJ
Do not write anything here! Write down your personal identification number (uco) only. When doing so, follow the digit templates please. D IE3H5E1B3
Church numerals Question 2
In the lecture you have seen the following terms for multiplication and addition 10 points
(for Church numerals):
plus := Xm.Xn.Xf.Xx.m f {n f x) times := Xm.Xn.Xf.m {n f)
a) Show that times 3 4 evaluates to 12.
b) Give an alternative definition of the term times using plus.
Do not write anything here! Write your solution on this side of a sheet only.
06.11.2014
IA014   Advanced Functional Programming        Duration: 60 minutes
Name: Room: Coordinates:
3
Sf}l&&1/ l_L      'J    ^H^J U(ZO l_L      'J    L"      J_l    L1"      J_l    L"      'J    C      J_l    L1"      '_l    L"      J_l SCO'PG C      J_l    l_L      '_l    L" JJ
Do not write anything here! Write down your personal identification number (uco) only. When doing so, follow the digit templates please. D IE3H5E1B3
simply typed lambda calculus Question 3
Lists can be easily added to the simply typed lambda calculus A-*. Here is the 12 points
additional syntax (note that these lists are parameterized by the type of elements
T):
t ::=    ... terms |    nil[T] empty list
|    cons[T] t t list constructor
|    isnil[T] t test for emptiness
J   hd[T] t head of a list
J   tl[T] t tail of a list
v ::= ... values
| nil[T] empty list
| cons[T] v v list constructor
T ::= ... types
| List T type of lists
a) You task is to write down the typing rules for lists (one has been provided for your convenience): (5 rules, including the one provided)
r h ti : T      r h t2 : List T        „ , 1 1 (T-CONS)
T h cons[T] ti t2 : List T
Do not write anything here! Write your solution on this side of a sheet only.
06.11.2014
IA014   Advanced Functional Programming        Duration: 60 minutes
Name: Room: Coordinates:
H
sh&&1/    i_l   jj i_l   I U(%0    i_l   'j i_l   j_i l1"   j_i l1   'j c   j_i l1"   '_i i_l   j_i     SCO'PG    c   j_i i_l   '_i l1 jj
Do not write anything here! Write down your personal identification number (uco) only. When doing so, follow the digit templates please. D IE3H5E1B3
(continuation of the previous sheet)
b) Also write down the evaluation rules for lists, using the call-by-value semantics (again, the first one has been provided for you convenience): (9 rules, including the one provided)
tx ~* ^ (E-CONSl)
cons[T] ti t2 ->• cons[T] t[ t2
Do not write anything here! Write your solution on this side of a sheet only.
06.11.2014
IA014   Advanced Functional Programming        Duration: 60 minutes
Name: Room: Coordinates:
E
Sf}l&&1/ l_L      'J    ^H^J U(ZO l_L      'J    L"      J_l    L1"      J_l    L"      'J    C      J_l    L1"      '_l    L"      J_l SCO'PG C      J_l    l_L      '_l    L" JJ
Do not write anything here! Write down your personal identification number (uco) only. When doing so, follow the digit templates please. D IE3H5E1B3
System hm Question 4
In the System HM, prove that the term 10 points
let i = Xx.x in i i
is well typed (and give its type).
Do not write anything here! Write your solution on this side of a sheet only.