SKI Calculus: Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
← Older edit
VisualWikitext
Loader3229 (talk | contribs)
131 edits
Δ⁵ (talk | contribs)
120 edits
m un-overestimated bound
 
(12 intermediate revisions by 3 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|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.  


Sfgx => fx(gx)
Sfgx = fx(gx)


Kfx => f
Kfx = f


Ix => x
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.
Line 78: Line 78:
|-
|-
|19
|19
|> 2^^^^2^^^19
|> 2^^^^2^^^17
|SSI(SSK(S(S(KS)K)I))(S(K(S(SSK)))K)
|SSI(SSK(S(S(KS)K)I))(S(K(S(SSK)))K)
|-
|-
Line 139: Line 139:
|7
|7
| 20
| 20
|≥ 41
|= 41
|SSS(S(SS))S
|SSS(S(SS))S
|-
|-
Line 204: Line 204:
|23
|23
|68
|68
|> 2^^^^2^^^19
|> 2^^^^2^^^17
|SS(S(SK))(SSK(SS(SK)(S(KS)K)))(S(K(S(SSK)))K)
|SS(S(SK))(SSK(SS(SK)(S(KS)K)))(S(K(S(SSK)))K)
|-
|-
|24
|24
|71
|71
|> 2^^^^2^^^19
|> 2^^^^2^^^17
|S(SS(S(SK))(SSK(SS(SK)(S(KS)K)))(S(K(S(SSK)))K))
|S(SS(S(SK))(SSK(SS(SK)(S(KS)K)))(S(K(S(SSK)))K))
|-
|-
Line 225: Line 225:


== BCKW system ==
== BCKW system ==
BCKW system is a variation of SK calculus that replace the S combinator by 3 new combinators B, C and W.
BCKW system is a variation of SK calculus that replace the S combinator with 3 new combinators B, C and W.


Bfgx => f(gx)
Bfgx = f(gx)


Cfxy => fyx
Cfxy = fyx


Kfx => f
Kfx = f


Wfx => fxx
Wfx = fxx


=== Champions for Ξ₀<sub>BCKW</sub> ===
=== Champions for Ξ₀<sub>BCKW</sub> ===
Line 245: Line 245:
| 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
Line 262: Line 262:
|-
|-
|9
|9
|> 2{5}2^^^^2^^^19
|> 2{5}2^^^^2^^^17
|WW(WB(C(WC))(WB))
|WW(WB(C(WC))(WB))
|-
|-
Line 268: Line 268:
|> f<sub>ω+1</sub>(2^^6/2-1)
|> f<sub>ω+1</sub>(2^^6/2-1)
|WW(C(WB)(C(CC(WB))))
|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))))
|}
|}


== Oracles ==
== 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>. 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 Ξ₂.
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 Ξ<sub>SKIO</sub> ===
=== Champions for Ξ ===
{| class="wikitable"
{| class="wikitable"
! n !! Value !! Champion  
! n !! Value !! Champion  
Line 289: Line 297:
|-
|-
| 6 || = 17 || SSS(SI)S  
| 6 || = 17 || SSS(SI)S  
|-
| 7 || ≥ 51 || SSS(SI)SO
|-
| 8 || ≥ 137 || SSK(S(SSO))S
|}
|}


Latest revision as of 08:45, 18 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
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 ≥ 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^^^^2^^2^^258 S(SS(SSS)I(SSK))I(S(S(KS)K)I)
18 > 2^^^^2^^2^^258 S(SS(SSS)I(SSK))I(S(S(KS)K)I)S
19 > 2^^^^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
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 ≥ 1530 S(SS)(SS)(SS(SS(SS)))S
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(SKS)(SSK)(SS(SK)(S(KS)K))
...
22 65 > 2^^^19 S(S(S(S(SK))))(SKS)(S(SSK)(K(SS(SK)(S(KS)K)))
23 68 > 2^^^^2^^^17 SS(S(SK))(SSK(SS(SK)(S(KS)K)))(S(K(S(SSK)))K)
24 71 > 2^^^^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
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^^^^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
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=9272"