SKI Calculus: Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
← Older editNewer edit →
VisualWikitext
Loader3229 (talk | contribs)
428 edits
Δ⁵ (talk | contribs)
153 edits
m standardised tables behind-the-scenes; above pentations used bower's notation instead of up-arrows to avoid confusion
Line 31: Line 31:
| 6 || = 17 || SSS(SI)S  
| 6 || = 17 || SSS(SI)S  
|-
|-
|7
| 7 || ≥ 41 || SSS(S(SS))S
|≥ 41
|SSS(S(SS))S
|-
|-
|8
| 8 || ≥ 80 || SSK(S(SS)S)S
|≥ 80
|SSK(S(SS)S)S
|-
|-
|9
| 9 || ≥ 1561 || S(SI)(SS)(SS)SS
|≥ 1561
|S(SI)(SS)(SS)SS
|-
|-
|10
| 10 || ≥ 1562 || S(S(SI)(SS)(SS)SS)
|≥ 1562
|S(S(SI)(SS)(SS)SS)
|-
|-
|11
| 11 || ≥ 1563 || SS(S(SI)(SS)(SS)SS)
|≥ 1563
|SS(S(SI)(SS)(SS)SS)
|-
|-
|12
| 12 || ≥ 2^2^513 × 8 - 2 || S(SI)(SSK)(S(S(KS)K)I)
|<math>\geq 2^{2^{513}} \times 8 - 2 </math>
|S(SI)(SSK)(S(S(KS)K)I)
|-
|-
|13
| 13 || > 2^^2^^2^258 || SI(SI)(SSK)(S(S(KS)K)I)
|<math>> 2 \uparrow\uparrow 2 \uparrow\uparrow 2^{258} </math>
|SI(SI)(SSK)(S(S(KS)K)I)
|-
|-
|14
| 14 || > 2^^2^^2^258 || SI(SI)(SSK)(S(S(KS)K)I)S
|<math>> 2 \uparrow\uparrow 2 \uparrow\uparrow 2^{258} </math>
|SI(SI)(SSK)(S(S(KS)K)I)S
|-
|-
|15
| 15 || > 2^^2^^2^^34 || S(S(SI)I(SSK))I(S(S(KS)K)I)
|<math>> 2 \uparrow\uparrow 2 \uparrow\uparrow 2 \uparrow\uparrow 34 </math>
|S(S(SI)I(SSK))I(S(S(KS)K)I)
|-
|-
|16
| 16 || > 2^^^19 || S(S(SI))I(S(SSK)(K(S(S(KS)K)I)))
|<math>> 2 \uparrow\uparrow\uparrow 19 </math>
|S(S(SI))I(S(SSK)(K(S(S(KS)K)I)))
|-
|-
|17
| 17 || > 2{4}2^^2^^258 || S(SS(SSS)I(SSK))I(S(S(KS)K)I)
|<math>> 2 \uparrow\uparrow\uparrow\uparrow 2 \uparrow\uparrow 2 \uparrow\uparrow 258</math>
|S(SS(SSS)I(SSK))I(S(S(KS)K)I)
|-
|-
|18
| 18 || > 2{4}2^^2^^258 || S(SS(SSS)I(SSK))I(S(S(KS)K)I)S
|<math>> 2 \uparrow\uparrow\uparrow\uparrow 2 \uparrow\uparrow 2 \uparrow\uparrow 258</math>
|S(SS(SSS)I(SSK))I(S(S(KS)K)I)S
|-
|-
|19
| 19 || > 2{4}2^^^17 || SSI(SSK(S(S(KS)K)I))(S(K(S(SSK)))K)
|<math>> 2 \uparrow\uparrow\uparrow\uparrow 2 \uparrow\uparrow\uparrow 17 </math>
|SSI(SSK(S(S(KS)K)I))(S(K(S(SSK)))K)
|-
|-
|20
| 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)
|> 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
| 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)
|> 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
| 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))
|> 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
| 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)
|> 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
| 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))
|> 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
| 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)
|> 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
| 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))
|> 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))
|-
|-
|...
| ... || ||
|
|
|}
|}


Line 141: Line 97:
| 6 || 17 || = 10 || SSS(SS)S  
| 6 || 17 || = 10 || SSS(SS)S  
|-
|-
|7
| 7 || 20 || = 41 || SSS(S(SS))S
| 20
|= 41
|SSS(S(SS))S
|-
|-
|8
| 8 || 23 || ≥ 80 || SSK(S(SS)S)S
| 23
|≥ 80
|SSK(S(SS)S)S
|-
|-
|9
| 9 || 26 || ≥ 169 || S(SS)(SS)(SS)SS
| 26
|≥ 169
|S(SS)(SS)(SS)SS
|-
|-
|10
| 10 || 29 || ≥ 1561 || SS(SS)(SSS)SSS
| 29
|≥ 1561
|SS(SS)(SSS)SSS
|-
|-
|11
| 11 || 32 || ≥ 1562 || S(SS(SS)(SSS)SSS)
| 32
|≥ 1562
|S(SS(SS)(SSS)SSS)
|-
|-
|12
| 12 || 35 || ≥ 1563 || S(S(SS(SS)(SSS)SSS))
| 35
|≥ 1563
|SS(SS(SS)(SSS)SSS)
|-
|-
|13
| 13 || 38 || ≥ 7811 || S(SS)(SS)(SS(SS(SSS)))S
| 38
|≥ 7811
|S(SS)(SS)(SS(SS(SSS)))S
|-
|-
|14
| 14 || 41 || ≥ 2^2097156 × 13 - 2 || SSS(SSK)(SS(SK)(S(KS)K))
|41
|<math>\geq 2^{2097156} \times 13 - 2 </math>
|SSS(SSK)(SS(SK)(S(KS)K))
|-
|-
|15
| 15 || 44 || ≥ 2^2^2097156 × 3 - 2 || SSS(SSK)(SS(SK)(S(KS)K))S
|44
|<math>\geq 2^{2^{2097156}} \times 3 - 2</math>
|SSS(SSK)(SS(SK)(S(KS)K))S
|-
|-
|16
| 16 || 47 || > 2^2^2^8193 || S(SS(SS))(SSK)(SS(SK)(S(KS)K))
|47
|<math>> 2^{2^{2^{8193}}}</math>
|S(SS(SS))(SSK)(SS(SK)(S(KS)K))
|-
|-
|17
| 17 || 50 || > 2^^2^^2^258 || SSS(S(SK))(SSK)(SS(SK)(S(KS)K))
|50
|<math>> 2 \uparrow\uparrow 2 \uparrow\uparrow 2^{258}</math>
|SSS(S(SK))(SSK)(SS(SK)(S(KS)K))
|-
|-
|...
|... || ||
|
|
|
|-
|-
|22
| 22 || 65 || > 2^^^19 ||S(S(S(S(SK))))(S(SK))(S(SSK)(K(SS(SK)(S(KS)K)))
|65
|<math>> 2 \uparrow\uparrow\uparrow 19</math>
|S(S(S(S(SK))))(S(SK))(S(SSK)(K(SS(SK)(S(KS)K)))
|-
|-
|23
| 23 || 68 || > 2{4}2^^^17 || SS(S(SK))(SSK(SS(SK)(S(KS)K)))(S(K(S(SSK)))K)
|68
|<math>> 2 \uparrow\uparrow\uparrow\uparrow 2 \uparrow\uparrow\uparrow 17</math>
|SS(S(SK))(SSK(SS(SK)(S(KS)K)))(S(K(S(SSK)))K)
|-
|-
|24
| 24 || 71 || > 2{4}2^^^17 || S(SS(S(SK))(SSK(SS(SK)(S(KS)K)))(S(K(S(SSK)))K))
|71
|<math>> 2 \uparrow\uparrow\uparrow\uparrow 2 \uparrow\uparrow\uparrow 17</math>
|S(SS(S(SK))(SSK(SS(SK)(S(KS)K)))(S(K(S(SSK)))K))
|-
|-
|25
| 25 || 74 || > 3{7}3 || SS(S(SK))(SSK(SS(SS(SK))(S(KS)K)))(S(K(S(SSK)))K)
|74
|<math>> 3 \uparrow^{7} 3</math>
|SS(S(SK))(SSK(SS(SS(SK))(S(KS)K)))(S(K(S(SSK)))K)
|-
|-
|26
| 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)
|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.
TODO: Champions analysis.
Line 255: Line 160:
| 5 || = 47 || W(WW)(WB)  
| 5 || = 47 || W(WW)(WB)  
|-
|-
|6
| 6 || ≥ 2^256 × 6 - 1 ||WW(WC(WB))
|<math>\geq 2^{256} \times 6 - 1 </math>
|WW(WC(WB))
|-
|-
|7
| 7 || > 2^^^17 || WW(C(WC)(WB))
|<math>> 2 \uparrow\uparrow\uparrow 17</math>
|WW(C(WC)(WB))
|-
|-
|8
| 8 || > 2^^^2^^^17 || W(WW)(C(WC)(WB))
|<math>> 2 \uparrow\uparrow\uparrow 2 \uparrow\uparrow\uparrow 17</math>
|W(WW)(C(WC)(WB))
|-
|-
|9
| 9 || > 2{5}2{4}2^^^17 || WW(WB(C(WC))(WB))
|<math>> 2 \uparrow^{5} 2 \uparrow\uparrow\uparrow\uparrow 2 \uparrow\uparrow\uparrow 17</math>
|WW(WB(C(WC))(WB))
|-
|-
|10
| 10 || > f<sub>ω+1</sub>(2^^6/2-1) || WW(C(WB)(C(CC(WB))))
|> f<sub>ω+1</sub>(2^^6/2-1)
|WW(C(WB)(C(CC(WB))))
|-
|-
|...
| ... || ||
|
|
|-
|-
|15
| 15 || > f<sub>ω<sup>2^^18-1</sup></sub>(2) ||WW(C(WB)(B(BC(CC(WB)))(C(BC))))
|> f<sub>ω<sup>2^^18-1</sup></sub>(2)
|WW(C(WB)(B(BC(CC(WB)))(C(BC))))
|}
|}


Revision as of 05:10, 29 October 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. The tree can be evaluated 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
0 = 0
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 ≥ 1561 S(SI)(SS)(SS)SS
10 ≥ 1562 S(S(SI)(SS)(SS)SS)
11 ≥ 1563 SS(S(SI)(SS)(SS)SS)
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{4}2^^2^^258 S(SS(SSS)I(SSK))I(S(S(KS)K)I)
18 > 2{4}2^^2^^258 S(SS(SSS)I(SSK))I(S(S(KS)K)I)S
19 > 2{4}2^^^17 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
0 -1 = 0
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 ≥ 1561 SS(SS)(SSS)SSS
11 32 ≥ 1562 S(SS(SS)(SSS)SSS)
12 35 ≥ 1563 S(S(SS(SS)(SSS)SSS))
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(S(SK))(SSK)(SS(SK)(S(KS)K))
...
22 65 > 2^^^19 S(S(S(S(SK))))(S(SK))(S(SSK)(K(SS(SK)(S(KS)K)))
23 68 > 2{4}2^^^17 SS(S(SK))(SSK(SS(SK)(S(KS)K)))(S(K(S(SSK)))K)
24 71 > 2{4}2^^^17 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 with 3 new combinators B, C and W.

Bfgx = f(gx)

Cfxy = fyx

Kfx = f

Wfx = fxx

Champions for Ξ₀BCKW

n Value Champion
0 = 0
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{4}2^^^17 WW(WB(C(WC))(WB))
10 > fω+1(2^^6/2-1) WW(C(WB)(C(CC(WB))))
...
15 > fω2^^18-1(2) WW(C(WB)(B(BC(CC(WB)))(C(BC))))

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 Ξ

n Value Champion
0 = 0
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=9786"