In combinatory logic for computer science, a fixed-point combinator (or fixpoint combinator),^[1]: p.26 is a higher-order function (i.e. a function which 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 ${\displaystyle {\textrm {fix}}}$ is a fixed-point combinator and the function ${\displaystyle f}$ has one or more fixed points, then ${\displaystyle {\textrm {fix}}\ f}$ is one of these fixed points, i.e.

${\displaystyle f\ ({\textrm {fix}}\ f)={\textrm {fix}}\ f\ .}$

Fixed-point combinators can be defined in the lambda calculus and in functional programming languages and provide a means to allow for recursive definitions.

Y combinator in lambda calculus

In the classical untyped lambda calculus, every function has a fixed point. A particular implementation of ${\displaystyle {\textrm {fix}}}$ is Haskell Curry's paradoxical combinator Y, given by^{[2]: 131 [note 1]}

${\displaystyle Y=\lambda f.\ (\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))}$

(Here we use 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 ${\displaystyle \lambda x.f\ (x\ x)}$ denotes a function that takes one argument x, thought of as a function, and returns the expression ${\displaystyle f\ (x\ x)}$, where ${\displaystyle (x\ x)}$ 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 ${\displaystyle Yg}$ is indeed a fixed point of the function ${\displaystyle g}$:

${\displaystyle Y\ g\ }$	${\displaystyle =(\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x)))\ g\ \ \ }$	by the definition of ${\displaystyle Y}$
	${\displaystyle =(\lambda x.g\ (x\ x))\ (\lambda x.g\ (x\ x))\ }$	by β-reduction: replacing the formal argument f of Y with the actual argument g
	${\displaystyle =g\ ((\lambda x.g\ (x\ x))\ (\lambda x.g\ (x\ x)))\ }$	by β-reduction: replacing the formal argument x of the first function with the actual argument ${\displaystyle (\lambda x.g\ (x\ x))}$
	${\displaystyle =g\ (Y\ g)}$	by second equality, above

The lambda term ${\displaystyle g\ (Y\ g)}$ may not, in general, β-reduce to the term ${\displaystyle Y\ g}$. However, both terms β-reduce to the same term, as shown.

Uses

Applied to a function with one variable, the Y combinator usually does not terminate. More interesting results are obtained by applying the Y combinator to functions of two or more variables. The additional variables may be used as a counter, or index. The resulting function behaves like a while or a for loop in an imperative language.

Used in this way, the Y combinator implements simple recursion. The lambda calculus does not allow a function to appear as a term in its own definition as is possible in many programming languages, but a function can be passed as an argument to a higher-order function that applies it in a recursive manner.

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.

Example implementations

An example implementation of the Y combinator in two languages is presented below.

# Y Combinator in Python

Y = lambda f: (lambda x: f(x(x)))(lambda x: f(x(x)))

Y(Y)

// Y Combinator in C++, using C++ 14 extensions

int main() {
    auto Y = (auto f) {
        auto f1 = (auto x) -> decltype(f) {
            return f(x(x));
        };
        return f1(f1);
    };

    Y(Y);
}

Note that both of these programs, while formally correct, are useless in practice; they both loop indefinitely until they terminate through stack overflow. More generally, as both Python and C++ use strict evaluation, the Y combinator is generally useless in those languages; see below for the Z combinator, which can be used in strict programming languages.

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 ${\displaystyle f:\mathbb {N} \to \mathbb {N} }$ with ${\displaystyle f(n)=n+1}$. 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 expression, 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.^[3] 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.^[4] 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.^{[1]: page 232}

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

Zdroj:https://en.wikipedia.org?pojem=Fixed_point_combinator
Text je dostupný za podmienok Creative Commons Attribution/Share-Alike License 3.0 Unported; prípadne za ďalších podmienok. Podrobnejšie informácie nájdete na stránke Podmienky použitia.

---