Incombinatory logic forcomputer science, afixed-point combinator (orfixpoint combinator)^[1]: p.26 is ahigher-order function (i.e., afunction that takes a function asargument) that returns somefixed point (a value that is mapped to itself) of its argument function, if one exists.

Formally, if${\displaystyle \mathrm{f}\mathrm{i}\mathrm{x}}$ is a fixed-point combinator and the function${\displaystyle f}$ has one or more fixed points, then${\displaystyle \mathrm{f}\mathrm{i}\mathrm{x}f}$ is one of these fixed points, i.e.,

${\displaystyle \mathrm{f}\mathrm{i}\mathrm{x}f=f(\mathrm{f}\mathrm{i}\mathrm{x}f).}$

Fixed-point combinators can be defined in thelambda calculus and infunctional programming languages, and provide a means to allow forrecursive definitions.

In the classical untypedlambda calculus, every function has a fixed point. A particular implementation of${\displaystyle \mathrm{f}\mathrm{i}\mathrm{x}}$ isHaskell Curry's paradoxical combinator Y, given by^{[2]: 131 [note 1][note 2]}

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

(Here using the standard notations and conventions of lambda calculus: Y is a function that takes one argumentf and returns the entire expression following the first period; the expression${\displaystyle \lambda x.f(xx)}$ denotes a function that takes one argumentx, thought of as a function, and returns the expression${\displaystyle f(xx)}$, where${\displaystyle (xx)}$ denotesx applied to itself. Juxtaposition of expressions denotesfunction application, is left-associative, and has higher precedence than the period.)

The following calculation verifies that${\displaystyle \mathrm{Y}g}$ is indeed a fixed point of the function${\displaystyle g}$:

${\displaystyle \mathrm{Y}g}$	${\displaystyle \triangleq (\lambda f.(\lambda x.f(xx))(\lambda x.f(xx)))g}$	by the definition of${\displaystyle \mathrm{Y}}$
	${\displaystyle {=}_{{}_{\beta }}(\lambda x.g(xx))(\lambda x.g(xx))}$	byβ-reduction: replacing the formal argumentf of Y with the actual argumentg
	${\displaystyle {=}_{{}_{\beta }}g((\lambda x.g(xx))(\lambda x.g(xx)))}$	by β-reduction: replacing the formal argumentx of the first function with the actual argument${\displaystyle (\lambda x.g(xx))}$
	${\displaystyle \equiv g(\mathrm{Y}g)}$	by second equality, above

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

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 added variables may be used as a counter, or index. The resulting function behaves like awhile or afor loop in an imperative language.

Used in this way, the Y combinator implements simplerecursion. The lambda calculus does not allow a function to appear as a term in its own definition as is possible in manyprogramming 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 implementingCurry'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 inmathematical logic.

An example implementation of Y in the languageR 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)1elsen*f(n-1)Y(fact)(5)# yields 5! = 120

Y 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)1elsen*f(n-1))(5)

This works because R useslazy evaluation.

Languages that usestrict evaluation, such asPython,C++, and otherstrict programming languages, can often express Y; however, any implementation is useless in practice since itloops indefinitely until terminating via astack overflow.

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:

• Generalmathematics
• Untypedlambda 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, likeChurch 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.

Many functions do not have any fixed points, for instance${\displaystyle f:\mathbb{N}\to \mathbb{N}}$ with${\displaystyle f(n)=n+1}$. UsingChurch encoding, natural numbers can be represented in lambda calculus, and this functionf can be defined in lambda calculus. However, itsdomain will now containall lambda expressions, not just those representing natural numbers. The Y combinator, applied tof, will yield a fixed-point forf, but this fixed-point won't represent anatural number. If trying to compute Yf in an actual programming language, an infinite loop will occur.

The fixed-point combinator may be defined in mathematics and then implemented in other languages. General mathematics defines a function based on itsextensional properties.^[3] That is, two functions are equal if they perform the same mapping. Lambda calculus and programming languages regard function identity as anintensional 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.

Combinatory logic is ahigher-order functions theory. Acombinator is aclosed lambda expression, meaning that it has nofree variables. The combinators may be combined to direct values to their correct places in the expression without ever naming them as variables.

Fixed-point combinators can be used to implementrecursive definition of functions. However, they are rarely used in practical programming.^[4]Strongly normalizingtype systems such as thesimply 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}

Thefactorial 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

wheren is a non-negativeinteger.Implementing this in lambda calculus, where integers are represented usingChurch encoding, encounters the problem that the lambda calculus disallows the name of a function ('fact') to be used in the function's definition. This can be circumvented using a fixed-point combinator${\displaystyle \mathsf{\text{fix}}}$ as follows.

Define a functionF of two argumentsf andn:

${\displaystyle Ffn=(\mathrm{IsZero}n)1(\mathrm{multiply}n(f(\mathrm{pred}n)))}$

(Here${\displaystyle (\mathrm{IsZero}n)}$ is a function that takes two arguments and returns its first argument ifn=0, and its second argument otherwise;${\displaystyle \mathrm{pred}n}$ evaluates ton–1.)

Now define${\displaystyle \mathrm{fact}=\mathsf{\text{fix}}F}$. Then${\displaystyle \mathrm{fact}}$ is a fixed-point ofF, which gives

as desired.

The Y combinator, discovered byHaskell Curry, is defined as

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

In untyped lambda calculus fixed-point combinators are not especially rare. In fact there are infinitely many of them.^[5] In 2005 Mayer Goldberg showed that the set of fixed-point combinators of untyped lambda calculus isrecursively enumerable.^[6]

The Y combinator can be expressed in theSKI-calculus as

${\displaystyle \mathsf{Y}\mathsf{=}\mathsf{S}\mathsf{(}\mathsf{K}\mathsf{(}\mathsf{S}\mathsf{I}\mathsf{I}\mathsf{)}\mathsf{)}\mathsf{(}\mathsf{S}\mathsf{(}\mathsf{S}\mathsf{(}\mathsf{K}\mathsf{S}\mathsf{)}\mathsf{K}\mathsf{)}\mathsf{(}\mathsf{K}\mathsf{(}\mathsf{S}\mathsf{I}\mathsf{I}\mathsf{)}\mathsf{)}\mathsf{)}\mathsf{=}\mathsf{S}\mathsf{S}\mathsf{(}\mathsf{S}\mathsf{(}\mathsf{S}\mathsf{(}\mathsf{K}\mathsf{S}\mathsf{)}\mathsf{K}\mathsf{)}\mathsf{)}\mathsf{(}\mathsf{K}\mathsf{(}\mathsf{S}\mathsf{I}\mathsf{I}\mathsf{)}\mathsf{)}}$

Additional combinators (B, C, K, W system) allow for much shorter encodings. With${\displaystyle \mathsf{U}\mathsf{=}\mathsf{S}\mathsf{I}\mathsf{I}}$ the self-application combinator, since${\displaystyle \mathsf{S}(\mathsf{K}x)yz=x(yz)=\mathsf{B}xyz}$ and${\displaystyle \mathsf{S}x(\mathsf{K}y)z=xzy=\mathsf{C}xyz}$, the above becomes

${\displaystyle \mathsf{Y}\mathsf{=}\mathsf{S}\mathsf{(}\mathsf{K}\mathsf{U}\mathsf{)}\mathsf{(}\mathsf{S}\mathsf{B}\mathsf{(}\mathsf{K}\mathsf{U}\mathsf{)}\mathsf{)}\mathsf{=}\mathsf{B}\mathsf{U}\mathsf{(}\mathsf{C}\mathsf{B}\mathsf{U}\mathsf{)};\mathsf{Y}\mathsf{=}\mathsf{S}\mathsf{S}\mathsf{I}\mathsf{(}\mathsf{B}\mathsf{W}\mathsf{B}\mathsf{)}}$

The shortest fixed-point combinator in the SK-calculus using S and K combinators only, found byJohn Tromp, is

${\displaystyle {\mathsf{Y}}^{\prime }\mathsf{=}\mathsf{S}\mathsf{S}\mathsf{K}\mathsf{(}\mathsf{S}\mathsf{(}\mathsf{K}\mathsf{(}\mathsf{S}\mathsf{S}\mathsf{(}\mathsf{S}\mathsf{(}\mathsf{S}\mathsf{S}\mathsf{K}\mathsf{)}\mathsf{)}\mathsf{)}\mathsf{)}\mathsf{K}\mathsf{)}\mathsf{=}\mathsf{W}\mathsf{C}\mathsf{(}\mathsf{S}\mathsf{B}\mathsf{(}\mathsf{C}\mathsf{(}\mathsf{W}\mathsf{C}\mathsf{)}\mathsf{)}\mathsf{)}}$

although note that it is not in normal form, which is longer. This combinator corresponds to the lambda expression

${\displaystyle {\mathsf{Y}}^{\prime }=(\lambda xy.xyx)(\lambda yx.y(xyx))}$

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:

${\displaystyle \mathsf{X}=\lambda f.(\lambda x.xx)(\lambda x.f(xx));\mathsf{X}\mathsf{f}\mathsf{=}\mathsf{U}\mathsf{(}\mathsf{B}\mathsf{f}\mathsf{U}\mathsf{)}}$

Another common fixed-point combinator is the Turing fixed-point combinator (named after its discoverer,Alan Turing):^{[7][2]: 132}

${\displaystyle \mathrm{\Theta }=(\lambda xy.y(xxy))(\lambda xy.y(xxy))=\mathsf{S}\mathsf{I}\mathsf{I}\mathsf{(}\mathsf{S}\mathsf{(}\mathsf{K}\mathsf{(}\mathsf{S}\mathsf{I}\mathsf{)}\mathsf{)}\mathsf{(}\mathsf{S}\mathsf{I}\mathsf{I}\mathsf{)}\mathsf{)}\mathsf{=}\mathsf{U}\mathsf{(}\mathsf{B}\mathsf{(}\mathsf{S}\mathsf{I}\mathsf{)}\mathsf{U}\mathsf{)}}$

Its advantage over${\displaystyle \mathsf{Y}}$ is that${\displaystyle \mathrm{\Theta }f}$ beta-reduces to${\displaystyle f(\mathrm{\Theta }f)}$,^{[note 3]}whereas${\displaystyle \mathsf{Y}f}$ and${\displaystyle f(\mathsf{Y}f)}$ only beta-reduce to a common term.

${\displaystyle \mathrm{\Theta }}$ also has a simplecall-by-value form:

${\displaystyle {\mathrm{\Theta }}_v=(\lambda xy.y(\lambda z.xxyz))(\lambda xy.y(\lambda z.xxyz))}$

The analog formutual recursion is apolyvariadic fix-point combinator,^[8][9][10] which may be denoted Y*.

In astrict programming language the Y combinator will expand untilstack overflow, or never halt in case oftail call optimization.^[11] The Z combinator will work instrict languages (also called eager languages, where applicative evaluation order is applied). The Z combinator has the next argument defined explicitly, preventing the expansion of${\displaystyle Zg}$ in the right-hand side of the definition:^[12]

${\displaystyle Zgv=g(Zg)v.}$

and in lambda calculus it is aneta-expansion of the Y combinator:

${\displaystyle Z=\lambda f.(\lambda x.f(\lambda v.xxv))(\lambda x.f(\lambda v.xxv)).}$

If F is a fixed-point combinator in untyped lambda calculus, then there is:

${\displaystyle \mathsf{F}=\lambda x.Fx=\lambda x.x(Fx)=\lambda x.x(x(Fx))=\cdots }$

Terms that have the sameBöhm tree as a fixed-point combinator, i.e., have the same infinite extension${\displaystyle \lambda x.x(x(x\cdots ))}$, are callednon-standard fixed-point combinators. Any fixed-point combinator is also a non-standard one, but not all non-standard fixed-point combinators are fixed-point combinators because some of them fail to satisfy the fixed-point equation that defines the "standard" ones. These combinators are calledstrictly non-standard fixed-point combinators; an example is the following combinator:

${\displaystyle \mathsf{N}\mathsf{=}\mathsf{B}\mathsf{U}\mathsf{(}\mathsf{B}\mathsf{(}\mathsf{B}\mathsf{U}\mathsf{)}\mathsf{B}\mathsf{)}}$

where

${\displaystyle \mathsf{B}=\lambda xyz.x(yz)}$

${\displaystyle \mathsf{U}=\lambda x.xx}$

since

${\displaystyle \mathsf{N}=\lambda x.Nx=\lambda x.x(N_{2}x)=\lambda x.x(x(x(N_{3}x)))=\lambda x.x(x(x(x(x(x(N_{4}x))))))=\cdots }$

where${\displaystyle {\mathsf{N}}_i}$ are modifications of${\displaystyle \mathsf{N}}$ created on the fly which add${\displaystyle i}$ instances of${\displaystyle x}$ at once into the chain while being replaced with${\displaystyle {\mathsf{N}}_{i+1}}$.

The set of non-standard fixed-point combinators is notrecursively enumerable.^[6]

The Y combinator is a particular implementation of a fixed-point combinator in lambda calculus. Its structure is determined by the limitations of lambda calculus. It is not necessary or helpful to use this structure in implementing the fixed-point combinator in other languages.

Simple examples of fixed-point combinators implemented in someprogramming paradigms are given below.

In a language that supportslazy evaluation, as inHaskell, it is possible to define a fixed-point combinator using the defining equation of the fixed-point combinator which is conventionally namedfix. Since Haskell has lazydata types, this combinator can also be used to define fixed points of data constructors (and not only to implement recursive functions). The definition is given here, followed by some usage examples. In Hackage, the original sample is:^[13]

fix,fix'::(a->a)->afixf=letx=fxinx-- Lambda dropped. Sharing.-- Original definition in Data.Function.-- alternative:fix'f=f(fix'f)-- Lambda lifted. Non-sharing.fix(\x->9)-- this evaluates to 9fix(\x->3:x)-- evaluates to the lazy infinite list [3,3,3,...]fact=fixfac-- evaluates to the factorial functionwherefacf0=1facfx=x*f(x-1)fact5-- evaluates to 120

In a strict functional language, as illustrated below withOCaml, the argument tof is expanded beforehand, yielding an infinite call sequence,

${\displaystyle f(f...(f(\mathsf{f}\mathsf{i}\mathsf{x}f))...)x}$.

This may be resolved by defining fix with an extra parameter.

letrecfixfx=f(fixf)x(* note the extra x; hence fix f = \x-> f (fix f) x *)letfactabsfact=function(* factabs has extra level of lambda abstraction *)0->1|x->x*fact(x-1)let_=(fixfactabs)5(* evaluates to "120" *)

In a multi-paradigm functional language (one decorated with imperative features), such asLisp,Peter Landin suggested the use of a variable assignment to create a fixed-point combinator,^[14] as in the below example usingScheme:

(defineY!(lambda(f)((lambda(g)(set!g(f(lambda(x)(gx))));; (set! g expr) assigns g the value of expr,g);; replacing g's initial value of #f, creating#f)));; thus the truly self-referential value in g

Using a lambda calculus with axioms for assignment statements, it can be shown thatY! satisfies the same fixed-point law as the call-by-value Y combinator:^[15][16]

${\displaystyle (Y_{!}\lambda x.e)e^{\prime }=(\lambda x.e)(Y_{!}\lambda x.e)e^{\prime }}$

In more idiomatic modern Scheme usage, this would typically be handled via aletrec expression, aslexical scope was introduced to Lisp in the 1970s:

(defineY*(lambda(f)(letrec;; (letrec ((g expr)) ...) locally defines g((g;; as expr recursively: g in expr refers to(f(lambda(x)(gx)))));; that same g being defined, g = f (λx. g x)g)));; ((Y* f) ...) = (g ...) = ((f (λx. g x)) ...)

Or without the internal label:

(defineY*(lambda(f)((lambda(i)(ii))(lambda(i)(f(lambdax(apply(ii)x)))))))

This example is a slightly interpretive implementation of a fixed-point combinator. A class is used to contain thefix() function, calledFixedPointCombinator. The function to be fixed is contained in a class that inherits from fixer. Thefix() function accesses the function to be fixed using aconcept to callapply(). As for the strict functional definition,fix() is explicitly given an extra parameterx, which means that lazy evaluation is not needed.

usingstd::same_as;template<typenameRet,typenameArg,typenameT>conceptFixedPointApplicable=requires(Argx){{T::apply(x)}->same_as<Ret>;};template<typenameRet,typenameArg,FixedPointApplicable<Ret,Arg>Derived>classFixedPointCombinator{public:staticRetfix(Argx)noexcept{returnDerived::apply(x);}};classFactorial:publicFixedPointCombinator<long,long,Factorial>{staticlongapply(longx)noexcept{if(x==0){return1;}returnx*fix(x-1);}};longresult=Factorial::fix(5);

Using only lambdas, one can create a fixed-point combinator like so:

autofix=[](autof){return[f](auto&&...args)->decltype(auto){returnf(f,std::forward<decltype(args)>(args)...);};};autofactorial=fix([](autoself,longn)->long{returnn==0?1:n*self(self,n-1);});std::println("5! = {}",factorial(5));// prints 120

Another example can be shown to demonstrateSKI combinator calculus (with given bird name fromcombinatory logic) being used to build up Z combinator to achievetail call-like behavior through trampolining:

// CombinatorsconstK=<A,B>(a:A)=>(_b:B)=>a;// KestrelconstS=<A,B,C>(a:(x:C)=>(y:B)=>A)=>(b:(x:C)=>B)=>(c:C)=>a(c)(b(c));// Starling// Derived combinatorsconstI=S(K)(K);// IdentityconstB=S(K(S))(K);// BluebirdconstC=S(B(B)(S))(K(K));// CardinalconstW=C(S)(I);// WarblerconstT=C(I);// ThrushconstV=B(C)(T);// VireoconstI1=C(C(I));// Identity Bird Once Removed; same as C(B(B)(I))(I)constC1=B(C);// Cardinal Once RemovedconstR1=C1(C1);// Robin Once RemovedconstV1=B(R1)(C1);// Vireo Once RemovedconstI2=R1(V);// Identity Bird Twice Removed// Z combinatorsconstZ=B(W(I1))(V1(B)(W(I2)));constZ2=S(K(S(S(K(S(S(K)(K))(S(K)(K))))(S(K(S(K(S))(K)))(S(K(S(S(K)(K))))(K))))(K(S(S(K))))))(S(S(K(S(S(K(S(K(S))(K)))(S))(K(K))))(S(K(S(S(K(S(K(S))(K)))(S))(K(K))))(S(K(S))(K))))(K(S(S(K(S(S(K)(K))(S(K)(K))))(S(K(S(K(S))(K)))(S(K(S(S(K)(K))))(K))))(K(S(K(S(S(K(S(S(K(S(K(S))(K)))(S))(K(K))))(S(K(S(S(K(S(K(S))(K)))(S))(K(K))))(S(K(S(S(K)(K))))(K))))))(K))))));// Alternative fully expanded form.constZ3=S(S(K(S(S)(K(S(S(K)(K))(S(K)(K))))))(K))(S(S(K(S))(K))(K(S(S(K(S))(S(K(S(K(S(K(S(K(S(S)(K(K))))(K)))(S)))(S(S(K)(K)))))(K)))(K(K(S(S(K)(K))(S(K)(K))))))));// Another shorter version.consttrampoline=<T>(fn:T|(()=>T)):T=>{letctx=fn;while(typeofctx==="function"){ctx=(ctxas()=>T)();}returnctx;};constcountFn=(self:(n:number)=>any)=>(n:number):any=>n===0?(console.log(n),n):()=>self(n-1);// Return thunk "() => self(n - 1)" instead.// Examplestrampoline(Z(countFn)(10));trampoline(Z2(countFn)(10));trampoline(Z3(countFn)(10));

InSystem F (polymorphic lambda calculus) a polymorphic fixed-point combinator has type^[17]

∀a.(a → a) → a

where${\displaystyle a}$ is atype variable. That is, if the type of${\displaystyle \mathrm{f}\mathrm{i}\mathrm{x}f}$ fulfilling the equation${\displaystyle \mathrm{f}\mathrm{i}\mathrm{x}f=f(\mathrm{f}\mathrm{i}\mathrm{x}f)}$ is${\displaystyle a}$—the most general type—then the type of${\displaystyle f}$ is${\displaystyle a\to a}$. So then,${\displaystyle \mathrm{f}\mathrm{i}\mathrm{x}}$ takes a function that maps${\displaystyle a}$ to${\displaystyle a}$ and uses it to return a value of type${\displaystyle a}$.

In the simply typed lambda calculus extended withrecursive data types, fixed-point operators can be written, but the type of a "useful" fixed-point operator (one whose application always returns) may be restricted.

In thesimply typed lambda calculus, the fixed-point combinator Y cannot be assigned a type^[18] because at some point it would deal with the self-application sub-term${\displaystyle xx}$ by the application rule:

$\frac{{\displaystyle \mathrm{\Gamma }⊢x:t_1\to t_2\mathrm{\Gamma }⊢x:t_1}}{\mathrm{\Gamma }⊢xx:t_2}$

where${\displaystyle x}$ has the infinite type${\displaystyle t_1=t_1\to t_2}$. No fixed-point combinator can in fact be typed; in those systems, any support for recursion must be explicitly added to the language.

In programming languages that support namedrecursive data types, the unbounded recursion in${\displaystyle t:=t\to a}$, which creates the would-be infinite type${\displaystyle t}$, is broken by naming the type${\displaystyle t}$ explicitly, as e.g. type${\displaystyle Ra}$ which is defined so as to be isomorphic to (or just to be a synonym of) the type${\displaystyle Ra\to a}$. Thus${\displaystyle Ra:=Ra\to a}$ is recognized as a recursive type. A datum (value) of the type${\displaystyle Ra}$ is created by simply tagging a value that is a function that has the type${\displaystyle Ra\to a}$, by the data constructor tag for the type${\displaystyle Ra}$.

For example, in the following Haskell code, letRec be that tag name, and thusRec andapp be the names of the two directions of the isomorphism, with types:^[19][20]

Rec::(Ra->a)->Raapp::Ra->(Ra->a)

(where${\displaystyle ::}$ means "has type"). This lets us write:

newtypeRa=Rec{app::Ra->a}-- app (Rec g) = g    -- g :: R a -> a--      Rec g      :: R a-- app             :: R a -> (R a -> a)y::(a->a)->ayf=(\x->f(appxx))(Rec(\x->f(appxx)))--       x :: R a--   app x :: R a -> a-- app x x ::        a

The usual lambda-calculus definition${\displaystyle \mathrm{Y}f=\mathrm{U}(\lambda x.f(\mathrm{U}x))}$ (where${\displaystyle \mathrm{U}x=xx}$, and thus the term${\displaystyle \mathrm{U}(\lambda x.f(\mathrm{U}x))}$ witnesses the equivalence${\displaystyle xx=f(xx)}$) contains at its core the self-application${\displaystyle xx}$, which is untypeable in the statically typed programming languages. But the expressionapp x x aboveis typeable. Equivalently, we can redefine the self-application combinator${\displaystyle \mathrm{U}}$ and use it as

U'g=g(Recg)yf=U'(\Recg->f(U'g))--     g (Rec g)  =  f (g (Rec g))U''x=appxxyf=U''(Rec(\x->f(U''x)))--        app x x  =  f (app x x)

Or in OCaml:

type'arecc=Inof('arecc->'a)letout(Inx)=xletyf=(funxa->f(outxx)a)(In(funxa->f(outxx)a))

Alternatively:

letyf=(funx->f(funz->outxxz))(In(funx->f(funz->outxxz)))

Some languages allow for explicitly marking general types as being recursive even without naming them. Doing that also allows for defining the${\displaystyle \mathrm{Y}}$ combinator in such languages.

Because fixed-point combinators can be used to implement recursion, it is possible to use them to describe specific types of recursive computations, such as those infixed-point iteration,iterative methods,recursive join inrelational databases,data-flow analysis, FIRST and FOLLOW sets of non-terminals in acontext-free grammar,transitive closure, and other types ofclosure operations.

A function for whichevery input is a fixed point is called anidentity function. Formally:

${\displaystyle \mathrm{\forall }x(fx=x)}$

In contrast touniversal quantification over all${\displaystyle x}$, a fixed-point combinator constructsone value that is a fixed point of${\displaystyle f}$. The remarkable property of a fixed-point combinator is that it constructs a fixed point for anarbitrary given function${\displaystyle f}$.

Other functions have the special property that, after being applied once, further applications don't have any effect. More formally:

${\displaystyle \mathrm{\forall }x(f(fx)=fx)}$

Such functions are calledidempotent (see alsoProjection (mathematics)). An example of such a function is the function that returns 0 for all even integers, and 1 for all odd integers.

Inlambda calculus, from a computational point of view, applying a fixed-point combinator to an identity function or an idempotent function typically results in non-terminating computation. For example, obtaining

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

where the resulting term can only reduce to itself and represents an infinite loop.

Fixed-point combinators do not necessarily exist in more restrictive models of computation. For instance, they do not exist insimply typed lambda calculus.

The Y combinator allowsrecursion to be defined as a set ofrewrite rules,^[21] without requiring native recursion support in the language.^[22]

In programming languages that supportanonymous functions, fixed-point combinators allow the definition and use of anonymousrecursive functions, i.e., without having tobind such functions toidentifiers. In this setting, the use of fixed-point combinators is sometimes calledanonymous recursion.^{[note 4][23]}

• Anonymous function
• Fixed-point iteration
• Lambda calculus#Recursion and fixed points
• Lambda lifting
• Lawvere's fixed-point theorem
• Let expression

• Werner Kluge,Abstract computing machines: a lambda calculus perspective, Springer, 2005,ISBN 3-540-21146-2, pp. 73–77
• Mayer Goldberg, (2005)On the Recursive Enumerability of Fixed-Point Combinators, BRICS Report RS-05-1, University of Aarhus
• Matthias Felleisen,A Lecture on theWhy ofY.

Wikibooks has a book on the topic of:Haskell/Fix and recursion

• Recursion Theory and Joy, Manfred von Thun, (2002 or earlier)
• The Lambda Calculus - notes by Don Blaheta, October 12, 2000
• Y CombinatorArchived 2009-03-23 at theWayback Machine
• "A Use of the Y Combinator in Ruby"
• "Functional programming in Ada"
• Rosetta code - Y combinator

• Combinatory logic
• Fixed points (mathematics)
• Lambda calculus
• Mathematics of computing
• Recursion
• Programming language comparisons

• Webarchive template wayback links
• Articles with short description
• Short description matches Wikidata
• Articles with example C++ code
• Articles with example Haskell code
• Articles with example JavaScript code
• Articles with example Lisp (programming language) code
• Articles with example OCaml code