Fixed-point combinator - Misplaced Pages

This is an old revision of this page, as edited by Pcap (talk | contribs) at 07:07, 21 August 2009 ("anonymous function" is a trivial property in lambda calculus, because all function are anonymous there. The example is thus uninformative. See talk page for more.). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

Revision as of 07:07, 21 August 2009 by Pcap (talk | contribs) ("anonymous function" is a trivial property in lambda calculus, because all function are anonymous there. The example is thus uninformative. See talk page for more.)(diff) ← Previous revision | Latest revision (diff) | Newer revision → (diff) "Y combinator" redirects here. For the technology venture capital firm, see Y 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) = p

or, alternately:

f(g(f)) = g(f).

In programming languages that first-order functions, fixed point combinators allow the definition and use of anonymous recursive functions, i.e. without having to bind such functions to identifiers.

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 in 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 and (rank-1) parametric polymorphism, 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" *)

The same idea can be used to implement a monomorphic strict Y combinator in C++, using function objects, which effectively simulate first-class functions, generated preferably using a helper function such as boost::bind. Code.

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

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

The set of fixed point combinators is recursively enumerable (Goldberg, 2005).

Strictly non-standard fixed point combinators

In untyped lambda calculus there are terms that have the same Böhm tree as fixed point combinator, that is they have the same infinite extension λx.x(x(x ... )) . These are called non-standard fixed point combinators. Evidently, any fixed point combinator is also a non-standard one, but not all non-standard fixed point combinators are fixed point combinators because some of them fail to satisfy the equation that defines the "standard" ones. These strange combinators are called strictly non-standard fixed point combinators; an example is the following combinator N = BM(B(BM)B), where B = λx.xx and M = λxyz.x(yz). The set of non-standard fixed point combinators is not recursively enumerable (Goldberg, 2005).

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

References

Mayer Goldberg, (2005) On the Recursive Enumerability of Fixed-Point Combinators, BRICS Report RS-05-1, University of Aarhus

External links

Categories: