SKI Calculus: Difference between revisions
→Champions: Added new champion and discoverer name. |
Added BCKW system. |
||
| Line 3: | Line 3: | ||
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. We change the tree according to any reducible redex. | ||
Ix | * Sxyz → xz(yz) | ||
* Kxy → 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 169: | Line 169: | ||
|≥ 7811 | |≥ 7811 | ||
|SS(SKK)(SS)(SS(SS(SSS)))S | |SS(SKK)(SS)(SS(SS(SSS)))S | ||
| | |||
|} | |||
TODO: Champions analysis. | |||
== BCKW system == | |||
BCKW system is a variation of SK calculus that replace the S combinator by 3 other simpler combinators. | |||
* Bxyz → x(yz) | |||
* Cxyz → xzy | |||
* Kxy → x | |||
* Wxy → xyy | |||
=== Champions === | |||
{| class="wikitable" | |||
! n !! Value !! Champion !! Discovered by | |||
|- | |||
| 1 || = 1 || B || | |||
|- | |||
| 2 || = 2 || BB || | |||
|- | |||
| 3 || = 3 || BBB || | |||
|- | |||
| 4 || = 5 || WB(BB) || | |||
|- | |||
| 5 || = 7 || WB(BBB) || | |||
|- | |||
|6 | |||
|= 11 | |||
|WB(WB(BB)) | |||
| | |||
|- | |||
|7 | |||
|= 15 | |||
|WB(WB(BBB)) | |||
| | |||
|- | |||
|8 | |||
|= 23 | |||
|WB(WB(WB(BB))) | |||
| | |||
|- | |||
|9 | |||
|= 31 | |||
|WB(WB(WB(BBB))) | |||
| | |||
|- | |||
|10 | |||
|= 47 | |||
|WB(WB(WB(WB(BB)))) | |||
| | | | ||
|} | |} | ||
Revision as of 08:00, 25 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.
- Sxyz → xz(yz)
- Kxy → x
- 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 (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 | Discovered by |
|---|---|---|---|
| 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 | "Boone" |
| 8 | ≥ 80 | SSK(S(SS)S)S | "Boone" |
| 9 | ≥ 169 | S(SS)(SS)(SS)SS | "Boone" |
| 10 | ≥ 376 | S(S(SS(KK)))(SS)(SS) | "Boone" |
| 11 | ≥ 912 | S(SS)S(SS)(S(S(KS))S) | "Boone" |
| 12 | ≥ 196606 | S(S(SI))I(S(S(KS)K)I)K | Komi Amiko |
| 13 | > 2^2^2^21 | S(S(SSS)I)I(S(S(KS)K)I) | Komi Amiko |
| 14 | > 2^^18 | S(S(S(SSS))I)I(S(S(KS)K)I) | Komi Amiko |
| 15 | > 2^^2^128 | SSK(S(S(KS)K)I)(S(SSSI)I) | Komi Amiko |
| 16 | > 2^^2^2^2^2^21 | SSK(S(S(KS)K)I)(S(S(SSS)I)I) | Komi Amiko |
| 17 | > 2^^^2^128 | S(SSK(S(SSSI)I))I(S(S(KS)K)I) | Komi Amiko |
| 18 | > 2{65535}4 | S(S(SI))I(S(K(S(SI(K(S(S(KS)K)I)))))K) | Komi Amiko |
| 19 | > 2{65535}4 | S(S(S(SI)))I(S(K(S(SI(K(S(S(KS)K)I)))))K) | Komi Amiko |
| 20 | > Graham's Number | S(S(S(SI)))I(S(K(S(SS(K(K(S(S(KS)K)I))))))K) | Komi Amiko |
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 | Discovered 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 | ≥ 41 | SSS(S(SS))S | "Boone" |
| 8 | 23 | ≥ 80 | SSK(S(SS)S)S | "Boone" |
| 9 | 26 | ≥ 169 | S(SS)(SS)(SS)SS | "Boone" |
| 10 | 29 | ≥ 376 | S(S(SS(KK)))(SS)(SS) | "Boone" |
| 11 | 32 | ≥ 912 | S(SS)S(SS)(S(S(KS))S) | "Boone" |
| 12 | 35 | ≥ 913 | S(S(SS)S(SS)(S(S(KS))S)) | "Boone" |
| 13 | 38 | ≥ 914 | S(S(S(SS)S(SS)(S(S(KS))S))) | "Boone" |
| 14 | 41 | ≥ 1530 | SS(SKK)(SS)(SS(SS(SS)))S | |
| 15 | 44 | ≥ 7811 | SS(SKK)(SS)(SS(SS(SSS)))S |
TODO: Champions analysis.
BCKW system
BCKW system is a variation of SK calculus that replace the S combinator by 3 other simpler combinators.
- Bxyz → x(yz)
- Cxyz → xzy
- Kxy → x
- Wxy → xyy
Champions
| n | Value | Champion | Discovered by |
|---|---|---|---|
| 1 | = 1 | B | |
| 2 | = 2 | BB | |
| 3 | = 3 | BBB | |
| 4 | = 5 | WB(BB) | |
| 5 | = 7 | WB(BBB) | |
| 6 | = 11 | WB(WB(BB)) | |
| 7 | = 15 | WB(WB(BBB)) | |
| 8 | = 23 | WB(WB(WB(BB))) | |
| 9 | = 31 | WB(WB(WB(BBB))) | |
| 10 | = 47 | WB(WB(WB(WB(BB)))) |
Oracles
We can extend BB_SKI with oracles, making it stronger than BB. For example, we can add an oracle combinator O where Ofxy=x iff for all z fz=z, and y otherwise. The resulting busy beaver, known as the Xi function, is estimated to be faster-growing than ordinal oracle busy beavers with the oracle degree <= w_1^CK. 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 Xi_2.