In combinatory logic for computer science, a fixed-point combinator (or fixpoint combinator) is a higher-order function (i.e., a function that takes a function as argument) that returns some fixed point (a value that is mapped to itself) of its argument function, if one exists.
Formally, if is a fixed-point combinator and the function has one or more fixed points, then is one of these fixed points, i.e.,
Fixed-point combinators can be defined in the lambda calculus and in functional programming languages, and provide a means to allow for recursive definitions.
Introduction Applied to a non-constant function of one variable that treats its argument as a piece of data (such as e.g. the sine function), the Y combinator usually does not terminate. Y really is meant to be used with codata, e.g. a colist constructor that places the first element there and expects "the rest of elements" as an argument, that will be fleshed out later; or a higher-order function that expects to be supplied as its first argument with a function "to compute the rest," which it might or might not call, as needed.
Applied to such "one step functional," Y arranges for the creation of that "rest of computation" function, consisting of that same step it was given and the "rest of computation" again, which really means just the original step repeated as many times as needed, calling "the rest" function as and if needed, but not always. The resulting function behaves like a while or a for loop. Used in this way, the Y combinator implements general recursion.
The lambda calculus does not have global names, for a function to refer to itself by name inside its own definition, as is possible in many programming languages. But it has local names, i.e. parameters in lambda abstractions. An abstraction term can receive another term as an argument, and refer to that argument by the parameter name inside the function's body.
The Y combinator may also be used in implementing Curry's paradox. The heart of Curry's paradox is that untyped lambda calculus is unsound as a deductive system, and the Y combinator demonstrates this by allowing an anonymous expression to represent zero, or even many values. This is inconsistent in mathematical logic.
Y combinator in lambda calculus In the classical untyped lambda calculus, every function has a fixed point. A particular implementation of is Haskell Curry's paradoxical combinator Y, given byThroughout this article, the syntax rules given in are used, to save parentheses.According to Barendregt p.132, the name originated from Curry.
(Here using the standard notations and conventions of lambda calculus: Y is a function that takes one argument f and returns the entire expression following the first period; the expression denotes a function that takes one argument x, thought of as a function, and returns the expression , where denotes x applied to itself. Juxtaposition of expressions denotes function application, is left-associative, and has higher precedence than the period.)
Verification The following calculation verifies that is indeed a fixed point of the function : {| cellpadding="0"
| by the definition of
| by β-reduction: replacing the formal argument f of Y with the actual argument g
| by β-reduction: replacing the formal argument x of the first function with the actual argument
| by second equality, above
The lambda term may not, in general, β-reduce to the term . However, both terms β-reduce to the same term, as shown.
Example implementations An example implementation of Y in the language R is presented below:Y <- \(f) { g <- \(x) f(x(x)) g(g) }This can then be used to implement factorial as follows:fact <- \(f) \(n) if (n == 0) 1 else n * f(n - 1)
Y(fact)(5) # yields 5! = 120Y is only needed when function names are absent. Substituting all the definitions into one line so that function names are not required gives:(\(f) (\(x) f(x(x)))(\(x) f(x(x)))) (\(f) \(n) if (n == 0) 1 else n * f(n - 1)) (5)This works because R uses lazy evaluation.
Languages that use strict evaluation, such as Python, C++, and other strict programming languages, can often express Y; however, any implementation is useless in practice since it loops indefinitely until terminating via a stack overflow.
Fixed-point combinator
The Y combinator is an implementation of a fixed-point combinator in lambda calculus. Fixed-point combinators may also be easily defined in other functional and imperative languages. The implementation in lambda calculus is more difficult due to limitations in lambda calculus. The fixed-point combinator may be used in a number of different areas: General mathematics Untyped lambda calculus Typed lambda calculus Functional programming Imperative programming
Fixed-point combinators may be applied to a range of different functions, but normally will not terminate unless there is an extra parameter. When the function to be fixed refers to its parameter, another call to the function is invoked, so the calculation never gets started. Instead, the extra parameter is used to trigger the start of the calculation.
The type of the fixed point is the return type of the function being fixed. This may be a real or a function or any other type.
In the untyped lambda calculus, the function to apply the fixed-point combinator to may be expressed using an encoding, like Church encoding. In this case particular lambda terms (which define functions) are considered as values. "Running" (beta reducing) the fixed-point combinator on the encoding gives a lambda term for the result, which may then be interpreted as fixed-point value.
Alternately, a function may be considered as a lambda term defined purely in lambda calculus.
These different approaches affect how a mathematician and a programmer may regard a fixed-point combinator. A mathematician may see the Y combinator applied to a function as being an expression satisfying the fixed-point equation, and therefore a solution.
In contrast, a person only wanting to apply a fixed-point combinator to some general programming task may see it only as a means of implementing recursion.
Values and domains Many functions do not have any fixed points, for instance with . Using Church encoding, natural numbers can be represented in lambda calculus, and this function f can be defined in lambda calculus. However, its domain will now contain all lambda expressions, not just those representing natural numbers. The Y combinator, applied to f, will yield a fixed-point for f, but this fixed-point won't represent a natural number. If trying to compute Y f in an actual programming language, an infinite loop will occur.
Function versus implementation
The fixed-point combinator may be defined in mathematics and then implemented in other languages. General mathematics defines a function based on its extensional properties. That is, two functions are equal if they perform the same mapping. Lambda calculus and programming languages regard function identity as an intensional property. A function's identity is based on its implementation.
A lambda calculus function (or term) is an implementation of a mathematical function. In the lambda calculus there are a number of combinators (implementations) that satisfy the mathematical definition of a fixed-point combinator.
Definition of the term "combinator"
Combinatory logic is a higher-order functions theory. A combinator is a closed lambda expression, meaning that it has no free variables. The combinators may be combined to direct values to their correct places in the expression without ever naming them as variables.
Recursive definitions and fixed-point combinators
Fixed-point combinators can be used to implement recursive definition of functions. However, they are rarely used in practical programming. Strongly normalizing type systems such as the simply typed lambda calculus disallow non-termination and hence fixed-point combinators often cannot be assigned a type or require complex type system features. Furthermore, fixed-point combinators are often inefficient compared to other strategies for implementing recursion, as they require more function reductions and construct and take apart a tuple for each group of mutually recursive definitions.
The factorial function
The factorial function provides a good example of how a fixed-point combinator may be used to define recursive functions. The standard recursive definition of the factorial function in mathematics can be written as
where n is a non-negative integer.
This poses a problem, though, as inside the definition of cannot possibly signify the inclusion of the definition as a whole inside itself. Instead, as it normally goes almost unnoticed, it is the reference to the definition by its name. This presupposes the existence of a global registry of names, so called "environment". And the lambda calculus lacks this entirely.
Still, name references do exist in lambda calculus – local names, names of parameters of a given function. And thus the above can be re-written as
Splitting off a separate copy of and passing it as an argument to itself makes it available to itself to be called, as and if needed, inside itself. In such a call it must again be passed along as an argument so it will be available to the next invocation, and so on, as the chain of invocations progresses. The definition of is open recursive, and calling with itself as an argument at the top closes the circle.
Implementing this in lambda calculus is now trivial, and directly leads to the definition of the Y combinator, one instance of a fixed-point combinator, such that . Or directly, define a function F of two arguments f and n:
(Here is a function that takes two arguments and returns its first argument if n=0, and its second argument otherwise; evaluates to n–1.)
Now define . Then is a fixed-point of F, which gives
as desired.
Fixed-point combinators in lambda calculus
The Y combinator, discovered by Haskell Curry, is defined as
Other fixed-point combinators
In untyped lambda calculus fixed-point combinators are not especially rare. In fact there are infinitely many of them. In 2005 Mayer Goldberg showed that the set of fixed-point combinators of untyped lambda calculus is recursively enumerable.Goldberg, 2005
The Y combinator can be expressed in the SKI-calculus as
Additional combinators (B, C, K, W system) allow for much shorter encodings. With the self-application combinator, since and , the above becomes
The shortest fixed-point combinator in the SK-calculus using S and K combinators only, found by John Tromp, is
although note that it is not in normal form, which is longer. This combinator corresponds to the lambda expression
The following fixed-point combinator is simpler than the Y combinator, and β-reduces into the Y combinator; it is sometimes cited as the Y combinator itself:
Another common fixed-point combinator is the Turing fixed-point combinator (named after its discoverer, Alan Turing):
Its advantage over is that beta-reduces to , whereas and only beta-reduce to a common term.
also has a simple call-by-value form:
The analog for mutual recursion is a polyvariadic fix-point combinator,Polyvariadic Y in pure Haskell98 , lang.haskell.cafe, October 28, 2003 which may be denoted Y*.
Strict fixed-point combinator
In a strict programming language the Y combinator will expand until stack overflow, or never halt in case of tail call optimization. The Z combinator will work in strict languages (also called eager languages, where applicative evaluation order is applied). The Z combinator has the next argument defined explicitly, preventing the expansion of in the right-hand side of the definition:
and in lambda calculus it is an eta-expansion of the Y combinator:
Non-standard fixed-point combinators
If F is a fixed-point combinator in untyped lambda calculus, then there is: