Literature and other notes to the lecture

Literature

Introduction to Lambda Calculus, Barendregt & Barensen, 2002.
- Section 1 - all.
- Section 2 - up to Def. 2.14; you don't need to remember the rest - the operations on Church numerals, just their basic definition is enough.
- Section 3 - just Definitions 3.1 and 3.2, Theorem 3.17
- Section 4 - up to 4.12. (no need to know the proof of Church-Roser theorem), and 4.20-4.23.
Converting λ terms into the combinatory calculi: Combinatory calculi, in particular section Completeness of the S-K basis. (A bit more advanced article I wrote on this topic can be found in The Monad Reader, Issue 17: The Reader Monad and Abstraction Elimination.)

Natural deduction - you can skip all parts concerning quantifiers as we're interested only in propositional logic.

Dependent types
- Programming in Martin-Löf's Type Theory. Bengt Nordström, Kent Petersson and Jan M. Smith. Oxford University, 1990.
- Dependently Typed Programming in Agda. Ulf Norell. 2009.
- Certified Programming with Dependent Types. Adam Chlipala.
- Software Foundations. Benjamin C. Pierce, Chris Casinghino, Michael Greenberg, Vilhelm Sjöberg, Brent Yorgey.

Church defined δ-reduction as follows:

Term is in δ-normal form if:

doesn't contain any subterm of the form (λx.M)N
doesn't contain any subterm of the form δMN, where M aand N are combinators (have no free variables).

We define δ-reduction as:

δMN →_δ T (true) if both M and N are in δ-normal form, don't contain variables, and they are α-equal.
δMN →_δ F (false) if both M and N are in δ-normal form, don't contain variables, and they are not α-equal.