A Lambda Calculus Guide

1. Combinators: The Building Blocks

The exam references specific standard combinators[cite: 15, 16, 17, 18]. Think of these as reusable function patterns.

Theory (Lambda)

I (Identity): λx.x
K (Constant): λxy.x
S (Substitution): λxyz.xz(yz)
B (Self-Apply): λx.xx

Python Equivalent

I = lambda x: x
K = lambda x: lambda y: x
S = lambda x: lambda y: lambda z: x(z)(y(z))
B = lambda x: x(x)

2. Alpha-Conversion & Beta-Reduction

These are the "computation" rules of the system.

Alpha-Conversion: Renaming variables (e.g., λx.x is the same as λy.y).
Beta-Reduction: Applying a function to an argument[cite: 27, 42].

# Beta Reduction Example: (λx.x) y  =>  y
print(I("y"))  # Output: y

3. Term Length (Inductive Definition)

The exam defines the "size" of a term [cite: 21-24]. This is critical for Question 1(c) and 2(c).

|v| = 1 (Variables)
|PQ| = |P| + |Q| (Applications)
|λv.P| = 1 + |P| (Abstractions)

Example: |λx.x| = 1 + |x| = 1 + 1 = 2. [cite: 25]

4. Normalization

A term is in Normal Form when it cannot be reduced further[cite: 39].

Normalizing: Does the reduction eventually stop?
Strongly Normalizing: Does every possible reduction path stop? [cite: 64]

Python Warning: Some terms (like the Y-Combinator or Omega (λx.xx)(λx.xx)) cause infinite loops (RecursionError).

5. De Bruijn Indices

Question 2(g) asks for De Bruijn indices[cite: 66]. This is a way to represent lambda terms without using variable names, using numbers to point to the "binder" (the λ).

λx.λy.x becomes λλ2 (the 2 points to the second λ out).