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.
What is the syntax of simply typed lambda calculus? What are its typing rules?
What is induction on typing derivations?
Prove that if
Γ ⊢ t : Tand
xis free in
x : S ∈ Γfor some type
Most students are not familiar with simply typed lambda calculus and cannot answer questions 1 and 2. One student managed to do exercise 3.