Programming Language Concepts
			  Jan-Apr 2016
			  Assignment 3

		  Due Wednesday, 20 April, 2016
		  ----------------------------

*** General Instructions -- Important ***

1. Use the Haskell notation \ for the greek letter lowercase lambda when writing expressions in the lambda calculus. Use the notation := for syntactic equality, and --> and = for (many-step) beta-reduction and beta-equality, respectively. Use M[x <- N] for substitution.
  
2. Submit your solutions as a plain text file named <un>-3.txt, where un is your username. For example, I would submit a file named spsuresh-3.txt.

3. Properly parenthesize your lambda expressions and use spacing to keep it readable.

================================================================================
Questions
---------

1. Let exp := \pqfx. qpfx. Prove by induction on n>=1 that 
		<exp><m><n> --> <m^n>. 

================================================================================

2. 
(a) Find a lambda-expression F such that for all M, FM = F.
(b) Find a lambda-expression F such that for all M, FM = MF.

Hint: You can use the combinator Y (which satisfies YF = F (YF) for all F), in your solutions.

================================================================================

3. 
Prove that every expression in normal form M is of the form 
\x1.\x2...\xk. y M1 M2 ... Ml,
where y is a variable and M1, ..., Ml are expressions in normal form

================================================================================

4.
Find an encoding for the predecessor function in lambda calculus. The predecessor function is given by:
	pred(0) 	= 0
	pred(n+1) 	= n

================================================================================
                                
5. 
Find an encoding for the maximum function:

          max(m,n) 	= m if m >= n,
		  			= n otherwise.

================================================================================

6. 
Combinatory logic is a related system which uses function applications, but no function abstraction. A CL term is either a variable or the constant S or the constant K or the application of term t to term t', denoted (tt'). 
The behaviour of S and K is given by the following rules:

Sxyz --> xz(yz)
Kxy --> x

A combinator is a variable-free CL term. Find combinators (expressions involving S, K, and previously defined combinators, but no variables) with the following behaviour:
(a) I such that Ix --> x. 
(b) T such that Txy --> yx.
(c) B such that Bxyz --> x(yz). 
(d) M such that Mx --> xx.

================================================================================

7.
For a variable x and any CL term M, define [x]M as follows:

[x]x 	= I
[x]y 	= Ky		y a variable other than x
[x](MN) = S([x]M)([x]N)

Prove that for any CL term M:
	a. x does not occur in [x]M
	b. ([x]M)N --> M[x <- N]
	
From b. above, [x]M behaves just like \x.M. So we have the following translation of lambda terms to CL terms.

CL(x) = x
CL(MN) = CL(M)CL(N)
CL(\x.M) = [x](CL(M))

Find combinatory logic terms corresponding to the following lambda terms
	c. \f.(\x.f(xx))(\x.f(xx))
	d. \f.\x.f(fx)
	
================================================================================