Added to Favorites

Popular Searches

A fixed point combinator (or fixed-point operator) is a higher-order function that computes a fixed point of other functions. This operation is relevant in programming language theory because it allows the implementation of recursion in the form of a rewrite rule, without explicit support from the language's runtime engine.

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*) = x^{2}, because 0^{2} = 0 and 1^{2} = 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 **p** such that **f**(**p**) = **p**. A fixed point combinator, then, is a function **g** which produces such a fixed point **p** for any function **f**:

**p**=**g**(**f**),**f**(**p**) =**p**

**f**(**g**(**f**)) =**g**(**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))

We can see that this function acts as a fixed point combinator by expanding it for an example function *g*:

Yg = (λf . (λx . f (x x)) (λx . f (x x))) g

Yg = (λx . g (x x)) (λx . g (x x)) (β-reduction of λf - applied main function to g)

Yg = (λy . g (y y)) (λx . g (x x)) (α-conversion - renamed bound variable)

Yg = g ((λx . g (x x)) (λx . g (x x))) (β-reduction of λy - applied left function to right function)

Yg = g (Yg) (definition ofY)

Note that the **Y** combinator is intended for the call-by-name evaluation strategy, since (**Y** *g*) diverges (for any *g*) in call-by-value settings.

In certain mathematical formalizations of computation, 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 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.

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)

- F = λf. λx. (ISZERO x) 1 (MULT x (f (PRED x))),

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

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

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 after 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:

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

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

For example, in the following Haskell code, we have In and out being the names of the two directions of the isomorphism, with types:

In :: (Rec a -> a) -> Rec a out :: Rec a -> (Rec a -> a)

which lets us write:

newtype Rec a = In { out :: Rec a -> a }y :: (a -> a) -> a y = f -> (x -> f (out x x)) (In (x -> f (out x x)))

- Fixed point (mathematics)
- Fixed point iteration
- combinatory logic
- untyped lambda calculus
- typed lambda calculus
- anonymous recursion
- eigenfunction

- 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)
- http://www.ececs.uc.edu/~franco/C511/html/Scheme/ycomb.html
- an example and discussion of a perl implementation
- "A Lecture on the Why of Y"
- "A Use of the Y Combinator in Ruby"

Wikipedia, the free encyclopedia © 2001-2006 Wikipedia contributors (Disclaimer)

This article is licensed under the GNU Free Documentation License.

Last updated on Wednesday August 27, 2008 at 14:45:24 PDT (GMT -0700)

View this article at Wikipedia.org - Edit this article at Wikipedia.org - Donate to the Wikimedia Foundation

This article is licensed under the GNU Free Documentation License.

Last updated on Wednesday August 27, 2008 at 14:45:24 PDT (GMT -0700)

View this article at Wikipedia.org - Edit this article at Wikipedia.org - Donate to the Wikimedia Foundation

Copyright © 2014 Dictionary.com, LLC. All rights reserved.