Lambda calculus ( $λ$ -calculus)

Lambda calculus forms terms from variables, abstraction, and application, and computes by substitution.

Table of contents

Lambda term

A lambda term is a variable, an abstraction

λ x . M

, or an application

MN

, formed recursively from lambda terms

M

and

N

.

Untyped lambda calculus

The untyped lambda calculus forms terms from variables, abstraction, and application without assigning types.

Beta reduction ( $β$ -reduction)

Beta reduction performs capture-avoiding substitution:

(λ x . M) N ⟶_{β} M [x := N] .

Capture-avoiding substitution

Capture-avoiding substitution

M [x := N]

replaces the free occurrences of

x

in

M

by

N

, renaming bound variables when necessary so that free variables of

N

do not become bound.

Beta equivalence ( $β$ -equivalence)

Beta equivalence is the smallest equivalence relation containing beta reduction; equivalently,

M \equiv_{β} N

when a finite sequence of beta reductions and reversed beta reductions connects

M

and

N

.

Beta-redex ( $β$ -redex)

A beta-redex is a subterm of the form

(λ x . M) N

, to which beta reduction can be applied.

Beta-normal form ( $β$ -normal form)

A lambda term is in beta-normal form when it contains no beta-redex.

Combinator

A combinator is a lambda term with no free variables.

Omega combinator ( $Ω$ )

The omega combinator is the divergent untyped lambda calculus term

Ω = (λ x . xx) (λ x . xx),

whose only beta reduction reproduces

Ω

.

Fixed-point combinator

An untyped lambda term

Y

is a fixed-point combinator when

Y f \equiv_{β} f (Y f)

for every term

f

.

Fixed-point theorem for the untyped lambda calculus

Every lambda term

F

has a fixed point: the term

X = (λ x . F (xx)) (λ x . F (xx))

satisfies

X \equiv_{β} F (X)

. Equivalently, a fixed-point combinator such as

Y = λ f . (λ x . f (xx)) (λ x . f (xx))

satisfies

Y F \equiv_{β} F (Y F)

for every

F

.

Recursively enumerable fixed-point combinators

The set of fixed-point combinators is recursively enumerable. Enumerate closed lambda terms and finite proofs of beta equivalence, and output

Y

whenever a proof of

Y f \equiv_{β} f (Y f)

appears for a fresh variable

f

.

Alpha equivalence ( $α$ -equivalence)

Two lambda terms are alpha-equivalent when they differ only by consistent renaming of bound variables.

Church-Rosser theorem

If a lambda term beta-reduces to both

M

and

N

, then

M

and

N

beta-reduce to a common term. Consequently two beta-equivalent beta-normal forms are alpha-equivalent.

Simply typed lambda calculus ( $λ^{\to}$ )

The simply typed lambda calculus assigns arrow types to variables, abstractions, and applications according to syntax-directed typing rules.

Weak normalization theorem for simply typed lambda calculus

Every well-typed term in the simply typed lambda calculus has some finite beta-reduction sequence ending in a beta-normal form.

Strong normalization theorem for simply typed lambda calculus

Every well-typed simply typed lambda term admits no infinite beta-reduction sequence.

Church numeral ( $c_{n}$ )

The Church numeral

c_{n} = λ f . λ x . f^{n} x

encodes the natural number

n

Lambda-definable function

g : N^{k} \to N

is lambda-definable when some combinator

G

satisfies

G c_{n_{1}} \dots c_{n_{k}} \equiv_{β} c_{g (n_{1}, \dots, n_{k})}

for every tuple of natural numbers.

Lambda definition of the successor function

The successor function is lambda-defined on Church numerals by

Succ = λn . λ f . λ x . f (n f x),

because

Succ c_{n} \equiv_{β} c_{n + 1}

.

Lambda definition of primitive recursion

Using a fixed-point combinator, Church Boolean conditionals, a zero test, and a predecessor term, lambda-definable

g

and

h

give

R x 0 = g (x), R x (n + 1) = h (x, n, R x n) .

Normal-order beta reduction evaluates only the selected conditional branch, so this term implements primitive recursion on Church numerals.

Lambda-definable partial function

A partial function is lambda-definable when one lambda term maps Church numerals in its domain to the numeral of the output and produces no numeral on inputs outside its domain.

Lambda definition of unbounded minimization

For a lambda-definable partial

g (x, n)

, a fixed-point search term tests

n = 0, 1, 2, \dots

and returns the first

n

for which

g (x, n) = 0

. If no such value is reached, reduction produces no Church numeral. This realizes unbounded minimization and therefore makes every partial recursive function lambda-definable.

Church Boolean

At type

σ \to σ \to σ

, the Church Booleans are

⊤ = λ x . λ y . x

and

⊥ = λ x . λ y . y

.

 Ancestors (5)

 View article source

 Discussion (0)

There are no discussions about this article yet.

 Articles by others on the same topic (1)

Lambda calculus by

Wikipedia Bot  1

Lambda calculus is a formal system in mathematical logic and computer science for expressing computation based on function abstraction and application. It was developed by Alonzo Church in the 1930s as part of his work on the foundations of mathematics. The key components of lambda calculus include: 1. **Variables**: These are symbols that can stand for values. 2. **Function Abstraction**: A lambda expression can describe anonymous functions.

 Read the full article

  See all articles in the same topic Create my own version