# Fixed point combinator

### From Wikipedia, the free encyclopedia

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

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

## Contents |

## [edit] 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*:

Yg = (λf . (λx . f (x x)) (λx . f (x x))) gYg = (λ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.

## [edit] 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.

In a language which supports lazy evaluation, the **Y** combinator can be written with type ∀a.(a→a)→a. For example, the following Haskell code correctly implements the Y combinator:

fix :: (a -> a) -> a fix f = f (fix f) -- "fix (const 9)" evaluates to "9" fact f 0 = 1 fact f x = x * f (x-1) -- "(fix fact) 5" evaluates to "120"

Note that this definition doesn't infinitely loop because of laziness. However, the above version loops forever when applied in a strict programming 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**.

The strict version of the **Y** combinator has the type ∀a.∀b.((a→b)→(a→b))→(a→b) (in other words, it only works on a function which itself takes and returns a function). For example, the following OCaml code implements this version of the Y combinator:

let rec fix f x = f (fix f) x let fact f = function 0 -> 1 | x -> x * f (x-1) let _ = (fix fact) 5 (* evaluates to "120" *)

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

Here is an example of this in Python:

>>> Z = lambda f: (lambda x: f(lambda *args: x(x)(*args)))(lambda x: f(lambda *args: x(x)(*args))) >>> fact = lambda f: lambda x: 1 if x == 0 else x * f(x-1) >>> Z(fact)(5) 120

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**= (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)_{k}

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

Or equivalently in OCaml:

type 'a recc = In of ('a recc -> 'a) let out (In x) = x let y f = (fun x a -> f (out x x) a) (In (fun x a -> f (out x x) a))

## [edit] See also

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

## [edit] External links

- http://www.latrobe.edu.au/philosophy/phimvt/joy/j05cmp.html
- http://okmij.org/ftp/Computation/fixed-point-combinators.html
- "Fixed-point combinators in Javascript"
- 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.ece.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"