g | x | w | all
Bytes Lang Time Link
nan241021T180617ZJohn Tro
13344 combinators211229T235730ZBubbler

69 combinators \$\approx f_{\epsilon_0+1}(4)\$

S (S (S I I) (K (S (S (S (S I (S (K (S (K (S (K (S (S (K S) (S (K (S S (K (S (K (S (K (S (K (S S (K (S (K (S (K (S S (K K))) K)) S)))) K)) S)) K)))) K)))) K)) (S I))) K)) (K (S K))) (K (S S (S K)))) I))) I (S (S (K S) K) I)

This is compiled from the lambda term in https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/BBE0.lam

We can also compile https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/melo.lam to the 25 combinator S I I (S I (S I (K (S (K (S (K (S S (K (K (S (S (K S) K) I))))) (S I))) K)))) scoring \$\approx f_{\omega+1}(2^ ^ 6)\$.

44 combinators, score: \$\approx f_{\omega+1}(3\uparrow\uparrow\uparrow\uparrow3)\$

(S (S (K S) (S S K)) (K I)) arrow_diag (S (S (K S) K) (S (S (K S) K) I)) S K
where arrow_diag = S (S (S I (K (S (S (K S) (S (K (S I)) K)) (K I)))) (S (K (S I)) K)) I

This reduces to an expression of S (S (S (...(S K)...))) which contains n copies of S, where n is the value obtained by repeatedly applying arrow_diag function (a 1-input function that diagonalizes over the Knuth's up arrow notation, explained below) arrow_diag 3 times to the number 3.

Edit: Fixed the arrow_diag function, and changed 2 to 3 because I found arrow_diag 2 was just 4. Though I guess arrow_diag (arrow_diag (arrow_diag (arrow_diag 2))) would still be insanely large.

The first idea is that we will construct a Church numeral for a very large natural number n, which is \f. \x. f (f (f ... f x)) (f applied n times to x), and then force it by applying S and K to it. Then the normal form would be S (S (... S K)) which has exactly n+1 combinators.

Now, let's find a way to build large numbers. A good start point is the deceptively short power function

-- x^y
exp x y = y x
exp = \x. \y. y x

Then we can repeat the partially applied exp to build tetration and beyond (corresponding to \$x\uparrow\uparrow y\$, \$x\uparrow\uparrow\uparrow y\$ and so on):

-- x^^y = x^(x^...(x^x))
tet x y = y (x^) 1
tet = \x. \y. y (\y. y x) 1
-- x^^^y = x^^(x^^...)
quad x y = y (x^^) 1
quad = \x. \y. y (\y. y (\y. y x) 1) 1
-- in general:
arrow<N> = \x. \y. y (arrow<N-1> x) 1

Then we can try converting these into SKI. Since the next arrow notation involves a partially applied previous one, just partially converting gives helpful insights.

exp = \x. \y. y x
= \x. S I (K x)
tet = \x. \y. y (\y. y x) 1
= \x. \y. y (S I (K x)) I
= \x. S (\y. y (S I (K x))) (K I)
= \x. S (S I (K (S I (K x)))) (K I)
quad = \x. \y. y (\y. y (\y. y x) 1) 1
= \x. \y. y (S (S I (K (S I (K x)))) (K I)) I
= ...

Here we can spot a pattern. Here comes the beauty of pure lambda calculus: we can extract arbitrary subexpression into a lambda. Meanwhile, we can change 1 to y to get a higher number and save 1 combinator.

\x. \y. y (someexpr) 1
= \x. S (S I (K someexpr)) (K I)
= \x. (\e. S (S I (K e)) (K I)) someexpr

\x. \y. y (someexpr) y
= \x. S (S I (K someexpr)) I
= \x. (\e. S (S I (K e)) I) someexpr

tet' = \x. 1 (\e. S (S I (K e)) I) (S I (K x))
arrow<n> = \x. n (\e. S (S I (K e)) I) (S I (K x))

Here arrow<n> x y (roughly) calculates \$x \uparrow^{n+1} y\$.

Now we diagonalize over the arrow notation, by using x, the input value, instead of n.

arrow_diag2 = \x. x (\e. S (S I (K e)) I) (S I (K x))
= S (S I (K (S (S (K S) (S (K (S I)) K)) (K I)))) (S (K (S I)) K)

But it is still a binary function that calculates (roughly) \$x \uparrow^{x+1} y\$, so let's make it unary:

arrow_diag = \x. arrow_diag2 x x
= S arrow_diag2 I
= S (S (S I (K (S (S (K S) (S (K (S I)) K)) (K I)))) (S (K (S I)) K)) I

This has just 22 combinators. To get a non-trivial number (don't forget, we're also adding S K at the end to get a deterministic combinator count), we evaluate

arrow_diag 3 arrow_diag 3 S K
= (\x y. x y x y) arrow_diag 3 S K
= (S (S (K S) (S S K)) (K I)) arrow_diag (S (S (K S) K) (S (S (K S) K) I)) S K

which has just 44 combinators but evaluates to an... extremely large number that I don't know how to express correctly.