Combinatory Logic

Combinatory logic is an term calculus proposed (independently?) by Schönfinkel in the 1920s and Haskell B. Curry in the 1930s. It was first developed in untyped form, but typed forms were later introduced.

Syntax

The terms of combinatory logic are defined by the following grammar, where x comes from a set of variables:

M, N ::=\ x\ |\ M N\ |\ \mathbf{S}\ |\ \mathbf{K}

The meaning of these terms is given by a basic equational theory, called CL. This theory is the least congruence (closed under all term formers) of the axioms

CL \vdash \textbf{K} M N = M

CL \vdash \textbf{S} M N X = (M X)(N X)

Intuitively, \textbf{K} takes a term M and returns the constant function which always returns M. On the other hand, \textbf{S} takes two functions M and N, which then 'share' the argument X.

Because of their behaviour, the combinators \mathbf{K} and \mathbf{S} are colloquially known as kill and split.

Alex Kavvos: I was told this as an undergraduate, and it seems to have been common terminology between functional programming researchers and enthusiasts in the 1980s. Is it documented anywhere in the literature?

Correspondence to \lambda-calculus

Please expand.

Semantics

The semantic structures corresponding to combinatory logic are combinatory algebras.

Other variants, other combinators

Untyped combinatory logic with \textbf{S} and \textbf{K} can simulate the entire \lambda-calculus, so it is as expressive as one needs.

However, typing and economy of expression often induce the need for additional combinators. The following table lists some of them.

These combinators are all definable in terms of \textbf{S} and \textbf{K}. For example, one may define \textbf{I} as \textbf{S}\textbf{K}\textbf{K}, and obtain the same equational behaviour.

However, one occasionally finds systems that contain some of them as primitives, which are usually named after the combinators included, e.g. SKI calculus, BCKW calculus and so on. In those terms the present formulation is known as the SK calculus.

Linear variants

If we formulate a system whose basic combinators which duplicate or discard arguments - such as \textbf{S}, \textbf{K} and \textbf{W} - we obtain a substructural systems of combinators.

Please expand: linear combinatory algebras.

Use in compilation of functional languages

Please expand: David Turner, supercombinators, Simon Peyton-Jones.

In terms of the Curry-Howard correspondence

Typed combinatory logic is a term assignment system corresponding to a Hilbert proof system. The correspondence is

• variables = use of assumptions
• combinators = axioms of the logic
• application = modus ponens

Illative combinatory logic

Please expand.

References

• A classic treatment of untyped combinatory logic can be found in chapter 7 of

@book{barendregt_1984,
	address = {Amsterdam},
	title = {Lambda {Calculus}: {Its} {Syntax} and {Semantics}},
	isbn = {978-0-444-87508-2},
	publisher = {North-Holland},
	author = {Barendregt, Henk},
	year = {1984}
}

Many lecture courses on untyped \lambda-calculus based on the book by Barendregt also repurpose or adapt this material.

• There is a Wikipedia page about combinatory logic.

• There is also a 2012 full-length treatment in the book

• A short and humorous "popular science" introduction is

@book{smullyan_mock_2000,
	title = {To {Mock} a {Mockingbird}: {And} {Other} {Logic} {Puzzles} {Including} an {Amazing} {Adventure} in {Combinatory} {Logic}},
	isbn = {978-0-19-280142-5},
	publisher = {Oxford University Press},
	author = {Smullyan, R.M.},
	year = {2000},
	lccn = {gb89045924}
}

• Haskell B. Curry introduced combinatory logic (with reference to Schönfinkel!) in the article

@article{curry_grundlagen_1930,
	title = {Grundlagen der {Kombinatorischen} {Logik}},
	volume = {52},
	issn = {00029327, 10806377},
	url = {http://www.jstor.org/stable/2370619},
	number = {3},
	journal = {American Journal of Mathematics},
	author = {Curry, H. B.},
	year = {1930},
	note = {Publisher: Johns Hopkins University Press},
	pages = {509--536}
}

• The first English-language presentation seems to have appeared in

• The first hint of the Curry-Howard correspondence is given in

@article{curry_1934,
 ISSN = {00278424},
 URL = {http://www.jstor.org/stable/86796},
 author = {H. B. Curry},
 journal = {Proceedings of the National Academy of Sciences of the United States of America},
 number = {11},
 pages = {584--590},
 publisher = {National Academy of Sciences},
 title = {Functionality in Combinatory Logic},
 volume = {20},
 year = {1934}
}