Untyped Lambda Calculus
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
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:
Concrete syntax for :
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. In general, we identify terms that differ only by renaming of fresh bound variables.
Here is a binary 'reduction' relation on terms. We build larger relations on terms by
- performing reduction in any context , so we have
- taking its transitive closure: computes all terms reachable by reduction
Non-termination and Difficulties with Semantics
Let denote term
Note that beta reduces to itself. It represents infinite loop.
Note that the set of total functions is not a model of untyped lambda calculus. Consider the self-application expression . Suppose the interpretation of variable ranges over a domain . This domain should be a set of total functions to enable application. But all possible values of are an argument, so we have that
that is, the set is equal to the set of all functions from to . But this is not possible in set theory, because we can prove that the set has larger cardinality (even if it is infinite). For example, if is the set of natural numbers (which is countably infinite), then would be uncountably infinite.
The models of untyped lambda calculus do exist, but they usually consider only certain 'continuous', partial, functions. These domains are studied in domain theory. Roughly speaking, in domain theory, a solution to equation such as is obtained by finding a fixpoint of a monotonic operator .
Thus, untyped lambda calculus is easy to understand syntactically (as a set of rules for manipulating formal expressions), rather than a system where each expression has some intuitive meaning.
- Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984)