SKI Calculus: Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
Azerty (talk | contribs)
→Champions: Updated SKI champions
Azerty (talk | contribs)
→Champions: Added new champion and discoverer name.
Line 30: Line 30:
|≥ 41
|≥ 41
|SSS(S(SS))S
|SSS(S(SS))S
|
|"Boone"
|-
|-
|8
|8
|≥ 80
|≥ 80
|SSK(S(SS)S)S
|SSK(S(SS)S)S
|
|"Boone"
|-
|-
|9
|9
|≥ 169
|≥ 169
|S(SS)(SS)(SS)SS
|S(SS)(SS)(SS)SS
|
|"Boone"
|-
|-
|10
|10
|≥ 376
|≥ 376
|S(S(SS(KK)))(SS)(SS)
|S(S(SS(KK)))(SS)(SS)
|
|"Boone"
|-
|-
|11
|11
|≥ 681
|≥ 912
|SII(SS(SS(SSS)))S
|S(SS)S(SS)(S(S(KS))S)
|
|"Boone"
|-
|-
|12
|12
|≥ 196606
|≥ 196606
|S(S(SI))I(S(S(KS)K)I)K
|S(S(SI))I(S(S(KS)K)I)K
|
|Komi Amiko
|-
|-
|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)
|
|Komi Amiko
|-
|-
|14
|14
|> 2^^18
|> 2^^18
|S(S(S(SSS))I)I(S(S(KS)K)I)
|S(S(S(SSS))I)I(S(S(KS)K)I)
|
|Komi Amiko
|-
|-
|15
|15
|> 2^^2^128
|> 2^^2^128
|SSK(S(S(KS)K)I)(S(SSSI)I)
|SSK(S(S(KS)K)I)(S(SSSI)I)
|
|Komi Amiko
|-
|-
|16
|16
|> 2^^2^2^2^2^21
|> 2^^2^2^2^2^21
|SSK(S(S(KS)K)I)(S(S(SSS)I)I)
|SSK(S(S(KS)K)I)(S(S(SSS)I)I)
|
|Komi Amiko
|-
|-
|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)
|
|Komi Amiko
|-
|-
|18
|18
|> 2{65535}4
|> 2{65535}4
|S(S(SI))I(S(K(S(SI(K(S(S(KS)K)I)))))K)
|S(S(SI))I(S(K(S(SI(K(S(S(KS)K)I)))))K)
|
|Komi Amiko
|-
|-
|19
|19
|> 2{65535}4
|> 2{65535}4
|S(S(S(SI)))I(S(K(S(SI(K(S(S(KS)K)I)))))K)
|S(S(S(SI)))I(S(K(S(SI(K(S(S(KS)K)I)))))K)
|
|Komi Amiko
|-
|-
|20
|20
|> Graham's Number
|> 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)
|
|Komi Amiko
|}
|}


Line 121: Line 121:
|≥ 41
|≥ 41
|SSS(S(SS))S
|SSS(S(SS))S
|
|"Boone"
|-
|-
|8
|8
Line 127: Line 127:
|≥ 80
|≥ 80
|SSK(S(SS)S)S
|SSK(S(SS)S)S
|
|"Boone"
|-
|-
|9
|9
Line 133: Line 133:
|≥ 169
|≥ 169
|S(SS)(SS)(SS)SS
|S(SS)(SS)(SS)SS
|
|"Boone"
|-
|-
|10
|10
Line 139: Line 139:
|≥ 376
|≥ 376
|S(S(SS(KK)))(SS)(SS)
|S(S(SS(KK)))(SS)(SS)
|
|"Boone"
|-
|-
|11
|11
| 32
| 32
|≥ 377
|≥ 912
|S(S(S(SS(KK)))(SS)(SS))
|S(SS)S(SS)(S(S(KS))S)
|
|"Boone"
|-
|-
|12
|12
| 35
| 35
|≥ 378
|≥ 913
|S(S(S(S(SS(KK)))(SS)(SS)))
|S(S(SS)S(SS)(S(S(KS))S))
|
|"Boone"
|-
|-
|13
|13
| 38
| 38
|≥ 681
|≥ 914
|SS(SKK)(SS)(SS(SSS))S
|S(S(S(SS)S(SS)(S(S(KS))S)))
|
|"Boone"
|-
|-
|14
|14

Revision as of 06:43, 25 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.

Ix -> x Kfx -> f Sfgx -> fx(gx)

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) 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 Discovered by
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 "Boone"
8 ≥ 80 SSK(S(SS)S)S "Boone"
9 ≥ 169 S(SS)(SS)(SS)SS "Boone"
10 ≥ 376 S(S(SS(KK)))(SS)(SS) "Boone"
11 ≥ 912 S(SS)S(SS)(S(S(KS))S) "Boone"
12 ≥ 196606 S(S(SI))I(S(S(KS)K)I)K Komi Amiko
13 > 2^2^2^21 S(S(SSS)I)I(S(S(KS)K)I) Komi Amiko
14 > 2^^18 S(S(S(SSS))I)I(S(S(KS)K)I) Komi Amiko
15 > 2^^2^128 SSK(S(S(KS)K)I)(S(SSSI)I) Komi Amiko
16 > 2^^2^2^2^2^21 SSK(S(S(KS)K)I)(S(S(SSS)I)I) Komi Amiko
17 > 2^^^2^128 S(SSK(S(SSSI)I))I(S(S(KS)K)I) Komi Amiko
18 > 2{65535}4 S(S(SI))I(S(K(S(SI(K(S(S(KS)K)I)))))K) Komi Amiko
19 > 2{65535}4 S(S(S(SI)))I(S(K(S(SI(K(S(S(KS)K)I)))))K) Komi Amiko
20 > Graham's Number S(S(S(SI)))I(S(K(S(SS(K(K(S(S(KS)K)I))))))K) Komi Amiko

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 Discovered by
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 "Boone"
8 23 ≥ 80 SSK(S(SS)S)S "Boone"
9 26 ≥ 169 S(SS)(SS)(SS)SS "Boone"
10 29 ≥ 376 S(S(SS(KK)))(SS)(SS) "Boone"
11 32 ≥ 912 S(SS)S(SS)(S(S(KS))S) "Boone"
12 35 ≥ 913 S(S(SS)S(SS)(S(S(KS))S)) "Boone"
13 38 ≥ 914 S(S(S(SS)S(SS)(S(S(KS))S))) "Boone"
14 41 ≥ 1530 SS(SKK)(SS)(SS(SS(SS)))S
15 44 ≥ 7811 SS(SKK)(SS)(SS(SS(SSS)))S

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=z, and y otherwise. The resulting busy beaver, known as the Xi 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 Xi_2.

See Also