- 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 inprogramming language theory because it allows the implementation ofrecursion in the form of arewrite 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) = x2, because 02 = 0 and 12 = 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 abstraction s.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 andcombinatory 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 withrecursive type s, 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 thecall-by-value variant of the Y combinator has the type ∀a.∀b.((a→b)→(a→b))→(a→b), whereas thecall-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:: Yk = (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"]
Wikimedia Foundation. 2010.