https://en.wikipedia.org/wiki/Fixed-point_combinator Jump to content [ ] Main menu Main menu move to sidebar hide Navigation * Main page * Contents * Current events * Random article * About Wikipedia * Contact us * Donate Contribute * Help * Learn to edit * Community portal * Recent changes * Upload file Languages Language links are at the top of the page. [wikipe] Wikipedia The Free Encyclopedia Search [ ] Search * Create account * Log in [ ] Personal tools * Create account * Log in Pages for logged out editors learn more * Contributions * Talk Contents move to sidebar hide * (Top) * 1Y combinator in lambda calculus Toggle Y combinator in lambda calculus subsection + 1.1Verification + 1.2Uses + 1.3Example implementations * 2Fixed-point combinator Toggle Fixed-point combinator subsection + 2.1Values and domains + 2.2Function versus implementation + 2.3Definition of the term "combinator" * 3Recursive definitions and fixed-point combinators Toggle Recursive definitions and fixed-point combinators subsection + 3.1The factorial function * 4Fixed-point combinators in lambda calculus Toggle Fixed-point combinators in lambda calculus subsection + 4.1Other fixed-point combinators + 4.2Strict fixed-point combinator + 4.3Non-standard fixed-point combinators * 5Implementation in other languages Toggle Implementation in other languages subsection + 5.1Lazy functional implementation + 5.2Strict functional implementation + 5.3Imperative language implementation * 6Typing Toggle Typing subsection + 6.1Type for the Y combinator * 7General information * 8See also * 9Notes * 10References * 11External links [ ] Toggle the table of contents Fixed-point combinator [ ] 7 languages * Deutsch * Eesti * Ri Ben Yu * Polski * Portugues * Russkii * Zhong Wen Edit links * Article * Talk [ ] English * Read * Edit * View history [ ] Tools Tools move to sidebar hide Actions * Read * Edit * View history General * What links here * Related changes * Upload file * Special pages * Permanent link * Page information * Cite this page * Get shortened URL * Download QR code * Wikidata item Print/export * Download as PDF * Printable version From Wikipedia, the free encyclopedia Higher-order function Y for which Y f = f (Y f) 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 f i x {\displaystyle fix} {\displaystyle fix} is a fixed-point combinator and the function f {\displaystyle f} {\ displaystyle f} has one or more fixed points, then f i x f {\ displaystyle fixf} {\displaystyle fixf} is one of these fixed points, i.e. f ( f i x f ) = f i x f . {\displaystyle f\ (fix\ f)=fix\ f\ .} {\displaystyle f\ (fix\ f)=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[edit] In the classical untyped lambda calculus, every function has a fixed point. A particular implementation of f i x {\displaystyle fix} {\ displaystyle fix} is Haskell Curry's paradoxical combinator Y, represented by^[2]^: 131 ^[note 1] Y = l f . ( l x . f ( x x ) ) ( l x . f ( x x ) ) {\ displaystyle Y=\lambda f.\ (\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))} {\displaystyle Y=\lambda f.\ (\lambda x.f\ (x\ x))\ (\ lambda x.f\ (x\ x))} Verification[edit] The following calculation verifies that Y g {\displaystyle Yg} {\ displaystyle Yg} is indeed a fixed point of the function g {\ displaystyle g} {\displaystyle g}: = ( l f . ( l x . f ( x Y g x ) ) ( l x . f ( x x {\ ) ) ) g {\displaystyle = displaystyle \ (\lambda f.(\lambda x.f\ (x by definition of Y {\ \ \ \ Y\ g\ } \ x))\ (\lambda x.f\ (x\ displaystyle Y} {\ {\displaystyle x)))\ g} {\displaystyle =(\ displaystyle Y} \ \ \ \ Y\ g\ lambda f.(\lambda x.f\ (x\ } x))\ (\lambda x.f\ (x\ x))) \ g} = ( l x . g ( x x ) ) ( l x . g ( x x ) ) {\ displaystyle =(\lambda x.g\ by b-reduction: replacing (x\ x))\ (\lambda x.g\ (x\ the formal argument f of Y x))} {\displaystyle =(\ with the actual argument g lambda x.g\ (x\ x))\ (\ lambda x.g\ (x\ x))} = g ( ( l x . g ( x x by b-reduction: replacing ) ) ( l x . g ( x x ) the formal argument x of ) ) {\displaystyle =g\ ((\ the first function with lambda x.g\ (x\ x))\ (\ the actual argument ( l x lambda x.g\ (x\ x)))} {\ . g ( x x ) ) {\ displaystyle =g\ ((\lambda displaystyle (\lambda x.g\ x.g\ (x\ x))\ (\lambda x.g\ (x\ x))} {\displaystyle (\ (x\ x)))} lambda x.g\ (x\ x))} = g ( Y g ) {\ displaystyle =g\ (Y\ g)} {\ by second equality, above displaystyle =g\ (Y\ g)} The lambda term g ( Y g ) {\displaystyle g\ (Y\ g)} {\ displaystyle g\ (Y\ g)} may not, in general, b-reduce to the term Y g {\displaystyle Y\ g} {\displaystyle Y\ g}. However, both terms b-reduce to the same term, as shown. Uses[edit] 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. In the lambda calculus, it is not possible to refer to the definition of a function inside its own body by name. Recursion though may be achieved by obtaining the same function passed in as an argument, and then using that argument to make the recursive call, instead of using the function's own name, as is done in languages which do support recursion natively. 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[edit] An example implementation of 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++ int main() { auto Y = [](auto f) { auto f1 = [f](auto x) -> decltype(f) { // A print statement may be inserted here, // to observe that we get an infinite loop // (at least until the stack overflows) return f(x(x)); }; return f1(f1); }; Y(Y); } Fixed-point combinator[edit] 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 lambda calculus 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[edit] Many functions do not have any fixed points, for instance f : N - N {\displaystyle f:\mathbb {N} \to \mathbb {N} } {\displaystyle f:\ mathbb {N} \to \mathbb {N} } with f ( n ) = n + 1 {\displaystyle f(n) =n+1} {\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[edit] 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"[edit] 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[edit] 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[edit] 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 fact [?] n = { 1 if n = 0 n x fact [?] ( n - 1 ) otherwise. {\ displaystyle \operatorname {fact} \ n={\begin{cases}1&{\text{if}} ~n=0\\n\times \operatorname {fact} (n-1)&{\text{otherwise.}}\end {cases}}} {\displaystyle \operatorname {fact} \ n={\begin{cases}1 &{\text{if}}~n=0\\n\times \operatorname {fact} (n-1)&{\text {otherwise.}}\end{cases}}} where n is a non-negative integer. If we want to implement this in lambda calculus, where integers are represented using Church encoding , we run into the problem that the lambda calculus does not allow the name of a function ('fact') to be used in the function's definition. This can be circumvented using a fixed-point combinator fix {\ displaystyle {\textsf {fix}}} {\displaystyle {\textsf {fix}}} as follows. Define a function F of two arguments f and n: F f n = ( IsZero [?] n ) 1 ( multiply [?] n ( f ( pred [?] n ) ) ) {\displaystyle F\ f\ n=(\operatorname {IsZero} \ n)\ 1\ (\operatorname {multiply} \ n\ (f\ (\operatorname {pred} \ n)))} {\displaystyle F\ f\ n=(\operatorname {IsZero} \ n)\ 1\ (\ operatorname {multiply} \ n\ (f\ (\operatorname {pred} \ n)))} (Here ( IsZero [?] n ) {\displaystyle (\operatorname {IsZero} \ n)} {\displaystyle (\operatorname {IsZero} \ n)} is a function that takes two arguments and returns its first argument if n=0, and its second argument otherwise; pred [?] n {\displaystyle \operatorname {pred} \ n} {\displaystyle \operatorname {pred} \ n} evaluates to n-1.) Now define fact = fix F {\displaystyle \operatorname {fact} ={\ textsf {fix}}\ F} {\displaystyle \operatorname {fact} ={\textsf {fix}}\ F}. Then fact {\displaystyle \operatorname {fact} } {\ displaystyle \operatorname {fact} } is a fixed-point of F, which gives fact [?] n = F fact [?] n = ( IsZero [?] n ) 1 ( multiply [?] n ( fact [?] ( pred [?] n ) ) ) {\displaystyle {\begin {aligned}\operatorname {fact} n&=F\ \operatorname {fact} \ n\\&= (\operatorname {IsZero} \ n)\ 1\ (\operatorname {multiply} \ n\ (\operatorname {fact} \ (\operatorname {pred} \ n)))\ \end {aligned}}} {\displaystyle {\begin{aligned}\operatorname {fact} n &=F\ \operatorname {fact} \ n\\&=(\operatorname {IsZero} \ n)\ 1\ (\operatorname {multiply} \ n\ (\operatorname {fact} \ (\ operatorname {pred} \ n)))\ \end{aligned}}} as desired. Fixed-point combinators in lambda calculus[edit] The Y combinator, discovered by Haskell B. Curry, is defined as Y = l f . ( l x . f ( x x ) ) ( l x . f ( x x ) ) {\ displaystyle Y=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))} {\displaystyle Y=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))} Other fixed-point combinators[edit] 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 is recursively enumerable.^[6] The Y combinator can be expressed in the SKI-calculus as Y = S ( K ( S I I ) ) ( S ( S ( K S ) K ) ( K ( S I I ) ) ) {\ displaystyle Y=S(K(SII))(S(S(KS)K)(K(SII)))} {\displaystyle Y=S(K (SII))(S(S(KS)K)(K(SII)))} Additional combinators (B, C, K, W system) allow for a much shorter definition. With U = SII the self-application combinator, since S(Kx) yz = x(yz) = Bxyz and Sx(Ky)z = xzy = Cxyz, the above becomes Y = S ( K U ) ( S B ( K U ) ) = B U ( C B U ) {\displaystyle Y=S (KU)(SB(KU))=BU(CBU)} {\displaystyle Y=S(KU)(SB(KU))=BU(CBU)} The simplest fixed-point combinator in the SK-calculus, found by John Tromp, is Y ' = S S K ( S ( K ( S S ( S ( S S K ) ) ) ) K ) {\displaystyle Y'=SSK(S(K(SS(S(SSK))))K)} {\displaystyle Y'=SSK(S(K(SS(S(SSK)))) K)} although note that it is not in normal form, which is longer. This combinator corresponds to the lambda expression Y ' = ( l x y . x y x ) ( l y x . y ( x y x ) ) {\displaystyle Y' =(\lambda xy.xyx)(\lambda yx.y(xyx))} {\displaystyle Y'=(\lambda xy.xyx)(\lambda yx.y(xyx))} The following fixed-point combinator is simpler than the Y combinator, and b-reduces into the Y combinator; it is sometimes cited as the Y combinator itself: X = l f . ( l x . x x ) ( l x . f ( x x ) ) {\displaystyle X=\ lambda f.(\lambda x.xx)(\lambda x.f(xx))} {\displaystyle X=\ lambda f.(\lambda x.xx)(\lambda x.f(xx))} Another common fixed-point combinator is the Turing fixed-point combinator (named after its discoverer, Alan Turing):^[7]^[2]^: 132 Th = ( l x y . y ( x x y ) ) ( l x y . y ( x x y ) ) {\ displaystyle \Theta =(\lambda xy.y(xxy))\ (\lambda xy.y(xxy))} {\ displaystyle \Theta =(\lambda xy.y(xxy))\ (\lambda xy.y(xxy))} Its advantage over Y {\displaystyle Y} {\displaystyle Y} is that Th f {\displaystyle \Theta \ f} {\displaystyle \Theta \ f} beta-reduces to f ( Th f ) {\displaystyle f\ (\Theta f)} {\displaystyle f\ (\ Theta f)},^[note 2] whereas Y f {\displaystyle Y\ f} {\displaystyle Y\ f} and f ( Y f ) {\displaystyle f\ (Yf)} {\displaystyle f\ (Yf)} only beta-reduce to a common term. Th {\displaystyle \Theta } {\displaystyle \Theta } also has a simple call-by-value form: Th v = ( l x y . y ( l z . x x y z ) ) ( l x y . y ( l z . x x y z ) ) {\displaystyle \Theta _{v}=(\lambda xy.y(\lambda z.xxyz))\ (\lambda xy.y(\lambda z.xxyz))} {\displaystyle \Theta _{v}=(\ lambda xy.y(\lambda z.xxyz))\ (\lambda xy.y(\lambda z.xxyz))} The analog for mutual recursion is a polyvariadic fix-point combinator,^[8]^[9]^[10] which may be denoted Y*. Strict fixed-point combinator[edit] In a strict programming language the Y combinator will expand until stack overflow, or never halt in case of tail call optimization.^[11] 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 Z g in the right-hand side of the definition:^[12] Z g v = g ( Z g ) v . {\displaystyle Zgv=g(Zg)v\ .} {\ displaystyle Zgv=g(Zg)v\ .} and in lambda calculus it is an eta-expansion of the Y combinator: Z = l f . ( l x . f ( l v . x x v ) ) ( l x . f ( l v . x x v ) ) . {\displaystyle Z=\lambda f.(\lambda x.f(\lambda v.xxv))\ (\ lambda x.f(\lambda v.xxv))\ .} {\displaystyle Z=\lambda f.(\ lambda x.f(\lambda v.xxv))\ (\lambda x.f(\lambda v.xxv))\ .} Non-standard fixed-point combinators[edit] In untyped lambda calculus there are terms that have the same Bohm tree as a fixed-point combinator, that is they have the same infinite extension lx.x (x (x ... )). These are called non-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 equation that defines the "standard" ones. These strange combinators are called strictly non-standard fixed-point combinators; an example is the following combinator: N = B M ( B ( B M ) B ) {\displaystyle N=BM(B(BM)B)} {\ displaystyle N=BM(B(BM)B)} where B = l x y z . x ( y z ) {\displaystyle B=\lambda xyz.x(yz)} {\ displaystyle B=\lambda xyz.x(yz)} M = l x . x x . {\displaystyle M=\lambda x.xx\ .} {\ displaystyle M=\lambda x.xx\ .} The set of non-standard fixed-point combinators is not recursively enumerable.^[6] Implementation in other languages[edit] (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 some programming paradigms are given below. Lazy functional implementation[edit] In a language that supports lazy evaluation, like in Haskell, it is possible to define a fixed-point combinator using the defining equation of the fixed-point combinator which is conventionally named fix. Since Haskell has lazy datatypes, 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) -> a fix f = let x = f x in x -- Lambda dropped. Sharing. -- Original definition in Data.Function. -- alternative: fix' f = f (fix' f) -- Lambda lifted. Non-sharing. fix (\x -> 9) -- this evaluates to 9 fix (\x -> 3:x) -- evaluates to the lazy infinite list [3,3,3,...] fact = fix fac -- evaluates to the factorial function where fac f 0 = 1 fac f x = x * f (x-1) fact 5 -- evaluates to 120 Strict functional implementation[edit] In a strict functional language, as illustrated below with OCaml, the argument to f is expanded beforehand, yielding an infinite call sequence, f ( f . . . ( f ( f i x f ) ) . . . ) x {\displaystyle f\ (f...(f\ ({\mathsf {fix}}\ f))...)\ x} {\displaystyle f\ (f...(f\ ({\mathsf {fix}}\ f))...)\ x}. This may be resolved by defining fix with an extra parameter. let rec fix f x = f (fix f) x (* note the extra x; here fix f = \x-> f (fix f) x *) let factabs fact = function (* factabs has extra level of lambda abstraction *) 0 -> 1 | x -> x * fact (x-1) let _ = (fix factabs) 5 (* evaluates to "120" *) In a multi-paradigm functional language (one decorated with imperative features), such as Lisp, Landin (1963)^[full citation needed] suggests the use of a variable assignment to create a fixed-point combinator, as in the below example using Scheme: (define Y! (lambda (f) ((lambda (i) (set! i (f (lambda (x) (i x)))) ;; (set! i expr) assigns i the value of expr i) ;; replacing it in the present lexical scope #f))) Using a lambda calculus with axioms for assignment statements, it can be shown that Y! satisfies the same fixed-point law as the call-by-value Y combinator:^[14]^[15] ( Y ! l x . e ) e ' = ( l x . e ) ( Y ! l x . e ) e ' {\ displaystyle (Y_{!}\ \lambda x.e)e'=(\lambda x.e)\ (Y_{!}\ \ lambda x.e)e'} {\displaystyle (Y_{!}\ \lambda x.e)e'=(\lambda x.e)\ (Y_{!}\ \lambda x.e)e'} In more idiomatic modern Lisp usage, this would typically be handled via a lexically scoped label (a let expression), as lexical scope was not introduced to Lisp until the 1970s: (define Y* (lambda (f) ((lambda (i) (let ((i (f (lambda (x) (i x))))) ;; (let ((i expr)) i) locally defines i as expr i)) ;; non-recursively: thus i in expr is not expr #f))) Or without the internal label: (define Y (lambda (f) ((lambda (i) (i i)) (lambda (i) (f (lambda (x) (apply (i i) x))))))) Imperative language implementation[edit] This example is a slightly interpretive implementation of a fixed-point combinator. A class is used to contain the fix function, called fixer. The function to be fixed is contained in a class that inherits from fixer. The fix function accesses the function to be fixed as a virtual function. As for the strict functional definition, fix is explicitly given an extra parameter x, which means that lazy evaluation is not needed. template class fixer { public: R fix(D x) { return f(x); } private: virtual R f(D) = 0; }; class fact : public fixer { virtual long f(long x) { if (x == 0) { return 1; } return x * fix(x-1); } }; long result = fact().fix(5); Typing[edit] In System F (polymorphic lambda calculus) a polymorphic fixed-point combinator has type^[citation needed]; [?]a.(a - a) - a where a is a type variable. That is, fix takes a function, which maps a - a and uses it to return a value of type a. In the simply typed lambda calculus extended with recursive 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 the simply typed lambda calculus, the fixed-point combinator Y cannot be assigned a type^[16] because at some point it would deal with the self-application sub-term x x {\displaystyle x~x} {\ displaystyle x~x} by the application rule: G [?] x : t 1 - t 2 G [?] x : t 1 G [?] x x : t 2 {\displaystyle {\ Gamma \vdash x\!:\!t_{1}\to t_{2}\quad \Gamma \vdash x\!:\!t_{1}} \over {\Gamma \vdash x~x\!:\!t_{2}}} {\displaystyle {\Gamma \ vdash x\!:\!t_{1}\to t_{2}\quad \Gamma \vdash x\!:\!t_{1}} \over {\Gamma \vdash x~x\!:\!t_{2}}} where x {\displaystyle x} {\displaystyle x} has the infinite type t 1 = t 1 - t 2 {\displaystyle t_{1}=t_{1}\to t_{2}} {\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. Type for the Y combinator[edit] In programming languages that support recursive data types, it is possible to type the Y combinator by appropriately accounting for the recursion at the type level. The need to self-apply 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:^[17]^ [18] 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)) Alternatively: let y f = (fun x -> f (fun z -> out x x z)) (In (fun x -> f (fun z -> out x x z))) General information[edit] 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 in fixed-point iteration, iterative methods, recursive join in relational databases, data-flow analysis, FIRST and FOLLOW sets of non-terminals in a context-free grammar, transitive closure, and other types of closure operations. A function for which every input is a fixed point is called an identity function. Formally: [?] x ( f x = x ) {\displaystyle \forall x(f\ x=x)} {\ displaystyle \forall x(f\ x=x)} In contrast to universal quantification over all x {\displaystyle x} {\displaystyle x}, a fixed-point combinator constructs one value that is a fixed point of f {\displaystyle f} {\displaystyle f}. The remarkable property of a fixed-point combinator is that it constructs a fixed point for an arbitrary given function f {\displaystyle f} {\ displaystyle f}. Other functions have the special property that, after being applied once, further applications don't have any effect. More formally: [?] x ( f ( f x ) = f x ) {\displaystyle \forall x(f\ (f\ x)= f\ x)} {\displaystyle \forall x(f\ (f\ x)=f\ x)} Such functions are called idempotent (see also Projection (mathematics)). An example of such a function is the function that returns 0 for all even integers, and 1 for all odd integers. In lambda 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, we obtain ( Y l x . x ) = ( l x . ( x x ) l x . ( x x ) ) {\ displaystyle (Y\ \lambda x.x)=(\lambda x.(xx)\ \lambda x.(xx))} {\displaystyle (Y\ \lambda x.x)=(\lambda x.(xx)\ \lambda 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 in simply typed lambda calculus. The Y combinator allows recursion to be defined as a set of rewrite rules,^[19] without requiring native recursion support in the language.^[20] In programming languages that support anonymous functions, fixed-point 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 fixed-point combinators is sometimes called anonymous recursion.^[note 3]^[21] See also[edit] * Anonymous function * Fixed-point iteration * Lambda calculus#Recursion and fixed points * Lambda lifting * Let expression Notes[edit] 1. ^ Throughout this article, the syntax rules given in Lambda calculus#Notation are used, to save parentheses. 2. ^ Th f {\displaystyle \Theta \ f} {\displaystyle \Theta \ f} [?] {\displaystyle \equiv } {\displaystyle \equiv } ( l x y . y ( x x y ) ) ( l x y . y ( x x y ) ) f {\displaystyle (\lambda xy.y (xxy))\ (\lambda xy.y(xxy))\ f} {\displaystyle (\lambda xy.y (xxy))\ (\lambda xy.y(xxy))\ f} - {\displaystyle \to } {\ displaystyle \to } ( l y . y ( ( l x y . y ( x x y ) ) ( l x y . y ( x x y ) ) y ) ) f {\displaystyle (\lambda y.y\ ((\ lambda xy.y(xxy))\ (\lambda xy.y(xxy))\ y))\ f} {\displaystyle (\ lambda y.y\ ((\lambda xy.y(xxy))\ (\lambda xy.y(xxy))\ y))\ f} - {\displaystyle \to } {\displaystyle \to } f ( ( l x y . y ( x x y ) ) ( l x y . y ( x x y ) ) f ) {\displaystyle f\ ((\lambda xy.y(xxy))\ (\lambda xy.y(xxy))\ f)} {\displaystyle f\ ((\lambda xy.y(xxy))\ (\lambda xy.y(xxy))\ f)} [?] {\displaystyle \equiv } {\ displaystyle \equiv } f ( Th f ) {\displaystyle f\ (\Theta \ f)} {\displaystyle f\ (\Theta \ f)} 3. ^ This terminology appears to be largely folklore, but it does appear in the following: + Trey Nash, Accelerated C# 2008, Apress, 2007, ISBN 1-59059-873-3, 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. References[edit] 1. ^ ^a ^b Peyton Jones, Simon L. (1987). The Implementation of Functional Programming (PDF). Prentice Hall International. 2. ^ ^a ^b Henk Barendregt (1985). The Lambda Calculus - Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. Vol. 103. Amsterdam: North-Holland. ISBN 0444867481. 3. ^ Selinger, Peter. "Lecture Notes on Lambda Calculus (PDF)". p. 6. 4. ^ "For those of us who don't know what a Y-Combinator is or why it's useful, ..." Hacker News. Retrieved 2 August 2020. 5. ^ Bimbo, Katalin (27 July 2011). Combinatory Logic: Pure, Applied and Typed. CRC Press. p. 48. ISBN 9781439800010. 6. ^ ^a ^b Goldberg, 2005 7. ^ Alan Mathison Turing (December 1937). "The p {\displaystyle p} {\displaystyle p}-function in l {\displaystyle \lambda } {\ displaystyle \lambda }- K {\displaystyle K} {\displaystyle K} -conversion". Journal of Symbolic Logic. 2 (4): 164. JSTOR 2268281. 8. ^ "Many faces of the fixed-point combinator". okmij.org. 9. ^ Polyvariadic Y in pure Haskell98 Archived 2016-03-04 at the Wayback Machine, lang.haskell.cafe, October 28, 2003 10. ^ "recursion - Fixed-point combinator for mutually recursive functions?". Stack Overflow. 11. ^ Bene, Adam (17 August 2017). "Fixed-Point Combinators in JavaScript". Bene Studio. Medium. Retrieved 2 August 2020. 12. ^ "CS 6110 S17 Lecture 5. Recursion and Fixed-Point Combinators" (PDF). Cornell University. 4.1 A CBV Fixed-Point Combinator. 13. ^ The original definition in Data.Function. 14. ^ Felleisen, Matthias (1987). The Lambda-v-CS Calculus. Indiana University. 15. ^ Talcott, Carolyn (1985). The Essence of Rum: A theory of the intensional and extensional aspects of Lisp-type computation (Ph.D. thesis). Stanford University. 16. ^ An Introduction to the Lambda Calculus Archived 2014-04-08 at the Wayback Machine 17. ^ Haskell mailing list thread on How to define Y combinator in Haskell, 15 Sep 2006 18. ^ Geuvers, Herman; Verkoelen, Joep. On Fixed point and Looping Combinators in Type Theory. CiteSeerX 10.1.1.158.1478. 19. ^ Daniel P. Friedman, Matthias Felleisen (1986). "Chapter 9 - Lambda The Ultimate". The Little Lisper. Science Research Associates. p. 179. "In the chapter we have derived a Y-combinator which allows us to write recursive functions of one argument without using define." 20. ^ Mike Vanier. "The Y Combinator (Slight Return) or: How to Succeed at Recursion Without Really Recursing". Archived from the original on 2011-08-22. "More generally, Y gives us a way to get recursion in a programming language that supports first-class functions but that doesn't have recursion built in to it." 21. ^ The If Works Deriving the Y combinator, January 10th, 2008 * 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 the Why of Y. External links[edit] [40px] 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 Combinator * "A Use of the Y Combinator in Ruby" * "Functional programming in Ada" * Rosetta code - Y combinator * Retrieved from "https://en.wikipedia.org/w/index.php?title= Fixed-point_combinator&oldid=1209870354" Categories: * Combinatory logic * Fixed points (mathematics) * Lambda calculus * Mathematics of computing * Recursion Hidden categories: * Webarchive template wayback links * Articles with short description * Short description matches Wikidata * All articles with incomplete citations * Articles with incomplete citations from December 2019 * All articles with unsourced statements * Articles with unsourced statements from August 2019 * This page was last edited on 23 February 2024, at 23:00 (UTC). * Text is available under the Creative Commons Attribution-ShareAlike License 4.0 ; additional terms may apply. By using this site, you agree to the Terms of Use and Privacy Policy. Wikipedia(r) is a registered trademark of the Wikimedia Foundation, Inc., a non-profit organization. * Privacy policy * About Wikipedia * Disclaimers * Contact Wikipedia * Code of Conduct * Developers * Statistics * Cookie statement * Mobile view * Wikimedia Foundation * Powered by MediaWiki * Toggle limited content width