Encyclopedia > Y combinator

  Article Content

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

External link



All Wikipedia text is available under the terms of the GNU Free Documentation License

 
  Search Encyclopedia

Search over one million articles, find something about almost anything!
 
 
  
  Featured Article
257

... 280s 290s 300s Years: 252 253 254 255 256 - 257 - 258 259 260 261 262 Events Pope Sixtus II succeeds Pope Stephen I Births Saint Gregory the Illuminator, ...