Strong Normalization (100 marks)

An important theorem for the λ -calculus is that simply-typed terms are strongly normalizing: every reduction path will eventually terminate. This is not easy to prove. In this coursework we will consider a proof method by R. O. Gandy. The idea is as follows: fifirst, calculate an upper bound to the length of all possible reductions of a typed term; then, prove that this bound always reduces when a reduction step is applied. Here, we will implement the first part, calculating the upper bound. We won’t do a formal proof that the bound reduces, but we will observe that it does in examples.

Simply-typed terms

First, we will extend the λ -calculus of the tutorials with simple types. Types are given by the following grammar, where o is a base type and σ τ an arrow type.

ρ, σ, τ ::= o | σ τ

The terms of the simply-typed λ -calculus are given by the following grammar.

M, N ::= x | λxτ .M | M N

Assignment 1: (20 marks)

In your fifile you are given the implementation of the λ -calculus from the tutorials. We will first extend this to the simply-typed calculus.

a) Complete the datatype Type to represent simple types following the grammar above.For the base type, use the constuctor Base , and for the arrow type, use the (infix) constructor :-> . Un-comment the function nice , the Show instance, and the examples type1 and type2 to see if everything type-checks.

b) Make the datatype Type a member of the type class Eq so that (==) gives equality of types.

c) Adapt the datatype Term for λ -terms from the tutorials to simply-typed terms, following the grammar above. Un-comment the function pretty and the Show instance to see if everything type-checks.

d) Un-comment the function numeral from the tutorials and adapt it to work with simply typed terms, following the defifinition here:

Nn = λf oo .λxo .Ln          L0 = x Ln+1 = f Ln

Un-comment also the other functions and examples for numerals, from sucterm to example7 .

e) Un-comment the functions used , rename , substitute , and beta from the tutorials and adapt them to work with simply-typed terms.

f) Un-comment normalize and prepare it to display a number before each term. We will adapt this to display the upper bound to reductions later, but any number will do for now.

*Main> type2

(o -> o) -> o -> o

*Main> type2 == type1 :-> type1

True

*Main> type2 == type1

False

*Main> numeral 4

\f: o -> o . \x: o . f (f (f (f x)))

*Main> example1

(\m: (o -> o) -> o -> o . \f: o -> o . \x: o . m f (f x))

(\f: o -> o . \x: o . x)

*Main> normalize it

0 — (\m: (o -> o) -> o -> o . \f: o -> o . \x: o . m f (f x))

(\f: o -> o . \x: o . x)

0 — \a: o -> o . \b: o . (\f: o -> o . \x: o . x) a (a b)

0 — \a: o -> o . \b: o . (\b: o . b) (a b)

0 — \a: o -> o . \b: o . a b

Type checking

The types we have added so far are only an annotation, but really we want those terms that are well-typed: where the types of functions and arguments match in the expected way. To check if a given term is well-typed is a simple inductive algorithm that we will implement here. (Note that this is different from type inference, which is the more involved algorithm that decides whether an untyped term can be given a type.) The defifinitions are as follows. E-mail: itcsdx@outlook.com  微信:itcsdx 