Y combinator
A fixed point combinator is a function which computes fixed points of other functions. A 'fixed point' of a function is a value left 'fixed' by that function; for example, 0 and 1 are fixed points of the squaring function.
In certain formalizations of mathematics, such as the lambda calculus and combinatorial calculus, every function has a fixed point. In these formalizations, it is possible to produce a function, often denoted Y, which computes a fixed point of any function it is given. Since a fixed point x of a function f is a value that has the property f(x) = x, a fixed point combinator Y is a function with the property that f(Y(f)) = Y(f) for all functions f.
From a more practical point of view, fixed point combinators allow the definition of anonymous recursive functions. Somewhat surprisingly, they can be defined with non-recursive lambda abstractions.
One well-known fixed point combinator, discovered by Haskell B. Curry, is
- Y = λf.(λx.(f (x x)) λx.(f (x x)))
and can be expressed in the SKI-calculus as
- Y = S (K (S I I)) (S (S (K S) K) (K (S I I)))
Another common fixed point combinator is the Turing fixed-point combinator (named for its discoverer Alan Turing):
- Θ = (λx.λy.(y (x x y)) λx.λy.(y (x x y)))
This combinator is of interest because a variation of it can be used with 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
