Fixed point combinator

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², because 0² = 0 and 1² = 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) = por, alternately:: 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.

Y combinator

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:

Y g = (λf . (λx . f (x x)) (λx . f (x x))) g Y g = (λx . g (x x)) (λx . g (x x)) (β-reduction of λf - applied main function to g) Y g = (λy . g (y y)) (λx . g (x x)) (α-conversion - renamed bound variable) Y g = g ((λx . g (x x)) (λx . g (x x))) (β-reduction of λy - applied left function to right function) Y g = g (Y g) (definition of Y)

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.

Existence of fixed point combinators

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.

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.

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

Example of encoding via recursive types

In systems with recursive types, it's possible to type the Y combinator by appropriately accounting for the recursion at the type level. The need to self-apply the variable x can be managed using a type (Rec a) which is defined so as to be isomorphic to (Rec a -> a).

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 aout :: Rec a -> (Rec a -> a)

which lets us write:

newtype Rec a = In { out :: Rec a -> a }

y :: (a -> a) -> ay = f -> (x -> f (out x x)) (In (x -> f (out x x)))

See also

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

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)
* http://www.ececs.uc.edu/~franco/C511/html/Scheme/ycomb.html
* [http://use.perl.org/~Aristotle/journal/30896 an example and discussion of a perl implementation]
* [http://www.ps.uni-sb.de/courses/sem-prog97/material/YYWorks.ps "A Lecture on the Why of Y"]
* [http://www.eecs.harvard.edu/~cduan/technical/ruby/ycombinator.shtml "A Use of the Y Combinator in Ruby"]