Editing SKI combinator calculus (section)

===Self-application and recursion===
'''SII''' is an expression that takes an argument and applies that argument to itself:
: '''SII'''α = '''I'''α('''I'''α) = αα

This is also known as '''U''' combinator, '''U'''''x'' = ''xx''. One interesting property of it is that its self-application is irreducible:
: '''SII'''('''SII''') = '''I'''('''SII''')('''I'''('''SII''')) = '''SII'''('''I'''('''SII''')) = '''SII'''('''SII''')
Or, using the equation as its definition directly, we immediately get '''U''' '''U''' = '''U''' '''U'''.

Another thing is that it allows one to write a function that applies one thing to the self application of another thing:
: ('''S'''('''K'''α)('''SII'''))β = '''K'''αβ('''SII'''β) = α('''I'''β('''I'''β)) = α(ββ)
or it can be seen as defining yet another combinator directly, '''H'''''xy'' = ''x''(''yy'').

This function can be used to achieve [[recursion]].  If β is the function that applies α to the self application of something else, 
: β = '''H'''α = '''S'''('''K'''α)('''SII''')
then the self-application of this β is the fixed point of that α:
: '''SII'''β = ββ = α(ββ) = α(α(ββ)) = <math>\ldots</math>
Or, directly again from the derived definition, '''H'''α('''H'''α) = α('''H'''α('''H'''α)).

If α expresses a "computational step" computed by αρν for some ρ and ν, that assumes ρν' expresses "the rest of the computation" (for some ν' that α will "compute" from ν), then its fixed point ββ expresses the whole recursive computation, since using ''the same function'' ββ for the "rest of computation" call (with ββν = α(ββ)ν) is the very definition of recursion: ρν' = ββν' = α(ββ)ν' = ... . α will have to employ some kind of conditional to stop at some "base case" and not make the recursive call then, to avoid divergence.

This can be formalized, with
: β = '''H'''α = '''S'''('''K'''α)('''SII''') = '''S'''('''KS''')'''K'''α('''SII''') = '''S'''('''S'''('''KS''')'''K''')('''K'''('''SII''')) α
as
: '''Y'''α = '''SII'''β = '''SII'''('''H'''α) = '''S'''('''K'''('''SII'''))'''H''' α = '''S'''('''K'''('''SII'''))('''S'''('''S'''('''KS''')'''K''')('''K'''('''SII'''))) α
which gives us [[Fixed-point_combinator#Other_fixed-point_combinators|one possible encoding]] of the '''Y''' combinator. A shorter variation replaces its two leading subterms with just '''SSI''', since '''H'''α('''H'''α) = '''SHH'''α = '''SSIH'''α.

This becomes much shorter with the use of the [[B, C, K, W system|'''B,C,W''' combinators]], as [[B, C, K, W system#Connection_to_other_combinators|the equivalent]]

: '''Y'''α = '''S'''('''KU''')('''SB'''('''KU'''))α = '''U'''('''B'''α'''U''') = '''BU'''('''CBU''')α = '''SSI'''('''CBU''')α

<!-- or, directly using the '''H''' combinator definition,

: '''H'''gx = g(xx) = '''B'''g'''U'''x = '''CBU'''gx = '''SB(KU)'''gx , or '''B'''gxx = '''W'''('''B'''g)x = '''BWB'''gx = '''S(KW)B'''gx 
: '''Y'''g = '''H'''g('''H'''g) = '''U'''('''H'''g) = '''BUH'''g, or '''SHH'''g = '''WSH'''g = '''SSIH'''g  -->
<!--
Yα = S(K(SII))(S(S(KS)K)(K(SII))) α = SSI(S(S(KS)K)(K(SII))) α
Yα = S(KU)(SB(KU))α = U(BαU) = BU(CBU)α = SSI(CBU)α = SSI(BWB) α
-->
And with a pseudo-[[Haskell (programming language)|Haskell]] syntax it becomes the exceptionally short '''Y''' = '''U''' . (. '''U''').

Following this approach, other fixpoint combinator definitions are possible. Thus,

* This '''Y''', by [[Haskell Curry]]:
: '''H'''''gx'' = ''g''(''xx'') ; '''Y'''''g'' = '''H'''''g''('''H'''''g'') ; '''Y = SSI(SB(KU)) = SSI(S(S(KS)K)(K(SII)))'''
* Turing's '''Θ''':
: '''H'''''hg'' = ''g''(''hhg'') ; '''Θ'''''g'' = '''HH'''''g'' ; '''Θ = U(B(SI)U) = SII(S(K(SI))(SII))'''
* '''Y'''' (with SK-encoding by [[John Tromp]]<ref>https://tromp.github.io/</ref>):
: '''H'''''gh'' = ''g''(''hgh'') ; '''Y''''''g'' = '''H'''''g'''''H''' ; '''Y' = WC(SB(C(WC))) = SSK(S(K(SS(S(SSK))))K)'''
* '''Θ₄''' by R.Statman:<ref>{{cite journal|first1=William McCune|last1=Larry Wos|author1-link=|title=Searching for Fixed Point Combinators by Using Automated Theorem Proving: A Preliminary Report|website=Argonne National Laboratory|date=September 1988|url=https://inis.iaea.org/collection/NCLCollectionStore/_Public/20/016/20016944.pdf|editor1-first=|editor1-last=|edition=|access-date=December 12, 2024}}, p.9</ref>
: '''H'''''gyz'' = ''g''(''yyz'') ; '''Θ₄'''''g'' = '''H'''''g''('''H'''''g'')('''H'''''g'') ; '''Θ₄ = B(WW)(BW(BBB))'''
* or in general,
: '''H'''''something'' = ''g''(''hsomething'') ; '''Y'''<sub><sub>H</sub></sub>&thinsp;''g'' = '''H'''_____'''H'''__&thinsp;''g''
:  (where anything goes instead of "_") or any other intermediary '''H''' combinator's definition, with its correspondent '''Y''' definition to jump-start it correctly. In particular,<ref>"A construction due to Klop 2007" https://ncatlab.org/nlab/show/fixed-point+combinator</ref>
: '''L'''''abcdefghijklmnopqstuvwxyzr'' = ''r''(''thisisafixedpointcombinator'') ; '''Y = LLLLLLLLLLLLLLLLLLLLLLLLLL''' 
<!--
      Hgh = g(hgh)
 Yg = HgH
 &nbsp;
      Hhg = g(hhg)
 Yg = HHg
 &nbsp;
      Hsomething = g(hsomething)
 Yg = H_____H__g
-->

In a [[strict programming language]] the [[Fixed-point combinator|Y combinator]] will expand until [[stack overflow]], or never halt in case of [[tail call optimization]].<ref>{{cite web |last1=Bene |first1=Adam |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 |date=17 August 2017}}</ref> The [[Z combinator]] will work in [[Strict programming language|strict languages]] (also called eager languages, where applicative evaluation order is applied).

: <math>\begin{align}
Z & = \lambda f. (\lambda x. f (\lambda v. x x v))(\lambda x. f (\lambda v. x x v)) \\
& = \lambda f. U (\lambda x. f (\lambda v. U x v)) \\
& = S(\lambda f. U)(\lambda f. \lambda x. f (\lambda v. U x v)) \\
& = S(KU)(\lambda f. S(\lambda x. f)(\lambda x. \lambda v. U x v)) \\
& = S(KU)(\lambda f. S(K f)(\lambda x. \lambda v. U x v)) \\
& = S(KU)(S(\lambda f. S(K f))(\lambda f. \lambda x. \lambda v. U x v)) \\
& = S(KU)(S(S(\lambda f. S)(\lambda f. K f))(K(\lambda x. \lambda v. U x v))) \\
& = S(KU)(S(S(KS)K)(K(\lambda x. \lambda v. U x v))) \\
& = S(KU)(S(S(KS)K)(K(\lambda x. S({\color{Red}\lambda v. U x})(\lambda v. v)))) \\
& = S(KU)(S(S(KS)K)(K(\lambda x. S(S(\lambda v. U)(\lambda v. x))I))) \\
& = S(KU)(S(S(KS)K)(K(\lambda x. S(S(KU)(Kx))I))) \\
& = S(KU)(S(S(KS)K)(K(S(\lambda x. S(S(KU)(Kx)))(\lambda x. I)))) \\
& = S(KU)(S(S(KS)K)(K(S(S(\lambda x. S)(\lambda x. S(KU)(Kx)))(KI)))) \\
& = S(KU)(S(S(KS)K)(K(S(S(KS)(S(\lambda x. S(KU))(\lambda x. Kx)))(KI)))) \\
& = S(KU)(S(S(KS)K)(K(S(S(KS)(S(K(S(KU)))K))(KI)))) \\
\end{align}</math>