# The Lambda Calculus

*First published Wed Dec 12, 2012*

The λ-calculus is, at heart, a simple notation for functions
and application. The main ideas are *applying* a function to
an argument and forming functions by *abstraction*. The syntax
of basic λ-calculus is quite sparse, making it an elegant,
focused notation for representing functions. Functions and arguments
are on a par with one another. The result is an intensional theory of
functions as rules of computation, contrasting with the traditional
extensional approach one of function as a set of pairs of a certain
kind. Despite its sparse syntax, the expressiveness and flexibility
of the λ-calculus make it a cornucopia of logic and
mathematics. This entry develops some of the central highlights of
the field and prepares the reader for further study of the subject and
its applications in philosophy, linguistics, computer science, and
logic.

- 1. Introduction
- 2. Syntax
- 3. Brief history of λ-calculus
- 4. Reduction
- 5. λ-theories
- 6. Consistency of the λ-calculus
- 7. Semantics of λ-calculus
- 8. Extensions and Variations
- 9. Applications
- Bibliography
- Academic Tools
- Other Internet Resources
- Related Entries
- Acknowledgments

## 1. Introduction

The λ-calculus is an elegant notation for working
with *applications* of *functions*
to *arguments*. To take a mathematical example, suppose we are
given a simple polynomial such
as *x*^{2} − 2·*x* + 5.
What is the value of this expression when *x* = 2? We compute
this by ‘plugging in’ 2 for *x* in the expression: we
get 2^{2} − 2·2 + 5,
which we can further reduce to get the answer 5. To use the
λ-calculus to represent the situation, we start with the
λ-term

λ

x[x^{2}− 2·x+ 5].

The λ operators allows us to *abstract* over *x*.
One can intuitively read
‘λ*x*[*x*^{2} − 2·*x* + 5]’
as an expression that is waiting for a value *a* for the
variable *x*. When given such a value *a* (such as the
number 2), the value of the expression is
*a*^{2} − 2·*a* + 5.
The ‘λ’ on its own has no significance; it
merely *binds* the variable *x*, guarding it, as it were,
from outside interference. The terminology in λ-calculus is
that we want to *apply* this expression to
an *argument*, and get a value. We write
‘*M**a*’ to denote the application of the
function *M* to the argument *a*. Continuing with the
example, we get:

(λ x[x^{2}− 2·x+ 5])2⊳ ⟨ Substitute 2 for x⟩2 ^{2}− 2·2 + 5= ⟨ Arithmetic ⟩ 4 − 4 + 5 = ⟨ Arithmetic ⟩ 5

The first step of this calculation, plugging in ‘2’ for
occurrences of *x* in the expression
‘*x*^{2} − 2·*x*
+ 5’, is the passage from an ** abstraction
term** to another term by the operation of substitution. The
remaining equalities are justified by computing with natural
numbers.

This example suggests the central principle of the
λ-calculus, called ** β-reduction**:

(β) (λ

x[M])N⊳M[x:=N]

The understanding is that we can *reduce* or *contract*
(⊳) an application (λ*x**M*)*N* of an
abstraction term (the left-hand side, λ*x**M*) to
something (the right-hand side, *N*) by simply plugging
in *N* for the occurrences of *x* inside *M* (that's
what the notation ‘*M*[*x* := *N*]’
expresses). This is the principle of ** β-reduction**;
it is the heart of the λ-calculus.

### 1.1 Multi-argument operations

What about functions of multiple arguments? Can the λ-calculus represent operations such as computing the length of the hypotenuse of a right triangle:

Hypotenuse of a right triangle with legs of length

xandy⇒ √(x² +y²),

The length-of-hypotenuse operation maps two positive real
numbers *x* and *y* and to another positive real number.
One can represent such multiple-arity operations using the apparatus
of the λ-calculus by viewing the operation as taking one input
at a time. Thus, the operation can be seen as taking one
input, *x*, a positive real number, and produces as its value not
a *number*, but an *operation*: namely, the operation
that takes a positive real number *y* as input and produces as
output the positive real number √(*x*²
+ *y*²). One could summarize the discussion by saying that
the operation, **hypotenuse-length**, that
computes the length of the hypotenuse of a right triangle given the
lengths *a* and *b* of its legs, is:

hypotenuse-length:= λa[λb[√(a² +b²)]]

By the principle of β-reduction, we have, for example,
that **hypotenuse-length** 3, the
application of **hypotenuse-length** to 3,
is λ*b*[√(3² + *b*²)], which is a
function of that is ‘waiting’ for another argument. The
λ-term **hypotenuse-length** 3 can
be viewed as a function that computes the length of the hypotenuse of
a right triangle the length of one of whose legs is 3. We find,
finally, that (**hypotenuse-length**
3)4—the application
of **hypotenuse-length** to 3 and then to
4—is 5, as expected.

Another way to understand the reduction of many-place functions to
one-place functions is to imagine a machine *M* that initially
starts out by loading the first *a* of multiple
arguments *a*, *b*, … into memory. If one then
suspends the machine after it has loaded the first argument into
memory, one can view the result as another machine
M_{a} that is awaiting one fewer input; the first
argument is now fixed.

### 1.2 Intensionality

The notion of function or operation at work in the λ-calculus
is an intensional one. We can view λ*x*[*M*] as
the *description* of an operation that, given *x*,
produces *M*; the body *M* of the abstraction term is itself
a description of what to do with *x*. Intuitively, given
descriptions *M* and *N*, we cannot in general decide
whether λ*x*[*M*] is equal to
λ*x*[*N*]. The two terms might ‘behave’
the same (have the same value given the same arguments), but it may
not be clear what resources are needed for showing the equality of the
terms.

By contrast, the definition of a function in set theory as a
set *f* of ordered pairs satisfying the property that
(*x*,*y*) ∈ f and (*x*,*z*) ∈ f
implies *y* = *z*. The notion of equality of functions is
equality of functions qua sets, which, under the standard principle of
extensionality of sets, entails that two functions are equal precisely
when they contain the same ordered pairs.

One can add a kind of extensionality principle to the λ-calculus; see section 5.2.

## 2. Syntax

The official syntax of the λ-calculus is quite simple; it is contained in the next definition.

DefinitionFor the alphabet of the language of the λ-calculus we take the left and right parentheses, left and right square brackets, the symbol ‘λ’, and an infinite set of variables. The class ofis defined inductively as follows:λ-terms

- Every variable is a λ-term.
- If
MandNare λ-terms, then so is (MN).- If
Mis a λ-term andxis a variable, then (λx[M]) is a λ-term.By ‘term’ we always mean ‘λ-term’. Terms formed according to rule (2) are called

. Terms formed according to rule (3) are calledapplication terms.abstraction terms

As is common when dealing with formal languages that have grouping symbols (the left and right parenthesis, in our case), some parentheses will be omitted when it is safe to do so (that is, when they can be reintroduced in only one sensible way). Juxtaposing more than two λ-terms is, strictly speaking, illegal. To avoid the tedium of always writing all needed parentheses, we adopt the following convention:

Convention(association to the left): When more than two termsM_{1}M_{2}M_{3}…M_{n}are juxtaposed we can recover the missing parentheses by: reading from left to right, groupassociating to the leftM_{1}andM_{2}together, yielding (M_{1}M_{2})M_{3}…M_{n}; then group (M_{1}M_{2}) withM_{3}: ((M_{1}M_{2})M_{3})…M_{n}, and so forth.

The convention thus gives a unique reading to any sequence of λ-terms whose length is greater than 2.

### 2.1 Variables, bound and free

The function of λ in an abstraction term
(λ*x*[*M*]) is that it ** binds** the
variable appearing immediately after it in the term

*M*. Thus λ is analogous to the universal and existential quantifiers ∀ and ∃ of first-order logic. One can define, analogously, the notions of free and bound variable in the expected way, as follows.

DefinitionThe syntactic functionsFVandBV(for ‘free variable’ and ‘bound variable’) are defined on the set of λ-terms by structural induction thus:

Free Bound

- For every variable
x,FV(x) = {x}.- For every term
Mand every termN,FV(MN) =FV(M) ∪FV(N).- For every variable
xand every termM,FV(λx[M]) =FV(M) − {x}.

- For every variable
x,BV(x) = ∅.- For every term
Mand every termN,BV(MN) =BV(M) ∪BV(N).- For every variable
xand every termM,BV(λx[M]) =BV(M) ∪ {x}.If

FV(M) = ∅ thenMis called a.combinator

Clause (3) in the two definitions supports the intention that
λ binds variables (ensures that they are not free). Note the
difference between **BV** and **FV** for variables.

As is typical in other subjects where the concepts appear, such as
first-order logic, one needs to be careful about the issue; a casual
attitude about substitution can lead to syntactic
difficulties.^{[1]} We can
defend a casual attitude by adopting the convention that we are
interested not in terms themselves, but in a certain equivalence class
of terms. We now define substitution, and then lay down a convention
that allows us to avoid such difficulties.

Definition(substitution) We write ‘M[x:=N]’ to denote the substitution ofNfor the free occurrences ofxinM. A precise definition^{[2]}by recursion on the set of λ-terms is as follows: for all terms A, B, and M, and for all variables x and y, we define

x[x:=M] ≡My[x:=M] ≡y(ydistinct fromx)- (
AB)[x:=M] ≡A[x:=M]B[x:=M]- (λ
x[A])[x:=M] ≡ λx[A]- (λ
y[A])[x:=M] ≡ λy[A[x:=M]] (ydistinct fromx)

Clause (1) of the definition simply says that if we are to
substitute *M* for *x* and we are dealing simply
with *x*, then the result is just *M*. Clause (2) says that
nothing happens when we are dealing (only) with a variable different
from *x* but we are to substitute something for *x*. Clause
(3) tells us that substitution unconditionally distributes over
applications. Clauses (4) and (5) concern abstraction terms and
parallel clauses (1) and (2) (or rather, clauses (2) and (1), in
opposite order): If the bound variable *z* of the abstraction
term λ*z*[*A*] is identical to the variable *x*
for which we are to do a substitution, then we do not perform any
substitution (that is, substitution “stops”). This
coheres with the intention that *M*[*x* := *N*] is
supposed to denote the substitution of *N* for the *free*
occurrences of *x* in *M*. If *M* is an abstraction
term λ*x*[*A*] whose bound variable is *x*,
then *x* does not occurr freely in *M*, so there is nothing
to do. This explains clause 4. Clause (5), finally, says that if the
bound variable of an abstrcation term differs from *x*, then at
least *x* has the “chance ” to occur freely in the
abstraction term, and substitution continues into the body of the
abstraction term.

Definition(change of bound variables, α-convertibility, no-capture convention on β-conversion) The termNis obtained from the termMby aif, roughly, any abstraction term λchange of bound variablesx[A] insideMhas been replaced by λy[A[x:=y]].Let us say that terms

MandNareif there is a sequence of changes of bound variables starting fromα-convertibleMand ending atN.Finally, we agree that when we write

‘(λ

x[M])Nreduces toM[x:=N]’,we require that no variable occurring freely in

Nbecomes bound after its substitution intoM.

Roughly, we need to adhere to the principle that free variables ought to remain free; when an occurrence of a variable is threatened to become bound by a substitution, simply perform enough α-conversions to sidestep the problem. If we keep this in mind, we can work with λ-calculus without worrying about these nettlesome syntactic difficulties.

The syntax of λ-calculus is quite flexible. One can form all
sorts of terms, even self-applications such as *x**x*. Such
terms appear at first blush to be suspicious; one might suspect that
using such terms could lead to inconsistency, and in any case one
might find oneself reaching for a tool with which to forbid such
terms. If one were to view functions and sets of ordered pairs of a
certain kind, then the *x* in *x**x* would be a
function (set of ordered pairs) that contains as an element a pair
(*x*,*y*) whose first element would be *x* itself. But
no set can contain itself in this way, lest the axiom of foundation
(or regularity) be violated. Thus, from a set theoretical perspective
such terms are clearly dubious. Below one can find a brief sketch of
one such tool, type theory. But in fact such terms do not lead to
inconsistency and serve a useful purpose in the context of
λ-calculus. Moreover, forbidding such terms, as in type
theory, does not come for free (e.g., some of the expressiveness of
untyped λ-calculus is lost).

### 2.2 Combinators

As defined earlier, a ** combinator** is a λ-term
with no free variables. One can intuitively understand combinators
are ‘completely specified’ operations, since they have no
free variables. There are a handful of combinators that have proven
useful in the history of λ-calculus; the next table highlights
some of these special combinators. Many more could be given (and
obviously there are infinitely many combinators), but the following
have concise definitions and have proved their utility.

Name | Definition & Comments | ||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|

S |
λx[λy[λz[xz(yz)]]]
Keep in mind that ‘ xz(yz)’ is to be understood as the application (xz)(yz) of xz to yz. S can thus be understood as a substitute-and-apply operator: z ‘intervenes’ between x and y: instead of applying x to y, we apply xz to yz. |
||||||||||

K |
λx[λy[x]]
The value of KM is the constant function whose value for any argument is simply M. |
||||||||||

I |
λx[x]
The identity function. |
||||||||||

B |
λx[λy[λz[x(yz)]]]
Recall that ‘ xyz’ is to be understood as (xy)z, so this combinator is not a trivial identity function. |
||||||||||

C |
λx[λy[λz[xzy]]]
Swaps an argument. |
||||||||||

T |
λx[λy[x]]
Truth value true. Identical to K. We shall see later how these representations of truth values plays a role in the blending of logic and λ-calculus. |
||||||||||

F |
λx[λy[y]]
Truth value false. |
||||||||||

ω |
λx[xx]
Self-application combinator |
||||||||||

Ω |
ωω
Self-application of the self-application combinator. Reduces to itself. |
||||||||||

Y |
λf[(λx[f(xx)])(λx[f(xx)])]
Curry's paradoxical combinator. For every λ-term X, we have:
YX reduces to the application term (λx[X(xx)])(λx[X(xx)]), which is recurring in the third step. Thus, Y has the curious property that YX and X(YX) reduce to a common term. |
||||||||||

Θ |
(λx[λf[f(xxf)]])(λx[λf[f(xxf)]])
Turing's fixed-point combinator. For every λ-term X, YX reduces to X(YX), which one can confirm by hand. (Curry's paradoxical combinator Y does not have this property.) |

Notation | Reading & Comments |
---|---|

MN |
The application of the function M to the argument N.
Usually, parentheses are used to separate the function from the argument, like so: ‘ |

PQR |
The application of the function PQ—which is itself the application of the function P to the argument Q—to R.
If we do not use parentheses to separate function and argument, how are we to disambiguate expressions that involve three or more terms, such as ‘ |

(λx[M]) |
The λ term that the variable bindsx in the term bodyM.
The official vocabulary of the λ-calculus consists of the symbol ‘λ’, left ‘(’and right ‘)’ parentheses, and a set of variables (assumed to be distinct from the three symbols ‘λ’, ‘(’, and ‘)’ lest we have syntactic chaos).
Some authors write ‘λ
Some authors write abstraction terms without any device
separating the bound variable from the body: such terms are
crisply written as, e.g.,
‘λ For the sake of uniformity, we will adopt the square bracket notation in this entry. (Incidentally, this notation is used in (Turing, 1937).) |

M[x := A] |
The λ-term that is obtained by substituting the λ-term A for all free occurrences of x inside M.
A bewildering array of notations to represent substitution can be found in the literature on λ-calculus and kindred subjects:
Which notation to use for substitution seems to be a personal matter. In this entry we use a linear notation, eschewing superscripts and subscripts. The practice of representing substitution with ‘:=’ comes from computer science, where ‘:=’ is read in some programming languages as assigning a value to a variable. As with the square brackets employed to write abstraction
terms, the square brackets employed to write substitution are
not officially part of the syntax of the
λ-calculus. |

M ≡ N |
The λ-terms M and N are identical: understood as
sequences of symbols, M and N have the same length and corresponding symbols of the sequences are identical.
The syntactic identity relation ≡ is not officially part of the official syntax of λ-calculus; this relation between λ-terms belongs to the metatheory of λ-calculus. It is clearly a rather strict notion of equality between λ-terms. Thus, it is not the case (if |

## 3. Brief history of λ-calculus

λ-calculus arose from the study of functions as rules.
Already the essential ingredients of the subject can be found in
Frege's pioneering work (Frege, 1893). Frege observed, as we did
above, that in the study of functions it is sufficient to focus on
unary functions (i.e., functions that take exactly one argument).
(The procedure of viewing a multiple-arity operation as a sequence of
abstractions that yield an equivalent unary operation is
called ** currying** the operation. Perhaps it would be more
historically accurate to call the operation

**, but there are often miscarriages of justice in the appellation of mathematical ideas.) In the 1920s, the mathematician Moses Schönfinkel took the subject further with his study of so-called**

*fregeing**combinators*. As was common in the early days of the subject, Schönfinkel was interested in the kinds of transformations that one sees in formal logic, and his combinators were intended to be a contribution to the foundations of formal logic. By analogy with the reduction that one sees in classical propositional logic with the Sheffer stroke, Schöfinkel established the astonishing result that the all functions (in the sense of all transformations) could be given in terms of the combinators

**K**and

**S**; later we will see the definition of these combinators.

TheoremFor every termMmade up ofKandSand the variablex, there exists a termF(built only fromKandS) such that we can deriveFx=M.

(The proof that these two suffice to represent all functions is
beyond the scope of this entry. For further discussion, see the entry
on
combinatory logic.)
One can prove the theorem constructively: there is an
algorithm that, given *M*, produces the required *F*.
Church called this *F*
‘λ*x*[*M*]’.^{[3]}
From this perspective, the β-rule can be justified: if
‘λ*x*[*M*]’ is to be a function *F*
satisfying *F**x* = *M*, then
λ*x*[*M*]x should transform to *M*. This is
just a special case of the more general principle that for
all *N*, (λ*x*[*M*])*N* should transform
to *M*[*x* := *N*].

Although today we have more clearly delimited systems of abstraction and rewriting, in the early days of λ-calculus and combinatory logic, à la Schönfinkel were bound up with investigations of foundations of mathematics. In the hands of Curry, Church, Kleene, and Rosser (some of the pioneers in the subject) the focus was on defining mathematical objects and carrying out logical reasoning inside the these new systems. It turned out that these early attempts at so-called illative λ-calculus and combinatory logic were inconsistent. Curry isolated and polished the inconsistency; the result is now known as Curry's paradox. See the entry on Curry's paradox and appendix B of (Barendregt, 1985).

The λ-calculus earns a special place in the history of logic
because it was the source of the first undecidable problem. The
problem is: given λ-terms *M* and *N*, determine
whether *M* = *N*. (A theory of
equational reasoning about λ-terms has not yet been defined;
the definition will come later.) This problem was shown to be
undecidable.

Another early problem in the λ-calculus was whether it is
consistent at all. In this context, inconsistency means that all
terms are equal: one can reduce any λ-term *M* to any
other λ-term *N*. That this is not the case is an early
result of λ-calculus. Initially one had results showing that
certain terms were not interconvertible (e.g., **K** and **S**);
later, a much more powerful result, the so-called Church-Rosser
theorem, helped shed more light on β-conversion and could be used
to give quick proofs of the non-inter-convertibility of whole classes
of λ-terms. See below for more detailed discussion of
consistency.

The λ-calculus was a somewhat obscure formalism until the 1960s, when, at last, a ‘mathematical’ semantics was found. Its relation to programming languages was also clarified. Till then the only models of λ-calculus were ‘syntactic’, that is, were generated in the style of Henkin and consisted of equivalence classes of λ-terms (for suitable notions of equivalence). Applications in the semantics of natural language, thanks to developments by Montague and other linguists, helped to ‘spread the word’ about the subject. Since then the λ-calculus enjoys a respectable place in mathematical logic, computer science, linguistics (see, e.g., Heim and Kratzer 1998), and kindred fields.

## 4. Reduction

Various notions of reduction for λ-terms are available, but the principal one is β-reduction, which we have already seen earlier. Earlier we used the notation ‘⊳’; we can be more precise. In this section we discuss β-reduction and some extensions.

Definition(one-step β-reduction ⊳_{β,1}) For λ-termsAandB, we say thatAβ-reduces in one step toB, writtenA⊳_{β,1}B, just in case there exists an (occurrence of a) subtermCofA, a variablex, and λ-termsMandNsuch thatC≡ (λx[M])NandBisAexcept that the occurrence ofCinAis replaced byM[x:=N].

Here are some examples of β-reduction:

The variable

*x*does not β-reduce to anything. (It does not have the right shape: it is simply a variable, not an application term whose left-hand side is an abstraction term.)(λ

*x*[*x*])*a*⊳_{β,1}*a*.If

*x*and*y*are distinct variables, then (λ*x*[*y*])*a*⊳_{β,1}*y*.The λ-term (λ

*x*[*(*λ*y*[*x**y*])*a*])*b*β-reduces in one step to two different λ-terms:(λ

*x*[*(*λ*y*[*x**y*])*a*])*b*⊳_{β,1}(λ*y*[*b**y*])*a*and

(λ

*x*[*(*λ*y*[*x**y*])*a*])*b*⊳_{β,1}(λ*x*[*x**a*])*b*Moreover, one can check that these two terms β-reduce in one step to a common term:

*b**a*. We thus have:(λ *y*[*b**y*])*a*↗ ↘ (λ *x*[*(*λ*y*[*x**y*])*a*])*b*ba ↘ ↗ (λ *x*[*x**a*])

As with any binary relation, one can ask many questions about the
relation ⊳_{β,1} holding between λ-terms,
and one can define various derived notions in terms of
⊳_{β,1}.

DefinitionAfrom a λ-termβ-reduction sequenceAto a λ-termBis a finite sequences_{1}, …s_{n}of λ-terms starting withA, ending withB, and whose adjacent terms (s_{k},s_{k+1}) satisfy the property thats_{k}⊳_{β,1}s_{k+1}.More generally, any sequence

s—finite or infinite—starting with a λ-termAis said to be a β-reduction sequence commencing withAprovided that the adjacent terms (s_{k},s_{k+1}) ofssatisfy the property thats_{k}⊳_{β,1}s_{k+1}.

Continuing with β-reduction Example 1, there are no β-reduction sequences at all commencing with the variable

*x*.Continuing with β-reduction Example 2, the two-term sequence

(λ

*x*[*x*])*a*,*a*is a β-reduction sequence from (λ

*x*[*x*])*a*to*a*. If*a*is a variable, then this β-reduction sequence cannot be prolonged, and there are no other β-reduction sequences commencing with (λ*x*[*x*])*a*; thus, the set of β-reduction sequences commencing with (λ*x*[*x*])*a*is finite and contains no infinite sequences.- The combinator
**Ω**has the curious property that Ω ⊳_{β,1}Ω. Every term of every β-reduction sequence commencing with**Ω**(finite or infinite) is equal to**Ω**. Consider the term

**K**a**Ω**. There are infinitely many reduction sequences commencing with this term:**K**a**Ω**⊳_{β,1}a**K**a**Ω**⊳_{β,1}**K**a**Ω**⊳_{β,1}a**K**a**Ω**⊳_{β,1}**K**a**Ω**⊳_{β,1}**K**a**Ω**⊳_{β,1}a**K**a**Ω**⊳_{β,1}**K**a**Ω**⊳_{β,1}**K**a**Ω**…

If

*a*is a variable, one can see that all finite reduction sequences commencing with**K**a**Ω**end at a, and there is exactly one infinite reduction sequence.

DefinitionAof a λ-termβ-redexMis (an occurrence of) a subterm ofMof the form (λx[P])Q. (‘redex’ comes from ‘reducible expression.) A β-redex is simply a candidate for an application of β-reduction. Doing so, onethe β-redex. A term is said to be incontractsif it has no β-redexes.β-normal form

(Can a term have multiple β-normal forms? The answer is
literally ‘yes’, but substantially the answer is
‘no’: If a *M* and *M*′ are β-normal
forms of some term, then *M* is α-convertible
to *M*′ Thus, β-normal forms are unique up to changes
of bound variables.)

So far we have focused only on one step of β-reduction. One
can combine multiple β-reduction steps into one by taking the
transitive closure of the relation ⊳_{β,1}.

DefinitionFor λ-termsAandB, one says thatAtoβ-reducesB, writtenA⊳_{β}B, if eitherA≡Bor there exists a finite β-reduction sequence fromAtoB.

DefinitionA termMif there exists a termhas a β-normal formNsuch thatNis in β-normal form anM⊳_{β}N.

Reducibility as defined is a one-way relation: it is generally not
true that if *A* ⊳_{β} *B*, then *B*
⊳_{β} *A*. However, depending on one's
purposes, one may wish to treat *A* and *B* as equivalent if
either *A* reduces to *B* or *B* reduces to *A*.
Doing so amounts to considering the reflexive, symmetric, and
transitive closure of the relation ⊳_{β,1,}.

DefinitionFor λ-termsAandB, we say thatA=_{β}Bif eitherA≡Bor there exists a sequences_{1}, …s_{n}starting withA, ending withB, and whose adjacent terms (s_{k},s_{k+1}) are such that eithers_{k}⊳_{β,1}s_{k+1}ors_{k+1}⊳_{β,1}s_{k}.

### 4.1 Other notions of reduction

We have thus far developed the theory of β-reduction. This is by
no means the only notion of reduction reduction available in the
λ-calculus. In addition to β-reduction, a standard
relation between λ-terms is that
of ** η-reduction**:

Definition(one-step η-reduction) For λ-termsAandB, we say thatAβη-reduces in one step toB, writtenA⊳_{βη,1}B, just in case there exists an (occurrence of a) subtermCofA, a variablex, and λ-termsMandNsuch that either

C≡ (λx[M])NandBisAexcept that the occurrence ofCinAis replaced byM[x:=N]or

C≡ (λx[Mx]) andBisAexcept that the occurrence ofCinAis replaced byM.

The first clause in the definition of ⊳_{βη,1}
ensures that the relation extends the relation of one-step
β-reduction. As we did for the relation of one-step
β-reduction, we can replay the development for η-reduction.
Thus, one has the notion of an η-redex, and from
⊳_{η,1} one can define the relation
⊳_{η} between λ-terms as the symmetric and
transitive closure of ⊳_{η,1}, which captures
zero-or-more-steps of η-reduction. Then one defines
=_{η} as the symmetric and transitive closure of
⊳_{η}.

If *A* ⊳_{η,1} *B*, then the length
of *B* is strictly smaller than that of *A*. Thus, there
can be no infinite η-reductions. This is not the case of
β-reduction, as we saw above
in β-reduction
sequence examples 3
and 4.

One can combine notions of reduction. One useful combination is to blend β- and η-reduction.

Definition(one-step βη-reduction) λx[Mx] ⊳_{βη,1}Mand (λx[M])N ⊳_{βη,1}M[x:=N]. A λ-termAβη-reduces in one step to a λ-termBjust in case eitherAβ-reduces toBin one step orAη-reduces toBin one step.

Again, one can replay the basic concepts of reduction, as we did for β-reduction, for this new notion of reduction βη.

### 4.2 Reduction strategies

Recall that a term is said to be in β-normal form if it has no
β-redexes, that is, subterms of the shape
(λ*x*[*M*])N. A term has a β-normal form if it
can be reduced to a term in β-normal form. It should be
intuitively clear that if a term has a β-normal form, then we can
find one by exhaustively contracting all all β-redexes of the
term, then exhaustively contracting all β-redexes of all
resulting terms, and so forth. To say that a term has a β-normal
form amounts to saying that this blind search for one will eventually
terminate.

Blind search for β-normal forms is not satisfactory. In
addition to be aesthetically unpleasant, it can be quite inefficient:
there may not be any need to exhaustively contract all β-redexes.
What is wanted is a *strategy*—preferably, a computable
one—for finding a β-normal form. The problem is to
effectively decide, if there are multiple β-redexes of a term,
which ought to be reduced.

DefinitionAis a function whose domain is the set of all λ-terms and whose value on a termβ-reduction strategyMnot in β-normal form is a redex subterm ofM, and whose value on all terms M in β-normal form is simplyM.

In other words, a β-reduction strategy selects, whenever a
term has multiple β-redexes, which one should be contracted. (If
a term is in β-normal form, then nothing is to be done, which is
why we require in the definition of β-reduction strategy that it
does not change any term in β-normal form.) One can represent a
strategy *S* as a relation ⊳_{S} on λ-terms,
with the understanding that *M* ⊳_{S} *N*
provided that *M* is obtained from *M* in one step by
adhering to the strategy S. When viewed as relations, strategies
constitute a subrelation of ⊳_{β,1}.

A β-reduction strategy may or may not have the property that adhering to the strategy will ensure that we (eventually) reach a β-normal form, if one exists.

DefinitionA β-reduction strategySisif for all λ-termsnormalizingM, ifMhas a β-normal formN, then the sequenceM,S(M),S(S(M)), … terminates atN.

Some β-reduction strategies are normalizing, but others are not.

- The
, whereby we always choose to reduce the rightmost β-redex (if there are any β-redexes) is not normalizing. Consider, for example, the term*rightmost strategy***K****I****ω**. This term has two β-redexes: itself, and**ω**(which, recall, is the term (λx[*x**x*])(λx[*x**x*])). By working with left-hand β-redexes, we can β-reduce**K****I****ω**to**I**in two steps. If we insist on working with the rightmost β-redex**ω**we reduce**K****I****ω**to**K****I**(**ω****ω**), then**K****I**(**ω****ω****ω**), … . - The
, whereby we always choose to reduce the leftmost β-redex (if there are any β-redexes) is normalizing. The proof of this fact is beyond the scope of this entry; see (Barendregt, 1985, section 13.2) for details.*leftmost strategy*

Once we have defined a reduction strategy, it is natural to ask
whether one can improve it. If a term has a β-normal form, then
a strategy will discover a normal form; but might there be a shorter
β-reduction sequence that reaches the same normal form (or a term
that is α-convertible to that normal form)? This is the
question of *optimality*. Defining optimal strategies and
showing that they are optimal is generally considerably more difficult
than simply defining a strategy. For more discussion, see
(Barendregt, 1984 chapter 10).

For the sake of concreteness, we have discussed only
β-reduction strategies. But in the definitions above the notion
of reduction β is but one possibility. For any notion *R*
of reduction we have the associated theory of *R*-reduction
strategies, and one can replay the problems of normalizability,
optimality, etc., for *R*.

## 5. λ-theories

We discussed earlier how the λ-calculus is an intensional
theory of functions. If, in the intensional spirit, we understand
λ-terms as descriptions, how should we treat equality of
λ-terms? Various approaches are available. In this section,
let us treat the equality relation = as a primitive, undefined
relation holding between two λ-terms, and try
to *axiomatize* the properties that equality should have. The
task is to identity axioms and formulate suitable ** rules of
inference** concerning the equality of λ-terms.

Some obvious properties of equality, having nothing to do with λ-calculus, are as follows:

Reflexivity, symmetry, and transitivity of equality of λ-terms as rules of inference Reflexivity Symmetry Transitivity X=YY=YX=ZX=XY=XX=Z

As is standard in proof theory, the way to read these rules of
inference is that above the horizontal
rule **—** are the
the ** premises** of the rule (which are equations) and the
equation below the horizontal rule is the

**of the rule of inference. In the case of the reflexivity rule, nothing is written above the horizontal rule. We understand such a case as saying that, for all terms**

*conclusion**X*, we may infer the equation

*X*=

*X*from no premises.

### 5.1 The basic theory λ

The three rules of inference listed in the previous section governing equality have nothing to do with the λ-calculus. The following lists rules of inference that relate the undefined notion of equality and the two term-building operations of the λ-calculus, application and abstraction.

M = N |
M = N |
M = N |
||

AM = AN |
MA = NA |
λx[M] = λx[N] |

These rules of inference say that = is a ** congruence
relation** on the set of λ-terms: it
‘preserves’ both the application and abstraction
term-building operations

The final rule of inference, β-conversion, is the most important:

β(λ x[M])A=M[x:=A]

As before with the reflexivity rule, the rule **β** has no
premises: for any variable *x* and any terms *M*
and *A*, one can infer the equation
(λ*x*[*M*])*A* = *M*[*x* := *A*]
at any point in a formal derivation in the theory **λ**.

### 5.2 Extending the basic theory λ

A number of extensions to **λ** are available. Consider,
for example, the rule (**η**), which expresses the principle of
η-reduction as a rule of inference:

( η)λ x[Mx] =M

Rule **η** tells us that a certain kind of abstraction is
otiose: it is safe to identify *M* with the function that, given
an argument *x*, applies *M* to *x*. Through this rule
we can also see that all terms are effectively functions. One can
intuitively justify this rule using the principle of
β-reduction.

( Ext)Mx=Nxprovided x∉FV(M) ∪FV(N)M=N

One can view rule **Ext** as a kind of generalization principle.
If we have derived that *M**x* = *N**x*,
but *x* figures in neither *M* nor *N*, then we have
effectively shown that *M* and *N* are alike. Compare this
principle to the principle of universal generalization in first-order
logic: if we have derived φ(*x*) from a set Γ of
hypotheses in which *x* is not free, then we can conclude that
Γ derives ∀*x*φ.

Another productive principle in the λ-calculus permits us to identify terms that ‘act’ the same:

( ω)For all terms x,Mx=NxM=N

The rule **ω** has infinitely many hypotheses: on the
assumption that *M**x* = *N**x*, no matter
what *x* may be, then we can conclude that *M* = *N*.
The **ω** rule is an analogue in the λ-calculus of the
rule of inference under the same name in formal number theory,
according to which one can conclude the universal formula
∀*x*φ provided one has proofs for φ(*x*
:= **0**), φ(*x* := **1**), … . Note that
unlike the rule **Ext**, the condition that *x* not occur
freely in *M* or *N* does not arise.

## 6. Consistency of the λ-calculus

Is the λ-calculus consistent? The question might not be
well-posed. The λ-calculus is not a logic for reasoning about
propositions; there is no apparent notion of contradiction (⊥) or
a method of forming absurd propositions
(e.g., *p* ∧ ¬*p*). Thus
‘consistency’ of the λ-calculus cannot mean that
⊥, or some formula tantamount to ⊥, is derivable. A
suitable notion of ‘consistent’ is, however, available.
Intuitively, a logic is inconsistent if it permits us to derive too
much. The theory **λ** is a theory of equations. We can
thus take inconsistency of **λ** to mean: *all equations
are derivable*. Such a property, if it were true
of **λ**, would clearly show that **λ** is of
little use as a formal theory.

Early formulations of the idea of λ-calculus by A. Church were
indeed inconsistent; see (Barendregt, 1985, appendix 2) or (Rosser,
1985) for a discussion. To take a concrete problem: how do we know
that the equation **K** = **I** is not a theorem
of **λ**? The two terms are obviously intuitively
distinct. **K** is a function of two arguments, whereas **I** is
a function of one argument. If we could show
that **K** = **I**, then we could show
that **K****K** = **I****K**, whence **K****K**
= **K** would be a theorem of **λ**, along with many
other equations that strike us as intuitively unacceptable. But when
we're investigating a formal theory such as **λ**, intuitive
unacceptability by no means implies underivability. What is missing
is a deeper understanding of β-reduction.

An early result that gave such an understanding is known as the Church-Rosser theorem:

Theorem(Church-Rosser) IfP⊳_{β}QandP⊳_{β}R, then there exists a termSsuch that bothQ⊳_{β}SandR⊳_{β}S.

(The proof of this theorem is quite non-trivial and is well-beyond
the scope of this entry.) The result is a deep fact about
β-reduction. It says that no matter how we diverge from *P*
by β-reductions, we can always converge again to a common
term.

The Church-Rosser theorem gives us, among other things, that the plain
λ-calculus—that is, the theory **λ** of
equations between λ-terms—is consistent, in the sense
that not all equations are derivable.

As an illustration, we can use the Church-Rosser theorem to solve
the earlier problem of showing that the two terms **K**
and **I** are not identified by **λ**. The two terms are
in β-normal form, so from them there are no β-reduction
sequences at all. If **K** = **I** were a theorem
of **λ**, then there would be a term *M* from which
there is a β-reduction path to both **I** and **K**. The
Church-Rosser theorem then implies the two paths diverging
from *M* can be merged. But this is impossible, since **K**
and **I** are distinct β-normal forms.

The Church-Rosser theorem implies the existence of β-reduction
sequences commencing from **K** and from **I** that end at a
common term. But there are no β-reduction sequences at all
commencing from **I**, because it is in β-normal form, and
likewise for **K**.

Theoremλis consistent, in the sense that not every equation is a theorem.

To prove the theorem, it is sufficient to produce one underivable
equation. We have already worked through an example: we used the
Church-Rosser theorem to show that the
equation **K** = **I** is not a theorem
of **λ**. Of course, there's nothing special about these
two terms. A significant generalization of this result is
available: *if M and N in β-normal form
but M is distinct from N, then the
equation M = N is not a theorem
of λ*. (This simple condition for underivability
does not generally hold if we add additional rules of inference
to

**λ**.)

The theories **λη** and **λω** are
likewise consistent. One can prove these consistency results along
the lines of the consistency proof for **λ** by extending
the Church-Rosser theorem to the wider senses of derivability of these
theories.

## 7. Semantics of λ-calculus

Although the λ-calculus is ‘about’ calculating with
functions by substituting values for arguments, this simple point of
view cannot support a semantics for the (untyped) λ-calculus if
by ‘function’ we understand, as is standard in set theory,
a relation *R* such that for every pair (*x*,*y*) and
(*x*,*z*) in *R* with the same first component *x*
we have *y* = *z*. For sets *X* and *Y*,
let *X*^{Y} denote the set of functions whose
domain is *Y* and with values in *X*. Intuitively,
if *X* is the domain of an interpretation of λ-calculus,
then *X* should be, in some sense, isomorphic
to *X*^{X} because the domain should be closed
under abstraction (as well as application). Taken literally, though,
this isomorphism is impossible, because the cardinality of *X*
always is of strictly smaller than the cardinality
of *X*^{X}.

If one is interested in simply the *existence* of some kind
of model of the λ-calculus—one whose domain not
necessarily consist of functions—one can find them by various
well-known ‘syntactic’ constructions involving the
theory **λ**, not unlike the well-known Henkin constructions
. These so-called term models, though, are an unsatisfactory solution
to the question of whether there are ‘mathematical’ models
of the λ-calculus.

The cardinality argument shows that if we are to have a semantics
for λ-calculus, the interpretation of λ-terms cannot
simply be functions in the set-theoretic sense of the term. There
are, however, interpretations of λ-calculus. The first
model, *D*_{∞}, was found by D. Scott; other
models were found later. These models solve the cardinality problem by
restricting the domain *X* of interpretation, so that, in
them, *X* is in a suitable sense isomorphic to the
‘function space’ *X*^{X}.

One of the advantages of having different interpretations is that
one sees different aspects of equality: each of these models takes a
different view on what λ-terms get identified. The definitions
of *D*_{∞} and other interpretations, the
verifications that they are indeed models of λ-calculus, and
the characterizations of the λ-theories of these models, are
beyond the scope of this entry; see (Barendregt, 1985, chapter 18) for
details.

## 8. Extensions and Variations

### 8.1 Combinatory logic

A sister formalism of the λ-calculus, developed slightly
earlier, deals with variable-free combinations. ** Combinatory
logic** is indeed even simpler than the λ-calculus, since
it lacks a notion of variable binding.

The language of combinatory logic is built up
from ** combinators** and variables. There is some
flexibility in precisely which combinators are chosen as basic, but
some standard ones are

**I**,

**K**,

**S**,

**B**and

**C**. (The names are not arbitrary.)

As with the λ-calculus, with combinatory logic one is
interested in *reducibility* and *provability*. The
principal reduction relations are:

Combinator Reduction Axiom IIx=xKKxy=xSSxyz=xz(yz)BBxyz=x(yz)CCxyz=xzy

There is a passage from λ-calculus to combinatory logic via translation. It turns out that although combinatory logic lacks a notion of abstraction, one can define such a notion and thereby simulate the λ-calculus in combinatory logic. Here is one translation; it is defined recursively.

Rule | Expression | Translation | Condition |
---|---|---|---|

1 | x |
x |
(unconditional) |

2 | MN |
M^{*}N^{*} |
(unconditional) |

3 | λx[M] |
KM |
x does not occur freely in M |

4 | λx[x] |
I |
(unconditional) |

5 | λx[Mx] |
M | x does not occur freely in M |

6 | λx[MN] |
BM(λx[N)]^{*} |
x does not occur freely in M |

7 | λx[MN] |
C(λx[M])^{*}N |
x does not occur freely in N |

8 | λx[MN] |
SM^{*}N^{*} |
x occurs freely in both M and N |

This translation works inside-out, rather than outside-in. To illustrate:

The translation of the term λ

*y*[*y*], a representative of the identity function, is mapped by this translation to the identity combinator**I**(because of Rule 4), as expected.The λ-term λ

*x*[λ*y*[*x*]] that we have been calling ‘**K**’is mapped by this translation to:λ *x*[λ*y*[*x*]]≡ ⟨ Rule 1 ⟩ λ *x*[**K***x*]≡ ⟨ Rule 3 ⟩ **K**The λ-term λ

*x*[λ*y*[*y**x*]] that switches its two arguments is mapped by this translation to:λ *x*[λ*y*[*y**x*]]≡ ⟨ Rule 8 ⟩ λ *x*[**C**(λ*y*[*y*])^{*}*x*]≡ ⟨ λ *y*[*y*] ≡**I**, by Rule 4 ⟩λ *x*[**C****I***x*]≡ ⟨ Rule 7 ⟩ **B**(**C****I**)(λ*x*[*x*])^{*}≡ ⟨ (λ *x*[*x*])^{*}≡**I**, by Rule 4 ⟩**B**(**C****I**)**I**We can confirm that the λ-term λ

*x*[λ*y*[*y**x*]] and the translated combinatory logic term**B**(**C****I**)**I**have analogous applicative behavior: for all λ-terms*P*and*Q*we have(λ

*x*[λ*y*[*y**x*]])*P**Q*⊳ λ*y*[*y**P*]) ⊳*Q**P*;likewise, for all combinatory logic terms

*P*and*Q*we have**B**(**C****I**)**I***P**Q*⊳ (**C****I**)(**I***P*)*Q*⊳**I***Q*(**I***P*) ⊳*Q*(**I**P) ⊳*Q**P*

We can give but a glimpse of combinatory logic; for more on the subject, consult the entry on combinatory logic. Many of the issues discussed here for λ-calculus have analogues in combinatory logic, and vice versa.

### 8.2 Adding types

In many contexts of reasoning and computing it is natural to
distinguish between different kinds of objects. The way this
distinction is introduced is by requiring that certain formulas,
functions, or relations accept arguments or permit substitution only
of some kinds of objects rather than others. We might require, for
example, that addition + take numbers as arguments. The effect of
this restriction is to forbid, say, the addition of 5 and the identity
function
λ*x*.*x*.(4). Regimenting
objects into types is also the idea behind the passage from (unsorted,
or one-sorted) first-order logic to *many-sorted* first-order
logic. (See (Enderton, 2001) and (Manzano, 2005) for more about
many-sorted first-order logic.) As it stands, the λ-calculus
does not support this kind of discrimination; any term can be applied
to any other term.

It is straightforward to extend the untyped λ-calculus so that
it discriminates between different kinds of objects. This entry
limits itself to the *type-free* λ-calculus. See the
entries on type theory
and
Church's type theory
for a detailed discussion of the extensions of λ-calculus that
we get when we add types.

## 9. Applications

### 9.1 Logic à la λ

Here are two senses in which λ-calculus is connected with logic.

#### 9.1.1 Terms as logical constants

In the table of combinators above,
we defined combinators **T** and **F** and said that they serve
as representations in the λ-calculus of the truth values true
and false, respectively. How do these terms function as truth
values?

It turns out that when one is treating λ-calculus as a kind
of programming language, one can write conditional statements
“If *P* then *A* else *B*” simply
as *P**A**B*, where of course *P*, *A*,
and *B* are understood as λ-terms. If *P*
⊳ **T**, that is, P is ‘true’, then we have

if-

P-then-A-else-B:=PAB⊳TAB⊳A,

(recall that, by definition, **T** ≡ **K**) and if P
⊳ **F**, that is, *P* is ‘false’, then

if-

P-then-A-else-B:=PAB⊳FAB⊳B,

(recall that, by definition, **T** ≡ **K****I**)
which is just what we expect from a notion of if-then-else.
If *P* reduces neither to **T** nor **F**, then we cannot
in general say what if-*P*-then-*A*-else-*B* is.

The encoding we've just sketched of some of the familiar truth values and logical connectives of classical truth-table logic does not show that λ-calculus and classical logic are intimately related. The encoding shows little more than embeddibility of the rules of computation of classical truth-table logic in λ-calculus. Logics other than classical truth-table logic can likewise be represented in the λ-calculus, if one has sufficient computable ingredients for the logic in question (e.g., if the logical consequence relation is computable, or if a derivability relation is computable, etc.). For more on computing with λ-calculus, see section 9.2 below. A more intrinsic relationship between logic and λ-calculus is discussed in the next section.

#### 9.1.2 Typed λ-calculus and the Curry-Howard-de Bruijn correspondence

The correspondence to be descried here between logic and the
λ-calculus is seen with the help of an apparatus known
as *types*. This section sketches the beginnings of the
development of the subject known as ** type theory**. We are
interested in developing type theory only so far as to make the
so-called Curry-Howard-de Bruijn correspondence visible. A more
detailed treatment can be found in the entry on
type theory; see also (Hindley 1997).

Type theory enriches the untyped λ-calculus by requiring
that terms be given ** types**. In the untyped
λ-calculus, the application

*M*

*N*is a legal term regardless of what

*M*and

*N*are. Such freedom permits one to form such suspicious terms as

*x*

*x*, and thence terms such as the paradoxical combinator

**Y**. One might wish to exclude terms like

*x*

*x*on the grounds that

*x*is serving both as a function (on the left-hand side of the application) and as an argument (on the right-hand side of the application). Type theory gives us the resources for making this intuitive argument more precise.

Assigning types to termsThe language of type theory begins with an (infinite) set of(which is assumed to be disjoint from the set of variables of the λ-calculus and from the symbol ‘λ’ itself). The set of types is made up of type variables and the operation σ → τ. Variables in type theory now come with atype variables(unlike the unadorned term variables of untyped λ-calculus). Typed variables are rendered ‘type annotationx: σ’; the intuitive reading is ‘the variablexhas the type σ’. The intuitive reading of the judgment ‘t: σ → τ’ is that the termtis a function that transforms arguments of type σ into arguments of type τ. Given an assignment of types to term variables, one has the typing rules:(

M: σ → τ)(N: σ) : τand

(λ

x: σ [M: τ]) : σ → τThe above two rules define the assignment of types to applications and to abstraction terms. The set of terms of type theory is the set of terms built up according to these formation rules.

The above definition of the set of terms of type theory is sufficient
to rule out terms such as *x**x*. Of course,
‘*x**x*’ is not a typed term at all for the
simple reason that no types have been assigned to it. What is meant
is that there is no type σ that could be assigned to *x*
such that ‘*x**x*’ could be annotated in a legal
way to make a typed term. We cannot assign to *x* a type
variable, because then the type of the left-hand *x* would fail
to be a function type (i.e., a type of the shape ‘σ →
τ’). Moreover, we cannot assign to *x* a function type
σ → τ, because then then σ would be equal to
σ → τ, which is impossible.

As a leading example, consider the types that are assigned to the
combinators **I**, **K**, and **S**:

Combinator | Type^{[5]} |
---|---|

I |
a → a |

K |
a → (b → a) |

S |
a → (b → c) → ((a → b) → (a → c)) |

(See Seldin (1997) *Table of principle types* for a more extensive listing.) If we read ‘→’ as implication and type variables as
propositional variables, then we recognize three familiar tautologies
in the right-hand column of the table. The language used is meager:
there are only propositional variables and implication; there are no
other connectives.

The table suggests an interesting correspondence between λ-calculus. Could it really be that the types assigned to formulas, when understood as logical formulas, are valid? Yes, though ‘validity’ needs to understood not as classical validity:

TheoremIf τ is the type of some λ-term, then τ is intuitionistically valid.

The converse of this theorem holds as well:

TheoremIf φ is an intuitionistically valid logical formula whose only connective is implication (→), then φ is the type of some λ-term.

The correspondence can be seen when one identifies intuitionistic validity with derivability in a certain natural deduction formalism. For a proof of these two theorems, see (Seldin, 1997, chapter 6).

The correspondence expressed by the previous two theorems between
intuitionistic validity and typability is known as
the *Curry-Howard-de Bruijn* correspondence, after three
logicians who noticed it independently. The correspondence, as
stated, is between only propositional intuitionistic logic, restricted
to the fragment containing only the implication connective →.
One can extend the correspondence to other connectives and to
quantifiers, too, but the most crisp correspondence is at the level of
the implication-only fragment. For details, see (Howard, 1980).

### 9.2 Computing

One can represent natural numbers in a simple way, as follows:

Definition(ordered tuples, natural numbers) The ordered tuple ⟨a_{0},…a_{n}⟩ of λ-terms is defined as λx[xa_{0}…a_{n}]. One then defines the λ-term ⌜n⌝ corresponding to the natural number n as: ⌜0⌝ =Iand, for everyk, ⌜k+ 1⌝ = ⟨F, ⌜k⌝⟩.

The λ-term corresponding to the number 1, on this representation, is:

⌜1⌝ ≡ ⟨ **F**,⌜0⌝⟩≡ ⟨ **F**,**I**⟩≡ λ *x*[*x***F****I**]The λ-term corresponding to the number 2, on this representation, is:

⌜2⌝ ≡ ⟨ **F**,⌜1⌝⟩≡ λ *x*[*x***F**λ*x*[*x***F****I**]]Similarly, ⌜3⌝ is λ

*x*[*x***F**λ*x*[*x***F**λ*x*[*x***F****I**]]].

Various representations of natural numbers are available; this
representation is but
one.^{[6]}

Using the ingredients provided by the λ-calculus, one can represent all recursive functions. This shows that the model is exactly as expressive as other models of computing, such as Turing machines and register machines. Priority goes to Turing's definition of his machine, but Church's proposal of the λ-calculus was developed at almost exactly the same time.

TheoremFor every recursive functionfof arityn, there exists a λ-termf^{*}such thatfor all natural numbers a

_{1},…a_{n}: f(a_{1},…a_{n}) =yiffλ⊢ f^{*}⟨a_{1},…a_{n}⟩ = y

For a proof, see the appendix.

Since the class of recursive functions is an adequate representation of the class of all computable (number-theoretic) functions, thanks to the work above we find that all computable (number-theoretic) functions can be faithfully represented in the λ-calculus.

### 9.3 Relations

The motivation for the λ-calculus given at the beginning of
the entry was based on reading λ-expressions as descriptions of
functions. Thus, we have understood
‘λ*x*[*M*]’ to be a (or the) function
that, given *x*, gives *M* (which generally, though not
necessarily, involves x). But it is not necessary to read
λ-terms as functions. One could understand λ-terms as
denoting relations, and read an abstraction term
‘λ*x*[*M*]’ as the unary
relation *R* that holds of an argument *x* just in
case *M* does. On the relational reading, we can understand an
application term *M**N* as a form of predication. One can
make sense of these terms using the principle of
β-conversion:

(λ

x[M])a=M[x:=A],

which says that the abstraction relation
λ*x*[*M*], predicated of A, is the relation obtained
by plugging in A for all free occurrences of *x*
inside *M*.

As a concrete example of this kind of approach to λ-calculus, consider an extension of first-order logic where one can form new atomic formulas using λ-terms, in the following way:

Syntax: For any formula φ and any finite sequencex_{1}, …,x_{n}of variables, the expression ‘λx_{1}…x_{n}[φ]’ is a predicate symbol of arity n. Extend the notion of free and bound variables (using the functionsFVandBV) in such a way that

FV(λx_{1}…x_{n}[φ]) =FV(φ) − {x_{1}, …x_{n}}and

BV(λx_{1}…x_{n}[φ]) =BV(φ) ∪ {x_{1}, …x_{n}}

DeductionAssume as axioms the universal closures of all equivalencesλ

x_{1}…x_{n}[φ](t_{1},…t_{n}) ↔ φ[x_{1},…x_{n}:= t_{1},…t_{n}]where φ[

x_{1},…x_{n}:= t_{1},…t_{n}] denotes the simultaneous substitution of the termst_{k}for the variablesx_{k}(1 ≤ k ≤ n).

SemanticsFor a first-order structureAand an assignmentsof elements ofAto variables, defineA ⊨ λ

x_{1}…x_{n}[φ](t_{1},…t_{n}) [s] iff A ⊨ φ[x_{1},…x_{n}:= t_{1},…t_{n}] [s]

According to this approach, one can use a λ to treat essentially any formula, even complex ones, as if they were atomic. We see the principle of β-reduction in the deductive and semantic parts. That this approach adheres to the relational reading of λ terms can be seen clearly in the semantics: according to the standard Tarski-style semantics for first-order logic, the interpretation of a formula (possibly with free variables) denotes a set of tuples of elements of the structure, as we vary the variable assignment that assigns elements of the structure to the variables.

One can ‘internalize’ this functional approach. This
is done in the case of various *property theories*, formal
theories for reasoning about properties as metaphysical objects
(Bealer 1982, Zalta 1983, Menzel 1986, and Turner 1987). This kind of
theory is employed in certain metaphysical investigations where
properties are metaphysical entities to be investigated. In these
theories, metaphysical relations are (or are among) the objects of
interest; just as we add term-building symbols + and × in formal
theories of arithmetic to build numbers, λ is used in property
theory to build relations. This approach contrasts with the approach
above. There, λ was added to the grammar of first-order logic
by making it a recipe for building atomic formulas; it was a new
formula-building operator, like ∨ or → or the other
connectives. In the case of property theories, the λ plays a
role more like + and × in formal theories of arithmetic: it is
used to construct relations (which, in this setting, are to be
understood as a kind of metaphysical object). Unlike + and ×,
though, the λ binds variables.

To give an illustration of how λ is used in this setting,
let us inspect the grammar of a typical application (McMichael and
Zalta, 1980). One typically has a *predication operator* (or,
more precisely, a family of predication
operators) *p*_{k} (*k* ≥ 0). In a
language where we have terms **mary**
and **john** and a binary relation loves,
we can formally express:

- John loves Mary: loves(
**john**,**mary**) - The property that John loves Mary: λ[loves(
**john**,**mary**)] (note that the λ is binding no variables; we might call this ‘vacuous binding’. Such properties can be understood as propositions.) - The property of an object
*x*that John loves it: λ*x*[loves(**john**,x)]. - The property that Mary is loved by something: λ[∃
*x*(loves(*x*,**mary**))] (another instance of vacuous binding, viz., proposition) - The predication of the property of
*x*that John loves*x*to Mary: p_{1}(λ*x*[loves(**john**,*x*)],**mary**). - The (0-ary) predication of the property that John loves Mary: p
_{0}(λ*x*[loves(**john**,**mary**)]). - The property of objects
*x*and*y*that*x*loves y: λ*x*y[loves(*x*,*y*)]. - The property of an objects
*x*that*x*loves itself: λ*x*[loves(*x*,*x*)]. - The predication of the property of objects
*x*and*y*that*x*loves*y*to John and Mary (in that order): p_{2}(λ*x*y[loves(*x*,*y*)],**john**,**mary**).

We reason with these λ-terms using a β-conversion principle such as:

p_{n}(λx_{1},…x_{n}[A],t_{1}, …,t_{n}) ↔ A[x_{1},…x_{n}:= t_{1},…t_{n}]

Formally, the predication operator p_{k} is a
(*k*+1)-ary predicate symbol. The first argument is intended to
be a λ-term of *k* arguments, and the rest of the
arguments are intended to be the arguments of the body of the
λ-term. The β-principle above says that the predication
of an *n*-ary λ-term *L* to *n* terms holds
precisely when the body of *L* holds of those terms.

It turns out that in these theories, we may or may not be able to be fully committed to the principle of β-conversion. Indeed, in some property theories, the full principle of β-conversion leads to paradox, because one can replay a Russell-style argument when the full principle of β-conversion is in place. In such settings, one restricts the formation of λ-formulas by requiring that the body of a λ-term not contain further λ-terms or quantifiers. For further discussion, see (Orilia, 2000).

## Bibliography

- Baader, Franz and Tobias Nipkow, 1999,
*Term Rewriting and All That*, Cambridge: Cambridge University Press. - Barendregt, H.P., 1985,
*The Lambda Calculus: Its Syntax and Semantics*(Studies in Logic and the Foundations of Mathematics 103), 2nd edition, Amsterdam: North-Holland. - Barendregt, H.P., 1993, “Lambda calculi with types”,
in S. Abramsky, D. Gabbay, T. Maibaum, and H. Barendregt
(eds.),
*Handbook of Logic in Computer Science*, Volume 2, New York: Oxford University Press, pp. 117–309. - Bealer, G., 1982,
*Quality and Concept*, Oxford: Clarendon Press. - van Benthem, Johan, 1998,
*A Manual of Intensional Logic*, Stanford: CSLI Publications. - Cutland, N. J., 1980,
*Computability*, Cambridge: Cambridge University Press. - Doets, Kees and Jan van Eijk, 2004,
*The Haskell Road to Logic, Maths and Programming*, London: College Publications. - Enderton, Herbert B., 2001,
*A Mathematical Introduction to Logic*, 2nd edition, San Diego: Harcourt/Academic Press. - Frege, Gottlob, 1893,
*Grundgesetze der Arithmetik*, Jena: Verlag Hermann Pohle, Band I. Partial translation as*The Basic Laws of Arithmetic*, M. Furth (trans.), Berkeley: University of California Press, 1964. - Kleene, Stephen C., 1981, “Origins of recursive function
theory”,
*Annals of the History of Computing*, 3(1): 52–67. - Heim, Irene and Angelika Kratzer, 1998,
*Semantics in Generative Grammar*, Malden, MA: Blackwell. - Hindley, J. Roger, 1997,
*Basic Simple Type Theory*(Cambridge Tracts in Theoretical Computer Science 42), New York: Cambridge University Press. - Hindley, J. Roger and Jonathan P. Seldin,
2008,
*Lambda-Calculus and Combinators: An Introduction*, 2nd edition, Cambridge: Cambridge University Press. - Howard, W., 1980, ‘The formula-as-types notion of
construction’, in J. Hindley and J. Seldin (eds.),
*To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus, and Formalism*, London: Academic Press, pp. 479–490. - Manzano, Maria, 2005,
*Extensions of First-order Logic*(Cambridge Tracts in Theoretical Computer Science 19), Cambridge: Cambridge University Press. - McCarthy, John, 1960, ‘Recursive functions of symbolic
expressions and their computation by machine (Part
I)’,
*Communications of the ACM*, 3(4): 184–195. - McMichael, Alan and Edward N. Zalta, 1980, ‘An alternative
theory of nonexistent objects’,
*Journal of Philosophical Logic*, 9: 297–313. - Menzel, Christopher, 1986, ‘A complete, type-free second order logic of properties, relations, and propositions’, Technical Report #CSLI-86-40, Stanford: CSLI Publications.
- Nederpelt, R., with H. Geuvers and R. de Vriejer (eds.),
1994,
*Selected Papers on Automath*(Studies in Logic and the Foundations of Mathematics 133), Amsterdam: North-Holland. - Orilia, Francesco, 2000, ‘Property theory and the revision
theory of definitions’,
*Journal of Symbolic Logic*, 65(1): 212–246. - Partee, Barbara H., with Alice ter Meulen and Robert E. Wall,
1990,
*Mathematical Methods in Linguistics*, Berlin: Springer. - Revesz, G. E., 1988,
*Lambda-Calculus, Combinators, and Functional Programming*, Cambridge: Cambridge University Press; reprinted 2008. - Rosser, J. Barkley, 1984, “Highlights of the History of the
Lambda-Calculus”,
*Annals of the History of Computing*, 6(4): 337–349. - Schönfinkel, M., 1924. ‘On the building blocks of
mathematical logic’, in J. van Heijenoort (ed.),
*From Frege to Gödel: A Source Book in Mathematical Logic*, Cambridge, MA: Harvard University Press, 1967, pp. 355–366. - Troelstra, A. S. and H. Schwichtenberg, 2000,
*Basic Proof Theory*(Cambridge Tracts in Theoretical Computer Science 43), 2nd edition, Cambridge: Cambridge University Press. - Turing, A. M., 1937, ‘Computability and
λ-definability’,
*Journal of Symbolic Logic*, 2(4): 153–163. - Turner, R., 1987, ‘A theory of
properties’,
*Journal of Symbolic Logic*, 52(2): 455–472. - Zalta, E., 1983,
*Abstract Objects: An Introduction to Axiomatic Metaphysics*, Dordrecht: D. Reidel.

## Academic Tools

How to cite this entry. Preview the PDF version of this entry at the Friends of the SEP Society. Look up this entry topic at the Indiana Philosophy Ontology Project (InPhO). Enhanced bibliography for this entry at PhilPapers, with links to its database.

## Other Internet Resources

- The Lambda Calculator, a tool for working with λ-terms with an eye toward their use in formal semantics of natural language.
- Lambda Evaluator, for visualizing reductions. Standard combinators and Church numerals are predefined.
- Lambda calculus reduction workbench, for visualizing reduction strategies

## Related Entries

computer science, philosophy of | Curry's paradox | logic: combinatory | logic: intensional | logic: intuitionistic | logic: second-order and higher-order | properties | type theory | type theory: Church's type theory

### Acknowledgments

The author wishes to acknowledge the contributions of Henk Barendregt, Elizabeth Coppock, Reinhard Kahle, Martin Sørensen, and Ed Zalta in helping to craft this entry. The author thanks Nic McPhee for introducing him to the λ-calculus.