 Fixedpoint combinator

"Y combinator" redirects here. For the technology venture capital firm, see Y Combinator (company).
In computer science, a fixedpoint combinator (or fixpoint combinator^{[1]} ) is a higherorder function that 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^{2}, because 0^{2} = 0 and 1^{2} = 1. Whereas a fixedpoint of a firstorder function (a function on "simple" values such as integers) is a firstorder value, a fixed point of a higherorder function f is another function p such that f(p) = p. A fixedpoint combinator, then, is a function g which produces such a fixed point p for any function f:
 p = g(f), f(p) = p
or, alternatively:
 f(g(f)) = g(f).
Because fixedpoint combinators are higherorder functions, their history is intimately related to the development of lambda calculus. One wellknown fixedpoint combinator in the untyped lambda calculus is Haskell Curry's Y = λf·(λx·f (x x)) (λx·f (x x)). The name of this combinator is sometimes incorrectly used to refer to any fixedpoint combinator. The untyped lambda calculus however, contains an infinitude of fixedpoint combinators^{[citation needed]}. Fixedpoint combinators do not necessarily exist in more restrictive models of computation. For instance, they do not exist in simply typed lambda calculus.
In programming languages that support function literals, fixedpoint combinators allow the definition and use of anonymous recursive functions, i.e. without having to bind such functions to identifiers. In this setting, the use of fixedpoint combinators is sometimes called anonymous recursion.^{[2]}^{[3]}
Contents
How it works
Ignoring for now the question whether fixedpoint combinators even exist (to be addressed in the next section), we illustrate how a function satisfying the fixedpoint combinator equation works. To easily trace the computation steps, we choose untyped lambda calculus as our programming language. The (computational) equality from the equation that defines a fixedpoint combinator corresponds to beta reduction in lambda calculus.
As a concrete example of a fixedpoint combinator applied to a function, we use the standard recursive mathematical equation that defines the factorial function
 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 the lambda abstraction
F = λf. λn. IFTHENELSE (ISZERO n) 1 (MULT n (f (PRED n)))
using the usual encoding for booleans, and Church encoding for numerals. The functions in CAPITALS above can all be defined as lambda abstractions with their intuitive meaning; see lambda calculus for their precise definitions. Intuitively, f in F is a placeholder argument for the factorial function itself.
We now investigate what happens when a fixedpoint combinator FIX is applied to F and the resulting abstraction, which we hope would be the factorial function, is in turn applied to a (Churchencoded) numeral.
(FIX F) n = (F (FIX F)) n  expanded the defining equation of FIX = (λx. IFTHENELSE (ISZERO x) 1 (MULT x ((FIX F) (PRED x)))) n  expanded the first F = IFTHENELSE (ISZERO n) 1 (MULT n ((FIX F) (PRED n)))  applied abstraction to n.
If we now abbreviate FIX F as FACT, we recognize that any application of the abstraction FACT to a Church numeral calculates its factorial
FACT n = IFTHENELSE (ISZERO n) 1 (MULT n (FACT (PRED n))).
Recall that in lambda calculus all abstractions are anonymous, and that the names we give to some of them are only syntactic sugar. Therefore, it's meaningless in this context to contrast FACT as a recursive function with F as somehow being "not recursive". What fixed point operators really buy us here is the ability to solve recursive equations. That is, we can ask the question in reverse: does there exist a lambda abstraction that satisfies the equation of FACT? The answer is yes, and we have a "mechanical" procedure for producing such an abstraction: simply define F as above, and then use any fixed point combinator FIX to obtain FACT as FIX F.
In the practice of programming, substituting FACT at a call site by the expression FIX F is sometimes called anonymous recursion. In the lambda abstraction F, FACT is represented by the bound variable f, which corresponds to an argument in a programming language, therefore F need not be bound to an identifier. F however is a higherorder function because the argument f is itself called as a function, so the programming language must allow passing functions as arguments. It must also allow function literals because FIX F is an expression rather than an identifier. In practice, there are further limitations imposed on FIX, depending on the evaluation strategy employed by the programming environment and the type checker. These are described in the implementation section.
Existence of fixedpoint combinators
In certain mathematical formalizations of computation, such as the untyped lambda calculus and combinatory logic, every expression can be considered a higherorder function. In these formalizations, the existence of a fixedpoint 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 welltyped fixedpoint combinator cannot be written. In those systems any support for recursion must be explicitly added to the language. In still others, such as the simplytyped lambda calculus extended with recursive types, fixedpoint operators can be written, but the type of a "useful" fixedpoint operator (one whose application always returns) may be restricted. In polymorphic lambda calculus (System F) a polymorphic fixedpoint combinator has type ∀a.(a→a)→a, where a is a type variable.
Y combinator
One wellknown (and perhaps the simplest) fixedpoint 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 fixedpoint combinator by applying it to an example function g and rewriting:
Y g = (λf . (λx . f (x x)) (λx . f (x x))) g (by definition of Y) = (λx . g (x x)) (λx . g (x x)) (βreduction of λf: applied main function to g) = (λy . g (y y)) (λx . g (x x)) (αconversion: renamed bound variable) = g ((λx . g (x x)) (λx . g (x x))) (βreduction of λy: applied left function to right function) = g (Y g) (by second equality) In programming practice, the Y combinator is useful only in those languages that provide a callbyname evaluation strategy, since (Y g) diverges (for any g) in callbyvalue settings.
Example in Scheme
(define Y (lambda (f) ((lambda (recur) (f (lambda arg (apply (recur recur) arg)))) (lambda (recur) (f (lambda arg (apply (recur recur) arg)))))))
Factorial definition using Y Combinator
(define fact (Y (lambda (f) (lambda (n) (if (<= n 0) 1 (* n (f ( n 1))))))))
Example in Common Lisp
(defun y (func) ((lambda (x) (funcall x x)) (lambda (y) (funcall func (lambda (&rest args) (apply (funcall y y) args))))))
Factorial program using the Y combinator
(funcall (y (lambda (f) (lambda (x) (if (<= x 1) 1 (* x (funcall f (1 x))))))) 5) => 120
Other fixedpoint combinators
In untyped lambda calculus fixedpoint combinators are not especially rare. In fact there are infinitely many of them. In 2005 Mayer Goldberg showed that the set of fixedpoint combinators of untyped lambda calculus is recursively enumerable.^{[4]}
A version of the Y combinator that can be used in callbyvalue (applicativeorder) 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(x1) >>> Z(fact)(5) 120
The Y combinator can be expressed in the SKIcalculus as
 Y = S (K (S I I)) (S (S (K S) K) (K (S I I)))
The simplest fixed point combinator in the SKcalculus, 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))
This fixedpoint combinator is simpler than the Y combinator, and βreduces into the Y combinator; it is sometimes cited as the Y combinator itself:
 X = λf.(λx.x x) (λx.f (x x))
Another common fixed point combinator is the Turing fixedpoint combinator (named after its discoverer, Alan Turing):
 Θ = (λx. λy. (y (x x y))) (λx. λy. (y (x x y)))
It also has a simple callbyvalue form:
 Θ_{v} = (λx. λy. (y (λz. x x y z))) (λx. λy. (y (λz. x x y z)))
Some fixed point combinators, 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))
Strictly nonstandard fixedpoint combinators
In untyped lambda calculus there are terms that have the same Böhm tree as a fixedpoint combinator, that is they have the same infinite extension λx.x(x(x ... )). These are called nonstandard fixedpoint combinators. Evidently, any fixedpoint combinator is also a nonstandard one, but not all nonstandard fixedpoint combinators are fixedpoint combinators because some of them fail to satisfy the equation that defines the "standard" ones. These strange combinators are called strictly nonstandard fixedpoint combinators; an example is the following combinator N = BM(B(BM)B), where B = λxyz.x(yz) and M = λx.xx. The set of nonstandard fixedpoint combinators is not recursively enumerable.^{[4]}
Implementing fixedpoint combinators
In a language that supports lazy evaluation, like in Haskell, it is possible to define a fixedpoint combinator using the defining equation of the fixedpoint combinator. A programming language of this kind effectively solves the fixedpoint combinator equation by means of its own (lazy) recursion mechanism. This implementation of a fixedpoint combinator in Haskell is sometimes referred to as defining the Y combinator in Haskell. This is incorrect because the actual Y combinator is rejected by the Haskell type checker^{[5]} (but see the following section for a small modification of Y using a recursive type which works). The listing below shows the implementation of a fixedpoint combinator in Haskell that exploits Haskell's ability to solve the fixedpoint combinator equation. This fixedpoint combinator is traditionally called
fix
in Haskell. Observe thatfix
is a polymorphic fixedpoint combinator (c.f. the discussion in previous section on System F); its type is only shown for clarity—it can be inferred in Haskell. The definition is followed by some usage examples.fix :: (a > a) > a fix f = f (fix f) fix (const 9)  const is a function that returns its first parameter and ignores the second;  this evaluates to 9 factabs fact 0 = 1  factabs is F from our lambda calculus example factabs fact x = x * fact (x1) (fix factabs) 5  evaluates to 120
The application of
fix
does not loop infinitely, because of lazy evaluation; e.g. in the expansion offix (const 9)
as(const 9)(fix f)
the subexpressionfix f
is not evaluated. In contrast, the definition of fix from Haskell loops forever when applied in a strict programming language, because the argument to f is expanded beforehand, yielding an infinite call sequencef (f ... (fix f) ... ))
, which causes a stack overflow in most implementations.In a strict language like OCaml, we can avoid the infinite recursion problem by forcing the use of a closure. The strict version of
fix
shall have the type ∀a.∀b.((a→b)→(a→b))→(a→b). In other words, it works only on a function which itself takes and returns a function. For example, the following OCaml code implements a strict version offix
:let rec fix f x = f (fix f) x (* note the extra x *) let factabs fact = function (* factabs now has extra level of lambda abstraction *) 0 > 1  x > x * fact (x1) let _ = (fix factabs) 5 (* evaluates to "120" *)
The same idea can be used to implement a (monomorphic) fixed combinator in strict languages that support inner classes inside methods (called local inner classes in Java), which are used as 'poor man's closures' in this case. Even when such classes may be anonymous, as in the case of Java, the syntax is still cumbersome. Java code. Function objects, e.g. in C++, simplify the calling syntax, but they still have to be generated, preferably using a helper function such as boost::bind. C++ code.
Example of encoding via recursive types
In programming languages that support recursive types (see System F_{ω}), it is possible to type the Y combinator by appropriately accounting for the recursion at the type level. The need to selfapply 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))
Anonymous recursion by other means
Although fixed point combinators are the standard solution for allowing a function not bound to an identifier to call itself, some languages like JavaScript provide a syntactical construct which allows anonymous functions to refer to themselves. For example, in Javascript one can write the following,^{[3]}^{[6]} although it has been removed in the strict mode of the latest standard edition.
function(x) { return x === 0 ? 1 : x * arguments.callee(x1); }
See also
 Fixedpoint iteration
 Anonymous function
 Eigenfunction
Notes
 ^ Peyton Jones, Simon L. (1987). The Implementation of Functional Programming. Prentice Hall International. http://research.microsoft.com/enus/um/people/simonpj/papers/slpjbook1987/.
 ^ This terminology appear to be largely folklore, but it does appear in the following:
 Trey Nash, Accelerated C# 2008, Apress, 2007, ISBN 1590598733, p. 462—463. Derived substantially from Wes Dyer's blog (see next item).
 Wes Dyer Anonymous Recursion in C#, February 02, 2007, contains a substantially similar example found in the book above, but accompanied by more discussion.
 ^ ^{a} ^{b} The If Works Deriving the Y combinator, January 10th, 2008
 ^ ^{a} ^{b} Goldberg, 2005
 ^ Haskell mailing list thread on How to define Y combinator in Haskell, 15 Sep 2006
 ^ Mozilla Developer Center, arguments.callee Examples, Core JavaScript 1.5 Reference
References
 Werner Kluge, Abstract computing machines: a lambda calculus perspective, Springer, 2005, ISBN 3540211462, pp. 73–77
 Mayer Goldberg, (2005) On the Recursive Enumerability of FixedPoint Combinators, BRICS Report RS051, University of Aarhus
 Matthias Felleisen. A Lecture on the Why of Y.
External links
 http://www.latrobe.edu.au/philosophy/phimvt/joy/j05cmp.html
 http://okmij.org/ftp/Computation/fixedpointcombinators.html
 "Fixedpoint combinators in Javascript"
 http://www.cs.brown.edu/courses/cs173/2002/Lectures/20021028lc.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"
 "Functional programming in Ada"
 "Y Combinator in Erlang"
 "The Y Combinator explained with JavaScript"
 "The Y Combinator (Slight Return)" (detailed derivation)
Categories: Lambda calculus
 Mathematics of computing
 Fixed points
 Combinatory logic
 Recursion
Wikimedia Foundation. 2010.