Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: daixieit

COMP31311

Giving Meaning to Programs

1. Consider the following term of the untyped λ-calculus.

a) Compute the parallel reduct ◊t of t. You may invoke several instances of the denition in each step.            (4 marks)

b) Give a sequence of βα-reduction steps from t to ◊t. (2 marks)

c) Consider the type-annotated term

What is the type of this term? Prove that your answer is correct by giving a formal derivation. Hint: You may find it useful to use abbreviations for some types and some type environments.          (9 marks)

d) Give a type annotated version of ◊t, find its type and prove that it may indeed be given that type. (5 marks)

2. Consider the set of booleans B = {0, 1}.

a) Give an example of two terms of the simply typed calculus of type ( → ) → → which are contextually equivalent, but not αβ-equivalent. (2 marks)

b) Compute the following: (8 marks)

c) Which of the terms in part (b) are contextually equivalent to which others? Give proofs of any claims you make; you may refer to your answer for part (b) if this is useful, or use any other method studied in this unit. (10 marks)

3. Consider the flat domain B⊥:

a) Compute the function space B⊥ ⇒ B⊥ and draw its Hasse diagram. (4 marks)

b) Consider the order-preserving function

which, given an input f ∶ B⊥ ⇒ B⊥ , gives an element of B⊥ ⇒ B⊥ , that is an order-preserving function from B⊥ to B⊥ , given by the following cases:

What are the fixed points of G? What is the least fixed point of G? (4 marks)

c) Assume we have a PCF term E∶nat → nat → nat with the following behaviour: If one of the inputs is ⊥ it returns ⊥ and otherwise

Consider the following PCF term t:

i) What is the type of t? (2 marks)

ii) Describe the denotation of t. (4 marks)

iii) Identify a significantly shorter term that is contextually equivalent to t. (2 marks)

iv) Show that your term from the previous part is indeed contextually equivalent to the given one. (4 marks)