Combinatory Logic

Abstract

Combinatory logic [calculus of combinators], called also lambda-calculus (LaC), is a formal theory developed by Schönfinkel (24), Curry (72), and Church (40, 41) who introduced the term ‘lambda calculus’. Further contributions come from C. Böhm, R. Feys, F.B. Fitch (cf. references in “Formalization”), J.B. Rosser, and others. It is a first-order theory with one two-argument function as primitive. This function, called application, is usually denoted by parentheses only (..,..) without being preceded by any special symbol; (x, y) denotes the result of the application of x (considered as a function) to y (considered as an argument). Hence (x, y) corresponds to the expression x(y) in the familiar mathematical notation. But the essential feature of the theory is that x and y, as well as the result of the application z = (x, y) are considered as belonging to the same type. Hence for example the expression (x, x) = x is meaningful in the theory (and true for some x).