SKI Calculus - Revision history

Δ⁵: un-overestimated bound

2026-10-18T08:45:06Z

un-overestimated bound

← Older revision		Revision as of 08:45, 18 October 2026
Line 78:		Line 78:
	\|-		\|-
	\|19		\|19
	\|> 2^^^^2^^^19		\|> 2^^^^2^^^17
	\|SSI(SSK(S(S(KS)K)I))(S(K(S(SSK)))K)		\|SSI(SSK(S(S(KS)K)I))(S(K(S(SSK)))K)
	\|-		\|-
Line 204:		Line 204:
	\|23		\|23
	\|68		\|68
	\|> 2^^^^2^^^19		\|> 2^^^^2^^^17
	\|SS(S(SK))(SSK(SS(SK)(S(KS)K)))(S(K(S(SSK)))K)		\|SS(S(SK))(SSK(SS(SK)(S(KS)K)))(S(K(S(SSK)))K)
	\|-		\|-
	\|24		\|24
	\|71		\|71
	\|> 2^^^^2^^^19		\|> 2^^^^2^^^17
	\|S(SS(S(SK))(SSK(SS(SK)(S(KS)K)))(S(K(S(SSK)))K))		\|S(SS(S(SK))(SSK(SS(SK)(S(KS)K)))(S(K(S(SSK)))K))
	\|-		\|-
Line 262:		Line 262:
	\|-		\|-
	\|9		\|9
	\|> 2{5}2^^^^2^^^19		\|> 2{5}2^^^^2^^^17
	\|WW(WB(C(WC))(WB))		\|WW(WB(C(WC))(WB))
	\|-		\|-

Δ⁵: new champ

2026-10-13T07:15:05Z

new champ

← Older revision		Revision as of 07:15, 13 October 2026
Line 268:		Line 268:
	\|> f<sub>ω+1</sub>(2^^6/2-1)		\|> f<sub>ω+1</sub>(2^^6/2-1)
	\|WW(C(WB)(C(CC(WB))))		\|WW(C(WB)(C(CC(WB))))
			\|-
			\|...
			\|
			\|
			\|-
			\|15
			\|> f<sub>ω<sup>2^^18-1</sup></sub>(2)
			\|WW(C(WB)(B(BC(CC(WB)))(C(BC))))
	\|}		\|}

Δ⁵: /* Champions for Ξ₀BCKW */

2026-10-12T03:35:18Z

Champions for Ξ₀BCKW

← Older revision		Revision as of 03:35, 12 October 2026
Line 247:		Line 247:
	\| 4 \|\| = 11 \|\| WW(WB)		\| 4 \|\| = 11 \|\| WW(WB)
	\|-		\|-
	\| 5 \|\| ≥ 47 \|\| W(WW)(WB)		\| 5 \|\| = 47 \|\| W(WW)(WB)
	\|-		\|-
	\|6		\|6

Δ⁵: /* Champions for Ξ₀SK */ noticed some llm smell, removed the link for now

2026-10-11T11:56:31Z

Champions for Ξ₀SK: noticed some llm smell, removed the link for now

← Older revision		Revision as of 11:56, 11 October 2026
Line 139:		Line 139:
	\|7		\|7
	\| 20		\| 20
	\|= 41 ~~<sup>[https://github.com/b00ne/bb-sk-7/blob/main/bbsk7.pdf[1<nowiki>]</nowiki>]</sup>~~		\|= 41
	\|SSS(S(SS))S		\|SSS(S(SS))S
	\|-		\|-

Δ⁵: /* Champions for Ξ₀SK */

2026-10-11T11:38:04Z

Champions for Ξ₀SK

← Older revision		Revision as of 11:38, 11 October 2026
Line 139:		Line 139:
	\|7		\|7
	\| 20		\| 20
	\|= 41		\|= 41 <sup>[https://github.com/b00ne/bb-sk-7/blob/main/bbsk7.pdf[1<nowiki>]</nowiki>]</sup>
	\|SSS(S(SS))S		\|SSS(S(SS))S
	\|-		\|-

Δ⁵: /* Champions for Ξ₀BCKW */

2026-10-11T11:05:42Z

Champions for Ξ₀BCKW

← Older revision		Revision as of 11:05, 11 October 2026
Line 245:		Line 245:
	\| 3 \|\| = 3 \|\| BBB		\| 3 \|\| = 3 \|\| BBB
	\|-		\|-
	\| 4 \|\| ≥ 11 \|\| WW(WB)		\| 4 \|\| = 11 \|\| WW(WB)
	\|-		\|-
	\| 5 \|\| ≥ 47 \|\| W(WW)(WB)		\| 5 \|\| ≥ 47 \|\| W(WW)(WB)

Cppdsucker: https://github.com/b00ne/bb-sk-7/blob/main/bbsk7.pdf

2026-10-11T11:00:04Z

https://github.com/b00ne/bb-sk-7/blob/main/bbsk7.pdf

← Older revision		Revision as of 11:00, 11 October 2026
Line 139:		Line 139:
	\|7		\|7
	\| 20		\| 20
	\|≥ 41		\|= 41
	\|SSS(S(SS))S		\|SSS(S(SS))S
	\|-		\|-

Δ⁵: Clarify the exact meaning of

2026-09-28T05:55:19Z

Clarify the exact meaning of

← Older revision		Revision as of 05:55, 28 September 2026
Line 1:		Line 1:
	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\|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. The tree can be evaluated according to any reducible redex.

	Sfgx => fx(gx)		Sfgx = fx(gx)

	Kfx => f		Kfx = f

	Ix => 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 225:		Line 225:

	== BCKW system ==		== BCKW system ==
	BCKW system is a variation of SK calculus that replace the S combinator by 3 new combinators B, C and W.		BCKW system is a variation of SK calculus that replace the S combinator with 3 new combinators B, C and W.

	Bfgx => f(gx)		Bfgx = f(gx)

	Cfxy => fyx		Cfxy = fyx

	Kfx => f		Kfx = f

	Wfx => fxx		Wfx = fxx

	=== Champions for Ξ₀<sub>BCKW</sub> ===		=== Champions for Ξ₀<sub>BCKW</sub> ===

Δ⁵: /* Champions for ΞSKIO */

2026-09-28T05:39:38Z

Champions for ΞSKIO

← Older revision		Revision as of 05:39, 28 September 2026
Line 274:		Line 274:
	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 ≤ ω₁<sup>CK</sup>. 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 Ξ₂.		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 ≤ ω₁<sup>CK</sup>. 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 Ξ~~<sub>SKIO</sub>~~ ===		=== Champions for Ξ ===
	{\| class="wikitable"		{\| class="wikitable"
	! n !! Value !! Champion		! n !! Value !! Champion

Δ⁵: /* Champions for ΞSKIΩ */

2026-09-24T01:07:13Z

Champions for ΞSKIΩ

← Older revision		Revision as of 01:07, 24 September 2026
Line 274:		Line 274:
	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 ≤ ω₁<sup>CK</sup>. 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 Ξ₂.		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 ≤ ω₁<sup>CK</sup>. 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 Ξ<sub>~~SKIΩ~~</sub> ===		=== Champions for Ξ<sub>SKIO</sub> ===
	{\| class="wikitable"		{\| class="wikitable"
	! n !! Value !! Champion		! n !! Value !! Champion