This tutorial is about homework 3 and structural induction on typing derivations of simply typed lambda calculus.

These points about homework 3 are noteworthy:

• Task 5 asks whether progress and preservation continue to hold for each of the 3 rules. It does not ask what would happen if all 3 rules were added at the same time.

• In Task 6, beta reduction is allowed in the subterms of applications. The relevant rules are E-App1 and E-App2.

Live exercises

1. What is the syntax of simply typed lambda calculus? What are its typing rules?

2. What is induction on typing derivations?

3. Prove that if Γ ⊢ t : T and x is free in t, then x : S ∈ Γ for some type S.

Result

Most students are not familiar with simply typed lambda calculus and cannot answer questions 1 and 2. One student managed to do exercise 3.