Fall 98, CSE 520: Solution of Assignment 3

Exercise 1

Let M be a typeable term of measure k (where the measure of a term is defined as the greatest of the orders of its beta-redexes, if they exist, and 0 otherwise). If k = 0 then M is already in normal form. If k > 0, we show by structural induction that we can reduce M to a term with measure < k.

M = x: not possible, since the measure of x is 0.
M = \x.N: the measure of M is equal to the measure of N. By inductive hypothesis we can reduce N to P with measure < k, and therefore we can reduce M to \x.P with measure < k.
M = NP: by inductive hypothesis we can reduce N to Q and P to R, where both Q and R have measure < k. If Q is not an abstraction, then we are done since QR has measure < k. Otherwise, let Q = \x.S. Make a beta-reduction (\x.S)R ->_betaS[R/x]. To conclude the proof, we need only to prove that the measure of S[R/x] is < k. Observe that the only possible way in which the above beta-reduction could introduce new beta-redexes (i.e. beta-redexes which where not already in S or in R) is when S contains a subterm of the form xT (and R is a lambda abstraction). The corresponding subterm after the reduction will be the beta-redex RT. Note that order(RT) < order((\x.S)R) since, if the type of R is A, then the type of (\x.S) is A->B. Finally, observe that order(A->B) is at most k.

Exercise 2

(A -> (B -> C)) -> (A -> B) -> (A -> C) is inhabited. One term with this type is \x\y\z.(xz)(yz).
(A -> B) -> (B -> A) is not inhabited. In fact (A -> B) -> (B -> A) (seen as a propositional formula, where -> represent implication) is not classically valid. In fact, for A=false and B=true the formula is false.
(A * B) -> A is inhabited. One term with this type is \x.(fst x)
A -> (A * B) is not inhabited. In fact A -> (A * B) (seen as a propositional formula, where * represent conjunction) is is not classically valid. In fact, for A=true and B=false the formula is false.
(A -> (B -> C)) -> ((A * B) -> C) is inhabited. One term with this type is \x\y.(x (fst y)(snd y))

The term for an inhabited type can be obtained by constructing the proof that a generic lambda term M has such type.

Exercise 3

One possible recursive definition of a buffer with n cells (for n arbitrary) is the following:

B¹ = in.^out.B¹ (buffer with one cell).
B^k+1 = (B^k[out -> a] | B¹[in -> a])\{a} (buffer with k+1 cells).

This definition constructs B^k+1 from B^k by adding a one-cell buffer at the end. Other solutions are of course possible.