Distributed: Published on the web on Sep 22.

Due: Oct 5 (in class).

Total maximum score: 100 points.

The purpose of this assignment is to provide experience with coding in lambda calculus, and with the notion of reduction in lambda calculus.

- (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 ->> ?

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 M
_{0}gives rise to an infinite chain of reductionsM

Is it the case that the "size" of the terms is monotonically increasing, i.e. that for every n, the size of M_{0}-> M_{1}-> M_{2}-> ... -> M_{n}-> ..._{n+1}is bigger than, or equal to, the size of M_{n}? 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.