SKI Calculus: Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
← Older editNewer edit →
VisualWikitext
Polygon (talk | contribs)
1,864 edits
Linked BBlambda
Δ⁵ (talk | contribs)
3 edits
Updated bounds and removed misinformation
Line 1: Line 1:
Busy Beaver for SKI calculus (we will call it BBSKI for now) is a variation of the [[Busy Beaver for lambda calculus|Busy Beaver problem for lambda calculus]].
Busy Beaver for SKI calculus (we will call it BB_SKI for now) is a variation of the [[Busy Beaver for lambda calculus|Busy Beaver problem for lambda calculus]].


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 the leftmost combinator.  
Like lambda calculus, SKI calculus has a process called beta-reduction. We change the tree according to any reducible redex.  


* <code>Ix -> I</code>
* <code>Ix -> I</code>
Line 12: Line 12:


We repeat this process and we say it terminates if the combinator cannot be beta-reduced.
We repeat this process and we say it terminates if the combinator cannot be beta-reduced.
BB_SKI(n) is defined as the size of the largest output of a terminating program of size n.


== Champions ==
== Champions ==
Line 27: Line 29:
| 5 || = 6 || SSS(SS) || ?
| 5 || = 6 || SSS(SS) || ?
|-
|-
| 6 || = 17 || SSS(SI)S || ?
| 6 || ≥ 17 || SSS(SI)S || ?
|-
|-
|7
|7
|≥ 18
|≥ 40
|S(SSS(SI)S)
|S(SS)S(SS)S
|?
|?
|-
|-
|8
|8
|≥ 19
|≥ 41
|SS(SSS(SI)S)
|SII(S(S(SS)))S
|?
|?
|-
|-
|9
|9
|≥ 519
|≥ 79
|SSI((S(SS)S)S)K
|SII(SS(SSS))S
|?
|?
|-
|-
|10
|10
|≥ 1041
|≥ 164
|SSI((S(SS)S)S)KS
|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+1
|S(S(S(SI)))I(S(S(KS)K)I)KK
|?
|-
|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
|?
|?
|}
|}
Line 63: Line 120:
| 3 || = 3 || SSS || ?
| 3 || = 3 || SSS || ?
|-
|-
| 4 || = 4 || <code>SSSS</code> || ?
| 4 || = 4 || SSSS || ?
|-
|-
| 5 || = 6 || <code>SSS(SS)</code> || ?
| 5 || = 6 || SSS(SS) || ?
|-
|-
| 6 || ≥ 8 || <code>SSS(SSS)</code> || ?
| 6 || ≥ 10 || SSS(SS)S || ?
|-
|-
|7
|7
|≥ 10
|≥ 40
|<code>SSS(SSSS)</code>
|S(SS)S(SS)S
|?
|?
|-
|-
|8
|8
|≥ 23
|≥ 41
|<code>SSS(S(SKS))S</code>
|S(S(SS)S(SS)S)
|?
|?
|}
|}


== See Also ==
== See Also ==
[https://komiamiko.me/math/ordinals/2020/06/21/ski-numerals.html Lower bounds of this function]
[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]


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

Revision as of 03:45, 7 May 2026

Busy Beaver for SKI calculus (we will call it BB_SKI for now) is a variation of the Busy Beaver problem for lambda calculus.

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.

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+1 S(S(S(SI)))I(S(S(KS)K)I)KK ?
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 ?

SK calculus

We can remove the I combinator and replace it by (SKS), (SKK) or any (SKx).

Champions

n Value Champion Discoverered by
1 = 1 S ?
2 = 2 SS ?
3 = 3 SSS ?
4 = 4 SSSS ?
5 = 6 SSS(SS) ?
6 ≥ 10 SSS(SS)S ?
7 ≥ 40 S(SS)S(SS)S ?
8 ≥ 41 S(S(SS)S(SS)S) ?

See Also

Lower bounds of this function (archived)

SKI interpreter

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