Fixed point 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 applicative-order reduction:

Θv = λh.(λx.(h λy.(y (x x y))) λx.(h λy.(y (x x y))))

Fixed point combinators are not especially rare. Here is one constructed by Jan Willem Klop:

Yk = (L L L L L L L L L L L L L L L L L L L L L L L L L L L L)


where

L = λabcdefghijklmnopqstuvwxyzr.(r (t h i s i s a f i x e d p o i n t c o m b i n a t o r)) WTFWTFWTF

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

See also

External link

This article is licensed under the GNU Free Documentation License. It uses material from Wikipedia article. Browse Wikipedia for more information.