SKI calculus golf: Half of a Church numeral Background

SKI combinator calculus, or simply SKI calculus, is a system similar to lambda calculus, except that SKI calculus uses a small set of combinators, namely S, K, and I instead of lambda abstraction. Unlike lambda calculus, beta reduction is possible only when a combinator is given enough arguments to reduce.

The three combinators in SKI calculus are defined as follows:

$$
\begin{aligned}
S\;x\;y\;z &amp; \overset{S}{\implies} x\;z\;(y\;z) \\
K\;x\;y &amp; \overset{K}{\implies} x \\
I\;x &amp; \overset{I}{\implies} x
\end{aligned}
$$

For example, the SKI expression \$ e=S(K(S\;I))K \$ is equivalent to the lambda expression \$ λx.λy.y\;x \$, as applying two arguments to \$ e \$ reduces to the desired result:

$$
\begin{aligned}
S(K(S\;I))K\;x\;y &amp; \overset{S}{\implies} (K(S\;I)x)(K\;x)y \\
&amp; \overset{K}{\implies} S\;I(K\;x)y \\
&amp; \overset{S}{\implies} (I\;y)(K\;x\;y) \\
&amp; \overset{I,K}{\implies} y\;x
\end{aligned}
$$

It is known that any lambda expression can be converted to a SKI expression.

A Church numeral is an encoding of natural numbers (including zero) as a lambda expression. The Church encoding of a natural number \$ n \$ is \$ λf. λx. f^n\;x \$ - given a function \$ f \$ and an argument \$ x \$, \$ f \$ repeatedly applied to \$ x \$ \$ n \$ times.

It is possible to construct a lambda expression (and therefore a SKI expression) that performs various arithmetic (e.g. addition, multiplication) in Church encoding. Here are a few examples of Church numerals and Church arithmetic functions: (The given SKI expressions are possibly not minimal.)

$$
\begin{array}{r|r|r}
\text{Expr} &amp; \text{Lambda}   &amp; \text{SKI} \\ \hline
0           &amp; λf. λx. x       &amp; K\;I       \\
1           &amp; λf. λx. f\;x    &amp; I          \\
2           &amp; λf. λx. f(f\;x) &amp; S (S (K\;S) K) I \\
\text{Succ} \; n &amp; λn. λf. λx. f(n\;f\;x) &amp; S (S (K\;S) K) \\
m+n         &amp; λm. λn. λf. λx. m\;f(n\;f\;x) &amp; S (K S) (S (K (S (K\;S) K)))
\end{array}
$$

Challenge

Write an SKI expression that accepts a Church numeral of \$ n \$ and evaluates to the Church numeral of \$ \lfloor n/2 \rfloor \$.

Scoring and winning criterion

The score is the total number of S, K, and I combinators used. The submission with the lowest score wins.

Here is a Python script to check the correctness and score of your SKI expression. For the record, I have a (relatively naïve) solution of score 126.
40 combinators

S(S(SI(K(S(S(KS)K)(K(S(S(KS)(S(KK)S))(K(S(KK)(S(S(KS)K)))))))))(K(S(SI(K(KI)))(K(KI)))))(KK)


Try it online!

Generated with a little help from a slightly modified version of my answer to Combinatory Conundrum:

$$\begin{align*}
\textit{zero} &amp;= λf. λx. x = KI \\
\textit{succ} &amp;= λn. λf. λx. f\,(n\,f\,x) = S(S(KS)K) \\
\textit{zero-pair} &amp;= λf. f\,\textit{zero}\,\textit{zero} = S(SI(K\,\textit{zero}))(K\,\textit{zero}) \\
\textit{next-pair-helper} &amp;= λf. λm. λn. f\,n\,(\textit{succ}\,m) \\ &amp;= S(S(KS)(S(KK)S))(K(S(KK)\,\textit{succ})) \\
\textit{next-pair} &amp;= λp. λf. p\,(\textit{next-pair-helper}\,f) \\ &amp;= S(S(KS)K)(K\,\textit{next-pair-helper}) \\
\textit{half} &amp;= λn. n\,\textit{next-pair}\,\textit{zero-pair}\,K \\ &amp;= S(S(SI(K\,\textit{next-pair}))(K\,\textit{zero-pair}))(KK)
\end{align*}$$