+ S(CI) =
+ S((\fxy.fyx)(\x.x)) =
+ S(\xy.(\x.x)yx) =
+ (\fgx.fx(gx))(\xy.yx) =
+ \gx.[\xy.yx]x(gx) =
+ \gx.(gx)x =
+ W
+
+Ok, here comes a shift in thinking. Instead of defining combinators as equivalent to certain lambda terms,
+we can define combinators by what they do. If we have the I combinator followed by any expression X,
+I will take that expression as its argument and return that same expression as the result. In pictures,
+
+ IX ~~> X
+
+Thinking of this as a reduction rule, we can perform the following computation
+
+ II(IX) ~~> IIX ~~> IX ~~> X
+
+The reduction rule for K is also straigtforward:
+
+ KXY ~~> X
+
+That is, K throws away its second argument. The reduction rule for S can be constructed by examining
+the defining lambda term:
+
+ S = \fgx.fx(gx)
+
+S takes three arguments, duplicates the third argument, and feeds one copy to the first argument and the second copy to the second argument. So:
+
+ SFGX ~~> FX(GX)
+
+If the meaning of a function is nothing more than how it behaves with respect to its arguments,
+these reduction rules capture the behavior of the combinators S,K, and I completely.
+We can use these rules to compute without resorting to beta reduction. For instance, we can show how the I combinator is equivalent to a certain crafty combination of S's and K's:
+
+ SKKX ~~> KX(KX) ~~> X
+
+So the combinator SKK is equivalent to the combinator I.