This tutorial is about evaluation of untyped lambda calculus. Participants are supposed to program in lambda calculus and carry out reductions by hand to prove equations about lambda terms.

Homework 3 was changed; metavariables v₁, v₂ etc. were introduced so that the call-by-value reduction rules from the lecture notes apply.

Live exercises

1. What are Church Booleans? What are tru, fls, and, or, not?

2. Define XOR on Church Booleans.

3. What are Church numerals? What is addition on Church numerals?

4. Prove 1 + 1 = 2. What did you prove actually?

5. Prove that addition is associative: (k + m) + n = k + (m + n) for all Church numerals k, m, n.

6. Can you prove that addition is commutative?

Result

Most students were not familiar with lambda calculus and got stuck writing XOR. A minority managed to prove 1 + 1 = 2.

How many tasks can you do after homework 4?