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)))))

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

• Fixed point combinator

External link

• http://okmij.org/ftp/Computation/fixed-point-combinators
• http://www.cs.brown.edu/courses/cs173/2002/Lectures/2002-10-28-lc.pdf
• http://www.mactech.com/articles/mactech/Vol.07/07.05/LambdaCalculus/