Lambda reduction is an umbrella term for all these transformations — that is, alpha-, beta-, and eta-conversion. With these, we can step-by-step transform lambda expressions into simpler, equivalent forms.

α- Conversion

This is essentially the renaming of variables. A lambda expression remains the same as long as we consistently rename the bound variables.

1𝜆𝑥.𝑥+1 is the same as 𝜆𝑦.𝑦+1

β- Reduction

Beta reduction is the actual execution of a function. That is applying a lambda expression to an argument.

1(𝜆𝑥.𝑥+1) 5 ⇒ 5 + 1 ⇒ 6

η- Conversion

Eta conversion describes that two functions are considered equal if they produce the same result for all arguments.

1𝜆𝑥.𝑓 𝑥 is the same as 𝑓

f: is a function

x: does not occur freely in f

This means that a function which does nothing but call another function is identical to that function.

Examples

Alpha-Conversion (Renaming Variables)

Question:

Perform an alpha-conversion on the following lambda expression:

1𝜆𝑥.𝑥² + 2𝑥 + 1

Rename x to another variable — but ensure that the meaning remains the same.

Solution:

1𝜆𝑥.𝑥² + 2𝑥 + 1 → 𝜆𝑦.𝑦² + 2𝑦 + 1

Following is valid, in the sence of an algebraic simplification, but its not an alpha conversion.

1𝑥² + 2𝑥 + 1 = (𝑥 + 1)²
2𝜆𝑥.(𝑥 + 1)²

Question:

Which of the following expressions is an alpha-variant of 𝜆𝑎.𝑎 + 3 ?

a) 𝜆𝑏.𝑏 + 3
b) 𝜆𝑥.𝑥 + 3
c) 𝜆𝑎.3 + 𝑎

Solution: a and b are valid alpha variants for 𝜆𝑎.𝑎 + 3