I'm having trouble converting the lambda for flip into the SKI combinators (I hope that makes sense). Here is my conversion:
/fxy.fyx
/f./x./y.fyx
/f./x.S (/y.fy) (/y.x)
/f./x.S f (/y.x)
/f./x.S f (K x)
/f.S (/x.S f) (/x.K x)
/f.S (/x.S f) K
/f.S (S (/x.S) (/x.f)) K
/f.S (S (K S) (K f)) K
S (/f.S (S (K S) (K f))) (/f.K)
S (/f.S (S (K S) (K f))) (K K)
S (S (/f.S) (/f.S (K S) (K f))) (K K)
S (S (K S) (/f.S (K S) (K f))) (K K)
S (S (K S) (S (/f.S (K S)) (/f.K f))) (K K)
S (S (K S) (S (/f.S (K S)) K)) (K K)
S (S (K S) (S (S (/f.S) (/f.K S)) K)) (K K)
S (S (K S) (S (S (K S) (/f.K S)) K)) (K K)
S (S (K S) (S (S (K S) (S (/f.K) (/f.S))) K)) (K K)
S (S (K S) (S (S (K S) (S (K K) (K S))) K)) (K K)
If I understand properly in the B, C, K, W system, C is flip and it's definition in SKI terms is S (S (K (S (K S) K)) S) (K K)
. obviously my answer isn't the same as the C combinator... Here are the rules I used for the conversions:
K y = /x.y - K combinator
(SKK) = /x.x - I combinator
(S (/x.f) (/x.g)) = (/x.fg) - S combinator
y = (/x.yx) - eta reduction
/x./y.f = /xy.f - currying
Note that the S rule can convert longer expressions - for example, λ x.abcdeg can be converted by setting f = abcde.
What am I missing?