Editing Fixed-point combinator (section)

==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 <math>f : \N \to \N</math> with <math>f(n)=n+1</math>. Using [[Church encoding]], natural numbers can be represented in lambda calculus, and this function ''f'' can be defined in lambda calculus. However, its [[domain of a function|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 [[extensionality|extensional]] properties.<ref>{{cite web |last1=Selinger |first1=Peter |date=2001–2013 |title=Lecture notes on the lambda calculus: Expository course notes |url=https://www.mscs.dal.ca/~selinger/papers/#lambdanotes |page=6 |format=PDF}} </ref> That is, two functions are equal if they perform the same mapping. Lambda calculus and programming languages regard function identity as an [[Intensional definition|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 function]]s theory. A [[combinator]] is a ''closed'' lambda expression, meaning that it has no [[Free variables and bound variables|free variables]]. The combinators may be combined to direct values to their correct places in the expression without ever naming them as variables.