- (25 points)
Encode in the lambda calculus the function "integer division",
defined as follows:
div(n,k) = p if n = k*p + r where r is non negative and r < k
Examples: div(7,3) = 2, div(9,3) = 3.
Hint: you can use either minimalization or recursion.
- (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 7.
- (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.