SKI Calculus: Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
← Older editNewer edit →
VisualWikitext
m link LC
Azerty (talk | contribs)
370 edits
Line 15: Line 15:
! n !! Value !! Champion !! Discoverered by
! n !! Value !! Champion !! Discoverered by
|-
|-
| 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
|≥ 40
|≥ 40
|S(SS)S(SS)S
|S(SS)S(SS)S
|?
|
|-
|-
|8
|8
|≥ 41
|≥ 41
|SII(S(S(SS)))S
|SII(S(S(SS)))S
|?
|
|-
|-
|9
|9
|≥ 79
|≥ 79
|SII(SS(SSS))S
|SII(SS(SSS))S
|?
|
|-
|-
|10
|10
|≥ 164
|≥ 164
|SII(SS(SS(SS)))S
|SII(SS(SS(SS)))S
|?
|
|-
|-
|11
|11
|≥ 681
|≥ 681
|SII(SS(SS(SSS)))S
|SII(SS(SS(SSS)))S
|?
|
|-
|-
|12
|12
|≥ 1530
|≥ 1530
|SII(SS(SS(SS(SS))))S
|SII(SS(SS(SS(SS))))S
|?
|
|-
|-
|13
|13
|≥ 65537
|≥ 65537
|S(S(SI))I(S(S(KS)K)I)KK
|S(S(SI))I(S(S(KS)K)I)KK
|?
|
|-
|-
|14
|14
|≥ 2^256+1
|≥ 2^256
|S(S(S(SI)))I(S(S(KS)K)I)KK
|S(S(S(SI)))I(S(S(KS)K)I)KK
|?
|Komi Amiko
|-
|-
|15
|15
|> 2^2^2^2^21
|> 2^2^2^2^21
|S(S(SSS)I)I(S(S(KS)K)I)KK
|S(S(SSS)I)I(S(S(KS)K)I)KK
|?
|
|-
|-
|16
|16
|> 2^^19
|> 2^^19
|S(S(S(SSS))I)I(S(S(KS)K)I)KK
|S(S(S(SSS))I)I(S(S(KS)K)I)KK
|?
|
|-
|-
|17
|17
|> 2^^2^128
|> 2^^2^128
|SSK(S(S(KS)K)I)(S(SI(SI))I)KK
|SSK(S(S(KS)K)I)(S(SI(SI))I)KK
|?
|
|-
|-
|18
|18
|> 2^^2^2^2^2^21
|> 2^^2^2^2^2^21
|SSK(S(S(KS)K)I)(S(S(SSS)I)I)KK
|SSK(S(S(KS)K)I)(S(S(SSS)I)I)KK
|?
|
|-
|-
|19
|19
|> 2^^^2^128
|> 2^^^2^128
|S(SSK(S(SI(SI))I))I(S(S(KS)K)I)KK
|S(SSK(S(SI(SI))I))I(S(S(KS)K)I)KK
|?
|
|-
|-
|20
|20
|> 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)KK
|S(SSK(S(S(SSS)I)I))I(S(S(KS)K)I)KK
|?
|
|-
|-
|21
|21
|> 2^^^2^^19
|> 2^^^2^^19
|S(SSK(S(S(S(SSS))I)I))I(S(S(KS)K)I)KK
|S(SSK(S(S(S(SSS))I)I))I(S(S(KS)K)I)KK
|?
|
|-
|-
|25
|25
Line 115: Line 115:
! n !! bits !! Value !! Champion !! Discoverered by
! n !! bits !! Value !! Champion !! Discoverered by
|-
|-
| 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 131: Line 131:
|≥ 40
|≥ 40
|S(SS)S(SS)S
|S(SS)S(SS)S
|?
|
|-
|-
|8
|8
Line 137: Line 137:
|≥ 41
|≥ 41
|S(S(SS)S(SS)S)
|S(S(SS)S(SS)S)
|?
|
|-
|-
|9
|9
Line 143: Line 143:
|≥ 42
|≥ 42
|S(S(S(SS)S(SS)S))
|S(S(S(SS)S(SS)S))
|?
|
|-
|-
|10
|10
Line 149: Line 149:
|≥ 66
|≥ 66
|SS(SSS)(SS(SS))S
|SS(SSS)(SS(SS))S
|?
|
|-
|-
|11
|11
Line 155: Line 155:
|≥ 79
|≥ 79
|SS(SSS)(SS(SSS))S
|SS(SSS)(SS(SSS))S
|?
|
|-
|-
|12
|12
Line 161: Line 161:
|≥ 164
|≥ 164
|SS(SKK)(SS)(SS(SS))S
|SS(SKK)(SS)(SS(SS))S
|?
|
|-
|-
|13
|13
Line 167: Line 167:
|≥ 681
|≥ 681
|SS(SKK)(SS)(SS(SSS))S
|SS(SKK)(SS)(SS(SSS))S
|?
|
|-
|-
|14
|14
Line 173: Line 173:
|≥ 1530
|≥ 1530
|SS(SKK)(SS)(SS(SS(SS)))S
|SS(SKK)(SS)(SS(SS(SS)))S
|?
|
|-
|-
|15
|15
Line 179: Line 179:
|≥ 7811
|≥ 7811
|SS(SKK)(SS)(SS(SS(SSS)))S
|SS(SKK)(SS)(SS(SS(SSS)))S
|?
|
|}
|}


Revision as of 18:43, 12 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 -> I
  • Kxy -> Kx
  • Sxyz -> Sxz(yz)

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 Discoverered by
1 = 1 S
2 = 2 SS
3 = 3 SSS
4 = 4 SSSS
5 = 6 SSS(SS)
6 ≥ 17 SSS(SI)S
7 ≥ 40 S(SS)S(SS)S
8 ≥ 41 SII(S(S(SS)))S
9 ≥ 79 SII(SS(SSS))S
10 ≥ 164 SII(SS(SS(SS)))S
11 ≥ 681 SII(SS(SS(SSS)))S
12 ≥ 1530 SII(SS(SS(SS(SS))))S
13 ≥ 65537 S(S(SI))I(S(S(KS)K)I)KK
14 ≥ 2^256 S(S(S(SI)))I(S(S(KS)K)I)KK Komi Amiko
15 > 2^2^2^2^21 S(S(SSS)I)I(S(S(KS)K)I)KK
16 > 2^^19 S(S(S(SSS))I)I(S(S(KS)K)I)KK
17 > 2^^2^128 SSK(S(S(KS)K)I)(S(SI(SI))I)KK
18 > 2^^2^2^2^2^21 SSK(S(S(KS)K)I)(S(S(SSS)I)I)KK
19 > 2^^^2^128 S(SSK(S(SI(SI))I))I(S(S(KS)K)I)KK
20 > 2^^^2^2^2^2^21 S(SSK(S(S(SSS)I)I))I(S(S(KS)K)I)KK
21 > 2^^^2^^19 S(SSK(S(S(S(SSS))I)I))I(S(S(KS)K)I)KK
25 > Graham's Number SII(SI(SI(K(S(K(S(K(SS(K(K(S(S(KS)K)I)))))(SI)))K)))) 2014MELO03

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 Discoverered 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 ≥ 40 S(SS)S(SS)S
8 23 ≥ 41 S(S(SS)S(SS)S)
9 26 ≥ 42 S(S(S(SS)S(SS)S))
10 29 ≥ 66 SS(SSS)(SS(SS))S
11 32 ≥ 79 SS(SSS)(SS(SSS))S
12 35 ≥ 164 SS(SKK)(SS)(SS(SS))S
13 38 ≥ 681 SS(SKK)(SS)(SS(SSS))S
14 41 ≥ 1530 SS(SKK)(SS)(SS(SS(SS)))S
15 44 ≥ 7811 SS(SKK)(SS)(SS(SS(SSS)))S

See Also

Lower bounds of this function (archived)

SKI interpreter

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