d

Recursion In Lambda Calculus

To achieve recursion in lambda calculus, a fixed-point function is required. The fixed-point function is generally referred to as Y, and must by definition satisfy Yf=f(Yf).

The function used for Y is λf.(λg.f(gg))(λg.f(gg)). Yf can be beta reduced to (λg.f(gg))(λg.f(gg)), which in turn can be beta reduced to fg.f(gg))(λg.f(gg)), satisfying Yf=f(Yf).

Using Y, a function has access to a bound copy of itself. If lambda expressions were named, you might want to write fx1...xnE, where E is some expresion refering to f. With the Y combinator, the function on the right becomes Yλfx1...xnE.