Elements of Lambda Calculus

Lambda Calculus

2026-08-19 09:15

Where we are

From motivation to mechanism

Introduction made the case: names as labels, order independence, recursion, functions as values.

It named the λ calculus but did not define it.

This unit defines it.

What this unit does not have

No numbers. No booleans. No data structures.

No conditionals. No recursion.

The only thing that exists is a function.

The only thing you can do is apply one to another.

How to read this unit

The book warns it will seem disjointed at first.

We build a set of useful functions bit by bit, and they become the building blocks of units 3 and 4.

Each example assumes the previous ones. Do the reductions by hand.

What abstraction is

One move

Take something concrete.

Notice a part that could vary.

Replace it with a name to be supplied later.

The result is a function of that name.

The cost calculation

A calculation for a particular item at a particular price.

The price could be anything — replace it with a name.

Instead of one answer, a function: something that gives an answer once told the price.

You already do this

  • procedures and functions abstract over a computation
  • parameters abstract over the values it works on
  • naming lets one thing stand for another

The λ calculus keeps the operation and throws away the wrapping.

The grammar of λ expressions

Church, 1930s

Devised as a model for computability — not as a programming language.

Very simple, very powerful, based on pure abstraction.

Three productions

<expression> ::= <name> | <function> | <application>

That is the entire language.

Names

Any sequence of non-blank characters:

fred    legs-11    19th_nervous_breakdown    33    +    -->

Functions

<function> ::= λ<name>.<body>
<body>     ::= <expression>

\[\lambda x.x \qquad \lambda first.\lambda second.first \qquad \lambda f.\lambda a.(f\ a)\]

The name after λ is the bound variable — like a formal parameter.

Two things more general than Pascal

The body may be any expression, including another function.

Functions do not have names.

In Pascal the name is always used to refer to the definition. Here a definition can appear directly where it is used.

Applications

<application> ::= (<function expression> <argument expression>)

\[(\lambda x.x\ \lambda a.\lambda b.b)\]

Also called a bound pair. The function expression is applied to the argument expression.

Evaluating an application

Evaluate the function expression to get a function.

Replace all occurrences of its bound variable in the body by either

  • the value of the argument expression, or
  • the unevaluated argument expression

Then evaluate the body.

Two orders

Applicative order

like Pascal call by value

evaluate the argument first

Normal order

like ALGOL 60 call by name

pass it unevaluated

Normal order is more powerful but may be less efficient.

This unit uses normal order throughout.

The first three functions

Identity

\[\lambda x . x\]

Returns whatever argument it is applied to.

\[(\lambda x . x\ \lambda x . x) \Rightarrow \lambda x.x\]

Self-application

\[\lambda s.(s\ s)\]

Applies its argument to its argument.

The body \((s\ s)\) has the name \(s\) as both function expression and argument expression.

Apply it to identity

\[(\lambda s.(s\ s)\ \lambda x.x)\]

Replace \(s\) by \(\lambda x.x\) in \((s\ s)\):

\[(\lambda x.x\ \lambda x.x)\]

\[\Rightarrow \lambda x.x\]

Now apply it to itself

\[(\lambda s.(s\ s)\ \lambda s.(s\ s))\]

Replace \(s\) by \(\lambda s.(s\ s)\) in \((s\ s)\):

\[(\lambda s.(s\ s)\ \lambda s.(s\ s))\]

The same expression.

No normal form

Two symbols. No recursion, no loop, no repetition construct.

It computes forever.

Function application

\[\lambda func.\lambda arg.(func\ arg)\]

Applied to a first argument, returns a function that applies it to a second.

\[((\lambda func.\lambda arg.(func\ arg)\ \lambda x.x)\ \lambda s.(s\ s))\]

Reducing it

The function expression is itself an application — evaluate it first:

\[\lambda arg.(\lambda x.x\ arg)\]

Now the whole expression is

\[(\lambda arg.(\lambda x.x\ arg)\ \lambda s.(s\ s))\]

\[\Rightarrow (\lambda x.x\ \lambda s.(s\ s)) \Rightarrow \lambda s.(s\ s)\]

Why bother?

Application is already in the grammar.

Making it a value is what lets application be passed around and abstracted over.

Naming and notation

Syntactic sugar

Named definitions, infix operations, an IF style conditional…

Syntactic sugaring: the representation changes, the underlying meaning stays the same.

The conditions on a sugar rule

  • applying it involves no choices
  • it reaches pure λ expressions in finitely many steps
  • so sugar can always be compiled away before evaluation

We never modify the calculus, so the existing theory keeps applying.

Naming functions

def <name> = <function>
def identity   = λx.x
def self_apply = λs.(s s)
def apply      = λfunc.λarg.(func arg)

A trap worth noticing now

A def name is an abbreviation, expanded where it appears.

Not a reference resolved at call time.

So a definition mentioning its own name expands forever.

Recursion cannot be had this way. Unit 4 is about escaping this.

Functions built from functions

A second identity

def identity2 = λx.((apply identity) x)
(identity2 identity) ==
(λx.((apply identity) x) identity) =>
((apply identity) identity) ==
((λfunc.λarg.(func arg) identity) identity) =>
(λarg.(identity arg) identity) =>
(identity identity) => ... =>
identity

Equivalent in general

Let <argument> stand for any expression:

(identity2 <argument>) ==
(λx.((apply identity) x) <argument>) =>
((apply identity) <argument>) => ... =>
(identity <argument>) => ... =>
<argument>

Same effect. And similarly:

def self_apply2 = λs.((apply s) s)

What “building” means here

There is no way to see the answer.

You reduce until you cannot, then recognise the result by comparing it with a definition you already have.

An error shows up as an expression that matches nothing.

Selectors and pairs

Select the first

def select_first = λfirst.λsecond.first
((select_first identity) apply) ==
((λfirst.λsecond.first identity) apply) =>
(λsecond.identity apply) =>
identity

Select the second

def select_second = λfirst.λsecond.second
((select_second identity) apply) ==
((λfirst.λsecond.second identity) apply) =>
(λsecond.second apply) =>
apply

identity was lost because first does not appear in the body.

Make a pair

def make_pair = λfirst.λsecond.λfunc.((func first) second)

first and second are used before func, to build:

\[\lambda func.((func\ first)\ second)\]

The trick

Apply that function to select_first → you get the first component.

Apply it to select_second → you get the second.

A pair is a function.

Watch it happen

((make_pair identity) apply) => λfunc.((func identity) apply)
(λfunc.((func identity) apply)
   select_first) ==
((select_first identity) apply) =>
identity
(λfunc.((func identity) apply)
   select_second) ==
((select_second identity) apply) =>
apply

Why this is the key section

  • storage replaced by a function that hands you what you ask for
  • data needs no separate mechanism — unit 1’s claim, demonstrated
  • structures nest: pairs of pairs give triples, lists, trees

Next unit: true and false are these two selectors.

Free and bound variables

When names are distinct, no problem

\[(\lambda f.(f\ \lambda x.x)\ \lambda s.(s\ s))\]

Three functions, bound variables \(f\), \(x\), \(s\).

\[\Rightarrow (\lambda s.(s\ s)\ \lambda x.x) \Rightarrow (\lambda x.x\ \lambda x.x) \Rightarrow \lambda x.x\]

The definition

A variable is bound to occurrences in the body of a function for which it is the bound variable — provided no other function within the body introduces the same name.

Otherwise it is free.

The same name, both ways

In the body of \(\lambda f.(f\ \lambda f.f)\), which is \((f\ \lambda f.f)\):

  • the first \(f\) is free — it corresponds to the outer bound variable
  • subsequent \(f\)s are bound, and distinct from it

The outer \(f\) is in scope except in the scope of the inner \(f\).

A harder one

\[\lambda g.((g\ \lambda h.(h\ (g\ \lambda h.(h\ \lambda g.(h\ g))))))\ g)\]

  • first, second and last \(g\) — free, so they are the outer bound variable
  • third and fourth — bound, and distinct

Why it matters

The distinction is per occurrence, not per name.

β reduction replaces the bound occurrences and must leave free ones alone.

Name clashes and α conversion

The setup

def apply = λfunc.λarg.(func arg)
((apply arg) boing) ==
((λfunc.λarg.(func arg) arg) boing)

arg is used as a bound variable name and as a free variable name.

Reduce literally, and…

((λfunc.λarg.(func arg) arg) boing) =>
(λarg.(arg arg) boing) =>
(boing boing)

Not intended at all.

The argument arg was substituted into the scope of the bound variable arg.

The fix: rename consistently

((λfunc.λarg1.(func arg1) arg) boing) =>
(λarg1.(arg arg1) boing) =>
(arg boing)

This is α conversion.

The rule

For \(\lambda \langle name1\rangle.\langle body\rangle\):

the name and all free occurrences of it in the body may be replaced by \(\langle name2\rangle\) —

provided \(\langle name2\rangle\) is not the name of a free variable in the function.

The replacement includes the name after the λ itself.

The error that does not announce itself

A captured variable still reduces.

It reduces to the wrong thing, silently.

The rule is easy. The noticing is the hard part.

Simplification through η reduction

The pattern

λ<name>.(<expression> <name>)

is equivalent to

<expression>

Why

(λ<name>.(<expression> <name>) <argument>) =>
(<expression> <argument>)

Which is what <expression> applied to that argument gives directly.

The wrapper carries no meaning.

Three conversions, three jobs

  • β — the actual computation: substitute and apply
  • α — housekeeping: rename to prevent capture
  • η — simplification: remove a redundant wrapper

Only β makes progress.

Summary

The library you built

def identity      = λx.x
def self_apply    = λs.(s s)
def apply         = λfunc.λarg.(func arg)
def select_first  = λfirst.λsecond.first
def select_second = λfirst.λsecond.second
def make_pair     = λfirst.λsecond.λfunc.((func first) second)

The core is complete

Three grammar productions. Three conversion rules.

Nothing further is added to the language in the rest of the module.

Everything from here is built inside it.

The five things to carry away

  • The λ calculus is a minimal, universal foundation — three productions.
  • β computes; α and η keep terms honest and readable.
  • Evaluation strategy decides termination, not the answer.
  • A pair is a function that takes a selector — data needs no separate mechanism.
  • Some expressions have no normal form.

Where next

Conditions, Booleans and Integers starts building.

  • the two selectors become true and false
  • the conditional expression follows almost immediately
  • then NOT, AND, OR
  • then the natural numbers, built inductively from pairs

Nothing but functions underneath.