| • Science | • People | • Locations | • Timeline |
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. Formally, a value x is a fixed point of a function f if f(x) = x; a fixed point combinator is a function Y which, given another function f, computes a fixed point of f, so that f(Y(f)) = Y(f) for all functions f.
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
and can be expressed in the SKI-calculus as
Another common fixed point combinator is the Turing fixed-point combinator (named for its discoverer Alan Turing):
This combinator is of interest because a variation of it can be used with applicative-order reduction :
Fixed point combinators are not especially rare. Here is one constructed by Jan Willem Klop :
where
Consider the factorial function. A single step in the recursion of the factorial function is
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
The fixed point combinator 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.