Busy Beaver for SKI calculus: Difference between revisions
Jump to navigation
Jump to search
Created page with "Busy Beaver for SKI calculus (we will call it BBSKI for now) is a variation of the Busy Beaver problem for lambda calculus. == Champions == {| class="wikitable" ! n !! Value !! Champion !! Discoverered by |- | 1 || = 1 || S || ? |- | 2 || = 2 || SS || ? |- | 3 || = 3 || SSS || ? |- | 4 || = 4 || SSSS || ? |- | 5 || = 6 || SSS(SS) || ? |- | 6 || >= 8 || SSS(SSS) || ? |} == See Also == [https://komiamiko.me/math/ordinals/2020/06/21/ski-numerals.html Lower bounds of this..." |
used proper greater/equals sign |
||
| (4 intermediate revisions by 2 users not shown) | |||
| Line 1: | Line 1: | ||
Busy Beaver for SKI calculus (we will call it BBSKI for now) is a variation of the Busy Beaver problem for lambda calculus. | Busy Beaver for SKI calculus (we will call it BBSKI 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 <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. | |||
* <code>Ix -> I</code> | |||
* <code>Kxy -> Kx</code> | |||
* <code>Sxyz -> Sxz(yz)</code> | |||
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. | |||
== Champions == | == Champions == | ||
| Line 15: | Line 27: | ||
| 5 || = 6 || SSS(SS) || ? | | 5 || = 6 || SSS(SS) || ? | ||
|- | |- | ||
| 6 || >= 8 || SSS(SSS) || ? | | 6 || = 17 || SSS(SI)S || ? | ||
|- | |||
|7 | |||
|≥ 18 | |||
|S(SSS(SI)S) | |||
|? | |||
|- | |||
|8 | |||
|≥ 19 | |||
|SS(SSS(SI)S) | |||
|? | |||
|- | |||
|9 | |||
|≥ 519 | |||
|SSI((S(SS)S)S)K | |||
|? | |||
|- | |||
|10 | |||
|≥ 1041 | |||
|SSI((S(SS)S)S)KS | |||
|? | |||
|} | |||
== SK calculus == | |||
We can remove the <code>I</code> combinator and replace it by <code>(SKS)</code>, <code>(SKK)</code> or any <code>(SKx)</code>. | |||
=== Champions === | |||
{| class="wikitable" | |||
! n !! Value !! Champion !! Discoverered by | |||
|- | |||
| 1 || = 1 || S || ? | |||
|- | |||
| 2 || = 2 || SS || ? | |||
|- | |||
| 3 || = 3 || SSS || ? | |||
|- | |||
| 4 || = 4 || <code>SSSS</code> || ? | |||
|- | |||
| 5 || = 6 || <code>SSS(SS)</code> || ? | |||
|- | |||
| 6 || ≥ 8 || <code>SSS(SSS)</code> || ? | |||
|- | |||
|7 | |||
|≥ 10 | |||
|<code>SSS(SSSS)</code> | |||
|? | |||
|- | |||
|8 | |||
|≥ 23 | |||
|<code>SSS(S(SKS))S</code> | |||
|? | |||
|} | |} | ||
== 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] | ||
[[Category:Functions]] | |||
Latest revision as of 13:21, 25 December 2025
Busy Beaver for SKI calculus (we will call it BBSKI 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 the leftmost combinator.
Ix -> IKxy -> KxSxyz -> 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.
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 | ≥ 18 | S(SSS(SI)S) | ? |
| 8 | ≥ 19 | SS(SSS(SI)S) | ? |
| 9 | ≥ 519 | SSI((S(SS)S)S)K | ? |
| 10 | ≥ 1041 | SSI((S(SS)S)S)KS | ? |
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 | ≥ 8 | SSS(SSS) |
? |
| 7 | ≥ 10 | SSS(SSSS)
|
? |
| 8 | ≥ 23 | SSS(S(SKS))S
|
? |