Fixed point combinator |
A fixed point combinator (or fixed-point operator ) is a higher-order function which computes a fixed point (mathematics) of other functions.
A fixed point of a function f is a value x such that f( x )= x . For example, 0 and 1 are fixed points of the function f( x )=x2, because 02=0 and 12=1. Wheras the fixed-point of a first-order function (a function on simple values such as integers) is a first-order value, the fixed point of a higher-order function f is another function g such that f(g) = g. A fixed point operator, then, is any function fix such that for any function f , : f (fix( f )) = fix( f ).
Fixed point combinators allow the definition of anonymous recursive functions (see the Fixed point combinator#Example below). Somewhat surprisingly, they can be defined with non-recursive lambda abstractions.
One well-known (and perhaps the simplest) fixed point combinator in the untyped lambda calculus is called the Y combinator. It was discovered by Haskell Curry, and is defined as
: Y = λf.(λx.f (x x)) (λx.f (x x))
= Existence of fixed point combinators =
In certain formalizations of mathematics, such as the untyped lambda calculus and combinatory logic, every expression can be considered a higher-order function. In these formalizations, the existence of a fixed-point combinator means that every function has at least one fixed point; a function may have more than one distinct fixed point.
In some other systems, for example the simply typed lambda calculus, a well-typed fixed-point combinator cannot be written -- in those systems any support for recursion must be explicitly added to the language. In still others, such as the simply-typed lambda calculus extended with recursive type, fixed-point operators can be written, but the type of a useful fixed-point operator (one whose application always returns) may be restricted.
For example, in Standard ML the call-by-value variant of the Y combinator has the type ∀a.∀b.→(a→b), whereas the call-by-name variant has the type ∀a.(a→a)→a. The call-by-name (normal) variant loops forever when applied in a call-by-value language -- every application Y(f) expands to f(Y(f)). The argument to f is then expanded, as required for a call-by-value language, yielding f(f(Y(f))). This process iterates forever (until the system runs out of memory), without ever actually evaluating the body of f.
= Example =
Consider the factorial function (under church numerals). The usual recursive mathematical equation is :fact( n ) = if n =0 then 1 else n * fact( n -1) We can express a single step of this recursion in lambda calculus as :F = λf. λx. (ISZERO x) 1 (MULT x (f (PRED x))), where f is a place-holder argument for the factorial function to be passed to itself. The function F performs a single step in the evaluation of the recursive formula. Applying the fix operator gives :fix(F)(n) = F(fix(F))(n) :fix(F)(n) = λx. (ISZERO x) 1 (MULT x (fix(F) (PRED x)))(n) :fix(F)(n) = (ISZERO n) 1 (MULT n (fix(F) (PRED n))) We can abbreviate fix(F) as fact, and we have :fact(n) = (ISZERO n) 1 (MULT n (fact(PRED n)))
So we see that a fixed-point operator really does turn our non-recursive factorial step function into a recursive function satisfying the intended equation.
= Other fixed point combinators =
A version of the Y combinator that can be used in call-by-value (applicative-order evaluation) evaluaton is given by Eta expansion of part of the ordinary Y combinator:
: Z = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))
The Y combinator can be expressed in the SKI combinator 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)))
It also has a simple call-by-value form:
: Θv = (λx. λy. (y (λz. x x y z))) (λx. λy. (y (λz. x x y z)))
Fixed point combinators are not especially rare (there are infinitely many of them). Some, such as this one (constructed by Jan Willem Klop) are useful chiefly for amusement:
: 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))
= See also =
= External links =
|
|