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.

1. 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