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.

This article was last edited on 26th September 2006. The author can be contacted using the form below.
Back to home page
Bookmark with: