- (10 points) Define in ML the function "composition"
which takes two arguments (one after the other, i.e. "composition"
should be in curried style)
and gives as result their functional composition, in the same
order of application (i.e. on a generic input, the first argument is applied first, then
the second is applied to the result).
Example: if "plus2" is the function that adds 2 to its argument,
and "mult3" is the function that multiplies its argument by 3, then
(composition plus2 mult3) is the function that, on input n, gives as result
(n+2)*3,
and
(composition mult3 plus2) is the function that, on input n, gives as result
(n*3)+2.
- (10 points) Define in ML the function "twice"
which takes one argument and gives as result its functional composition
with itself.
Example: if "plus2" and "mult3" are the functions
defined as in Exercise 1, then
(twice plus2) is the function that, on input n, gives as result
n+4, and
(twice mult3) is the function that, on input n, gives as result
n*9.
- (5 points) Given the function twice defined as in Exercise 2,
and a generic function f,
is (twice twice f) equivalent to (twice (twice f)) ?
Justify your answer.
Note: by "equivalent" here we mean the same functional behaviour,
i.e. same output for every input.
- (20 points) For each of the following properties,
say whether it holds or not on lambda terms. Justify
your answers.
P, M, N, and Q represent generic lambda terms, and -> and ->> are the
relations defined in Lecture 6.
- (Confluence of ->) If P -> M and P -> N, then there exist Q such that
M -> Q and N -> Q.
- (Weak confluence of ->) If P -> M and P -> N, then there exist Q such that
M ->> Q and N ->> Q.
- (25 points) Consider an arbitrary binary relation -> on an arbitrary
set A, and let ->> be the reflexive and transitive closure of ->
as defined in Lecture 6. (For example, -> could be the relation
of beta-reduction on lambda terms,
or the standard ordering relation on natural numbers, or...)
- Does the confluence of -> imply the confluence of ->> ?
- Does the weak conluence of -> imply the confluence of ->> ?
Justify your answers.
Note: "Confluence of ->>" means of course that, if a ->> b and
a ->> c, then there exists d such that b ->> d and c ->> d.
The symbols a, b, c, and d here are arbitrary elements of the set
A where -> and ->> are defined.
- (20 points) For each of the following lambda terms, say whether
it is strongly normalizing, weakly normalizing, or not normalizing.
Justify your answers. In case a term is normalizing (weakly or strongly),
give its normal form.
- (5 points) [if_then_else]([is_zero] [0]) [1] Omega
- (5 points) [if_then_else]([is_zero] Omega) [0] [1]
- (10 points) Y F [3], where F is the lambda term which represents
the functional used in the fixpoint equation of the factorial function,
i.e.
F =def= \u.\x. [if_then_else] ([is_zero] x) [1]
([times] x (u ([predecessor] x)))
Note: Omega is the lambda term defined in Lecture 8.
- (10 points) Suppose that a lambda term M0
gives rise to an infinite
chain of reductions
M0 -> M1 -> M2 -> ... -> Mn -> ...
Is it the case that the "size" of the terms is monotonically increasing,
i.e. that for every n, the size of Mn+1 is bigger than, or
equal to, the size of Mn ?
Justify your answer.
Note: by "size" of a lambda term M, here we mean its structural
complexity, i.e. the height of a parse tree (or derivation tree)
for M in the grammar generating M. If you don't know the definition of
parse tree, please refer to the book
Ravi Sethi. Programming Languages
Concepts and Constructs. 2nd edition, Addison-Wesley, 1996.
or to any other book on programming languages.