# 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 & \overset{S}{\implies} x\;z\;(y\;z) \\ K\;x\;y & \overset{K}{\implies} x \\ I\;x & \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 & \overset{S}{\implies} (K(S\;I)x)(K\;x)y \\ & \overset{K}{\implies} S\;I(K\;x)y \\ & \overset{S}{\implies} (I\;y)(K\;x\;y) \\ & \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} & \text{Lambda} & \text{SKI} \\ \hline 0 & λf. λx. x & K\;I \\ 1 & λf. λx. f\;x & I \\ 2 & λf. λx. f(f\;x) & S (S (K\;S) K) I \\ \text{Succ} \; n & λn. λf. λx. f(n\;f\;x) & S (S (K\;S) K) \\ m+n & λm. λn. λf. λx. m\;f(n\;f\;x) & 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.

• Could you maybe explain how S(S(KS)K) is the successor? I'm finding the ...K) hard to comprehend to start with - does it get the input? Feb 3 '20 at 0:18
• @JonathanAllan When you give three arguments to it, you get $$S(S(KS)K)nfx = S(KS)Kf(nf)x = KSf(Kf)(nf)x = S(Kf)(nf)x = Kfx(nfx) = f(nfx),$$ which is exactly what we want the successor function to do. Feb 3 '20 at 0:36

# 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} &= λf. λx. x = KI \\ \textit{succ} &= λn. λf. λx. f\,(n\,f\,x) = S(S(KS)K) \\ \textit{zero-pair} &= λf. f\,\textit{zero}\,\textit{zero} = S(SI(K\,\textit{zero}))(K\,\textit{zero}) \\ \textit{next-pair-helper} &= λf. λm. λn. f\,n\,(\textit{succ}\,m) \\ &= S(S(KS)(S(KK)S))(K(S(KK)\,\textit{succ})) \\ \textit{next-pair} &= λp. λf. p\,(\textit{next-pair-helper}\,f) \\ &= S(S(KS)K)(K\,\textit{next-pair-helper}) \\ \textit{half} &= λn. n\,\textit{next-pair}\,\textit{zero-pair}\,K \\ &= S(S(SI(K\,\textit{next-pair}))(K\,\textit{zero-pair}))(KK) \end{align*}

• How does (KK) work if K requires two parameters? Feb 3 '20 at 0:13
• @JerryJeremiah All combinators in SKI calculus are curried higher-order functions; $K x y = x$ is an abbreviation for $K = λx. λy. x$, so $KK = λy. K$ is a perfectly fine value. (If that doesn’t make sense to you yet, that’s understandable, but you may need to do some more reading about lambda calculus and SKI calculus instead of asking me to explain it in 600 character coments. ☺) Feb 3 '20 at 0:30

# 56 combinators

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


Try it online!

This is the hand-optimized version of my own solution (originally of score 126). I also used the "pair" construct, but in rather basic way.

\begin{align*} \textit{zero} &= λf. λx. x = KI \\ \textit{succ} &= λn. λf. λx. f\,(n\,f\,x) = S(S(KS)K) \\ \textit{pair} &= λx. λy. λf. f\,x\,y \\ \textit{zero-pair} &= \textit{pair}\,\textit{zero}\,\textit{zero} \\ \textit{fst} &= λp. p\,(λx. λy. x) \\ \textit{snd} &= λp. p\,(λx. λy. y) \\ \textit{next-pair} &= λp. \textit{pair}\,(\textit{snd}\,p)\,(\textit{succ}\,(\textit{fst}\,p))\\ \textit{half} &= λn. \textit{fst}\,(n\,\textit{next-pair}\,\textit{zero-pair}) \end{align*}

Then I used $$\SKIBC\$$-conversion. Those reverse-applications generated lots of $$\C\$$s ($$\C = (S (S (K (S (K S) K)) S) (K K))\$$), which turned out to be very heavy even after reduction.