Largest SKI output in less than 200 combinators

Question

The Challenge

Create an terminating expression in SKI Combinator Calculus in less than 200 combinators (S, K, I) that reduces to the expression with the most combinators.

There will be no limit on how many parenthesis/applications can be used.

SKI

SKI expressions are created using S, K, I and parenthesis. They are reduced like so:

(((Sx)y)z) => ((xz)(yz))
((Kx)y) => x
(Ix) => x

When parenthesis with more than two expressions are in an expression, they are assumed to be nested to the left.

(xyz) = ((xy)z)

Scoring

The score will be the number of combinators in the output, the goal is for this to be as large as possible.

Examples

Here is an example of a reduction in SKI using the rules stated above.

(((SI)I)(((SI)I)S))
((I(((SI)I)S))(I(((SI)I)S)))
((((SI)I)S)(I(((SI)I)S)))
(((IS)(IS))(I(((SI)I)S)))
((S(IS))(I(((SI)I)S)))
((SS)(I(((SI)I)S)))
((SS)(((SI)I)S))
((SS)((IS)(IS)))
((SS)(S(IS)))
((SS)(SS))

So the expression (((SI)I)(((SI)I)S)) scores 4.

Answer 1

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.