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. We change the tree 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. BB_SKI(n) is defined as the size of the largest output of a terminating program of size n.

Champions

n	Value	Champion
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	≥ 169	S(SS)(SS)(SS)SS
10	≥ 376	S(S(SS(KK)))(SS)(SS)
11	≥ 912	S(SS)S(SS)(S(S(KS))S)
12	≥ 196606	S(S(SI))I(S(S(KS)K)I)K
13	> 2^2^2^21	S(S(SSS)I)I(S(S(KS)K)I)
14	> 2^^33	SI(SSK)(SSK(S(S(KS)K)I))
15	> 2^^2^^33	SII(SSK(SSK(S(S(KS)K)I)))
16	> 2^^2^^65	S(SI)I(SSK(SSK(S(S(KS)K)I)))
17	> 2^^^2^128	S(SSK(S(SSSI)I))I(S(S(KS)K)I)
18	> 2^^^2^2^2^2^21	S(SSK(S(S(SSS)I)I))I(S(S(KS)K)I))
19	> 2^^^2^^19	S(SSK(S(S(S(SSS))I)I))I(S(S(KS)K)I)
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
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	≥ 376	S(S(SS(KK)))(SS)(SS)
11	32	≥ 912	S(SS)S(SS)(S(S(KS))S)
12	35	≥ 913	S(S(SS)S(SS)(S(S(KS))S))
13	38	≥ 914	S(S(S(SS)S(SS)(S(S(KS))S)))
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 new combinators.

Bfgx => f(gx)

Cfxy => fyx

Kfx => f

Wfx => fxx

Champions for Ξ₀_BCKW

n	Value	Champion
1	= 1	B
2	= 2	BB
3	= 3	BBB
4	≥ 11	WW(WB)
5	≥ 47	W(WW)(WB)
6	≥ 3*2^66-1	WB(WW)(WB)
7	> 2^2^2^20	WB(W(WW))(WB)
8	> 2^^34	WC(WW(WB))(WW)
9	> 2^^2^^33	W(WK)(WC(WC(WB)))
10	> 2^^2^^33	W(W(WK))(WC(WC(WB)))
11	> fω (2^2^18)	WB(W(C(WC)(C(WC))))(WB)
12	> fω+1 (2^2^18-2)	W(WC(W(C(WC)(C(WC)))))(WB)

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 beta-reduces to z, and y otherwise. The resulting busy beaver, known as the Ξ 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 Ξ₂.

See Also

• Lower bounds of this function (archived)
• SKI interpreter