ABSTRACT

Combinatory logic is sufficiently expressive to allow a definition of a function abstraction operation — as we already saw in chapter 1. The bracket abstraction operation is not part of the language of CL, rather it is a meta-notation for certain CL-terms (or certain classes of CL-terms, depending on the definition of the bracket abstraction). It is one of the great intellectual discoveries of the 20th century that a mathematically rigorous theory of functions does not need to include a variable binding abstraction operator.