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)))))
The Y-constructor causes the H combinator to repeat itself indefinitely until it trips itself up with (ISZERO 0) = TRUE.
By the way, these equations are meta-equations; functions in lambda calculus are all anonymous. The function labels Y, H, FACT, PRED, MULT, ISZERO, 1, 0 (defined in the article for lambda calculus) are meta-labels, to which correspond meta-definitions and meta-equations, and with which a user can perform algebraic meta-substitutions. That is how mathematicians can prove properties of the lambda calculus. The equals sign as an assignment operation is not part of the lambda calculus.
See Also
External link
All Wikipedia text
is available under the
terms of the GNU Free Documentation License