Y combinator
A special case of a combinator is the Y combinator or Y constructor, also sometimes known as "fix". The Y combinator is a formula in lambda calculus which allows the definition of recursive functions in that formalism. The Y combinator is a fixed point combinator that has the property that:
Y x = x (Y x)
Somewhat surprisingly, the Y combinator can be defined as the non-recursive lambda abstraction:
Y = λ h . (λ x . h (x x)) (λ x . h (x x))
See the lambda calculus article for a detailed explanation.
As an example, consider the factorial function. A single step in the recursion of the factorial function is
- h = (λf.λn.(ISZERO n) 1 (MULT n (f (PRED n))))
which is non-recursive. If the factorial function is like a chain (of factors), then the h function above joins two links. Then the factorial function is simply
- FACT = (Y h)
- FACT = (((λ h . (λ x . h (x x)) (λ x . h (x x))) (λf.λn.(ISZERO n) 1 (MULT n (f (PRED n)))))