Elements of Lambda Calculus

Lambda Calculus · v1.1.0

2026-09-25 23:01:09

Where we are

Scope and prerequisites

• The previous unit named two mechanisms: abstraction and application
• That unit motivated; this one defines
• No numbers, booleans, data structures, conditionals or recursion
• Only functions, and only application

Everything built in this module comes from those two mechanisms alone.

Outline of key topics

• Abstraction, as an idea you already use
• The grammar: three productions, and every expression is one of them
• The first functions: identity, self-application, function application
• Notation for naming things
• Building new functions from old ones; selectors and pairs
• Free and bound variables, α and η conversion

From motivation to mechanism

The order of work

1. Abstraction as an idea, and where it already appears
2. The grammar — three productions
3. The first functions: identity, self-application, function application
4. Notation for naming things
5. Building new functions from old ones, then selectors and pairs
6. Free and bound variables, α and η conversion

How to read this unit

• Each example assumes the previous ones
• These functions are the building blocks of every later unit
• Work through the reductions by hand, in order

The material will seem disjointed at first — it is hard to introduce all of a new topic at once, so some details are sketchy to begin with. That is expected, not a sign of missing something.

What abstraction is

Definition — abstraction

Abstraction: replace a concrete part with a name, supplied later.

• notice a part that could vary
• replace it with a name
• the result is a function of that name

A cost for one price becomes a function of price.

The same move, in languages you know

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

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

The grammar of λ expressions

Three productions

\[\langle expression \rangle ::= \langle name \rangle \mid \langle function \rangle \mid \langle application \rangle\]

• a name — any sequence of non-blank characters
• a function — an abstraction over a λ expression
• an application — specialising an abstraction by supplying a value

Definition — function

\[\langle function \rangle ::= \lambda\langle name \rangle.\langle body \rangle\]

• the name after λ is the bound variable — like a formal parameter
• the body may be any λ expression, including another function
• functions have no names — a definition can sit where it is used

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

Definition — application

\[ \begin{align} \langle application \rangle &::= (\langle function\ expr \rangle\ \langle argument\ expr \rangle) \end{align} \]

• also called a bound pair
• the function expression is applied to the argument expression

\[ \begin{align} &(\lambda x.x\ \lambda a.\lambda b.b) \end{align} \]

Evaluating an application

Occurrences of the bound variable in the body are replaced by:

Applicative order

the value of the argument

like Pascal’s call by value

Normal order

the unevaluated argument

like ALGOL 60’s call by name

All applications in this unit are evaluated in normal order.

The first three functions

Example 1: identity

\[\lambda x.x\]

Returns whatever argument it is applied to.

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

The body is \(x\), so the argument comes back unchanged.

Example 2: self-application

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

Applies its argument to its argument.

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

It reduces to itself, forever.

No normal form

• A two-symbol function, no recursion, no loop, no repetition construct
• It computes forever
• The λ calculus can express computations with no normal form

The unsolvability of halting, appearing here in a few characters.

Example 3: function application

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

Returns a function that applies its first argument to its second.

\[ \begin{align} &((\lambda func.\lambda arg.(func\ arg)\ \lambda x.x)\ \lambda s.(s\ s)) \\ \Rightarrow\ &(\lambda x.x\ \lambda s.(s\ s)) \\ \Rightarrow\ &\lambda s.(s\ s) \end{align} \]

As a value, application can be passed and abstracted over.

Naming and notation

Syntactic sugar

• New syntax is introduced through substitution rules
• Applying a rule involves no choices
• Rules expand to pure λ expressions in finitely many steps

Any sugared form compiles back to λ calculus before evaluation.

When the next unit writes true, false and cond, and the unit after writes rec, none of them is a new construct — each is an abbreviation with a pure λ expression behind it, and each can always be expanded.

Naming functions

\[\text{def}\ \langle name \rangle = \langle function \rangle\]

def identity   = λx.x
def self_apply = λs.(s s)
def apply      = λfunc.λarg.(func arg)

• A name is an abbreviation, expanded where it appears
• Not a reference resolved at call time

A definition naming itself expands forever: no recursion this way.

Functions built from functions

A second identity

def identity2 = λx.((apply identity) x)

\[(identity2\ identity) \Rightarrow \ldots \Rightarrow identity\]

Any argument reduces back to itself — the effect of identity.

What “building” means here

• There is no way to see the answer in advance
• Reduce until stuck, then match the result against a known definition
• An error shows up as an expression that matches nothing

Write every step; when a derivation stalls, check the bracketing first.

Selectors and pairs

Example 4: selecting the first argument

def select_first = λfirst.λsecond.first

\[ \begin{align} &((select\_first\ identity)\ apply) \\ \Rightarrow\ &(\lambda second.identity\ apply) \\ \Rightarrow\ &identity \end{align} \]

The second argument is discarded; the body never mentions second.

Example 5: selecting the second argument

def select_second = λfirst.λsecond.second

\[ \begin{align} &((select\_second\ identity)\ apply) \\ \Rightarrow\ &(\lambda second.second\ apply) \\ \Rightarrow\ &apply \end{align} \]

first never appears in the body, so the first argument is lost.

Example 6: making a pair

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

• Apply it to select_first and the first argument comes back
• Apply it to select_second and the second does

\[(make\_pair\ identity\ apply\ select\_first) \Rightarrow identity\] \[(make\_pair\ identity\ apply\ select\_second) \Rightarrow apply\]

What a pair is

• A pair is a function, not a container — it takes a selector
• Storage is replaced by a function that hands back what you ask for
• Structures nest: a pair of pairs gives triples, lists, trees

Next unit’s true is exactly “select the first argument”.

Free and bound variables

Definition — bound and free

• bound — an occurrence in the body of the λ that introduces that name
• unless a nested λ rebinds the name; then it belongs to the inner λ
• free — every other occurrence

In \(\lambda x.x\), \(x\) is bound. In \((f\ \lambda x.x)\), \(f\) is free.

Example: nested rebinding

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

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

The distinction is per occurrence, not per name.

Name clashes and α conversion

The clash

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

\[ \begin{align} &((apply\ arg)\ boing) \\ \Rightarrow\ &(\lambda arg.(arg\ arg)\ boing) \\ \Rightarrow\ &(boing\ boing) \end{align} \]

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

The fix — α conversion

Rename the bound variable consistently:

\[ \begin{align} &((\lambda func.\lambda arg1.(func\ arg1)\ arg)\ boing) \\ \Rightarrow\ &(\lambda arg1.(arg\ arg1)\ boing) \\ \Rightarrow\ &(arg\ boing) \end{align} \]

A name clash: β reduction puts a free variable in the scope of a bound variable of the same name. α conversion renames to remove it.

A captured variable still reduces — to the wrong thing, silently.

Simplification through η reduction

η reduction

\[\lambda\langle name \rangle.(\langle expression \rangle\ \langle name \rangle) \quad \equiv \quad \langle expression \rangle\]

\[ \begin{align} &(\lambda\langle name \rangle.(\langle expression \rangle\ \langle name \rangle)\ \langle argument \rangle) \\ \Rightarrow\ &(\langle expression \rangle\ \langle argument \rangle) \end{align} \]

The wrapper adds nothing: both give the same result.

Three conversions, three jobs

β

substitutes an argument for a bound variable

the only one that computes

α

renames to prevent capture

changes no meaning

η

removes a redundant wrapper

changes no meaning

Everything is eventually a β reduction.

Summary

The complete library

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)

Nothing more is added to the language. Everything is built inside it.

Summary

• Three grammar productions: name, function, application
• Computation is governed by three conversions: β, α, η
• Normal and applicative order can disagree on termination

• Data and control encode as functions — a pair takes a selector
• Some expressions have no normal form

Where next

Conditions, Booleans and Integers — the next unit in this module.

• The two selectors built here become true and false
• NOT, AND, OR, then the natural numbers, built inductively out of pairs