Lambda calculus is a simple and powerful notation for defining functions. Among its uses are
- foundation of programming languages, especially functional languages such as Ocaml, Haskell, and Scala
- basis of higher order logic
In lambda calculus, functions have no side effects
- they are mathematical functions from arguments to results
- lambda calculus also supports higher-order functions
- this model is appropriate for studying type checking
- directly applicable to purely functional languages (like Haskell)
- applies to other languages if we ensure that assignments do not change types
Anonymous Functions in Lambda Calculus
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, writing instead of . Here are some example expressions and their values:
Concrete syntax for :
Abstract syntax of untyped lambda expressions:
That is, an expression is 1) a variable, 2) a lambda expression defining a function, or 3) an application of one expression to another.
Certain predefined variables are called constants (e.g. 7, 42, 13, but also operations +, *).
Types are given by the following grammar:
There can be additional primitive types .
Therefore is a function that increments its argument by
- expression is just a shorthand for
In general, instead of function
we can use function
The main rule of lambda calculus is beta reduction, which formalizes function application:
Here we assume capture-avoiding substitution
- we do renaming to avoid name clashes
Rules for Constants
For each constant we have appropriate rule, for example we have
and so on, for each pair of integer constants. Similarly,
we can introduce conditional constant , writing , with rules
and so on.
If we get something like
this is a run-time type error
- program would crash at run-time or produce bad result
- we introduce a type system to avoid this