A short introduction to the Lambda Calculus
Achim Jung · 2004
The lambda calculus can appear arcane on first encounter. Viewed pu rely as a “naming device”, however, it is a straighforward extension of ordinary mathematical notation. This is the point of view taken in these notes. 1. A brief history of mathematical notation. Our notation for numbers was introduced in the Western World in the Renaissance (around 1200) by people like Fibonacci. It is characterised by a small fixed set of digits, whose value vari es with their position in a number. This place-value system was adopted from the Arabs who themselves credit the Indians. We don’t know when and where in India it was invented . A notation for expressions and equations was not available until the 17th century, when Francois Vi` ete started to make systematic use of placeholders for parameters and abbreviations for the arithmetic operations. Until then, a simple expression such as 3x 2 had to be described by spelling out the actual computations which are necessary to obtain 3x 2 from a value for x. It took another 250 years before Alonzo Church developed a notation for arbitrary functions. His notation is called ¸-calculus (“lambda calculus”). Church introduced his formalism to give a functional foundation for Mathematics but in the end mathematicians preferred (axiomatic) set theory. The ¸-calculus was re-discovered as a versatile tool in Computer Science by people like McCarthy, Strachey, Landin, and Scott in the 1960s.