15
4
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.
Bubbler
Posted 2020-02-02T23:15:22.153
Reputation: 16 616
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? – Jonathan Allan – 2020-02-03T00:18:13.2902@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. – Anders Kaseorg – 2020-02-03T00:36:23.140