Fixed point combinator

Encyclopedia : F : FI : FIX : Fixed point combinator

---

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 which computes a fixed point 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) = 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 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 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 B. 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 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.

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

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

See also

• 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

 

---

From Wikipedia, the Free Encyclopedia. Original article here. Support Wikipedia by contributing or donating.
All text is available under the terms of the GNU Free Documentation License See Wikipedia Copyrights for details.

Search Titles

0

1

2

3

4

5

6

7

8

9

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

?