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.
The terms of combinatory logic are defined by the following grammar, where comes from a set of variables:
The meaning of these terms is given by a basic equational theory, called . This theory is the least congruence (closed under all term formers) of the axioms
Intuitively, takes a term and returns the constant function which always returns . On the other hand, takes two functions and , which then 'share' the argument .
Because of their behaviour, the combinators and 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?
Please expand.
The semantic structures corresponding to combinatory logic are combinatory algebras.
Untyped combinatory logic with and can simulate the entire -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.
Name | Meaning | Defining equation | Notes |
---|---|---|---|
identity function | |||
function composition | due to [Schonfinkel 1924] | ||
flip arguments | due to [Schonfinkel 1924] | ||
duplicate |
These combinators are all definable in terms of and . For example, one may define as , 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.
If we formulate a system whose basic combinators which duplicate or discard arguments - such as , and - we obtain a substructural systems of combinators.
Please expand: linear combinatory algebras.
Please expand: David Turner, supercombinators, Simon Peyton-Jones.
Typed combinatory logic is a term assignment system corresponding to a Hilbert proof system. The correspondence is
Please expand.
Barendregt, Henk. 1984. Lambda Calculus: Its Syntax and Semantics. Amsterdam: North-Holland. [link]
@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 -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
Bimbó, Katalin. 2012. Combinatory Logic: Pure, Applied and Typed. Discrete Mathematics and Its Applications. Boca Raton, FL: CRC Press. [link]
Smullyan, R.M. 2000. To Mock a Mockingbird: And Other Logic Puzzles Including an Amazing Adventure in Combinatory Logic. Oxford University Press.
@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}
}
Curry, H. B. 1930. ‘Grundlagen Der Kombinatorischen Logik’. American Journal of Mathematics 52 (3): 509–536.
@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}
}
Curry, H. B. "The Universal Quantifier in Combinatory Logic." Annals of Mathematics, Second Series, 32, no. 1 (1931): 154-80. Accessed November 27, 2020. doi:10.2307/1968422.
Curry, H. B. "Functionality in Combinatory Logic." Proceedings of the National Academy of Sciences of the United States of America 20, no. 11 (1934): 584-90. Accessed November 27, 2020. http://www.jstor.org/stable/86796.
@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}
}