Lecture notes — Elements of Lambda Calculus

Published

2026-08-19 00:00

Keywords

ver. 1.0.0

Where we are

In Introduction you saw the case for the functional style: a name is a label rather than a place, execution order stops mattering, repetition is recursion, and functions are values. You were also told that the λ calculus has two mechanisms — abstraction and application — and that everything else is notation on top.

That unit motivated. This one defines.

What makes this unit unusual is what it does not have. No numbers. No booleans. No data structures. No conditionals. No recursion. The only thing that exists is a function, and the only thing you can do is apply one to another.

What you will be able to do

explain-abstraction — Explain abstraction as replacing a concrete value with a name that can be supplied later.
read-and-write-lambda-expressions — Read and write λ expressions against the formal grammar.
apply-beta-reduction — Evaluate an application by β-reduction, substituting the argument for the bound variable.
build-functions-from-functions — Build new functions by applying functions to functions, and verify the result by reduction.
recognise-non-termination — Recognise a reduction sequence that never terminates.
build-selectors-and-pairs — Build argument selection and pairing functions from pure λ terms.
identify-free-and-bound-variables — Identify which occurrences of a variable are free and which are bound.
apply-alpha-conversion — Rename bound variables by α conversion to avoid a name clash.
apply-eta-reduction — Simplify an expression with η reduction.
distinguish-evaluation-orders — Distinguish normal order from applicative order evaluation.

What we will cover

Abstraction — generalising an expression by introducing a name for a part of it.
λ expression — a name, a function, or an application; nothing else.
Bound variable — the name a λ introduces, like a formal parameter.
β reduction — evaluating an application by substituting the argument for the bound variable.
Normal and applicative order — substituting the argument unevaluated, or evaluating it first.
Syntactic sugar — notation that abbreviates a pure λ expression and can always be expanded back.
Free and bound variables — occurrences captured by an enclosing λ, and occurrences that are not.
α conversion — consistent renaming of a bound variable to remove a name clash.
η reduction — simplifying λ<name>.(<expression> <name>) to <expression>.

From motivation to mechanism

The previous unit left off having named the λ calculus but not defined it. This unit supplies the definition and then builds inside it.

The order of work:

Abstraction as an idea, and where you already meet it
The grammar — three productions, and every expression is one of them
The first functions: identity, self-application, function application
Notation for naming things, so expressions stay readable
Building new functions from old ones, then selectors and pairs — the first data structure
Free and bound variables, and the conversions that keep substitution honest

A word on how to read this unit. The book warns that it 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. We build up a set of useful functions bit by bit, and the functions introduced here are used as building blocks in the units that follow.

Each example assumes the previous ones. Work through slowly and consistently, and do the reductions by hand.

Learning outcomes

explain-abstraction: Explain abstraction as replacing a concrete value with a name that can be supplied later.
read-and-write-lambda-expressions: Read and write λ expressions against the formal grammar.

What abstraction is

Before the formalism, the idea — and it is one you already use constantly.

Abstraction is one move: take something concrete, notice a part that could vary, replace that part with a name, and mark that the name must be supplied later. The result is a function of that name.

The book works it on a cost calculation. Take a calculation for a particular item at a particular price. Notice the price could be anything. Replace it with a name, and instead of one answer you have a function: something that gives an answer once told the price.

The same move, in languages you know

Programming languages offer several abstraction mechanisms, and they are all this operation with different syntax around it:

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

The λ calculus keeps the operation and throws away the wrapping. That is the whole design, and it is why the language has so few parts.

Learning outcomes

explain-abstraction: Explain abstraction as replacing a concrete value with a name that can be supplied later.

Concepts

abstraction: introduces abstraction by generalising a concrete calculation over one of its parts

The grammar of λ expressions

The λ calculus was devised by Alonzo Church in the 1930s as a model for computability, and has since been central to computer science. It is a very simple but very powerful language based on pure abstraction, and it is particularly suited for use as a machine code for functional languages.

Three productions

The λ calculus is a system for manipulating λ expressions. An expression may be a name identifying an abstraction point, a function introducing an abstraction, or an application specialising an abstraction:

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

A name may be any sequence of non-blank characters:

fred    legs-11    19th_nervous_breakdown    33    +    -->

A function is an abstraction over a λ expression:

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

for example:

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

The λ precedes and introduces a name used for abstraction. That name is the function’s bound variable, and it is like a formal parameter in a Pascal function declaration. The expression after the dot is the function’s body.

Two things to notice, both more general than Pascal:

the body may be any λ expression, including another function
functions do not have names — in Pascal the function’s name is always used to refer to its definition; here a definition can appear directly where it is used

An application has the form:

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

for example $(\lambda x.x\ \lambda a.\lambda b.b)$.

An application specialises an abstraction by providing a value for the name. It is also called a bound pair, and the function expression is said to be applied to the argument expression.

Evaluating an application

For both approaches, the function expression is evaluated to return a function. Then all occurrences of the function’s bound variable in the body are replaced by either

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

and the body is then evaluated.

The first is applicative order, like Pascal’s call by value: the actual parameter is evaluated before being passed.
The second is normal order, like ALGOL 60’s call by name: it is not.

Normal order is more powerful than applicative order but may be less efficient. For the whole of this unit, all applications are evaluated in normal order.

Why single names are avoided

The grammar allows a single name as an expression, but in general we restrict single names to the bodies of functions. This avoids having to treat names as objects in their own right — as LISP or Prolog literals are — which would complicate everything. §2.14 returns to this.

Learning outcomes

read-and-write-lambda-expressions: Read and write λ expressions against the formal grammar.
distinguish-evaluation-orders: Distinguish normal order from applicative order evaluation.

Concepts

lambda-calculus: introduces Church’s calculus and gives its formal grammar
evaluation-order: distinguishes applicative order from normal order as the two ways to evaluate an application

The first three functions

With the grammar in hand we can write functions. There is nothing to write them out of except λ, names and brackets.

Identity

\[\lambda x . x\]

The identity function returns whatever argument it is applied to. Its bound variable is $x$ and its body is the name $x$. Used as a function expression, the bound variable $x$ is replaced by the argument expression in the body $x$, giving back the original argument.

Apply it to itself:

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

The function expression is $\lambda x.x$ and the argument expression is $\lambda x.x$. Replacing $x$ by the argument in the body gives $\lambda x.x$ — the argument, unchanged.

Self-application

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

This rather odd function applies its argument to its argument. Its bound variable is $s$; its body is the application $(s\ s)$, which has the name $s$ as both function expression and argument expression.

Apply identity to it:

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

Nothing surprising — identity returns its argument.

Now apply self-application to identity:

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

The bound variable $s$ is replaced by $\lambda x.x$ in the body $(s\ s)$, giving a new application

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

which reduces to $\lambda x.x$.

Now apply self-application to itself

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

Replace $s$ by $\lambda s.(s\ s)$ in the body $(s\ s)$ and you get

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

— the expression you started with. Reduce again and the same thing happens.

This is a two-symbol function with no recursion, no loop and no repetition construct, and it computes forever. The λ calculus can express computations with no normal form. That is the unsolvability of halting, which unit 1 mentioned, appearing here in a few characters.

Function application

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

Its bound variable is func and its body is another function, $\lambda arg.(func\ arg)$, whose body is the application $(func\ arg)$.

Applied to a first argument it returns a second function, which then applies the first argument to the second. Let us use it to apply identity to self-application:

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

The function expression is itself an application, so it is evaluated first. func is replaced by $\lambda x.x$ in the body, giving

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

a new function which applies identity to its argument. The original expression is now

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

so arg is replaced by $\lambda s.(s\ s)$, giving $(\lambda x.x\ \lambda s.(s\ s))$, which reduces to $\lambda s.(s\ s)$.

This looks redundant — application is already in the grammar. Making it a value is what lets application be passed around and abstracted over.

Learning outcomes

build-functions-from-functions: Build new functions by applying functions to functions, and verify the result by reduction.
apply-beta-reduction: Evaluate an application by β-reduction, substituting the argument for the bound variable.
recognise-non-termination: Recognise a reduction sequence that never terminates.

Concepts

beta-reduction: shows substitution of the argument for the bound variable, worked on the first three functions
lambda-calculus: builds the first functions using only abstraction and application

Naming and notation

Expressions become harder to work with as they grow. This section adds no power — it adds readability.

Syntactic sugar

We allow more concise notations: named function definitions, infix operations, an IF style conditional and so on. Adding higher level layers to a language this way is called syntactic sugaring, because the representation changes but the underlying meaning stays the same.

New syntax is introduced through substitution rules, and the book imposes strict conditions on them:

applying a rule involves no choices
the rules lead to pure λ expressions after a finite number of simple substitutions
so a higher level representation can always be completely compiled into λ calculus before evaluation

That last point is the whole discipline. It means we only ever need the original λ calculus rules for evaluation, and we never modify or augment the calculus itself — so the existing theory keeps applying.

There is a second reason for the conditions. We are using the λ calculus as a time-order-independent language in order to investigate time ordering. If substitution rules were order-dependent, different substitution orders could produce expressions with different meanings. Insisting substitutions can all be made statically, before evaluation starts, rules that out.

In practice we will not always expand everything — that would produce pages of incomprehensible λ expressions. But it must always remain possible.

Keep this rule for the rest of the module

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 you can always expand it.

Naming functions

It is tedious writing functions out repeatedly, so we name them:

def <name> = <function>

Our three functions so far:

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

A trap to notice now

A name introduced by def is an abbreviation, expanded where it appears — not a reference resolved at call time.

So a definition that mentions its own name does not work: expanding it produces another copy of the name, which expands again, forever. Recursion cannot be obtained this way.

Notice the trap now. Unit 4 is entirely about escaping it.

Learning outcomes

read-and-write-lambda-expressions: Read and write λ expressions against the formal grammar.
apply-beta-reduction: Evaluate an application by β-reduction, substituting the argument for the bound variable.

Concepts

syntactic-sugar: introduces notation that abbreviates pure λ expressions and can always be expanded back

Functions built from functions

We have three functions and one operation. This section does the only thing available: applies them to one another and works out what results.

A second identity

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

Apply it to identity:

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

To show identity and identity2 are equivalent in general, let <argument> stand for any expression:

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

So they have the same effect.

A second self-application

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

built the same way, from apply rather than written directly.

What “building” means here

There is no way to see the answer to these. 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.

That is what construction means in a language whose only values are functions. There is no data to hold and no state to change — you apply things to things, reduce, and see what you have.

Two habits to carry forward: write every step, and when a derivation stalls, check the bracketing first.

Learning outcomes

build-functions-from-functions: Build new functions by applying functions to functions, and verify the result by reduction.
apply-beta-reduction: Evaluate an application by β-reduction, substituting the argument for the bound variable.

Concepts

beta-reduction: verifies equivalence of derived functions by full reduction

Selectors and pairs

This is the most important section of the unit, because it is the pattern the rest of the module runs on.

Selecting the first of two arguments

def select_first = λfirst.λsecond.first

Bound variable first, body $\lambda second.first$. Applied to one argument it returns a function which, applied to another, returns the first:

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

In general:

((select_first <argument1>) <argument2>) ==
((λfirst.λsecond.first <argument1>) <argument2>) =>
(λsecond.<argument1> <argument2>) =>
<argument1>

Selecting the second

def select_second = λfirst.λsecond.second

Its body, $\lambda second.second$, is another version of the identity function.

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

The first argument identity was lost, because the bound variable first does not appear in the body.

Two small results worth noticing:

select_second applied to anything returns a version of identity — since $(select\_second\ \langle argument\rangle) \Rightarrow \lambda second.second$, and renaming second to $x$ gives $\lambda x.x$
select_first applied to identity returns a version of select_second — since it gives $\lambda second.identity == \lambda second.\lambda x.x$, and renaming gives $\lambda first.\lambda second.second$

Making a pair

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

This applies argument func to argument first to build a new function which may be applied to argument second. Note that first and second are used before func, to build the function

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

Now the trick. Apply that function to select_first and the first argument comes back; apply it to select_second and the second does.

((make_pair identity) apply) ==
((λfirst.λsecond.λfunc.((func first) second) identity) apply) =>
(λsecond.λfunc.((func identity) second) apply) =>
λfunc.((func identity) apply)

Then with select_first:

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

and with select_second:

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

Key ideas

A pair is a function, not a container: it takes a selector and applies it to the two components.
Storage has been replaced by a function that hands you what you ask for.
Data needs no separate mechanism — the claim from unit 1, now demonstrated.
The same trick generalises: unit 3 defines true and false as exactly these two selectors.
Structures nest — a pair whose components are pairs gives triples, lists, trees.

When you meet true as “select the first argument” in the next unit, this is where it came from.

Learning outcomes

build-selectors-and-pairs: Build argument selection and pairing functions from pure λ terms.
build-functions-from-functions: Build new functions by applying functions to functions, and verify the result by reduction.
apply-beta-reduction: Evaluate an application by β-reduction, substituting the argument for the bound variable.

Concepts

lambda-calculus: builds selection and pairing entirely from abstraction and application
beta-reduction: verifies that a pair returns each component when applied to the matching selector

Free and bound variables

We now consider how to ensure arguments are substituted correctly for bound variables. If all bound variables in an expression have distinct names there is no problem. For example, in

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

there are three functions with bound variables $f$, $x$ and $s$, and reduction is straightforward:

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

But bound variables in different functions may share a name.

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 bound variable. Otherwise it is free.

So in $\lambda x.x$ the variable $x$ is bound, but in the expression $x$ alone it is free. In $\lambda f.(f\ \lambda x.x)$ the variable $f$ is bound, but in $(f\ \lambda x.x)$ it is free.

In general, for $\lambda \langle name\rangle.\langle body\rangle$, the name refers to the same variable throughout the body except where another function has that name as its bound variable. References there correspond to the new bound variable, not the old.

Two examples worth working

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

the first $f$ is free, so it corresponds to the original bound variable
subsequent $f$s are bound and are distinct from it
the outer $f$ is in scope except in the scope of the inner $f$

And in the body of $\lambda g.((g\ \lambda h.(h\ (g\ \lambda h.(h\ \lambda g.(h\ g))))))\ g)$:

the first, second and last occurrences of $g$ occur free, so they correspond to the outer bound variable
the third and fourth are bound and distinct

The distinction is per occurrence, not per name. That is the part to get right, because β reduction replaces the bound occurrences and must leave free ones alone.

Learning outcomes

identify-free-and-bound-variables: Identify which occurrences of a variable are free and which are bound.

Concepts

free-and-bound-variables: defines bound and free occurrences, and scope under nested binders

Name clashes and α conversion

Restricting names to the bodies of functions can be restated as: there should be no free variables in a λ expression. Without that restriction, names become objects in their own right — which eases data representation but makes reduction much more complicated.

The clash

Take the function application function:

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

and consider:

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

Here arg is used both as a function’s bound variable name and as a free variable name in the leftmost application. These are two distinct uses: the bound variable will be replaced by β reduction, and the free variable should stay the same.

Carry out β reduction literally and:

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

which was not intended at all. The argument arg has been substituted into the scope of the bound variable arg and appears to create a new occurrence of it.

The fix

Rename consistently. Replace the bound variable arg with, say, arg1:

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

A name clash arises when a β reduction places an expression with a free variable in the scope of a bound variable with the same name as the free variable. Consistent renaming, known as α conversion, removes the clash.

The rule: for a function $\lambda \langle name1\rangle.\langle body\rangle$, the name and all free occurrences of it in the body may be replaced by a new name $\langle name2\rangle$, provided $\langle name2\rangle$ is not the name of a free variable in $\lambda \langle name1\rangle.\langle body\rangle$. The replacement includes the name after the λ itself.

This is 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.

Learning outcomes

apply-alpha-conversion: Rename bound variables by α conversion to avoid a name clash.
identify-free-and-bound-variables: Identify which occurrences of a variable are free and which are bound.

Concepts

alpha-conversion: defines consistent renaming and the side condition it requires
free-and-bound-variables: shows what goes wrong when a free variable is captured

Simplification through η reduction

Consider an expression of the form

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

This is a bit like the function application function after application to a function expression only. It is equivalent to <expression>, because applying it to an arbitrary argument gives:

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

which is what <expression> applied to that argument gives directly. This simplification is called η reduction, and we will use it in later units.

The three conversions now do three different jobs:

β — the actual computation: apply a function by substituting

This is the one that makes progress. Everything is eventually a β reduction.
α — housekeeping: rename to prevent capture

Changes no meaning. It exists so that β can be applied safely.
η — simplification: remove a redundant wrapper

Changes no meaning either. It exists to keep expressions readable.

Learning outcomes

apply-eta-reduction: Simplify an expression with η reduction.
identify-free-and-bound-variables: Identify which occurrences of a variable are free and which are bound.

Concepts

eta-reduction: simplifies a function that does nothing but pass its argument on

What you can now reduce

The formal core is complete. A grammar with three productions, and three conversion rules. Nothing further is added to the language in the rest of the module — everything from here is built inside it, and every abbreviation can be expanded back down to these terms.

The library you have 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 chapter’s exercises are worth doing before moving on, particularly the reductions. The derivations in the next two units are longer than anything here and assume the mechanics are automatic.

Learning outcomes

explain-abstraction: Explain abstraction as replacing a concrete value with a name that can be supplied later.
read-and-write-lambda-expressions: Read and write λ expressions against the formal grammar.
apply-beta-reduction: Evaluate an application by β-reduction, substituting the argument for the bound variable.
build-functions-from-functions: Build new functions by applying functions to functions, and verify the result by reduction.
recognise-non-termination: Recognise a reduction sequence that never terminates.
build-selectors-and-pairs: Build argument selection and pairing functions from pure λ terms.
identify-free-and-bound-variables: Identify which occurrences of a variable are free and which are bound.
apply-alpha-conversion: Rename bound variables by α conversion to avoid a name clash.
apply-eta-reduction: Simplify an expression with η reduction.
distinguish-evaluation-orders: Distinguish normal order from applicative order evaluation.

Concepts

lambda-calculus: summarises the grammar and reduction rules that make up the complete language
beta-reduction: collects the reduction machinery the following units assume

Conclusion

The λ calculus is the minimal, universal foundation for functional programming.

Three grammar productions — name, function, application — and nothing else. Church designed it as a model of computability, not a language, which is why it is small enough to reason about.
Computation is governed by three formal conversions.

β substitutes an argument for a bound variable and is the only one that computes. α renames to prevent capture. η removes a redundant wrapper.
Evaluation strategy matters.

Normal order passes the argument unevaluated; applicative order evaluates it first. The results agree when both terminate, but they do not always both terminate.
Data and control can be encoded as pure higher-order functions.

A pair is a function that takes a selector. That single idea replaces storage, and it is what the next two units build everything else out of.
Some expressions have no normal form.

$(\lambda s.(s\ s)\ \lambda s.(s\ s))$ reduces to itself forever. Unsolvable halting, in a handful of characters — and in unit 4 this same self-application becomes the tool that makes recursion possible.

Where next

The next unit, Conditions, Booleans and Integers, starts building. The two selectors you just wrote become true and false, which makes the conditional expression almost immediate. Then NOT, AND and OR, and then the natural numbers — built inductively out of pairs, with nothing but functions underneath.

← Elements of Lambda Calculus Conditions, Booleans and Integers →

--- title: Lecture notes — Elements of Lambda Calculus keywords: - ver. 1.0.0 date: '2026-08-19' --- [← Elements of Lambda Calculus](index.qmd){.hg-back} ## Where we are In **Introduction** you saw the case for the functional style: a name is a label rather than a place, execution order stops mattering, repetition is recursion, and functions are values. You were also told that the λ calculus has two mechanisms — abstraction and application — and that everything else is notation on top. That unit motivated. This one defines. What makes this unit unusual is what it does *not* have. No numbers. No booleans. No data structures. No conditionals. No recursion. The only thing that exists is a function, and the only thing you can do is apply one to another. ## What you will be able to do 1. `explain-abstraction` — Explain abstraction as replacing a concrete value with a name that can be supplied later. 2. `read-and-write-lambda-expressions` — Read and write λ expressions against the formal grammar. 3. `apply-beta-reduction` — Evaluate an application by β-reduction, substituting the argument for the bound variable. 4. `build-functions-from-functions` — Build new functions by applying functions to functions, and verify the result by reduction. 5. `recognise-non-termination` — Recognise a reduction sequence that never terminates. 6. `build-selectors-and-pairs` — Build argument selection and pairing functions from pure λ terms. 7. `identify-free-and-bound-variables` — Identify which occurrences of a variable are free and which are bound. 8. `apply-alpha-conversion` — Rename bound variables by α conversion to avoid a name clash. 9. `apply-eta-reduction` — Simplify an expression with η reduction. 10. `distinguish-evaluation-orders` — Distinguish normal order from applicative order evaluation. ## What we will cover - **Abstraction** — generalising an expression by introducing a name for a part of it. - **λ expression** — a name, a function, or an application; nothing else. - **Bound variable** — the name a λ introduces, like a formal parameter. - **β reduction** — evaluating an application by substituting the argument for the bound variable. - **Normal and applicative order** — substituting the argument unevaluated, or evaluating it first. - **Syntactic sugar** — notation that abbreviates a pure λ expression and can always be expanded back. - **Free and bound variables** — occurrences captured by an enclosing λ, and occurrences that are not. - **α conversion** — consistent renaming of a bound variable to remove a name clash. - **η reduction** — simplifying `λ<name>.(<expression> <name>)` to `<expression>`. ## From motivation to mechanism The previous unit left off having named the λ calculus but not defined it. This unit supplies the definition and then builds inside it. The order of work: 1. **Abstraction** as an idea, and where you already meet it 2. The **grammar** — three productions, and every expression is one of them 3. The first **functions**: identity, self-application, function application 4. **Notation** for naming things, so expressions stay readable 5. Building **new functions** from old ones, then **selectors and pairs** — the first data structure 6. **Free and bound** variables, and the conversions that keep substitution honest A word on how to read this unit. The book warns that it 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. We build up a set of useful functions bit by bit, and the functions introduced here are used as building blocks in the units that follow. Each example assumes the previous ones. Work through slowly and consistently, and do the reductions by hand. ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "explain-abstraction" >}}: Explain abstraction as replacing a concrete value with a name that can be supplied later. - {{< badge outcome "read-and-write-lambda-expressions" >}}: Read and write λ expressions against the formal grammar. ::: ## What abstraction is Before the formalism, the idea — and it is one you already use constantly. **Abstraction** is one move: take something concrete, notice a part that could vary, replace that part with a name, and mark that the name must be supplied later. The result is a function of that name. The book works it on a cost calculation. Take a calculation for a particular item at a particular price. Notice the price could be anything. Replace it with a name, and instead of one answer you have a function: something that gives an answer once told the price. ### The same move, in languages you know Programming languages offer several abstraction mechanisms, and they are all this operation with different syntax around it: - **procedures and functions**, which abstract over a computation - **parameters**, which abstract over the values it works on - **naming** generally, which lets one thing stand for another The λ calculus keeps the operation and throws away the wrapping. That is the whole design, and it is why the language has so few parts. ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "explain-abstraction" >}}: Explain abstraction as replacing a concrete value with a name that can be supplied later. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "abstraction" >}}: introduces abstraction by generalising a concrete calculation over one of its parts ::: ## The grammar of λ expressions The λ calculus was devised by **Alonzo Church** in the 1930s as a model for computability, and has since been central to computer science. It is a very simple but very powerful language based on pure abstraction, and it is particularly suited for use as a machine code for functional languages. ### Three productions The λ calculus is a system for manipulating λ expressions. An expression may be a **name** identifying an abstraction point, a **function** introducing an abstraction, or an **application** specialising an abstraction: ```text <expression> ::= <name> | <function> | <application> ``` A **name** may be any sequence of non-blank characters: ```text fred legs-11 19th_nervous_breakdown 33 + --> ``` A **function** is an abstraction over a λ expression: ```text <function> ::= λ<name>.<body> <body> ::= <expression> ``` for example: $$\lambda x.x \qquad \lambda first.\lambda second.first \qquad \lambda f.\lambda a.(f\ a)$$ The λ precedes and introduces a name used for abstraction. That name is the function's **bound variable**, and it is like a formal parameter in a Pascal function declaration. The expression after the dot is the function's **body**. Two things to notice, both more general than Pascal: - the body may be **any** λ expression, including another function - **functions do not have names** — in Pascal the function's name is always used to refer to its definition; here a definition can appear directly where it is used An **application** has the form: ```text <application> ::= (<function expression> <argument expression>) <function expression> ::= <expression> <argument expression> ::= <expression> ``` for example $(\lambda x.x\ \lambda a.\lambda b.b)$. An application specialises an abstraction by providing a value for the name. It is also called a **bound pair**, and the function expression is said to be **applied to** the argument expression. ### Evaluating an application For both approaches, the function expression is evaluated to return a function. Then all occurrences of the function's bound variable in the body are replaced by *either* - the **value** of the argument expression, or - the **unevaluated** argument expression and the body is then evaluated. - The first is **applicative order**, like Pascal's call by value: the actual parameter is evaluated before being passed. - The second is **normal order**, like ALGOL 60's call by name: it is not. Normal order is more powerful than applicative order but may be less efficient. [For the whole of this unit, all applications are evaluated in normal order.]{.hg-key} ::: {.callout-note title="Why single names are avoided"} The grammar allows a single name as an expression, but in general we restrict single names to the bodies of functions. This avoids having to treat names as objects in their own right — as LISP or Prolog literals are — which would complicate everything. §2.14 returns to this. ::: ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "read-and-write-lambda-expressions" >}}: Read and write λ expressions against the formal grammar. - {{< badge outcome "distinguish-evaluation-orders" >}}: Distinguish normal order from applicative order evaluation. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "lambda-calculus" >}}: introduces Church's calculus and gives its formal grammar - {{< badge concept "evaluation-order" >}}: distinguishes applicative order from normal order as the two ways to evaluate an application ::: ## The first three functions With the grammar in hand we can write functions. There is nothing to write them out of except λ, names and brackets. ### Identity $$\lambda x . x$$ The **identity function** returns whatever argument it is applied to. Its bound variable is $x$ and its body is the name $x$. Used as a function expression, the bound variable $x$ is replaced by the argument expression in the body $x$, giving back the original argument. Apply it to itself: $$(\lambda x . x\ \lambda x . x)$$ The function expression is $\lambda x.x$ and the argument expression is $\lambda x.x$. Replacing $x$ by the argument in the body gives $\lambda x.x$ — the argument, unchanged. ### Self-application $$\lambda s.(s\ s)$$ This rather odd function applies its argument to its argument. Its bound variable is $s$; its body is the application $(s\ s)$, which has the name $s$ as *both* function expression and argument expression. Apply identity to it: $$(\lambda x.x\ \lambda s.(s\ s)) \Rightarrow \lambda s.(s\ s)$$ Nothing surprising — identity returns its argument. Now apply self-application to identity: $$(\lambda s.(s\ s)\ \lambda x.x)$$ The bound variable $s$ is replaced by $\lambda x.x$ in the body $(s\ s)$, giving a new application $$(\lambda x.x\ \lambda x.x)$$ which reduces to $\lambda x.x$. ::: {.callout-important title="Now apply self-application to itself"} $$(\lambda s.(s\ s)\ \lambda s.(s\ s))$$ Replace $s$ by $\lambda s.(s\ s)$ in the body $(s\ s)$ and you get $$(\lambda s.(s\ s)\ \lambda s.(s\ s))$$ — the expression you started with. Reduce again and the same thing happens. This is a two-symbol function with no recursion, no loop and no repetition construct, and it computes forever. The λ calculus can express computations with **no normal form**. That is the unsolvability of halting, which unit 1 mentioned, appearing here in a few characters. ::: ### Function application $$\lambda func.\lambda arg.(func\ arg)$$ Its bound variable is `func` and its body is another function, $\lambda arg.(func\ arg)$, whose body is the application $(func\ arg)$. Applied to a first argument it returns a second function, which then applies the first argument to the second. Let us use it to apply identity to self-application: $$((\lambda func.\lambda arg.(func\ arg)\ \lambda x.x)\ \lambda s.(s\ s))$$ The function expression is itself an application, so it is evaluated first. `func` is replaced by $\lambda x.x$ in the body, giving $$\lambda arg.(\lambda x.x\ arg)$$ a new function which applies identity to its argument. The original expression is now $$(\lambda arg.(\lambda x.x\ arg)\ \lambda s.(s\ s))$$ so `arg` is replaced by $\lambda s.(s\ s)$, giving $(\lambda x.x\ \lambda s.(s\ s))$, which reduces to $\lambda s.(s\ s)$. This looks redundant — application is already in the grammar. Making it a *value* is what lets application be passed around and abstracted over. ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "build-functions-from-functions" >}}: Build new functions by applying functions to functions, and verify the result by reduction. - {{< badge outcome "apply-beta-reduction" >}}: Evaluate an application by β-reduction, substituting the argument for the bound variable. - {{< badge outcome "recognise-non-termination" >}}: Recognise a reduction sequence that never terminates. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "beta-reduction" >}}: shows substitution of the argument for the bound variable, worked on the first three functions - {{< badge concept "lambda-calculus" >}}: builds the first functions using only abstraction and application ::: ## Naming and notation Expressions become harder to work with as they grow. This section adds no power — it adds readability. ### Syntactic sugar We allow more concise notations: named function definitions, infix operations, an `IF` style conditional and so on. Adding higher level layers to a language this way is called **syntactic sugaring**, because the representation changes but the underlying meaning stays the same. New syntax is introduced through **substitution rules**, and the book imposes strict conditions on them: - applying a rule involves **no choices** - the rules lead to pure λ expressions after a **finite** number of simple substitutions - so a higher level representation can always be completely *compiled* into λ calculus before evaluation That last point is the whole discipline. It means we only ever need the original λ calculus rules for evaluation, and we never modify or augment the calculus itself — so the existing theory keeps applying. There is a second reason for the conditions. We are using the λ calculus as a time-order-independent language in order to *investigate* time ordering. If substitution rules were order-dependent, different substitution orders could produce expressions with different meanings. Insisting substitutions can all be made statically, before evaluation starts, rules that out. In practice we will not always expand everything — that would produce pages of incomprehensible λ expressions. But it must always remain *possible*. ::: {.callout-tip title="Keep this rule for the rest of the module"} 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 you can always expand it. ::: ### Naming functions It is tedious writing functions out repeatedly, so we name them: ```text def <name> = <function> ``` Our three functions so far: ```text def identity = λx.x def self_apply = λs.(s s) def apply = λfunc.λarg.(func arg) ``` ::: {.callout-important title="A trap to notice now"} A name introduced by `def` is an **abbreviation**, expanded where it appears — not a reference resolved at call time. So a definition that mentions its own name does not work: expanding it produces another copy of the name, which expands again, forever. Recursion cannot be obtained this way. Notice the trap now. Unit 4 is entirely about escaping it. ::: ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "read-and-write-lambda-expressions" >}}: Read and write λ expressions against the formal grammar. - {{< badge outcome "apply-beta-reduction" >}}: Evaluate an application by β-reduction, substituting the argument for the bound variable. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "syntactic-sugar" >}}: introduces notation that abbreviates pure λ expressions and can always be expanded back ::: ## Functions built from functions We have three functions and one operation. This section does the only thing available: applies them to one another and works out what results. ### A second identity ```text def identity2 = λx.((apply identity) x) ``` Apply it to identity: ```text (identity2 identity) == (λx.((apply identity) x) identity) => ((apply identity) identity) == ((λfunc.λarg.(func arg) identity) identity) => (λarg.(identity arg) identity) => (identity identity) => ... => identity ``` To show `identity` and `identity2` are equivalent in general, let `<argument>` stand for any expression: ```text (identity2 <argument>) == (λx.((apply identity) x) <argument>) => ((apply identity) <argument>) => ... => (identity <argument>) => ... => <argument> ``` So they have the same effect. ### A second self-application ```text def self_apply2 = λs.((apply s) s) ``` built the same way, from `apply` rather than written directly. ### What "building" means here There is no way to *see* the answer to these. 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. That is what construction means in a language whose only values are functions. There is no data to hold and no state to change — you apply things to things, reduce, and see what you have. Two habits to carry forward: write every step, and when a derivation stalls, check the bracketing first. ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "build-functions-from-functions" >}}: Build new functions by applying functions to functions, and verify the result by reduction. - {{< badge outcome "apply-beta-reduction" >}}: Evaluate an application by β-reduction, substituting the argument for the bound variable. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "beta-reduction" >}}: verifies equivalence of derived functions by full reduction ::: ## Selectors and pairs This is the most important section of the unit, because it is the pattern the rest of the module runs on. ### Selecting the first of two arguments ```text def select_first = λfirst.λsecond.first ``` Bound variable `first`, body $\lambda second.first$. Applied to one argument it returns a function which, applied to another, returns the first: ```text ((select_first identity) apply) == ((λfirst.λsecond.first identity) apply) => (λsecond.identity apply) => identity ``` In general: ```text ((select_first <argument1>) <argument2>) == ((λfirst.λsecond.first <argument1>) <argument2>) => (λsecond.<argument1> <argument2>) => <argument1> ``` ### Selecting the second ```text def select_second = λfirst.λsecond.second ``` Its body, $\lambda second.second$, is another version of the identity function. ```text ((select_second identity) apply) == ((λfirst.λsecond.second identity) apply) => (λsecond.second apply) => apply ``` The first argument `identity` was lost, because the bound variable `first` does not appear in the body. Two small results worth noticing: - `select_second` applied to anything returns a version of `identity` — since $(select\_second\ \langle argument\rangle) \Rightarrow \lambda second.second$, and renaming `second` to $x$ gives $\lambda x.x$ - `select_first` applied to `identity` returns a version of `select_second` — since it gives $\lambda second.identity == \lambda second.\lambda x.x$, and renaming gives $\lambda first.\lambda second.second$ ### Making a pair ```text def make_pair = λfirst.λsecond.λfunc.((func first) second) ``` This applies argument `func` to argument `first` to build a new function which may be applied to argument `second`. Note that `first` and `second` are used *before* `func`, to build the function $$\lambda func.((func\ first)\ second)$$ Now the trick. Apply that function to `select_first` and the first argument comes back; apply it to `select_second` and the second does. ```text ((make_pair identity) apply) == ((λfirst.λsecond.λfunc.((func first) second) identity) apply) => (λsecond.λfunc.((func identity) second) apply) => λfunc.((func identity) apply) ``` Then with `select_first`: ```text (λfunc.((func identity) apply) select_first) == ((select_first identity) apply) == ((λfirst.λsecond.first identity) apply) => (λsecond.identity apply) => identity ``` and with `select_second`: ```text (λfunc.((func identity) apply) select_second) == ((select_second identity) apply) == ((λfirst.λsecond.second identity) apply) => (λsecond.second apply) => apply ``` ::: {.highlights} <h1>Key ideas</h1> - A **pair is a function**, not a container: it takes a selector and applies it to the two components. - Storage has been replaced by a function that hands you what you ask for. - **Data needs no separate mechanism** — the claim from unit 1, now demonstrated. - The same trick generalises: unit 3 defines `true` and `false` as exactly these two selectors. - Structures nest — a pair whose components are pairs gives triples, lists, trees. ::: When you meet `true` as "select the first argument" in the next unit, this is where it came from. ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "build-selectors-and-pairs" >}}: Build argument selection and pairing functions from pure λ terms. - {{< badge outcome "build-functions-from-functions" >}}: Build new functions by applying functions to functions, and verify the result by reduction. - {{< badge outcome "apply-beta-reduction" >}}: Evaluate an application by β-reduction, substituting the argument for the bound variable. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "lambda-calculus" >}}: builds selection and pairing entirely from abstraction and application - {{< badge concept "beta-reduction" >}}: verifies that a pair returns each component when applied to the matching selector ::: ## Free and bound variables We now consider how to ensure arguments are substituted **correctly** for bound variables. If all bound variables in an expression have distinct names there is no problem. For example, in $$(\lambda f.(f\ \lambda x.x)\ \lambda s.(s\ s))$$ there are three functions with bound variables $f$, $x$ and $s$, and reduction is straightforward: $$(\lambda f.(f\ \lambda x.x)\ \lambda s.(s\ s)) \Rightarrow (\lambda s.(s\ s)\ \lambda x.x) \Rightarrow (\lambda x.x\ \lambda x.x) \Rightarrow \lambda x.x$$ But bound variables in different functions may share a name. ### 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 bound variable*. Otherwise it is **free**. So in $\lambda x.x$ the variable $x$ is bound, but in the expression $x$ alone it is free. In $\lambda f.(f\ \lambda x.x)$ the variable $f$ is bound, but in $(f\ \lambda x.x)$ it is free. In general, for $\lambda \langle name\rangle.\langle body\rangle$, the name refers to the same variable throughout the body *except* where another function has that name as its bound variable. References there correspond to the new bound variable, not the old. ### Two examples worth working In the body of $\lambda f.(f\ \lambda f.f)$, which is $(f\ \lambda f.f)$: - the **first** $f$ is free, so it corresponds to the original bound variable - subsequent $f$s are bound and are distinct from it - the outer $f$ is in scope except in the scope of the inner $f$ And in the body of $\lambda g.((g\ \lambda h.(h\ (g\ \lambda h.(h\ \lambda g.(h\ g))))))\ g)$: - the first, second and last occurrences of $g$ occur free, so they correspond to the outer bound variable - the third and fourth are bound and distinct [The distinction is per occurrence, not per name.]{.hg-key} That is the part to get right, because β reduction replaces the *bound* occurrences and must leave free ones alone. ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "identify-free-and-bound-variables" >}}: Identify which occurrences of a variable are free and which are bound. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "free-and-bound-variables" >}}: defines bound and free occurrences, and scope under nested binders ::: ## Name clashes and α conversion Restricting names to the bodies of functions can be restated as: there should be **no free variables** in a λ expression. Without that restriction, names become objects in their own right — which eases data representation but makes reduction much more complicated. ### The clash Take the function application function: ```text def apply = λfunc.λarg.(func arg) ``` and consider: ```text ((apply arg) boing) == ((λfunc.λarg.(func arg) arg) boing) ``` Here `arg` is used both as a function's bound variable name **and** as a free variable name in the leftmost application. These are two distinct uses: the bound variable will be replaced by β reduction, and the free variable should stay the same. Carry out β reduction literally and: ```text ((λfunc.λarg.(func arg) arg) boing) => (λarg.(arg arg) boing) => (boing boing) ``` which was not intended at all. The argument `arg` has been substituted into the scope of the bound variable `arg` and appears to create a new occurrence of it. ### The fix Rename consistently. Replace the bound variable `arg` with, say, `arg1`: ```text ((λfunc.λarg1.(func arg1) arg) boing) => (λarg1.(arg arg1) boing) => (arg boing) ``` > A **name clash** arises when a β reduction places an expression with a free variable in the scope of a bound variable with the same name as the free variable. Consistent renaming, known as **α conversion**, removes the clash. The rule: for a function $\lambda \langle name1\rangle.\langle body\rangle$, the name and all free occurrences of it in the body may be replaced by a new name $\langle name2\rangle$, **provided** $\langle name2\rangle$ is not the name of a free variable in $\lambda \langle name1\rangle.\langle body\rangle$. The replacement includes the name after the λ itself. ::: {.callout-important title="This is 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. ::: ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "apply-alpha-conversion" >}}: Rename bound variables by α conversion to avoid a name clash. - {{< badge outcome "identify-free-and-bound-variables" >}}: Identify which occurrences of a variable are free and which are bound. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "alpha-conversion" >}}: defines consistent renaming and the side condition it requires - {{< badge concept "free-and-bound-variables" >}}: shows what goes wrong when a free variable is captured ::: ## Simplification through η reduction Consider an expression of the form ```text λ<name>.(<expression> <name>) ``` This is a bit like the function application function after application to a function expression only. It is equivalent to `<expression>`, because applying it to an arbitrary argument gives: ```text (λ<name>.(<expression> <name>) <argument>) => (<expression> <argument>) ``` which is what `<expression>` applied to that argument gives directly. This simplification is called **η reduction**, and we will use it in later units. The three conversions now do three different jobs: - **β** — the actual computation: apply a function by substituting > This is the one that makes progress. Everything is eventually a β reduction. - **α** — housekeeping: rename to prevent capture > Changes no meaning. It exists so that β can be applied safely. - **η** — simplification: remove a redundant wrapper > Changes no meaning either. It exists to keep expressions readable. ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "apply-eta-reduction" >}}: Simplify an expression with η reduction. - {{< badge outcome "identify-free-and-bound-variables" >}}: Identify which occurrences of a variable are free and which are bound. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "eta-reduction" >}}: simplifies a function that does nothing but pass its argument on ::: ## What you can now reduce The formal core is complete. A grammar with three productions, and three conversion rules. **Nothing further is added to the language in the rest of the module** — everything from here is built inside it, and every abbreviation can be expanded back down to these terms. The library you have built: ```text 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 chapter's exercises are worth doing before moving on, particularly the reductions. The derivations in the next two units are longer than anything here and assume the mechanics are automatic. ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "explain-abstraction" >}}: Explain abstraction as replacing a concrete value with a name that can be supplied later. - {{< badge outcome "read-and-write-lambda-expressions" >}}: Read and write λ expressions against the formal grammar. - {{< badge outcome "apply-beta-reduction" >}}: Evaluate an application by β-reduction, substituting the argument for the bound variable. - {{< badge outcome "build-functions-from-functions" >}}: Build new functions by applying functions to functions, and verify the result by reduction. - {{< badge outcome "recognise-non-termination" >}}: Recognise a reduction sequence that never terminates. - {{< badge outcome "build-selectors-and-pairs" >}}: Build argument selection and pairing functions from pure λ terms. - {{< badge outcome "identify-free-and-bound-variables" >}}: Identify which occurrences of a variable are free and which are bound. - {{< badge outcome "apply-alpha-conversion" >}}: Rename bound variables by α conversion to avoid a name clash. - {{< badge outcome "apply-eta-reduction" >}}: Simplify an expression with η reduction. - {{< badge outcome "distinguish-evaluation-orders" >}}: Distinguish normal order from applicative order evaluation. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "lambda-calculus" >}}: summarises the grammar and reduction rules that make up the complete language - {{< badge concept "beta-reduction" >}}: collects the reduction machinery the following units assume ::: ## Conclusion - The λ calculus is the minimal, universal foundation for functional programming. > Three grammar productions — name, function, application — and nothing else. Church designed it as a model of computability, not a language, which is why it is small enough to reason about. - Computation is governed by three formal conversions. > **β** substitutes an argument for a bound variable and is the only one that computes. **α** renames to prevent capture. **η** removes a redundant wrapper. - Evaluation strategy matters. > Normal order passes the argument unevaluated; applicative order evaluates it first. The results agree when both terminate, but they do not always both terminate. - Data and control can be encoded as pure higher-order functions. > A pair is a function that takes a selector. That single idea replaces storage, and it is what the next two units build everything else out of. - Some expressions have no normal form. > $(\lambda s.(s\ s)\ \lambda s.(s\ s))$ reduces to itself forever. Unsolvable halting, in a handful of characters — and in unit 4 this same self-application becomes the tool that makes recursion possible. ### Where next The next unit, **Conditions, Booleans and Integers**, starts building. The two selectors you just wrote become `true` and `false`, which makes the conditional expression almost immediate. Then `NOT`, `AND` and `OR`, and then the natural numbers — built inductively out of pairs, with nothing but functions underneath. ::: {.hg-nav} [← Elements of Lambda Calculus](index.qmd){.hg-prev} [Conditions, Booleans and Integers →](../3_conditions_booleans_and_integers/index.qmd){.hg-next} :::