Editing Fixed-point combinator (section)

==Fixed-point combinators in lambda calculus==

The Y combinator, discovered by [[Haskell Curry]], is defined as
: <math>Y = \lambda f.(\lambda x.f\ (x\ x)) \ (\lambda x.f\ (x\ x))</math>

===Other fixed-point combinators===

In untyped lambda calculus fixed-point combinators are not especially rare. In fact there are infinitely many of them.<ref name="bimbo">{{cite book |last1=Bimbó |first1=Katalin |author1-link= Katalin Bimbó |date=27 July 2011 |title=Combinatory Logic: Pure, Applied and Typed |page=48 |publisher=CRC Press |isbn=9781439800010 |url=https://books.google.com/books?id=iQjMBQAAQBAJ&q=%22fixed-point+combinator%22}}</ref> In 2005 Mayer Goldberg showed that the set of fixed-point combinators of untyped lambda calculus is [[recursively enumerable]].<ref name=gold>Goldberg, 2005</ref>

The Y combinator can be expressed in the [[SKI combinator calculus#Self-application and recursion|SKI-calculus]] as
: <math>\mathsf{Y = S (K (S I I)) (S (S (K S) K) (K (S I I))) = S S I (S (S (K S) K) (K (S I I)))}</math>

Additional combinators ([[B, C, K, W system]]) allow for much shorter encodings. With <math>\mathsf{U = SII}</math> the self-application combinator, since <math>\mathsf S(\mathsf Kx)yz = x(yz) = \mathsf Bxyz</math> and <math>\mathsf Sx(\mathsf Ky)z = xzy = \mathsf Cxyz</math>, the above becomes
: <math>\mathsf{Y = S (K U) (S B (K U)) = B U (C B U)} \ \ \ ; \ \ \mathsf{Y = S S I (B W B)} </math>

The shortest fixed-point combinator in the SK-calculus using S and K combinators only, found by [[John Tromp]], is
: <math>\mathsf{Y' = S S K (S (K (S S (S (S S K)))) K) = W C (S B (C (W C)))} </math>

although note that it is not in normal form, which is longer. This combinator corresponds to the lambda expression
: <math>\mathsf Y' = (\lambda x y. x y x) (\lambda y x. y (x y x))</math>

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:
: <math>\mathsf X = \lambda f.(\lambda x.x x) (\lambda x.f (x x)) \ \ \ ; \ \ \mathsf{X f = U (B f U)} </math>

Another common fixed-point combinator is the Turing fixed-point combinator (named after its discoverer, [[Alan Turing]]):<ref>{{cite journal |jstor=2268281 |author=Alan Mathison Turing |title=The <math>p</math>-function in <math>\lambda</math>-<math>K</math>-conversion |journal=[[Journal of Symbolic Logic]] |volume=2 |number=4 |pages=164 |date=December 1937}}</ref><ref name="Barendregt.1985"/>{{rp|132}}
: <math>\Theta = (\lambda x y. y (x x y))\ (\lambda x y. y (x x y)) = \mathsf{S I I (S (K (S I)) (S I I)) = U (B (S I) U)} </math>

Its advantage over <math>\mathsf Y</math> is that <math>\Theta\ f</math> beta-reduces to <math>f\ (\Theta f)</math>,<ref group="note">
{{tmath|\Theta\ f}} {{tmath|\equiv}} {{tmath|(\lambda xy.y(xxy))\ (\lambda xy.y(xxy))\ f}} {{tmath|\to}} {{tmath|( \lambda y.y\ ((\lambda xy.y(xxy))\ (\lambda xy.y(xxy))\ y) )\ f}} {{tmath|\to}} {{tmath|f\ ((\lambda xy.y(xxy))\ (\lambda xy.y(xxy))\ f)}} {{tmath|\equiv}} {{tmath|f\ (\Theta\ f)}}
</ref>
whereas <math>\mathsf Y\ f</math> and <math>f\ (\mathsf Y f)</math> only beta-reduce to a common term.

<math>\Theta</math> also has a simple call-by-value form:
: <math>\Theta_{v} = (\lambda x y. y (\lambda z. x x y z))\ (\lambda x y. y (\lambda z. x x y z))</math>

The analog for [[mutual recursion]] is a ''polyvariadic fix-point combinator'',<ref>{{cite web |url=http://okmij.org/ftp/Computation/fixed-point-combinators.html#Poly-variadic |title=Many faces of the fixed-point combinator |website=okmij.org}}</ref><ref>[http://osdir.com/ml/lang.haskell.cafe/2003-10/msg00211.html Polyvariadic Y in pure Haskell98] {{webarchive|url=https://web.archive.org/web/20160304101809/http://osdir.com/ml/lang.haskell.cafe/2003-10/msg00211.html |date=2016-03-04}}, lang.haskell.cafe, October 28, 2003</ref><ref>{{cite web |url=https://stackoverflow.com/questions/4899113/fixed-point-combinator-for-mutually-recursive-functions |title=recursion - Fixed-point combinator for mutually recursive functions? |website=Stack Overflow}}</ref> which may be denoted Y*.

===<span class="anchor" id="Z combinator"></span>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]].<ref>{{cite web |last1=Bene |first1=Adam |date=17 August 2017 |title=Fixed-Point Combinators in JavaScript |url=https://blog.benestudio.co/fixed-point-combinators-in-javascript-c214c15ff2f6 |website=Bene Studio |publisher=Medium |access-date=2 August 2020 |language=en}}</ref> The Z combinator will work in [[Strict programming language|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 <math>Z g</math> in the right-hand side of the definition:<ref>{{cite web |title=CS 6110 S17 Lecture 5. Recursion and Fixed-Point Combinators |url=https://www.cs.cornell.edu/courses/cs6110/2017sp/lectures/lec05.pdf |website=Cornell University |at=4.1 A CBV Fixed-Point Combinator}}</ref>
: <math>Z g v = g (Z g) v\ .</math>

and in lambda calculus it is an [[Eta expansion|eta-expansion]] of the ''Y'' combinator:
: <math>Z = \lambda f.(\lambda x.f (\lambda v.x x v)) \ (\lambda x.f (\lambda v.x x v))\ .</math>

=== Non-standard fixed-point combinators ===

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

:<math>\mathsf F=\lambda x. F x = \lambda x. x (F x)= \lambda x. x (x (F x)) = \cdots </math>

Terms that have the same [[Böhm tree]] as a fixed-point combinator, i.e., have the same infinite extension <math>\lambda x.x (x (x \cdots ))</math>, 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 fixed-point equation that defines the "standard" ones. These combinators are called ''strictly non-standard fixed-point combinators''; an example is the following combinator:
: <math>\mathsf{N = B U (B (B U) B)}</math>
where
: <math>\mathsf B = \lambda x y z.x (y z)</math>
: <math>\mathsf U = \lambda x.x x\ </math>
since
<!-- Ng = (U . (U .) . (.)) g
             = (U . (g .)) (U . (g .)) = 
             =  U (  g .    U . (g .))
             =       g (    U ( (g . g . U . (g .)) ))
             =       g          (g ( g ( U (  g .  g . g . U . (g .) ))))
 -->
:<math>\mathsf N=\lambda x. N x = \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 </math>
where <math>\mathsf N_i</math> are modifications of <math>\mathsf N</math> created on the fly which add <math>i</math> instances of <math>x</math> at once into the chain while being replaced with <math>\mathsf N_{i+1}</math>.

The set of non-standard fixed-point combinators is not [[recursively enumerable]].<ref name=gold/>