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) Consider the term

Is there an irreducible term S with the property that

Justify your answer. (3 marks)

b) For the term F from the previous part, how many times does f occur in ◊ ◊(FF)? Justify your answer. (5 marks)

c) Consider the following statement: If t is a λ-term containing exactly one redex and  then t' contains no redexes.

We consider this statement in two settings. For each, decide whether the statement is true or false and justify your answer.

i) Assume that t and t' are terms in the untyped λ-calculus. (2 marks)

ii) Assume that t and t' are terms in the simply typed λ-calculus, and that there exists a type  such that ⊢ t∶ is derivable. (3 marks)

d) Consider the logical predicate  given by setting, for the base type,

i) Which of the following pairs are elements of 

Justify your answers. (3 marks)

ii) Show that at all types  we have that (4 marks)

2. Consider the simply typed λ-calculus where we have added the constants tt, ff, and, for each type ,  with the following additional type derivation rules

a) Find suitable typing decorations (for bound variables, and replacing ? for the occurrences of the constant T) and derive a type for the term (3 marks)

b) Assume we add the following β-reduction rules to the system:

Let E be the type-decorated term from the previous part. Reduce the following term as far as possible. (2 marks)

c) Assume we want to define denotations for terms in our system using the underlying set B = {0, 1}. We have to extend our rules by saying how to interpret the constants, which we do as follows for a type environment Γ and corresponding valuation φ:

while  is interpreted by as follows:

where tst is a function that takes as input a value x from B and values y, z from  and delivers an output in  and is given as follows:

For E from the previous two parts, calculate  (2 marks)

d)  Give a term C in this system that implements logical conjunction, also known as ‘and’, that is, a term of a suitable type that evaluates to tt precisely when both its arguments evaluate to tt.                                                                        (2 marks)

e) We look at the semantics from part c).

i) How many elements does  have? (2 marks)

ii) How many of these are commutative binary operations? (2 marks)

f) In this part we are concerned with terms of type ( →  → ) →  and their semantics from part c).

i) Give two terms F and G each of which uses exactly three occurrences of the constant tt, and no occurrence of the constant ff, such that

is derivable, and which have different denotations. Make sure to justify the last claim. (5 marks)

ii) For the term E from parts a) to c), do FE and GE have the same denotation? Justify your answer. (2 marks)