SKI Calculus prefix notation of odd/even number

Question

I'm working on a homework with SKI calculus. I saw the hints in this very useful post.

We basically defined SKI functions as:

def tt  = K;
def ff  = S K;

def inc = S (S (K S) K);
def _0  = S K;
def _1  = inc _0;
def _2  = inc _1;
def _3  = inc _2;

def not  = S (S (K (S (K S) K)) S) (K K);
(not tt) x y;  # y
(not ff) x y;  # x

By the hint provided by the above post, I found out that _3 f x = f(f(f(x))).

If I do _3 not ff, I can basically get the answer I'm looking for: (_3 is_odd) x y and it will output x, therefore is_odd = not ff.

However, the hw requirement is to write the function as (is_odd _3) x y -- a prefix notation.

I tried to use the reverse order operator def reverse = S (K (S I)) K; where reverse x y -> y x, but when you apply this to three arguments: reverse (not ff) _3 -> _3 (not ff), which is not the right order (_3 not) ff.

Am I going down the wrong path here? How to deal with the prefix notation problem in SKI calculus?

Answer 1

Your on the right track here with the _3 not ff and the reverse operator. But you seem to be have a small amount of confusion with the bracketing. _3 not ff is (_3 not) ff instead of the of the _3 (not ff) you seem to be implying by setting is_odd to not ff.

Since reverse x y is equivalent to y x ¹ we can transform (_3 not) ff into reverse ff (_3 not). We can apply the same transformation to the subterm _3 not to get reverse ff (reverse not _3) This is almost but not quite what we what: here _3 all the way on the right, but buried inside some parentheses. We can fix this by noticing we have a composition of the functions reverse ff and reverse not applied to _3. The composition of a function f with a function g can be made as S (K f) g. Applying this to reverse ff (reverse not (_3)) gives (S (K (reverse ff)) (reverse not)) _3. Note we didn't use anything special about _3 so we could do the same transformation for any numeral.

Overall we have is_odd can be defined as (S (K (reverse ff)) (reverse not)).

---

¹ I'm assuming that claim from your question is true, I haven't checked myself