+We can test this translation by seeing if it behaves like the original lambda term does.
+The orginal lambda term lifts its first argument (think of it as reversing the order of its two arguments):
+
+ S(K(SI))(S(KK)I) X Y =
+ (K(SI))X ((S(KK)I) X) Y =
+ SI ((KK)X (IX)) Y =
+ SI (KX) Y =
+ IY (KX)Y =
+ Y X
+
+Viola: the combinator takes any X and Y as arguments, and returns Y applied to X.
+
+Back to linguistic applications: one consequence of the equivalence between the lambda calculus and combinatory
+logic is that anything that can be done by binding variables can just as well be done with combinators.
+This has given rise to a style of semantic analysis called Variable Free Semantics (in addition to
+Szabolcsi's papers, see, for instance,
+Pauline Jacobson's 1999 *Linguistics and Philosophy* paper, `Towards a variable-free Semantics').
+Somewhat ironically, reading strings of combinators is so difficult that most practitioners of variable-free semantics
+express there meanings using the lambda-calculus rather than combinatory logic; perhaps they should call their
+enterprise Free Variable Free Semantics.
+
+A philosophical application: Quine went through a phase in which he developed a variable free logic.
+
+
+
+
+
+
+
+