Submission Details

Marks: 100

Weighting: 20%

Submission  Guidelines:  Submissions can be typed in LATEX, typed as a simple text doc- ument, or handwritten, either written on a tablet or as a scan.

If you are typing your answer as a text document, then use the following conventions:

● backslash“/”for λ;

● a combination of hyphen and greater than, i.e.,“_ ;”for -8  or -;

● round brackets“( ,)”for input e.g., on channel a of z with continuation P , i.e., a(z)．P

● less than, greater than“←．;”for output e.g., on channel a of z with continuation P , i.e., a ← z ;．P

● pipe from the keyboard“)”for parallel composition and

● simply the word“new”for channel creation, e.g., (new z)P .

If your submission is handwritten, you must make sure it is clear and legible. If not, you will be marked down.

Put your name and student number on it. Include a“own work” declaration.

Note: For all the questions on proving, you should state clearly what it is that you are proving (a complete statement), the proof technique and clear structure of the proof.  If not, you will be marked down.

λ-calculus (60 marks)

Throughout this section, we use the variable convention or Barendregt convention, assuming that all bound variables in λ-terms are different from each other and from all free variables.

Question 1 [15 marks]:

1. We define the size of a λ-term as follows, recursively on the structure of the term.

size(z)          =   1

size(λz．疝)   =   size(疝) + 1

size(疝N)     =   size(疝) + size(N)

Recall the representation of natural numbers (Lab Week 3), using the λ-terms Z (for zero) and s (for successor). For a natural number n, write rn厂 for the λ-term that represents it (this notation is used in Hankin’s book). So r0厂 = Z = λz．z, r1厂 = s(Z), and so on...

Following the above definition, calculate  size(Z) and  size(s) and work out a general formula for size(rn厂) in terms of n.  [10 marks]

2. A λ-term is said to be linear if every free variable occurs exactly once and every bound variable occurs exactly once (note that the z in λz．疝 is not an occurrence of z, it is just denoting that z is bound). For example:

● λz．z is linear because the bound variable z occurs exactly once.

●  (λz．λy．zy)3 is linear because the bound variables, z and y, occur exactly once each and the free variable, 3 , occurs exactly once.

● λz．λy．z is not linear, because there is no bound occurrence of y .

For each of the following λ-terms (from Lab Week 3), answer whether or not the term is linear, and why: T, 尹 , Z , s, pair.  [5 marks]

Question 2 [30 marks]:

1. Theorem 1: For all linear λ-terms 疝 and N, if FV (疝) 0 FV (N) = -, then 疝[z := N] is linear. Prove this theorem and state what proof technique you are using.  [15 marks]

2. Theorem 2: If 疝 is linear and 疝 -8  N, then N is linear. Prove this theorem and state what proof technique you are using.  [15 marks]

Question 3 [15 marks]:

Simply-typed lambda  calculus  is introduced in Week 5 (check the lectures for details on the types and typing rules).

1. Recall the S, K, and I combinators from Week 3. In Week 5 we saw in class the typing derivation for K, and I. Draw the typing derivation for S. [5 marks]

2. Try to construct a typing derivation for the term (zy)(z(λ3．y)). What happens? Discuss. [5 marks]

3. Try to construct a typing derivation for the term zz. What happens? Discuss. [5 marks]