This is a very brief introduction to lambda calculus.
Lambda calculus is a notation for defining functions. It is very simple and powerful. Two of its main uses are
- foundation of programming languages, especially functional languages such as Ocaml, Haskell, and Scala
- higher order logic notations, such as Isabelle, HOL, PVS
For example, a function which takes its argument and increments it by 2 is given by lambda expression . The operator is a binder used to indicate that a variable is to be treated as an argument of a function. We indicate function application by juxtaposition. Here are some example expressions and their values:
Untyped lambda expressions are given by following grammar:
That is, an expression is a variable, a lambda expression defining a function, or an application of one expression to another.
The main rule of lambda calculus is beta reduction, which formalizes function application:
where we assume capture-avoiding substitution.
One simple use of lambda expressions to introduce shorthands: instead of writing
we can write
- Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984) (Chad Brown's notes on this book)