Fixed point combinator

From Free net encyclopedia

Y combinator redirects here. For the technology seed firm started by Paul Graham, see Y Combinator.

A fixed point combinator (or fixed-point operator) is a higher-order function which computes a fixed point 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. Whereas a fixed-point of a first-order function (a function on "simple" values such as integers) is a first-order value, a 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 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 B. Curry, and is defined as

Y = λf.(λx.f (x x)) (λx.f (x x))

Contents

[edit]

Existence of fixed point combinators

In certain formalizations of mathematics, such as the untyped lambda calculus and combinatorial calculus, 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 types, 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)→(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.

[edit]

Example

Consider the factorial function (under Church encoding). 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.

[edit]

Other fixed point combinators

A version of the Y combinator that can be used in call-by-value (applicative-order) evaluation is given by η-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-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)

which corresponds to the lambda expression

Y = (λx. λy. x y x) (λy. λx. y (x y x))

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)

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))
[edit]

See also

[edit]

External links

Retrieved from "http://www.netipedia.com/index.php/Fixed_point_combinator"