The lambda calculus and adjoint functors. (English) Zbl 1023.03010

Anderson, C. Anthony (ed.) et al., Logic, meaning and computation. Essays in memory of Alonzo Church. Dordrecht: Kluwer Academic Publishers. Synth. Libr. 305, 181-184 (2001).
Summary: The well-known lambda calculus was first formulated by Alonzo Church (1932). It was originally intended as a new foundation of mathematics; but soon the remarkable connection between lambda definability and recursive functions was developed. Only much later was the connection with rewrite systems noted, while the remarkable influence of the calculus in computer languages was also noted later. This note is to point out that the Galois connections and this lambda calculus are perhaps the first appearances of an explicit pair of adjoint functors. These functors in general were not found until the work of Daniel Kan in 1958.
For the entire collection see [Zbl 1017.00057].


03B40 Combinatory logic and lambda calculus
18A40 Adjoint functors (universal constructions, reflective subcategories, Kan extensions, etc.)
03-03 History of mathematical logic and foundations
18-03 History of category theory