Editing SKI combinator calculus (section)

==SKI expressions==

===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>

===The reversal expression===
'''S'''('''K'''('''SI'''))'''K''' reverses the two terms following it:
: '''S'''('''K'''('''SI'''))'''K'''αβ →
: '''K'''('''SI''')α('''K'''α)β →
: '''SI'''('''K'''α)β →
: '''I'''β('''K'''αβ) →
: '''I'''βα →
: βα
It is thus equivalent to '''CI'''. And in general, '''S'''('''K'''('''S'''''f''))'''K''' is equivalent to '''C'''''f'', for any ''f''.

===Boolean logic===
SKI combinator calculus can also implement [[Boolean logic]] in the form of an ''if-then-else'' structure.  An ''if-then-else'' structure consists of a Boolean expression that is either true ('''T''') or false ('''F''') and two arguments, such that:
: '''T'''''xy'' = ''x''
and
: '''F'''''xy'' = ''y''

The key is in defining the two Boolean expressions.  The first works just like one of our basic combinators:
: '''T''' = '''K'''
: '''K'''''xy'' = ''x''

The second is also fairly simple:
: '''F''' = '''SK'''
: '''SK'''''xy'' = '''K'''''y(xy)'' = y

Once true and false are defined, all Boolean logic can be implemented in terms of ''if-then-else'' structures.

Boolean '''NOT''' (which returns the opposite of a given Boolean) works the same as the ''if-then-else'' structure, with '''F''' and '''T''' as the second and third values, so it can be implemented as a postfix operation:
: '''NOT''' = λb.b ('''F''')('''T''') = λb.b ('''SK''')('''K''')
If this is put in an ''if-then-else'' structure, it can be shown that this has the expected result
: ('''T''')'''NOT''' = '''T'''('''F''')('''T''') = '''F'''
: ('''F''')'''NOT''' = '''F'''('''F''')('''T''') = '''T'''

Boolean '''OR''' (which returns '''T''' if either of the two Boolean values surrounding it is '''T''') works the same as an ''if-then-else'' structure with '''T''' as the second value, so it can be implemented as an infix operation:
: '''OR''' = '''T''' = '''K'''
If this is put in an ''if-then-else'' structure, it can be shown that this has the expected result:
: ('''T''')'''OR'''('''T''') = '''T'''('''T''')('''T''') = '''T'''
: ('''T''')'''OR'''('''F''') = '''T'''('''T''')('''F''') = '''T'''
: ('''F''')'''OR'''('''T''') = '''F'''('''T''')('''T''') = '''T'''
: ('''F''')'''OR'''('''F''') = '''F'''('''T''')('''F''') = '''F'''

Boolean '''AND''' (which returns '''T''' if both of the two Boolean values surrounding it are '''T''') works the same as an ''if-then-else'' structure with '''F''' as the third value, so it can be implemented as a postfix operation:
: '''AND''' = '''F''' = '''SK'''
If this is put in an ''if-then-else'' structure, it can be shown that this has the expected result:
: ('''T''')('''T''')'''AND''' = '''T'''('''T''')('''F''') = '''T'''
: ('''T''')('''F''')'''AND''' = '''T'''('''F''')('''F''') = '''F'''
: ('''F''')('''T''')'''AND''' = '''F'''('''T''')('''F''') = '''F'''
: ('''F''')('''F''')'''AND''' = '''F'''('''F''')('''F''') = '''F'''

Because this defines '''T''', '''F''', '''NOT''' (as a postfix operator), '''OR''' (as an infix operator), and '''AND''' (as a postfix operator) in terms of SKI notation, this proves that the SKI system can fully express Boolean logic.

As the SKI calculus is [[Combinatory logic#Completeness of the S-K basis|complete]], it is also possible to express '''NOT''', '''OR''' and '''AND''' as prefix operators:
: '''NOT''' = '''S'''('''SI'''('''KF'''))('''KT''') (as '''S'''('''SI'''('''KF'''))('''KT''')''x'' = '''SI'''('''KF''')''x''('''KT'''''x'') = '''I'''''x''('''KF'''''x'')'''T''' = ''x'''''FT''')
: '''OR''' = '''SI'''('''KT''') (as '''SI'''('''KT''')''xy'' = '''I'''''x''('''KT'''''x'')''y'' = ''x'''''T'''''y'')
: '''AND''' = '''SS'''('''K'''('''KF''')) (as '''SS'''('''K'''('''KF'''))''xy'' = '''S'''''x''('''K'''('''KF''')''x'')''y'' = ''xy''('''KF'''''y'') = ''xy'''''F''')