Application as an operation, Introduction to Combinatory Logic and Lambda Calculus

Henri Volken

Department of Applied Mathematics
University of Lausanne - Switzerland

Combinatory Logic started in 1924 with a paper by Moses Schönfinkel. The aim was an elimination of variables and a reduction of the primitive notions of logic. This work was continued by H.B. Curry who introduced the term of combinatory logic. At about the same time. Church introduced his lambda calculus as a new way to study the concept of rule. Originally his purpose was to provide a foundation for mathematics. Combinatory logic and lambda calculus, in their type-free version, proved to generate essentially the same algebraic and logic structures.
This tutorial is intended as a short introduction to both fields of combinatory logic and lambda calculus. In the first part, the historical context and the underlying conceptual problems are presented for both cases. Especially the Kleene-Rosser paradox is discussed, which shows the inconsistency of Church’s first system, hence the failure of his foundational claim. In the second part we will present some of the essential properties of theses theories, briefly discuss their typed versions and also give a few examples of more recent developments.
References

Barendregt, H.P. The Lambda-Calculus, its Syntax and Semantics, Amsterdam, North-Holland, 1978
Curry, H. and Feys, R. Combinatory Logic, Vol. 1. Amsterdam, Netherlands: North-Holland, 1958.
Hindley, J. R.; Lercher, B.; Seldin, J. P. Introduction to Combinatory Logic. London: Cambridge University Press, 1972.
Hindley, J. R. and Seldin, J. P. Introduction to Combinators and -Calculus. Cambridge, England: Cambridge University Press, 1986.
Holmes, M. R. "Systems of Combinatory Logic Related to Quine's 'New Foundations."' Annals Pure Appl. Logic 53, 103-133, 1991.
Schönfinkel, M. "Über die Bausteine der mathematischen Logik." Math. Ann. 92, 305-316, 1924.