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

COMP31311

Giving Meaning to Programs

1. a) Let

G = λx. λy. y.

Show that for all terms t it is the case that there exists a term u such that

(3 marks)

b) Consider the following term.

i) Draw a graph that shows the βα-reductions for this term. (4 marks)

ii) For the terms in your graph from the previous part, which ones can be given type annotations in such a way that a type may be derived for the term? Either give such an annotation and a type derivation or argue that the term in question is not typeable. (5 marks)

iii) Consider the parallel reduct operation as applied to the term T.

• Compute ◊T up to α-equivalence. (2 marks)

• For n ∈ ℕ, compute ◊ nT up to α-equivalence. (2 marks)

c) Consider the logical predicate V which is given by

i) Which of the following are elements of

Justify your answers. (3 marks)

ii) Is the following an element of

Justify your answer. (1 mark)

2. Let X be a set. For n ∈ ℕ, let

be the ‘iterate the input function n times’ operation.

a) Construct a term J in the simply typed λ-calculus with the property that (3 marks)

b) Consider the following term in the simply typed λ-calculus.

i) What is the type of V? (1 mark)

ii) Compute Explain how you arrive at your answer. (3 marks)

c) Let

Assume we have terms E, M and S such that the following are derivable

and that we further have the following information about the behaviour of these terms:

Let

For k ∈ ℕ, calculate (5 marks)

d) Consider the term Y = (V G)(λf∶  → . λx∶. f x), where V is the term from part b), and G the one from part c).

The term Y is known to βα-reduce to (at least) one of the following terms.

Which ones does it reduce to? Justify your answer. (8 marks)