`λ*a. X`

; Hindley & Seldin write it as `[a] X`.) It is possible to omit line 6, and some presentations do, but Hindley & Seldin observe that this "enormously increases" the length of "most" translations.
It's easy to understand these rules based on what `S`, `K` and `I` do.
Rule (1) says that variables are mapped to themselves. If the original
lambda expression had no free variables in it, then any such
translations will only be temporary. The variable will later get
eliminated by the application of other rules.
Rule (2) says that the way to translate an application is to
first translate the body (i.e., `[X]`), and then prefix a kind of
temporary psuedo-lambda built from `@` and the original variable.
Rule (3) says that the translation of an application of `X` to `Y` is
the application of the translation of `X` to the translation of `Y`.
As we'll see, the first three rules sweep through the lambda term,
changing each lambda to an @.
Rules (4) through (7) tell us how to eliminate all the `@`'s.
In rule (4), if we have `@aa`, we need a CL expression that behaves
like the lambda term `\aa`. Obviously, `I` is the right choice here.
In rule (5), if we're binding into an expression that doesn't contain
any variables that need binding, then we need a CL term that behaves
the same as `\aX` would if `X` didn't contain `a` as a free variable.
Well, how does `\aX` behave? When `\aX` occurs in the head position
of a redex, then no matter what argument it occurs with, it throws
away its argument and returns `X`. In other words, `\aX` is a
constant function returning `X`, which is exactly the behavior
we get by prefixing `K`.
Rule (6) should be intuitive; and as we said, we could in principle omit it and just handle such cases under the final rule.
The easiest way to grasp rule (7) is to consider the following claim:
\a(XY) <~~> S(\aX)(\aY)
To prove it to yourself, just consider what would happen when each term is applied to an argument `a`. Or substitute `\x y a. x a (y a)` in for `S`
and reduce.
Persuade yourself that if the original lambda term contains no free
variables --- i.e., is a Lambda Calculus combinator --- then the translation will
consist only of `S`, `K`, and `I` (plus parentheses).
Various, slightly differing translation schemes from Combinatory Logic to the
Lambda Calculus are also possible. These generate different meta-theoretical
correspondences between the two calculi. Consult Hindley & Seldin for
details.
Also, note that the combinatorial proof theory needs to be
strengthened with axioms beyond anything we've here described in order to make
`[M]` convertible with `[N]` whenever the original lambda-terms `M` and `N` are
convertible. But then, we've been a bit cavalier about giving the full set of
reduction rules for the Lambda Calculus in a similar way.
For instance, one issue we mentioned in the notes on [[Reduction
Strategies|week3_reduction_strategies]] is whether reduction rules (in
either the Lambda Calculus or Combinatory Logic) apply to embedded
expressions. Often, we do want that to happen, but making it happen
requires adding explicit axioms.
Let's see the translation rules in action. We'll start by translating
the combinator we use to represent false:
[\y (\n n)]
== @y [\n n] rule 2
== @y (@n n) rule 2
== @y I rule 4
== KI rule 5
Let's check that the translation of the `false` boolean behaves as expected by feeding it two arbitrary arguments:
KIXY ~~> IY ~~> Y
Throws away the first argument, returns the second argument---yep, it works.
Here's a more elaborate example of the translation. Let's say we want
to establish that combinators can reverse order, so we set out to
translate the **T** combinator (`\x y. y x`):
[\x(\y(yx))]
== @x[\y(yx)]
== @x(@y[yx])
== @x(@y([y][x]))
== @x(@y(yx))
== @x(S(@yy)(@yx))
== @x(S I (@yx))
== @x(S I (Kx))
== S(@x(SI))(@x(Kx))
== S (K(SI))(S(@xK)(@xx))
== S (K(SI))(S (KK) I)
By now, you should realize that all rules (1) through (3) do is sweep
through the lambda term turning lambdas into @'s.
We can test this translation by seeing if it behaves like the original lambda term does.
The original lambda term "lifts" its first argument `x`, in the sense of wrapping it into a "one-tuple" or a package that accepts an operation `y` as a further argument, and then applies `y` to `x`. (Or just think of **T** 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 (K X) Y ~~>
IY (KXY) ~~>
Y X
Voilà: the combinator takes any X and Y as arguments, and returns Y applied to X.
One very nice property of Combinatory Logic is that there is no need to worry about alphabetic variance, or
variable collision---since there are no (bound) variables, there is no possibility of accidental variable capture,
and so reduction can be performed without any fear of variable collision. We haven't mentioned the intricacies of
alpha equivalence or safe variable substitution, but they are in fact quite intricate. (The best way to gain
an appreciation of that intricacy is to write a program that performs lambda reduction.)
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 their meanings using the Lambda Calculus rather than Combinatory Logic. Perhaps they should call their
enterprise *Free Variable*-Free Semantics.
A philosophical connection: Quine went through a phase in which he developed a variable-free logic.
> Quine, Willard. 1960. "Variables explained away" Proceedings of the American Philosophical Society. Volume 104: 343--347. Also in W. V. Quine. 1960. Selected Logical Papers. Random House: New York. 227--235.
The reason this was important to Quine is similar to the worry that using
non-referring expressions such as `Santa Claus` might commit one to believing in
non-existent things. Quine's slogan was that "to be is to be the value of a
variable." What this was supposed to mean is that if and only if an object
could serve as the value of some variable, we are committed to recognizing the
existence of that object in our ontology. Obviously, if there *are* no
variables, this slogan has to be rethought.
Quine did not appear to appreciate that Shoenfinkel had already invented Combinatory Logic, though
he later wrote an introduction to Shoenfinkel's key paper reprinted in Jean
van Heijenoort (ed) 1967 From Frege to Goedel, a source book in mathematical logic, 1879--1931.
Cresswell also developed a variable-free approach of some philosophical and linguistic interest
in two books in the 1990s.
A final linguistic application: Steedman's Combinatory Categorial Grammar, where the "Combinatory" is
from Combinatory Logic (see especially his 2012 book, Taking Scope). Steedman attempts to build
a syntax/semantics interface using a small number of combinators, including `T` (`\x y. y x`), `B` (`\f g x. f (g x)`),
and our friend `S`. Steedman used Smullyan's fanciful bird
names for these combinators: Thrush, Bluebird, and Starling.
Many of these combinatory logics, in particular, the SKI system,
are Turing Complete. In other words: every computation we know how to describe can be represented in a logical system consisting of only primitive combinators, even some systems with only a *single* primitive combinator.
###A connection between Combinatory Logic and Sentential Logic###
The combinators `K` and `S` correspond to two well-known axioms of sentential logic:
AK: A ⊃ (B ⊃ A)
AS: (A ⊃ (B ⊃ C)) ⊃ ((A ⊃ B) ⊃ (A ⊃ C))
When these two axiom schemas are combined with the rule of modus ponens (from `A` and `A ⊃ B`, conclude `B`), the resulting proof system
is complete for the "implicational fragment" of intuitionistic logic. (That is, the part of intuitionistic logic you get when `⊃` is your only connective. To get a complete proof system for *classical* sentential logic, you
need only add one more axiom schema, constraining the behavior of a new connective `¬`.)
The way we'll favor viewing the relationship between these axioms
and the `S` and `K` combinators is that the axioms correspond to *type
schemas* for the combinators. This will become more clear once we have
a theory of types in view.
Here's more to read about Combinatory Logic. Surely the most entertaining exposition is Smullyan's [[!wikipedia To_Mock_a_Mockingbird]].
Other sources include:
* [[!wikipedia Combinatory logic]] at Wikipedia
* [Combinatory logic](http://plato.stanford.edu/entries/logic-combinatory/) at the Stanford Encyclopedia of Philosophy
* [[!wikipedia SKI combinatory calculus]]
* [[!wikipedia B,C,K,W system]]
* [Chris Barker's Iota and Jot](http://semarch.linguistics.fas.nyu.edu/barker/Iota/)
* Jeroen Fokker, "The Systematic Construction of a One-combinator Basis for Lambda-Terms" Formal Aspects of Computing 4 (1992), pp. 776-780.