SKI Calculus: Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
← Older editNewer edit →
VisualWikitext
Azerty (talk | contribs)
379 edits
I prefer keeping BB_SKI because it's more consistent with other systems like SK or BKWC
Δ⁵ (talk | contribs)
120 edits
m Removed unused columns
Line 15: Line 15:
== Champions ==
== Champions ==
{| class="wikitable"
{| class="wikitable"
! n !! Value !! Champion !! Discovered 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
|≥ 41
|≥ 41
|SSS(S(SS))S
|SSS(S(SS))S
|
|-
|-
|8
|8
|≥ 80
|≥ 80
|SSK(S(SS)S)S
|SSK(S(SS)S)S
|
|-
|-
|9
|9
|≥ 169
|≥ 169
|S(SS)(SS)(SS)SS
|S(SS)(SS)(SS)SS
|
|-
|-
|10
|10
|≥ 376
|≥ 376
|S(S(SS(KK)))(SS)(SS)
|S(S(SS(KK)))(SS)(SS)
|
|-
|-
|11
|11
|≥ 912
|≥ 912
|S(SS)S(SS)(S(S(KS))S)
|S(SS)S(SS)(S(S(KS))S)
|
|-
|-
|12
|12
|≥ 196606
|≥ 196606
|S(S(SI))I(S(S(KS)K)I)K
|S(S(SI))I(S(S(KS)K)I)K
|
|-
|-
|13
|13
|> 2^2^2^21
|> 2^2^2^21
|S(S(SSS)I)I(S(S(KS)K)I)
|S(S(SSS)I)I(S(S(KS)K)I)
|
|-
|-
|14
|14
|> 2^^33
|> 2^^33
|SI(SSK)(SSK(S(S(KS)K)I))
|SI(SSK)(SSK(S(S(KS)K)I))
|
|-
|-
|15
|15
|> 2^^2^^33
|> 2^^2^^33
|SII(SSK(SSK(S(S(KS)K)I)))
|SII(SSK(SSK(S(S(KS)K)I)))
|
|-
|-
|16
|16
|> 2^^2^^65
|> 2^^2^^65
|S(SI)I(SSK(SSK(S(S(KS)K)I)))
|S(SI)I(SSK(SSK(S(S(KS)K)I)))
|
|-
|-
|17
|17
|> 2^^^2^128
|> 2^^^2^128
|S(SSK(S(SSSI)I))I(S(S(KS)K)I)
|S(SSK(S(SSSI)I))I(S(S(KS)K)I)
|
|-
|-
|18
|18
|> 2^^^2^2^2^2^21
|> 2^^^2^2^2^2^21
|S(SSK(S(S(SSS)I)I))I(S(S(KS)K)I))
|S(SSK(S(S(SSS)I)I))I(S(S(KS)K)I))
|
|-
|-
|19
|19
|> 2^^^2^^19
|> 2^^^2^^19
|S(SSK(S(S(S(SSS))I)I))I(S(S(KS)K)I)
|S(SSK(S(S(S(SSS))I)I))I(S(S(KS)K)I)
|
|-
|-
|20
|20
|> 3<nowiki>{{1}}</nowiki>(2^^7/2-1) = {3,(2^^7/2-1),1,2} > [[Graham's number]]
|> 3<nowiki>{{1}}</nowiki>(2^^7/2-1) = {3,(2^^7/2-1),1,2} > [[Graham's number]]
|S(S(S(SI)))I(S(K(S(SS(K(K(S(S(KS)K)I))))))K)
|S(S(S(SI)))I(S(K(S(SS(K(K(S(S(KS)K)I))))))K)
|
|}
|}


Line 105: Line 91:
=== Champions ===
=== Champions ===
{| class="wikitable"
{| class="wikitable"
! n !! bits !! Value !! Champion !! Discovered by
! n !! bits !! Value !! Champion  
|-
|-
| 1 || 2 || = 1 || S ||
| 1 || 2 || = 1 || S  
|-
|-
| 2 || 5 || = 2 || SS ||
| 2 || 5 || = 2 || SS  
|-
|-
| 3 || 8 || = 3 || SSS ||
| 3 || 8 || = 3 || SSS  
|-
|-
| 4 || 11 || = 4 || SSSS ||
| 4 || 11 || = 4 || SSSS  
|-
|-
| 5 || 14 || = 6 || SSS(SS) ||
| 5 || 14 || = 6 || SSS(SS)  
|-
|-
| 6 || 17 || = 10 || SSS(SS)S ||
| 6 || 17 || = 10 || SSS(SS)S  
|-
|-
|7
|7
Line 123: Line 109:
|≥ 41
|≥ 41
|SSS(S(SS))S
|SSS(S(SS))S
|
|-
|-
|8
|8
Line 129: Line 114:
|≥ 80
|≥ 80
|SSK(S(SS)S)S
|SSK(S(SS)S)S
|
|-
|-
|9
|9
Line 135: Line 119:
|≥ 169
|≥ 169
|S(SS)(SS)(SS)SS
|S(SS)(SS)(SS)SS
|
|-
|-
|10
|10
Line 141: Line 124:
|≥ 376
|≥ 376
|S(S(SS(KK)))(SS)(SS)
|S(S(SS(KK)))(SS)(SS)
|
|-
|-
|11
|11
Line 147: Line 129:
|≥ 912
|≥ 912
|S(SS)S(SS)(S(S(KS))S)
|S(SS)S(SS)(S(S(KS))S)
|
|-
|-
|12
|12
Line 153: Line 134:
|≥ 913
|≥ 913
|S(S(SS)S(SS)(S(S(KS))S))
|S(S(SS)S(SS)(S(S(KS))S))
|
|-
|-
|13
|13
Line 159: Line 139:
|≥ 914
|≥ 914
|S(S(S(SS)S(SS)(S(S(KS))S)))
|S(S(S(SS)S(SS)(S(S(KS))S)))
|
|-
|-
|14
|14
Line 165: Line 144:
|≥ 1530
|≥ 1530
|SS(SKK)(SS)(SS(SS(SS)))S
|SS(SKK)(SS)(SS(SS(SS)))S
|
|-
|-
|15
|15
Line 171: Line 149:
|≥ 7811
|≥ 7811
|SS(SKK)(SS)(SS(SS(SSS)))S
|SS(SKK)(SS)(SS(SS(SSS)))S
|
|}
|}
TODO: Champions analysis.
TODO: Champions analysis.
Line 188: Line 165:
=== Champions ===
=== Champions ===
{| class="wikitable"
{| class="wikitable"
! n !! Value !! Champion !! Discovered by
! n !! Value !! Champion  
|-
|-
| 1 || = 1 || B ||
| 1 || = 1 || B  
|-
|-
| 2 || = 2 || BB ||
| 2 || = 2 || BB  
|-
|-
| 3 || = 3 || BBB ||
| 3 || = 3 || BBB  
|-
|-
| 4 || ≥ 11 || WW(WB) ||
| 4 || ≥ 11 || WW(WB)  
|-
|-
| 5 || ≥ 47 || W(WW)(WB) ||
| 5 || ≥ 47 || W(WW)(WB)  
|-
|-
|6
|6
|≥ 3*2^66-1
|≥ 3*2^66-1
|WB(WW)(WB)
|WB(WW)(WB)
|
|-
|-
|7
|7
|> 2^2^2^20
|> 2^2^2^20
|WB(W(WW))(WB)
|WB(W(WW))(WB)
|
|-
|-
|8
|8
|> 2^^34
|> 2^^34
|WC(WW(WB))(WW)
|WC(WW(WB))(WW)
|
|-
|-
|9
|9
|> 2^^2^^33
|> 2^^2^^33
|W(WK)(WC(WC(WB)))
|W(WK)(WC(WC(WB)))
|
|-
|-
|10
|10
|> 2^^2^^33
|> 2^^2^^33
|W(W(WK))(WC(WC(WB)))
|W(W(WK))(WC(WC(WB)))
|
|-
|-
|11
|11
|> f<sub>ω</sub> (2^2^18)
|> f<sub>ω</sub> (2^2^18)
|WB(W(C(WC)(C(WC))))(WB)
|WB(W(C(WC)(C(WC))))(WB)
|
|-
|-
|12
|12
|> f<sub>ω+1</sub> (2^2^18-2)
|> f<sub>ω+1</sub> (2^2^18-2)
|W(WC(W(C(WC)(C(WC)))))(WB)
|W(WC(W(C(WC)(C(WC)))))(WB)
|
|}
|}


Revision as of 06:04, 28 May 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 BB_SKI (also known as Ξ₀) is a variation of the Busy Beaver problem for lambda calculus. BB_SKI(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 ≥ 196606 S(S(SI))I(S(S(KS)K)I)K
13 > 2^2^2^21 S(S(SSS)I)I(S(S(KS)K)I)
14 > 2^^33 SI(SSK)(SSK(S(S(KS)K)I))
15 > 2^^2^^33 SII(SSK(SSK(S(S(KS)K)I)))
16 > 2^^2^^65 S(SI)I(SSK(SSK(S(S(KS)K)I)))
17 > 2^^^2^128 S(SSK(S(SSSI)I))I(S(S(KS)K)I)
18 > 2^^^2^2^2^2^21 S(SSK(S(S(SSS)I)I))I(S(S(KS)K)I))
19 > 2^^^2^^19 S(SSK(S(S(S(SSS))I)I))I(S(S(KS)K)I)
20 > 3{{1}}(2^^7/2-1) = {3,(2^^7/2-1),1,2} > Graham's number S(S(S(SI)))I(S(K(S(SS(K(K(S(S(KS)K)I))))))K)

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

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 ≥ 913 S(S(SS)S(SS)(S(S(KS))S))
13 38 ≥ 914 S(S(S(SS)S(SS)(S(S(KS))S)))
14 41 ≥ 1530 SS(SKK)(SS)(SS(SS(SS)))S
15 44 ≥ 7811 SS(SKK)(SS)(SS(SS(SSS)))S

TODO: Champions analysis.

BCKW system

BCKW system is a variation of SK calculus that replace the S combinator by 3 new combinators.

Bfgx => f(gx)

Cfxy => fyx

Kfx => f

Wfx => fxx

Champions

n Value Champion
1 = 1 B
2 = 2 BB
3 = 3 BBB
4 ≥ 11 WW(WB)
5 ≥ 47 W(WW)(WB)
6 ≥ 3*2^66-1 WB(WW)(WB)
7 > 2^2^2^20 WB(W(WW))(WB)
8 > 2^^34 WC(WW(WB))(WW)
9 > 2^^2^^33 W(WK)(WC(WC(WB)))
10 > 2^^2^^33 W(W(WK))(WC(WC(WB)))
11 > fω (2^2^18) WB(W(C(WC)(C(WC))))(WB)
12 > fω+1 (2^2^18-2) W(WC(W(C(WC)(C(WC)))))(WB)

Oracles

We can extend BB_SKI with oracles, making it stronger than BB. For example, we can add an oracle combinator O where Ofxy=x iff for all z fz beta-reduces to z, and y otherwise. The resulting busy beaver, known as the Ξ function, is estimated to be faster-growing than ordinal oracle busy beavers with the oracle degree <= w_1^CK. 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 Ξ₂.

See Also

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