From Bvio

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: : '''Y_k''' = (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 == * combinatory logic * lambda calculus. == External link == * http://okmij.org/ftp/Computation/fixed-point-combinators.html * 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/ * http://www.csse.monash.edu.au/~lloyd/tildeFP/Lambda/Examples/Y/ (executable)