Google
 
   
Login
Username:

Password:


Lost Password?

Register now!
Search
Main Menu
top books
Polls
What do you think about php-deluxe.net?
Excellent!
Cool
Hmm..not bad
What the hell is this?
encyclopedia
recommendation
compare webbrowser
Freenet DSL
Who's Online
3 user(s) are online (3 user(s) are browsing encyclopedia)

Members: 0
Guests: 3

more...
browser tip
Unix Befehle
manual of unix befehle
recommendation!
Sponsored
partner

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 =

  • combinatory logic
  • untyped lambda calculus
  • typed lambda calculus
  • = External links =

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