SKI Calculus: Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
← Older edit
VisualWikitext
Polygon (talk | contribs)
2,147 edits
used proper greater/equals sign
Δ⁵ (talk | contribs)
77 edits
 
(97 intermediate revisions by 9 users not shown)
Line 1: Line 1:
Busy Beaver for SKI calculus (we will call it BBSKI for now) is a variation of the Busy Beaver problem for lambda calculus.
A '''SKI calculus''' program is a binary tree where the leaves are combinators, the three symbols <code>S</code>, <code>K</code>, <code>I</code>. Using parentheses to notate the tree, a simple example of a SKI program is <code>(((SK)S)((KI)S))</code>. We can omit parentheses by assuming they are left-binding by default, so we simplify our program to <code>SKS(KIS)</code>.


A SKI calculus program is a binary tree where the leaves are combinators, the three symbols <code>S</code>, <code>K</code>, <code>I</code>. Using parentheses to notate the tree, a simple example of a SKI program is <code>(((SK)S)((KI)S))</code>. We can omit parentheses by assuming they are left-binding by default, so we simplify our program to <code>SKS(KIS)</code>.
Like [[Lambda Calculus|lambda calculus]], SKI calculus has a process called beta-reduction. We change the tree according to any reducible redex.  


Like lambda calculus, SKI calculus has a process called beta-reduction. We change the tree according to the leftmost combinator.
Sfgx => fx(gx)


* <code>Ix -> I</code>
Kfx => f
* <code>Kxy -> Kx</code>
* <code>Sxyz -> Sxz(yz)</code>


Note that <code>xyz</code> represent any valid trees, not just single combinators.
Ix => x


We repeat this process and we say it terminates if the combinator cannot be beta-reduced.
Note that <code>xyz</code> represent any valid trees, not just single combinators. We repeat this process and we say it terminates if the combinator cannot be beta-reduced.
 
Busy Beaver for SKI calculus (Ξ₀) is a variation of the [[Busy Beaver for lambda calculus|Busy Beaver problem for lambda calculus]]. Ξ₀(n) is defined as the size of the largest output of a terminating program of size n.


== Champions ==
== Champions ==
{| class="wikitable"
{| class="wikitable"
! n !! Value !! Champion !! Discoverered by
! n !! Value !! Champion  
|-
|-
| 1 || = 1 || S || ?
| 1 || = 1 || S  
|-
|-
| 2 || = 2 || SS || ?
| 2 || = 2 || SS  
|-
|-
| 3 || = 3 || SSS || ?
| 3 || = 3 || SSS  
|-
|-
| 4 || = 4 || SSSS || ?
| 4 || = 4 || SSSS  
|-
|-
| 5 || = 6 || SSS(SS) || ?
| 5 || = 6 || SSS(SS)  
|-
|-
| 6 || = 17 || SSS(SI)S || ?
| 6 || = 17 || SSS(SI)S  
|-
|-
|7
|7
|≥ 18
|≥ 41
|S(SSS(SI)S)
|SSS(S(SS))S
|?
|-
|-
|8
|8
|≥ 19
|≥ 80
|SS(SSS(SI)S)
|SSK(S(SS)S)S
|?
|-
|-
|9
|9
|≥ 519
|≥ 169
|SSI((S(SS)S)S)K
|S(SS)(SS)(SS)SS
|?
|-
|-
|10
|10
|≥ 1041
|≥ 376
|SSI((S(SS)S)S)KS
|S(S(SS(KK)))(SS)(SS)
|?
|-
|11
|≥ 912
|S(SS)S(SS)(S(S(KS))S)
|-
|12
|≥ 2^2^513*8-2
|S(SI)(SSK)(S(S(KS)K)I)
|-
|13
|> 2^^2^^2^258
|SI(SI)(SSK)(S(S(KS)K)I)
|-
|14
|> 2^^2^^2^258
|SI(SI)(SSK)(S(S(KS)K)I)S
|-
|15
|> 2^^2^^2^^34
|S(S(SI)I(SSK))I(S(S(KS)K)I)
|-
|16
|> 2^^^19
|S(S(SI))I(S(SSK)(K(S(S(KS)K)I)))
|-
|17
|> 2^^^^2^^2^^258
|S(SS(SSS)I(SSK))I(S(S(KS)K)I)
|-
|18
|> 2^^^^2^^2^^258
|S(SS(SSS)I(SSK))I(S(S(KS)K)I)S
|-
|19
|> 2^^^^2^^^19
|SSI(SSK(S(S(KS)K)I))(S(K(S(SSK)))K)
|-
|20
|> f<sub>ω+1</sub> (2^^7/2-1) > [[Graham's number]]
|S(S(S(SI)))I(S(K(S(SS(K(K(S(S(KS)K)I))))))K)
|-
|...
|
|
|-
|27
|> f<sub>ω+2</sub> (2^2^21)
|SI(SI(SI(S(S(K(SS(KI))))I)))(S(K(S(SSK)))K)(S(S(KS)K)I)
|-
|28
|> f<sub>ω+2</sub> (2^2^21)
|S(SI(SI(SI(S(S(K(SS(KI))))I)))(S(K(S(SSK)))K)(S(S(KS)K)I))
|-
|29
|> f<sub>ω+3</sub> (2^2^21)
|SI(SI(SI(SI(S(S(K(SS(KI))))I))))(S(K(S(SSK)))K)(S(S(KS)K)I)
|-
|30
|> f<sub>ω+3</sub> (2^2^21)
|S(SI(SI(SI(SI(S(S(K(SS(KI))))I))))(S(K(S(SSK)))K)(S(S(KS)K)I))
|-
|31
|> f<sub>ω+4</sub> (2^2^21)
|SI(SI(SI(SI(SI(S(S(K(SS(KI))))I)))))(S(K(S(SSK)))K)(S(S(KS)K)I)
|-
|32
|> f<sub>ω+4</sub> (2^2^21)
|S(SI(SI(SI(SI(SI(S(S(K(SS(KI))))I)))))(S(K(S(SSK)))K)(S(S(KS)K)I))
|-
|...
|
|
|}
|}


== SK calculus ==
== SK calculus ==
We can remove the <code>I</code> combinator and replace it by <code>(SKS)</code>, <code>(SKK)</code> or any <code>(SKx)</code>.
We can remove the <code>I</code> combinator and replace it by <code>(SKS)</code>, <code>(SKK)</code> or any <code>(SKx)</code>. These terms have a straightforward binary encoding where (prefix) application is 1, K=00, and S=01. Since n combinators take n-1 applications to combine, their code length is 2n + n-1 = 3n-1 bits.


=== Champions ===
=== Champions for Ξ₀<sub>SK</sub> ===
{| class="wikitable"
{| class="wikitable"
! n !! Value !! Champion !! Discoverered by
! n !! bits !! Value !! Champion  
|-
|-
| 1 || = 1 || S || ?
| 1 || 2 || = 1 || S  
|-
|-
| 2 || = 2 || SS || ?
| 2 || 5 || = 2 || SS  
|-
|-
| 3 || = 3 || SSS || ?
| 3 || 8 || = 3 || SSS  
|-
|-
| 4 || = 4 || <code>SSSS</code> || ?
| 4 || 11 || = 4 || SSSS  
|-
|-
| 5 || = 6 || <code>SSS(SS)</code> || ?
| 5 || 14 || = 6 || SSS(SS)  
|-
|-
| 6 || ≥ 8 || <code>SSS(SSS)</code> || ?
| 6 || 17 || = 10 || SSS(SS)S
|-
|-
|7
|7
|≥ 10
| 20
|<code>SSS(SSSS)</code>
|≥ 41
|?
|SSS(S(SS))S
|-
|-
|8
|8
|≥ 23
| 23
|<code>SSS(S(SKS))S</code>
|≥ 80
|?
|SSK(S(SS)S)S
|-
|9
| 26
|≥ 169
|S(SS)(SS)(SS)SS
|-
|10
| 29
|≥ 376
|S(S(SS(KK)))(SS)(SS)
|-
|11
| 32
|≥ 912
|S(SS)S(SS)(S(S(KS))S)
|-
|12
| 35
|≥ 1530
|S(SS)(SS)(SS(SS(SS)))S
|-
|13
| 38
|≥ 7811
|S(SS)(SS)(SS(SS(SSS)))S
|-
|14
|41
|≥ 2^2097156*13-2
|SSS(SSK)(SS(SK)(S(KS)K))
|-
|15
|44
|≥ 2^2^2097156*3-2
|SSS(SSK)(SS(SK)(S(KS)K))S
|-
|16
|47
|> 2^2^2^8193
|S(SS(SS))(SSK)(SS(SK)(S(KS)K))
|-
|17
|50
|> 2^^2^^2^258
|SSS(SKS)(SSK)(SS(SK)(S(KS)K))
|-
|...
|
|
|
|-
|22
|65
|> 2^^^19
|S(S(S(S(SK))))(SKS)(S(SSK)(K(SS(SK)(S(KS)K)))
|-
|23
|68
|> 2^^^^2^^^19
|SS(S(SK))(SSK(SS(SK)(S(KS)K)))(S(K(S(SSK)))K)
|-
|24
|71
|> 2^^^^2^^^19
|S(SS(S(SK))(SSK(SS(SK)(S(KS)K)))(S(K(S(SSK)))K))
|-
|25
|74
|> 3{7}3
|SS(S(SK))(SSK(SS(SS(SK))(S(KS)K)))(S(K(S(SSK)))K)
|-
|26
|77
|> f<sub>ω+1</sub>(2^^7/2-1) > [[Graham's number]]
|S(S(S(S(SKS))))(SKS)(S(K(S(SS(K(K(SS(SK)(S(KS)K)))))))K)
|}
TODO: Champions analysis.
 
== BCKW system ==
BCKW system is a variation of SK calculus that replace the S combinator by 3 new combinators B, C and W.
 
Bfgx => f(gx)
 
Cfxy => fyx
 
Kfx => f
 
Wfx => fxx
 
=== Champions for Ξ₀<sub>BCKW</sub> ===
{| class="wikitable"
! n !! Value !! Champion
|-
| 1 || = 1 || B
|-
| 2 || = 2 || BB
|-
| 3 || = 3 || BBB
|-
| 4 || ≥ 11 || WW(WB)
|-
| 5 || ≥ 47 || W(WW)(WB)
|-
|6
|≥ 2^256*6-1
|WW(WC(WB))
|-
|7
|> 2^^^17
|WW(C(WC)(WB))
|-
|8
|> 2^^^2^^^17
|W(WW)(C(WC)(WB))
|-
|9
|> 2{5}2^^^^2^^^19
|WW(WB(C(WC))(WB))
|-
|10
|> f<sub>ω+1</sub>(2^^6/2-1)
|WW(C(WB)(C(CC(WB))))
|}
 
== Oracles ==
 
We can extend Ξ₀ with oracles, making it stronger than BB. For example, we can add an oracle combinator O where Ofxy=x iff for all z fz is equivalent to z, and y otherwise. The resulting busy beaver, known as the Ξ function, is estimated to be faster-growing than oracle busy beavers with the oracle degree ≤ ω₁<sup>CK</sup>. In addition, Ξ is independent of True Arithmetic, requiring Δ¹₁ truth to fully decide. A further extension would be to add another oracle, O’, where O’fxy=x iff f is well-founded, and y otherwise, where a term is well-founded iff there is no infinitely nested outermost-redex oracle calls. The resulting busy beaver is called Ξ₂.
 
=== Champions for Ξ<sub>SKIO</sub> ===
{| class="wikitable"
! n !! Value !! Champion
|-
| 1 || = 1 || S
|-
| 2 || = 2 || SS
|-
| 3 || = 3 || SSS
|-
| 4 || = 4 || SSSS
|-
| 5 || = 6 || SSS(SS)
|-
| 6 || = 17 || SSS(SI)S
|}
|}


== See Also ==
== See Also ==
[https://komiamiko.me/math/ordinals/2020/06/21/ski-numerals.html Lower bounds of this function]
* [https://web.archive.org/web/20250217071017/https://komiamiko.me/math/ordinals/2020/06/21/ski-numerals.html Lower bounds of this function] (archived)
* [https://dallaylaen.github.io/ski-interpreter/ SKI interpreter]


[[Category:Functions]]
[[Category:Functions]]

Latest revision as of 01:07, 24 September 2026

A SKI calculus program is a binary tree where the leaves are combinators, the three symbols S, K, I. Using parentheses to notate the tree, a simple example of a SKI program is (((SK)S)((KI)S)). We can omit parentheses by assuming they are left-binding by default, so we simplify our program to SKS(KIS).

Like lambda calculus, SKI calculus has a process called beta-reduction. We change the tree according to any reducible redex.

Sfgx => fx(gx)

Kfx => f

Ix => x

Note that xyz represent any valid trees, not just single combinators. We repeat this process and we say it terminates if the combinator cannot be beta-reduced.

Busy Beaver for SKI calculus (Ξ₀) is a variation of the Busy Beaver problem for lambda calculus. Ξ₀(n) is defined as the size of the largest output of a terminating program of size n.

Champions

n Value Champion
1 = 1 S
2 = 2 SS
3 = 3 SSS
4 = 4 SSSS
5 = 6 SSS(SS)
6 = 17 SSS(SI)S
7 ≥ 41 SSS(S(SS))S
8 ≥ 80 SSK(S(SS)S)S
9 ≥ 169 S(SS)(SS)(SS)SS
10 ≥ 376 S(S(SS(KK)))(SS)(SS)
11 ≥ 912 S(SS)S(SS)(S(S(KS))S)
12 ≥ 2^2^513*8-2 S(SI)(SSK)(S(S(KS)K)I)
13 > 2^^2^^2^258 SI(SI)(SSK)(S(S(KS)K)I)
14 > 2^^2^^2^258 SI(SI)(SSK)(S(S(KS)K)I)S
15 > 2^^2^^2^^34 S(S(SI)I(SSK))I(S(S(KS)K)I)
16 > 2^^^19 S(S(SI))I(S(SSK)(K(S(S(KS)K)I)))
17 > 2^^^^2^^2^^258 S(SS(SSS)I(SSK))I(S(S(KS)K)I)
18 > 2^^^^2^^2^^258 S(SS(SSS)I(SSK))I(S(S(KS)K)I)S
19 > 2^^^^2^^^19 SSI(SSK(S(S(KS)K)I))(S(K(S(SSK)))K)
20 > fω+1 (2^^7/2-1) > Graham's number S(S(S(SI)))I(S(K(S(SS(K(K(S(S(KS)K)I))))))K)
...
27 > fω+2 (2^2^21) SI(SI(SI(S(S(K(SS(KI))))I)))(S(K(S(SSK)))K)(S(S(KS)K)I)
28 > fω+2 (2^2^21) S(SI(SI(SI(S(S(K(SS(KI))))I)))(S(K(S(SSK)))K)(S(S(KS)K)I))
29 > fω+3 (2^2^21) SI(SI(SI(SI(S(S(K(SS(KI))))I))))(S(K(S(SSK)))K)(S(S(KS)K)I)
30 > fω+3 (2^2^21) S(SI(SI(SI(SI(S(S(K(SS(KI))))I))))(S(K(S(SSK)))K)(S(S(KS)K)I))
31 > fω+4 (2^2^21) SI(SI(SI(SI(SI(S(S(K(SS(KI))))I)))))(S(K(S(SSK)))K)(S(S(KS)K)I)
32 > fω+4 (2^2^21) S(SI(SI(SI(SI(SI(S(S(K(SS(KI))))I)))))(S(K(S(SSK)))K)(S(S(KS)K)I))
...

SK calculus

We can remove the I combinator and replace it by (SKS), (SKK) or any (SKx). These terms have a straightforward binary encoding where (prefix) application is 1, K=00, and S=01. Since n combinators take n-1 applications to combine, their code length is 2n + n-1 = 3n-1 bits.

Champions for Ξ₀SK

n bits Value Champion
1 2 = 1 S
2 5 = 2 SS
3 8 = 3 SSS
4 11 = 4 SSSS
5 14 = 6 SSS(SS)
6 17 = 10 SSS(SS)S
7 20 ≥ 41 SSS(S(SS))S
8 23 ≥ 80 SSK(S(SS)S)S
9 26 ≥ 169 S(SS)(SS)(SS)SS
10 29 ≥ 376 S(S(SS(KK)))(SS)(SS)
11 32 ≥ 912 S(SS)S(SS)(S(S(KS))S)
12 35 ≥ 1530 S(SS)(SS)(SS(SS(SS)))S
13 38 ≥ 7811 S(SS)(SS)(SS(SS(SSS)))S
14 41 ≥ 2^2097156*13-2 SSS(SSK)(SS(SK)(S(KS)K))
15 44 ≥ 2^2^2097156*3-2 SSS(SSK)(SS(SK)(S(KS)K))S
16 47 > 2^2^2^8193 S(SS(SS))(SSK)(SS(SK)(S(KS)K))
17 50 > 2^^2^^2^258 SSS(SKS)(SSK)(SS(SK)(S(KS)K))
...
22 65 > 2^^^19 S(S(S(S(SK))))(SKS)(S(SSK)(K(SS(SK)(S(KS)K)))
23 68 > 2^^^^2^^^19 SS(S(SK))(SSK(SS(SK)(S(KS)K)))(S(K(S(SSK)))K)
24 71 > 2^^^^2^^^19 S(SS(S(SK))(SSK(SS(SK)(S(KS)K)))(S(K(S(SSK)))K))
25 74 > 3{7}3 SS(S(SK))(SSK(SS(SS(SK))(S(KS)K)))(S(K(S(SSK)))K)
26 77 > fω+1(2^^7/2-1) > Graham's number S(S(S(S(SKS))))(SKS)(S(K(S(SS(K(K(SS(SK)(S(KS)K)))))))K)

TODO: Champions analysis.

BCKW system

BCKW system is a variation of SK calculus that replace the S combinator by 3 new combinators B, C and W.

Bfgx => f(gx)

Cfxy => fyx

Kfx => f

Wfx => fxx

Champions for Ξ₀BCKW

n Value Champion
1 = 1 B
2 = 2 BB
3 = 3 BBB
4 ≥ 11 WW(WB)
5 ≥ 47 W(WW)(WB)
6 ≥ 2^256*6-1 WW(WC(WB))
7 > 2^^^17 WW(C(WC)(WB))
8 > 2^^^2^^^17 W(WW)(C(WC)(WB))
9 > 2{5}2^^^^2^^^19 WW(WB(C(WC))(WB))
10 > fω+1(2^^6/2-1) WW(C(WB)(C(CC(WB))))

Oracles

We can extend Ξ₀ with oracles, making it stronger than BB. For example, we can add an oracle combinator O where Ofxy=x iff for all z fz is equivalent to z, and y otherwise. The resulting busy beaver, known as the Ξ function, is estimated to be faster-growing than oracle busy beavers with the oracle degree ≤ ω₁CK. In addition, Ξ is independent of True Arithmetic, requiring Δ¹₁ truth to fully decide. A further extension would be to add another oracle, O’, where O’fxy=x iff f is well-founded, and y otherwise, where a term is well-founded iff there is no infinitely nested outermost-redex oracle calls. The resulting busy beaver is called Ξ₂.

Champions for ΞSKIO

n Value Champion
1 = 1 S
2 = 2 SS
3 = 3 SSS
4 = 4 SSSS
5 = 6 SSS(SS)
6 = 17 SSS(SI)S

See Also

Retrieved from "https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&oldid=8673"