SKI 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. 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)) |
| ... |
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)))) |
Thutus calculus
Thutus is a combinatorial rewriting system whose syntax and expression application follow the SKI calculus.
- Alphabet
For each integer n ≥ 1, the available alphabet is: L₁, L₂, ..., Lₙ.
2. Initial expression
The initial expression contains exactly n occurrences of symbols. Parentheses do not count toward the size.
3. Arity
Each symbol Lₖ has between 1 and k−1 arguments, with the exception of L₁, which always follows the rule: L₁ x1 → x1. The arguments x1, x2, x3, etc., may be arbitrarily complex expressions.
4. Rewriting rules
The rules for each symbol are chosen prior to execution and remain fixed throughout the execution. For each symbol Lₖ, the right-hand side of its rule contains between 1 and k occurrences of arguments, excluding parentheses. Arguments may be reused, rearranged, nested, or deleted. Examples: L₄ x1 x2 → x1 (x2 (x1 x1)) L₄ x1 x2 x3 → x3 (x1 x2)
5. Reduction and termination
At each step, a rule may be applied to any reducible occurrence, as in the SKI calculus. An expression terminates when it reaches a normal form—that is, when no further rules can be applied. Expressions that diverge do not contribute to the maximum.
6. Definition of T(n)
T(n) (also written as Ξ₀T) the maximum number of symbols in the final normal form, taken over all initial expressions of size exactly n and all admissible Thutus rule systems. The available alphabet is L₁, ..., Lₙ. The rules are chosen at the outset, must satisfy the aforementioned constraints, and remain fixed throughout the execution.
Champions for T(n) / Ξ₀T
| n | Value | Champion Initiate Term | Champion Rule |
|---|---|---|---|
| 0 | = 0 | ||
| 1 | = 1 | L1 | L1 x1 -> x1 |
| 2 | = 1 | L1L2 | L1 x1 -> x1
L2 x1 -> x1 x1 |
| 3 | = 4 | L2(L3L3) | L1 x1 -> x1
L2 x1 -> x1 x1 L3 x1 x2 -> x1 (x1 x2) |
| 4 | ≥ 522 | L3(L3(L4L4)) | L1 x1 -> x1
L2 x1 -> x1 x1 L3 x1 -> (x1 x1) x1 L4 x1 x2 x3 -> x1 x2 (x2 x3) |
| 5 | ≥ fω+1(2^^6/2) | L1(L2(L4(L5L3)) | L1 x1 -> x1
L2 x1 -> x1 x1 L3 x1 x2 -> x1 (x1 x2) L4 x1 x2 -> x2 (x2 x1) L5 x1 x2 x3 -> x3 x2 x1 |
| ... | |||
| 15 | > fω2^^18-1(2) | L4L4(L5(L4L6)(L6(L6L5(L5L5(L4L6)))(L5(L6L5)))) | L1 x1 -> x1
L2 x1 -> x1 L3 x1 x2 -> x1 L4 x1 x2 -> x1 x2 x2 L5 x1 x2 x3 -> x1 x3 x2 L6 x1 x2 x3 -> x1 (x2 x3) L7 x1 -> x1 L8 x1 -> x1 L9 x1 -> x1 L10 x1 -> x1 L11 x1 -> x1 L12 x1 -> x1 L13 x1 -> x1 L14 x1 -> x1 L15 x1 -> x1 |
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
- Lower bounds of this function (archived)
- SKI interpreter