Science Fair Project Encyclopedia
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. Formally, a value x is a fixed point of a function f if f(x) = x.
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. 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)))
The simplest fixed point combinator in the SK-calculus, found by John Tromp , is
- Y = S S K (S (K (S S (S (S S K)))) K
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))
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
The contents of this article is licensed from www.wikipedia.org under the GNU Free Documentation License. Click here to see the transparent copy and copyright details