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

Intuition

A function which takes its argument and increments it by 2 is given by lambda expression $\lambda x.\, x+2$ . The $\lambda$ 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:

$\begin{eqnarray*} (\lambda x.\, x + 2)\, 7 &=& 9 \\ ((\lambda x.\, (\lambda y.\, x - y))\, 5)\, 3 &=& (\lambda y.\, 5 - y) 3 = 5 - 3 = 2 \\ (((\lambda f.\, (\lambda x.\, f(f x))) (\lambda y.\, y^2))) 3 &=& (\lambda x.\, (\lambda y.\, y^2) ((\lambda y.\, y^2) x))) 3 = (\lambda y.\, y^2) ((\lambda y.\, y^2) 3) = (\lambda y.\, y^2) 9 = 81 \end{eqnarray*}$

Concrete syntax for $(\lambda x.x+2)5$ :

Isabelle (and Jahob): '(% x.x+2)5' or '(\<lambda> x.x+2)5'
ocaml: '(function x → x+2)5'
Haskell: '(\ x → x+2)5'
Scala: '((x:int) ⇒ x+2)(5)'

Lambda expressions

Untyped lambda expressions are given by following grammar:

$\begin{equation*}\begin{array}{l} T ::= v \mid \lambda v.T \mid T\, T \\ v ::= v_1 \mid v_2 \mid ... \end{array}\end{equation*}$

That is, an expression is a variable, a lambda expression defining a function, or an application of one expression to another.

Beta reduction

The main rule of lambda calculus is beta reduction, which formalizes function application:

$\begin{equation*} (\lambda x.\, s) t\ \mathop{\to}\limits^{\beta}\ s[x:=t] \end{equation*}$

where we assume capture-avoiding substitution. In general, we identify terms that differ only by renaming of fresh bound variables.

Here $\mathop{\to}\limits^{\beta}$ is a binary 'reduction' relation on terms. We build larger relations on terms by

performing reduction in any context $C$ , so we have $C[(\lambda x.\, s) t]\ \mathop{\to}\limits^{\beta}\ C[s[x:=t]]$
taking its transitive closure: computes all terms reachable by reduction

Non-termination and Difficulties with Semantics

Let $\omega$ denote term

$\begin{equation*} (\lambda x.xx)(\lambda x.xx) \end{equation*}$

Note that $\omega$ 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 $x x$ . Suppose the interpretation of variable $x$ ranges over a domain $D$ . This domain should be a set of total functions $f : A \to B$ to enable application. But all possible values of $x$ are an argument, so we have that

$\begin{equation*} D = [D \to D] \end{equation*}$

that is, the set $D$ is equal to the set of all functions from $D$ to $D$ . But this is not possible in set theory, because we can prove that the set $D^D$ has larger cardinality (even if it is infinite). For example, if $D$ is the set of natural numbers (which is countably infinite), then $D^D$ 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 $D \simeq [D \leadsto D]$ is obtained by finding a fixpoint of a monotonic operator $F(D) = [D \leadsto D]$ .

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.

References:

Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984)
Domain Theory and pdf file