SKI Calculus: Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
← Older edit
VisualWikitext
C7X (talk | contribs)
162 edits
Replace with archived version
Δ⁵ (talk | contribs)
158 edits
m new bounds
 
(108 intermediate revisions by 8 users not shown)
Line 1: Line 1:
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, SKI calculus has a process called beta-reduction. We change the tree according to any reducible redex.  
Like [[Lambda Calculus|lambda calculus]], SKI calculus has a process called beta-reduction. The tree can be evaluated according to any reducible redex.  


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


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.
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 ('''BB_SKI''') is a variation of the [[Busy Beaver for lambda calculus|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.
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  
|-
| 0 || = 0 ||
|-
| 1 || = 1 || S
|-
| 2 || = 2 || SS
|-
| 3 || = 3 || SSS
|-
| 4 || = 4 || SSSS
|-
|-
| 1 || = 1 || S || ?
| 5 || = 6 || SSS(SS)
|-
|-
| 2 || = 2 || SS || ?
| 6 || = 17 || SSS(SI)S
|-
|-
| 3 || = 3 || SSS || ?
| 7 || ≥ 41 || SSS(S(SS))S
|-
|-
| 4 || = 4 || SSSS || ?
| 8 || ≥ 80 || SSK(S(SS)S)S
|-
|-
| 5 || = 6 || SSS(SS) || ?
| 9 || ≥ 1561 || S(SI)(SS)(SS)SS
|-
|-
| 6 || ≥ 17 || SSS(SI)S || ?
| 10 || ≥ 1562 || S(S(SI)(SS)(SS)SS)
|-
|-
|7
| 11 || ≥ 1563 || SS(S(SI)(SS)(SS)SS)
|≥ 40
|S(SS)S(SS)S
|?
|-
|-
|8
| 12 || ≥ 2^2^513 × 8 - 2 || S(SI)(SSK)(S(S(KS)K)I)
|≥ 41
|SII(S(S(SS)))S
|?
|-
|-
|9
| 13 || > 2^^2^^2^258 || SI(SI)(SSK)(S(S(KS)K)I)
|≥ 79
|SII(SS(SSS))S
|?
|-
|-
|10
| 14 || > 2^^2^^2^258 || SI(SI)(SSK)(S(S(KS)K)I)S
|≥ 164
|SII(SS(SS(SS)))S
|?
|-
|-
|11
| 15 || > 2^^2^^2^^34 || S(S(SI)I(SSK))I(S(S(KS)K)I)
|≥ 681
|SII(SS(SS(SSS)))S
|?
|-
|-
|12
| 16 || > 2{3}19 || S(S(SI))I(S(SSK)(K(S(S(KS)K)I)))
|≥ 1530
|SII(SS(SS(SS(SS))))S
|?
|-
|-
|13
| 17 || > 2{4}2^^2^^258 || S(SS(SSS)I(SSK))I(S(S(KS)K)I)
|≥ 65537
|S(S(SI))I(S(S(KS)K)I)KK
|?
|-
|-
|14
| 18 || > 2{4}2^^2^^258 || S(SS(SSS)I(SSK))I(S(S(KS)K)I)S
|≥ 2^256+1
|S(S(S(SI)))I(S(S(KS)K)I)KK
|?
|-
|-
|15
| 19 || > 2{4}2{3}17 || SSI(SSK(S(S(KS)K)I))(S(K(S(SSK)))K)
|> 2^2^2^2^21
|S(S(SSS)I)I(S(S(KS)K)I)KK
|?
|-
|-
|16
| 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)
|> 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
| 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)
|> 2^^2^2^2^2^21
|SSK(S(S(KS)K)I)(S(S(SSS)I)I)KK
|?
|-
|-
|19
| 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))
|> 2^^^2^128
|S(SSK(S(SI(SI))I))I(S(S(KS)K)I)KK
|?
|-
|-
|20
| 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)
|> 2^^^2^2^2^2^21
|S(SSK(S(S(SSS)I)I))I(S(S(KS)K)I)KK
|?
|-
|-
|21
| 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))
|> 2^^^2^^19
|S(SSK(S(S(S(SSS))I)I))I(S(S(KS)K)I)KK
|?
|-
|-
|25
| 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)
|> Graham's Number
|-
|SII(SI(SI(K(S(K(S(K(SS(K(K(S(S(KS)K)I)))))(SI)))K))))
| 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))
| 2014MELO03
|-
| ... || ||
|-
| 61 || > f<sub>ε₀</sub> (255) || SSK(S(S(KS)K)I)(S(S(S(SI(K(S(K(SS(K(SI(KI)))))(S(K(SS(K(S(K(S(K(S(K(SS(K(S(K(S(S(KS)K)(KK)))S))))K))S))K))))K))))(K(KI)))(K(SS(KI))))I)
|-
| ... || ||
|-
| 71 || > f<sub>ψ(Ω<sub>ω</sub>)</sub> (f<sub>ω<sup>ω65536</sup></sub> (2)) || SSK(S(S(KS)K)I)(S(S(S(S(S(K(SS(KI))))(K(S(K(S(K(S(K(S(K(SS(KI)))))(S(S(K(S(KS)K))S)(KK))))))(S(K(S(S(K(S(KS)K))S)(KK)))(S(K(S(S(K(SS(KI)))(SS(KI)))))K)))))I)I)I)
|}
|}


Line 111: Line 85:
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.
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 !! bits !! Value !! Champion !! Discoverered by
! n !! bits !! Value !! Champion  
|-
|-
| 1 || 2 || = 1 || S || ?
| 0 || -1 || = 0 ||
|-
|-
| 2 || 5 || = 2 || SS || ?
| 1 || 2 || = 1 || S
|-
|-
| 3 || 8 || = 3 || SSS || ?
| 2 || 5 || = 2 || SS
|-
|-
| 4 || 11 || = 4 || SSSS || ?
| 3 || 8 || = 3 || SSS
|-
|-
| 5 || 14 || = 6 || SSS(SS) || ?
| 4 || 11 || = 4 || SSSS
|-
|-
| 6 || 17 || ≥ 10 || SSS(SS)S || ?
| 5 || 14 || = 6 || SSS(SS)  
|-
|-
|7
| 6 || 17 || = 10 || SSS(SS)S  
| 20
|≥ 40
|S(SS)S(SS)S
|?
|-
|-
|8
| 7 || 20 || = 41 || SSS(S(SS))S
| 23
|≥ 41
|S(S(SS)S(SS)S)
|?
|-
|-
|9
| 8 || 23 || ≥ 80 || SSK(S(SS)S)S
| 26
|≥ 42
|S(S(S(SS)S(SS)S))
|?
|-
|-
|10
| 9 || 26 || ≥ 169 || S(SS)(SS)(SS)SS
| 29
|≥ 66
|SS(SSS)(SS(SS))S
|?
|-
|-
|11
| 10 || 29 || ≥ 1561 || SS(SS)(SSS)SSS
| 32
|≥ 79
|SS(SSS)(SS(SSS))S
|?
|-
|-
|12
| 11 || 32 || ≥ 1562 || S(SS(SS)(SSS)SSS)
| 35
|≥ 164
|SS(SKK)(SS)(SS(SS))S
|?
|-
|-
|13
| 12 || 35 || ≥ 1563 || S(S(SS(SS)(SSS)SSS))
| 38
|≥ 681
|SS(SKK)(SS)(SS(SSS))S
|?
|-
|-
|14
| 13 || 38 || ≥ 7811 || S(SS)(SS)(SS(SS(SSS)))S
| 41
|≥ 1530
|SS(SKK)(SS)(SS(SS(SS)))S
|?
|-
|-
|15
| 14 || 41 || ≥ 2^2097156 × 13 - 2 || SSS(SSK)(SS(SK)(S(KS)K))
| 44
|-
|≥ 7811
| 15 || 44 || ≥ 2^2^2097156 × 3 - 2 || SSS(SSK)(SS(SK)(S(KS)K))S
|SS(SKK)(SS)(SS(SS(SSS)))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{3}19 ||S(S(S(S(SK))))(S(SK))(S(SSK)(K(SS(SK)(S(KS)K)))
|-
| 23 || 68 || > 2{4}2{3}17 || SS(S(SK))(SSK(SS(SK)(S(KS)K)))(S(K(S(SSK)))K)
|-
| 24 || 71 || > 2{4}2{3}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<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 calculus ==
BCKW calculus 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 Ξ₀<sub>BCKW</sub> ===
{| class="wikitable"
! 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{3}17 || WW(C(WC)(WB))
|-
| 8 || > 2{3}2{3}17 || W(WW)(C(WC)(WB))
|-
| 9 || > 2{5}2{4}2{3}17 || WW(WB(C(WC))(WB))
|-
| 10 || > f<sub>ω+1</sub>(2^^6/2-1) || WW(C(WB)(C(CC(WB))))
|-
| ... || ||
|-
| 15 || > f<sub>ω<sup>2^^18-1</sup></sub>(2) || WW(C(WB)(B(BC(CC(WB)))(C(BC))))
|-
| ... || ||
|-
| 22 || > f<sub>ψ(Ω<sub>ω</sub>)</sub> (f<sub>ω<sup>ω65536</sup></sub> (2)) || WB(W(W(W(C(BW)(B(B(B(BW)C))(BC(C(BWW))))))))(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 Ξ ===
{| class="wikitable"
! 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 ==
== See Also ==
[https://web.archive.org/web/20250217071017/https://komiamiko.me/math/ordinals/2020/06/21/ski-numerals.html Lower bounds of this function] (archived)
* [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]
[https://dallaylaen.github.io/ski-interpreter/ SKI interpreter]


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

Latest revision as of 13:05, 9 November 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{3}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{3}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))
...
61 > fε₀ (255) SSK(S(S(KS)K)I)(S(S(S(SI(K(S(K(SS(K(SI(KI)))))(S(K(SS(K(S(K(S(K(S(K(SS(K(S(K(S(S(KS)K)(KK)))S))))K))S))K))))K))))(K(KI)))(K(SS(KI))))I)
...
71 > fψ(Ωω) (fωω65536 (2)) SSK(S(S(KS)K)I)(S(S(S(S(S(K(SS(KI))))(K(S(K(S(K(S(K(S(K(SS(KI)))))(S(S(K(S(KS)K))S)(KK))))))(S(K(S(S(K(S(KS)K))S)(KK)))(S(K(S(S(K(SS(KI)))(SS(KI)))))K)))))I)I)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{3}19 S(S(S(S(SK))))(S(SK))(S(SSK)(K(SS(SK)(S(KS)K)))
23 68 > 2{4}2{3}17 SS(S(SK))(SSK(SS(SK)(S(KS)K)))(S(K(S(SSK)))K)
24 71 > 2{4}2{3}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 calculus

BCKW calculus 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{3}17 WW(C(WC)(WB))
8 > 2{3}2{3}17 W(WW)(C(WC)(WB))
9 > 2{5}2{4}2{3}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))))
...
22 > fψ(Ωω) (fωω65536 (2)) WB(W(W(W(C(BW)(B(B(B(BW)C))(BC(C(BWW))))))))(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 Ξ

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=10480"