SKI Calculus - Revision history

ADucharme: introduction reorganization

2026-05-09T23:07:17Z

introduction reorganization

← Older revision		Revision as of 23:07, 9 May 2026
Line 1:		Line 1:
	~~Busy Beaver for SKI calculus (we will call it BB_SKI for now) is a variation of the [[Busy Beaver for lambda calculus\|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>.

	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 any reducible redex.		Like lambda calculus, SKI calculus has a process called beta-reduction. We change the tree according to any reducible redex.
Line 9:		Line 7:
	* <code>Sxyz -> Sxz(yz)</code>		* <code>Sxyz -> Sxz(yz)</code>

	Note that <code>xyz</code> represent any valid trees, not just single combinators.		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.

	We repeat this process and we say it terminates if the combinator cannot be beta-reduced.

	BB_SKI(n) is defined as the size of the largest output of a terminating program of size n.		Busy Beaver for SKI calculus ('''BB_SKI''') is a variation of the [[Busy Beaver for lambda calculus\|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 ==		== Champions ==

ADucharme: ADucharme moved page Busy Beaver for SKI calculus to SKI Calculus: standardization

2026-05-09T23:04:50Z

ADucharme moved page Busy Beaver for SKI calculus to SKI Calculus: standardization

← Older revision		Revision as of 23:04, 9 May 2026
(No difference)

Tromp: /* Champions */

2026-05-07T09:05:18Z

Champions

← Older revision		Revision as of 09:05, 7 May 2026
Line 109:		Line 109:
	\|> Graham's Number		\|> Graham's Number
	\|SII(SI(SI(K(S(K(S(K(SS(K(K(S(S(KS)K)I)))))(SI)))K))))		\|SII(SI(SI(K(S(K(S(K(SS(K(K(S(S(KS)K)I)))))(SI)))K))))
	\|?		\| 2014MELO03
	\|}		\|}

Tromp: /* Champions */

2026-05-07T09:02:23Z

Champions

← Older revision		Revision as of 09:02, 7 May 2026
Line 104:		Line 104:
	\|> 2^^^2^^19		\|> 2^^^2^^19
	\|S(SSK(S(S(S(SSS))I)I))I(S(S(KS)K)I)KK		\|S(SSK(S(S(S(SSS))I)I))I(S(S(KS)K)I)KK
			\|?
			\|-
			\|25
			\|> Graham's Number
			\|SII(SI(SI(K(S(K(S(K(SS(K(K(S(S(KS)K)I)))))(SI)))K))))
	\|?		\|?
	\|}		\|}

Tromp: /* SK calculus */

2026-05-07T08:48:43Z

SK calculus

← Older revision		Revision as of 08:48, 7 May 2026
Line 108:		Line 108:

	== SK calculus ==		== 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>. 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.		We can remove the <code>I</code> combinator and replace it by <code>(SKS)</code>, <code>(SKK)</code> or any <code>(SKx)</code>. 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 ===		=== Champions ===

Tromp: /* SK calculus */

2026-05-07T08:48:12Z

SK calculus

← Older revision		Revision as of 08:48, 7 May 2026
Line 108:		Line 108:

	== SK calculus ==		== 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>. These terms have a straightforward binary encoding where (prefix) application is 1, K=00, and S=01.		We can remove the <code>I</code> combinator and replace it by <code>(SKS)</code>, <code>(SKK)</code> or any <code>(SKx)</code>. 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.

	=== Champions ===		=== Champions ===

Tromp: /* SK calculus */

2026-05-07T08:46:19Z

SK calculus

← Older revision		Revision as of 08:46, 7 May 2026
Line 108:		Line 108:

	== SK calculus ==		== 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>.		We can remove the <code>I</code> combinator and replace it by <code>(SKS)</code>, <code>(SKK)</code> or any <code>(SKx)</code>. These terms have a straightforward binary encoding where (prefix) application is 1, K=00, and S=01.

	=== Champions ===		=== Champions ===

Tromp: n S/K combinators take 3n-1 bits to encode in Binary Combinatory Logic

2026-05-07T08:42:27Z

n S/K combinators take 3n-1 bits to encode in Binary Combinatory Logic

← Older revision		Revision as of 08:42, 7 May 2026
Line 112:		Line 112:
	=== Champions ===		=== Champions ===
	{\| class="wikitable"		{\| class="wikitable"
	! n !! Value !! Champion !! Discoverered by		! n !! bits !! Value !! Champion !! Discoverered by
	\|-		\|-
	\| 1 \|\| = 1 \|\| S \|\| ?		\| 1 \|\| 2 \|\| = 1 \|\| S \|\| ?
	\|-		\|-
	\| 2 \|\| = 2 \|\| SS \|\| ?		\| 2 \|\| 5 \|\| = 2 \|\| SS \|\| ?
	\|-		\|-
	\| 3 \|\| = 3 \|\| SSS \|\| ?		\| 3 \|\| 8 \|\| = 3 \|\| SSS \|\| ?
	\|-		\|-
	\| 4 \|\| = 4 \|\| SSSS \|\| ?		\| 4 \|\| 11 \|\| = 4 \|\| SSSS \|\| ?
	\|-		\|-
	\| 5 \|\| = 6 \|\| SSS(SS) \|\| ?		\| 5 \|\| 14 \|\| = 6 \|\| SSS(SS) \|\| ?
	\|-		\|-
	\| 6 \|\| ≥ 10 \|\| SSS(SS)S \|\| ?		\| 6 \|\| 17 \|\| ≥ 10 \|\| SSS(SS)S \|\| ?
	\|-		\|-
	\|7		\|7
			\| 20
	\|≥ 40		\|≥ 40
	\|S(SS)S(SS)S		\|S(SS)S(SS)S
Line 132:		Line 133:
	\|-		\|-
	\|8		\|8
			\| 23
	\|≥ 41		\|≥ 41
	\|S(S(SS)S(SS)S)		\|S(S(SS)S(SS)S)
Line 137:		Line 139:
	\|-		\|-
	\|9		\|9
			\| 26
	\|≥ 42		\|≥ 42
	\|S(S(S(SS)S(SS)S))		\|S(S(S(SS)S(SS)S))
Line 142:		Line 145:
	\|-		\|-
	\|10		\|10
			\| 29
	\|≥ 66		\|≥ 66
	\|SS(SSS)(SS(SS))S		\|SS(SSS)(SS(SS))S
Line 147:		Line 151:
	\|-		\|-
	\|11		\|11
			\| 32
	\|≥ 79		\|≥ 79
	\|SS(SSS)(SS(SSS))S		\|SS(SSS)(SS(SSS))S
Line 152:		Line 157:
	\|-		\|-
	\|12		\|12
			\| 35
	\|≥ 164		\|≥ 164
	\|SS(SKK)(SS)(SS(SS))S		\|SS(SKK)(SS)(SS(SS))S
Line 157:		Line 163:
	\|-		\|-
	\|13		\|13
			\| 38
	\|≥ 681		\|≥ 681
	\|SS(SKK)(SS)(SS(SSS))S		\|SS(SKK)(SS)(SS(SSS))S
Line 162:		Line 169:
	\|-		\|-
	\|14		\|14
			\| 41
	\|≥ 1530		\|≥ 1530
	\|SS(SKK)(SS)(SS(SS(SS)))S		\|SS(SKK)(SS)(SS(SS(SS)))S
Line 167:		Line 175:
	\|-		\|-
	\|15		\|15
			\| 44
	\|≥ 7811		\|≥ 7811
	\|SS(SKK)(SS)(SS(SS(SSS)))S		\|SS(SKK)(SS)(SS(SS(SSS)))S

Δ⁵: /* Champions */ new bounds

2026-05-07T04:41:29Z

Champions: new bounds

@@ Line 134: / Line 134: @@
 |≥ 41
 |S(S(SS)S(SS)S)
 |?
 |}

Δ⁵: Updated bounds and removed misinformation

2026-05-07T03:45:17Z

Updated bounds and removed misinformation

← Older revision		Revision as of 03:45, 7 May 2026
Line 1:		Line 1:
	Busy Beaver for SKI calculus (we will call it ~~BBSKI~~ for now) is a variation of the [[Busy Beaver for lambda calculus\|Busy Beaver problem for lambda calculus]].		Busy Beaver for SKI calculus (we will call it BB_SKI for now) is a variation of the [[Busy Beaver for lambda calculus\|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>.		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~~.		Like lambda calculus, SKI calculus has a process called beta-reduction. We change the tree according to any reducible redex.

	* <code>Ix -> I</code>		* <code>Ix -> I</code>
Line 12:		Line 12:

	We repeat this process and we say it terminates if the combinator cannot be beta-reduced.		We repeat this process and we say it terminates if the combinator cannot be beta-reduced.

			BB_SKI(n) is defined as the size of the largest output of a terminating program of size n.

	== Champions ==		== Champions ==
Line 27:		Line 29:
	\| 5 \|\| = 6 \|\| SSS(SS) \|\| ?		\| 5 \|\| = 6 \|\| SSS(SS) \|\| ?
	\|-		\|-
	\| 6 \|\| = 17 \|\| SSS(SI)S \|\| ?		\| 6 \|\| ≥ 17 \|\| SSS(SI)S \|\| ?
	\|-		\|-
	\|7		\|7
	\|≥ 18		\|≥ 40
	\|S(~~SSS~~(SI)S)		\|S(SS)S(SS)S
	\|?		\|?
	\|-		\|-
	\|8		\|8
	\|≥ 19		\|≥ 41
	\|SS(~~SSS~~(SI)S)		\|SII(S(S(SS)))S
	\|?		\|?
	\|-		\|-
	\|9		\|9
	\|≥ ~~519~~		\|≥ 79
	\|~~SSI~~((~~S(SS~~)S)S)K		\|SII(SS(SSS))S
	\|?		\|?
	\|-		\|-
	\|10		\|10
	\|≥ ~~1041~~		\|≥ 164
	\|~~SSI~~((S(SS)S)S)KS		\|SII(SS(SS(SS)))S
			\|?
			\|-
			\|11
			\|≥ 681
			\|SII(SS(SS(SSS)))S
			\|?
			\|-
			\|12
			\|≥ 1530
			\|SII(SS(SS(SS(SS))))S
			\|?
			\|-
			\|13
			\|≥ 65537
			\|S(S(SI))I(S(S(KS)K)I)KK
			\|?
			\|-
			\|14
			\|≥ 2^256+1
			\|S(S(S(SI)))I(S(S(KS)K)I)KK
			\|?
			\|-
			\|15
			\|> 2^2^2^2^21
			\|S(S(SSS)I)I(S(S(KS)K)I)KK
			\|?
			\|-
			\|16
			\|> 2^^19
			\|S(S(S(SSS))I)I(S(S(KS)K)I)KK
			\|?
			\|-
			\|17
			\|> 2^^2^128
			\|SSK(S(S(KS)K)I)(S(SI(SI))I)KK
			\|?
			\|-
			\|18
			\|> 2^^2^2^2^2^21
			\|SSK(S(S(KS)K)I)(S(S(SSS)I)I)KK
			\|?
			\|-
			\|19
			\|> 2^^^2^128
			\|S(SSK(S(SI(SI))I))I(S(S(KS)K)I)KK
			\|?
			\|-
			\|20
			\|> 2^^^2^2^2^2^21
			\|S(SSK(S(S(SSS)I)I))I(S(S(KS)K)I)KK
			\|?
			\|-
			\|21
			\|> 2^^^2^^19
			\|S(SSK(S(S(S(SSS))I)I))I(S(S(KS)K)I)KK
	\|?		\|?
	\|}		\|}
Line 63:		Line 120:
	\| 3 \|\| = 3 \|\| SSS \|\| ?		\| 3 \|\| = 3 \|\| SSS \|\| ?
	\|-		\|-
	\| 4 \|\| = 4 \|\| ~~<code>~~SSSS~~</code>~~ \|\| ?		\| 4 \|\| = 4 \|\| SSSS \|\| ?
	\|-		\|-
	\| 5 \|\| = 6 \|\| ~~<code>~~SSS(SS)~~</code>~~ \|\| ?		\| 5 \|\| = 6 \|\| SSS(SS) \|\| ?
	\|-		\|-
	\| 6 \|\| ≥ 8 \|\| ~~<code>~~SSS(~~SSS~~)~~</code>~~ \|\| ?		\| 6 \|\| ≥ 10 \|\| SSS(SS)S \|\| ?
	\|-		\|-
	\|7		\|7
	\|≥ 10		\|≥ 40
	\|~~<code>SSS~~(~~SSSS~~)~~</code>~~		\|S(SS)S(SS)S
	\|?		\|?
	\|-		\|-
	\|8		\|8
	\|≥ 23		\|≥ 41
	\|~~<code>SSS~~(S(~~SKS~~))S~~</code>~~		\|S(S(SS)S(SS)S)
	\|?		\|?
	\|}		\|}

	== 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] (archived)

			[https://dallaylaen.github.io/ski-interpreter/ SKI interpreter]

	[[Category:Functions]]		[[Category:Functions]]