Fixed point combinator: Encyclopedia II - Fixed point combinator - Existence of fixed point combinators

Fixed point combinator - 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.

Adapted from the Wikipedia article "Existence of fixed point combinators", under the G.N U Free Docmentation License. Please also see http://en.wikipedia.org/wiki