Chapter 5. The untyped/pure lambda-calculus

Review the definition and properties of the untyped or pure lambda calculus.

-> The underlying "computational substrate" for most of the type systems.

Context & history ​

• Mid 1960, Peter Landin observed that a complex programming language can be understood by:

  • The formulation of the language as a tiny core calculus capturing the language's essential mechanisms.

  • Together with a collection of convenient derived forms whose behavior is understood by translating them into the core.

    (Landin, 1964, 1965, 1966; Tennent, 1981)

• The core language used by Landin was the lambda-calculus, a formal system invented in the 1920s by (Alonzo Church, 1936, 1941), in which all computation is reduced to the basic operations of function definition and application.

• Following Landin's insight, as well as the pioneering work on Lisp (John McCarthy, 1959, 1981), the lambda-calculus has seen widespread use in many areas.

  • The specification of programming language features.

  • Language design.

  • Language implementation.

  • The study of type systems.

• The lambda calculus's importance arises from the fact that it can be viewed simultaneously as:

  • A simple programming language in which computations can be described.

  • A mathematical object about which rigorous statements can be proved.

• The λ-calculus is just one among many core calculi used to study and define programming languages.

  • The π-calculus (Milner, Parrow, Walker, 1991-1992) serves as a core language for modeling message-passing concurrency.

  • Abadi and Cardelli's object calculus (1996) captures the essential features of object-oriented languages.

    -> Most of the ideas and techniques for the λ-calculus transfer quite directly to the other calculi.

• The λ-calculus can be enriched in several ways.

  • We can add concrete syntax for features like numbers, tuples, records, etc., whose behavior can already be encoded in the core language, but which are more convenient to work with in "built-in" form.

  • We can also add more complex features such as:

    • Mutable reference cells.

    • Nonlocal exception handling.

      These can, in principle, be simulated in the pure λ-calculus, but only via heavy and indirect encodings.

  • Such extensions gradually lead to full-fledged programming languages, for example:

    • ML (Gordon, Milner, Wadsworth, 1979; Milner, Tofte, Harper, 1990; Milner, Tofte, Harper, MacQueen, 1997; etc.)

    • Haskell (Hudak et al., 1992)

    • Scheme (Sussman and Steele, 1975; Kelsey, Clinger, Rees, 1998)

  • Extending the core language almost always goes hand-in-hand with extending the type system: richer language features typically require richer typing disciplines to describe and control their behavior.

Basics ​

• Procedural (or functional) abstraction is a key feature of essentially all programming languages.

  $\lambda n.\text{expr}$ -> a shorthand for "the function that, for each $n$, yields $\text{expr}$".

  Example: $\text{factorial}=\lambda n.\text{ if }n=0\text{ then }0\text{ else }n\ast \text{factorial }(n-1)$

  -> $\text{factorial}(0)$ means "the function $\lambda n.\text{ if }n=0\text{ then }0\text{ else }n\ast \text{factorial }(n-1)$ applied to $0$".

• Lambda-calculus (or λ-calculus) consists of:

  • Function definition.

  • Function application.

    …in the purest possible form.

• In the lambda-calculus, everything is a function:

  • The arguments accepted by functions are themselves functions.

  • The result returned by a function is another function.

• Lambda-calculus comprises just 3 sorts of terms:

  • A variable $x$ by itself is a term.

  • The abstraction of a variable $x$ from a term $t_1$, written $\lambda x.t_1$, is a term.

  • The application of a term $t_1$ to another term $t_2$, written $t_1{t}_2$, is a term.

The syntax of lambda calculus

Abstract and concrete syntax ​

• It's useful to distinguish two levels of structure:

  • Concrete syntax (surface syntax): the actual strings of characters that programmers read and write.

  • Abstract syntax: a simpler, internal representation of programs as labeled trees, usually called abstract syntax trees (ASTs).

• Abstract syntax trees (ASTs) make the structure of programs explicit:

  • They represent programs as trees instead of raw text.

  • This tree structure is ideal for:

    • Formal language definitions and proofs about languages.

    • The internal workings of compilers and interpreters, which need to manipulate program structure precisely.

• Concrete syntax -> Abstract syntax usually happens in two stages:

  • Lexical analysis (lexing)

    • A lexer converts the raw character stream into a sequence of tokens: identifiers, keywords, constants, punctuation, etc.

    • It also:

      • Removes comments.

      • Handles whitespace and capitalization conventions.

      • Deals with formats for numeric and string literals.

  • Parsing

    • A parser takes the sequence of tokens and builds an abstract syntax tree.

    • During parsing, rules like operator precedence and associativity reduce the need for excessive parentheses in the source code.

    • For example:

      • The operator binds more tightly than +.

      • So the expression 1 + 2 * 3 is parsed as 1 + (2 * 3) rather than (1 + 2) * 3.

• The main focus is on abstract syntax, not concrete syntax:

  • Grammars (like the grammar for λ-terms) should be read as descriptions of legal tree structures, not just valid strings of characters.

  • When we write terms in text-examples, definitions, theorems, proofs-we use a linear concrete notation, but we always implicitly mean the corresponding abstract syntax tree.

• To avoid writing too many parentheses when λ-terms are written in linear form, we adopt two standard conventions:

  • Application is left-associative

    • The expression s t u is read as (s t) u, not s (t u).

  • Abstraction bodies extend as far to the right as possible

    • The expression λx. λy. x y x is read as:

      • λx. (λy. ((x y) x))

    • That is, the body of each λ-abstraction includes everything to its right unless parentheses say otherwise.

Variables and metavariables ​

• Metavariables vs object-language variables

  • $t$, $s$, $u$ (with subscripts) are metavariables for arbitrary terms.

  • $x$, $y$, $z$ are often metavariables for arbitrary variables (i.e., they range over variable names).

• Name overloading & disambiguation

  • The same symbols $x$, $y$, etc. are also used as actual variables in the object language (inside terms).

  • The intended role-metavariable vs. object-language variable-is always clear from context.

• Example: In "The term $\lambda x.\lambda y.xy$ has the form $\lambda z.s$, where $z=x$ and $s=\lambda y.xy$":

  • $z$ and $s$ are metavariables.

  • $x$ and $y$ are object-language variables.

Scope ​

• In $\lambda x.t$, $\lambda x$ is a binder and its scope is the body $t$.

• An occurrence of $x$ is bound if it appears inside the body $t$ of some enclosing abstraction $\lambda x.t$.

• An occurrence of x is free if it is not bound by any surrounding abstraction on x.

• Examples:

  • $xy$ -> both $x$ and $y$ are free.

  • $\lambda y.xy$ -> $y$ is bound, $x$ is free.

  • $\lambda x.x$ -> $x$ is bound.

  • $\lambda z.\lambda x.\lambda y.x(yz)$ -> all occurrences of $x$, $y$, and $z$ are bound.

  • $(\lambda x.x)x$ -> the first $x$ (inside $\lambda x.x$) is bound, the second $x$ (the argument) is free.

• A term with no free variables is called closed.

• Closed terms are also called combinators.

• Example: the identity combinator.

  • $id=\lambda x.x$

  • It simply returns its argument unchanged.

Operational semantics ​

• In its pure form, the lambda-calculus has:

  • No built-in constants or primitive operators.

  • No numbers, arithmetic, conditionals, records, loops, sequencing, or I/O.

  • The only way to compute is by applying functions to arguments (and both are just terms).

• A single computation step:

  • Rewrite a function application whose left side is an abstraction.

  • Substitute the argument for the bound variable in the body.

    $$(\lambda x.t_{12})t_2\to [x\mapsto t_2]t_{12}$$

    where [x \mapsto t_2] t_1_2 ParseError: Double subscript at position 20: …mapsto t_2] t_1_̲2 means "the term obtained by replacing all free occurrences of $x$ in t_1_2 ParseError: Double subscript at position 4: t_1_̲2 with $t_2$."

• Examples:

  • $(\lambda x.x)y\to y$

  • $(\lambda x.x(\lambda x.x))(ur)\to ur(\lambda x.x)$

• Follow Church:

  • A term of the form $(\lambda x.t_{12})t_2$ is called a redex (reducible expression).

  • The act of rewriting a redex using the rule above is called beta-reduction (\beta-reduction).

• Evaluation strategy: Which redex (or redexes) in a term may be reduced at the next evaluation step.

  • There can be multiple evaluation strategies for the lambda calculus.

  • Different strategies (e.g., normal order, call by value) choose different redexes, but all are based on the same beta-reduction rule above.

Evaluation strategies ​

• Context:

  • $\text{id}=\lambda x.x$.

  • Consider this term: $t=\text{id}(\text{id}(\lambda z.\text{id}z))$.

    There are 3 redexes: The outer $\text{id}(...)$, the inner $\text{id}(\text{lambdaz}.\text{id}z)$, and the $\text{id}z$ inside.

• There can be many reductions for the full beta-reduction strategy.

• Full beta-reduction

  • Any redex can be reduced anywhere in the term at any step.

    $(\lambda x.t_{12})t_2\to [x\mapsto t_2]t_{12}$

  • One possible full-reduction sequence (reducing innermost first):

    $\text{id}(\text{id}(\lambda z.\text{id}z))$

    $\to \text{id}(\text{id}(\lambda z.z))$

    $\to \text{id}(\lambda z.z)$

    $\to \lambda z.z$

    $\to ̸$

• Under the later strategies, the one-step evaluation relation is a partial function: each term has at most one next step.

• Normal order

  • Always reduce the leftmost, outermost redex first.

  • The normal-order reduction:

    $\text{id}(\text{id}(\lambda z.\text{id}z))$

    $\to \text{id}(\lambda z.\text{id}z)$

    $\to \lambda z.\text{id}z$

    $\to \lambda z.z$

    $\to ̸$

• Call by name

  • Like normal order, but no reduction inside abstractions.

  • Same first steps as normal order, but stop once the result is a \lambda-abstraction:

    $\text{id}(\text{id}(\lambda z.\text{id}z))$

    $\to \text{id}(\lambda z.\text{id}z)$

    $\to \lambda z.\text{id}z$

    $\to ̸$

  • Here, $\text{lambdaz}.\text{id}z$ is treated as a normal form (no further reduction inside the body).

  • Variants of call by name appear in languages like Algol 60 and in optimized form (call by need), Haskell.

• Call by need

  • An optimized non-strict strategy (used in Haskell).

  • Similar to call by name, but shares the result of evaluating an argument:

    • First use of the argument evaluates it.

    • All other uses reuse that value (no re-evaluation).

  • Conceptually works on graphs (shared structure), not just trees.

• Call by value

  • Only outermost redexes are reduced, and only when the argument is already a value.

  • The example reduces as:

    $\text{id}(\text{id}(\lambda z.\text{id}z))$

    $\to \text{id}(\lambda z.\text{id}z)$

    $\to \lambda z.\text{id}z$

    $\to ̸$

  • This is a strict strategy: function arguments are always evaluated, whether or not they are actually used.

  • In contrast, non-strict (or lazy) strategies like call by name/need only evaluate arguments that are actually used.

• The choice of evaluation strategy has little effect on the core issues of type system design. Most typing concepts and techniques apply similarly across strategies.

Programming in the lambda calculus ​

• The lambda-calculus has an extremely small core (just variables, abstraction, application) but is surprisingly powerful.

• Many language features (multi-argument functions, booleans, pairs, numbers, lists, etc.) can be encoded inside the pure calculus.

• Motivations:

  • These encodings are "warm-up exercises" to understand the system.

  • Not endorsements of \lambda-calculus as a practical programming language.

Multiple arguments (currying) ​

• The pure lambda-calculus has no built-in multi-argument functions.

• Instead of writing something like $f(x,y)$, we use higher-order functions and currying:

  • Desired informal form: $f(x,y)=s[x\mapsto v,y\mapsto w]$

  • Curried encoding:

    $f=\lambda x.\lambda y.s$

    • First apply $f$ to $v$: $fv=\lambda y.[x\mapsto v]s$.

    • Then apply to $w$: $fvw=(\lambda y.[x\mapsto v]s)w\to [y\mapsto w][x\mapsto v]s$ .

• This transformation of multi-argument functions to chains of single-argument functions is called currying (after Haskell Curry).

Church booleans ​

• Encode booleans as functions:

  • $\text{tru}=\lambda t.\lambda f.t$

  • $\text{fls}=\lambda t.\lambda f.f$

• A generic "if" (conditional) combinator: $\text{test}=\lambda l.\lambda m.\lambda n.lmn$

  • $\text{test}\text{tru}vw\to v$

  • $\text{test}\text{fls}vw\to w$

• Intuition: the boolean itself acts as the conditional:

  • $\text{tru}vw$ chooses the first argument.

  • $\text{fls}vw$ chooses the second argument.

Boolean operators ​

• $\text{and}=\lambda b.\lambda c.bc\text{fls}$

  • If $b=\text{tru}$, result is $c$.

  • If $b=\text{fls}$, result is $\text{fls}$.

  • So $\text{and}bc$ is $\text{tru}$ iff both $b$ and $c$ are $\text{tru}$.

Exercise 5.2.1 Define logical $\text{or}$ and $\text{not}$ functions.

Pairs ​

• Encode a pair of values using booleans:

  $\text{pair}=\lambda f.\lambda s.\lambda b.bfs$

  $\text{fst}=\lambda p.p\text{tru}$

  $\text{snd}=\lambda p.p\text{fls}$

• Intuition:

  • $\text{pair}vw$ is a function expecting a boolean $b$ and returning $bvw$.

  • If $b=\text{tru}$, we get $v$ if $b=\text{fls}$, we get $w$.

  • So:

    • $\text{fst}(\text{pair}vw)\to v$

    • $\text{snd}(\text{pair}vw)\to w$

Church numerals ​

• Encode natural numbers as "iterate a function $n$ times":

  $c_0=\lambda s.\lambda z.z$

  $c_1=\lambda s.\lambda z.sz$

  $c_2=\lambda s.\lambda z.s(sz)$

  $c_3=\lambda s.\lambda z.s(s(sz))$

  $\dots$

• In general, $c_n$ represents "apply $s$ to $z$, $n$ times".

• Note: $c_0$ and $\text{fls}$ are actually the same term, just used with different intended meanings. This is interesting, as $0$ is falsy in most programming languages.

• Looks like fixed point approximation?

• Successor ($n\mapsto n+1$): $\text{scc}=\lambda n.\lambda s.\lambda z.s(nsz)$

• Addition ($m+n$):

  $\text{plus}=\lambda m.\lambda n.\lambda s.\lambda z.ms(nsz)$

  • First use $nsz$ to apply $s$ n times.

  • Then apply $s$ m more times via $m$.

• Multiplication ($m\times n$) using plus:

  $\text{times}=\lambda m.\lambda n.m(\text{plus}n)c_0$

  • $\text{plus}n$ is a function "add $n$".

  • $m(\text{plus}n)c_0$ means "start at $0$, add $n$, $m$ times" \to $m\times n$.

Exercise 5.2.2 Find another way to define the successor function on Church numerals.

Exercise 5.2.3 Is it possible to define multiplication on Church numerals without using $\text{plus}$?

Exercise 5.2.4 Define a term for raising one number to the power of another.

Exercise 5.2.6 Approximately how many steps of evaluation (as a function of $n$) are required to calculate $\text{prd}{c}_n$?

Exercise 5.2.7 Write a function $\text{equal}$ that tests two numbers for equality and returns a Church boolean.

Other datatypes ​

Many other structures (lists, trees, variants, arrays) can be encoded similarly.

Exercise 5.2.8 A list can be represented in the lambda-calculus by its $\text{fold}$ function. (OCaml's name for this function is $\text{fold\_left}$; it is also sometimes called $\text{reduce}$.) For example, the list $[x,y,z]$ becomes a function that takes two arguments $c$ and $n$ and returns$cx(cy(czn)))$. What would the representation of $\text{nil}$ be? Write a function $\text{cons}$ that takes an element $h$ and a list (that is, a $\text{fold}$ function) $t$ and returns a similar representation of the list formed by prepending $h$ to $t$. Write $\text{isnil}$ and $\text{head}$ functions, each taking a list parameter. Finally, write a $\text{tail}$ function for this representation of lists (this is quite a bit harder and requires a trick analogous to the one used to define $\text{prd}$ for numbers).

Observations ​

The definitions for the Church numerals and lists encoding get me thinking about the technique:

• Think of a base value in the domain: $0$ for numbers and $\text{nil}$ for lists.

• Think of a base operation in the domain that can create any values from the base value: addition for numbers and cons-ing for lists.

• Then:

  • For numerals:

    • The 0-th value: $\lambda c.\lambda z.z$.

    • The $n$-th value: $\lambda c.\lambda z.c(v_{n-1}cz)$.

  • For lists:

    • The 0-th value: $\lambda c.\lambda n.n$.

    • The 1-st value: $\lambda c.\lambda n.c{e}_1(v_{0}cn)$ .

    • The $n$-th value: $\lambda c.\lambda n.c{e}_n(v_{n-1}cn)$.

Enriching the calculus ​

• In the pure lambda-calculus we can already encode booleans, numbers, and their operations, so in principle we can write all our programs there.

• In practice, it is often more convenient to work in an enriched language that has primitive booleans and numbers as well.

• Pure lambda-calculus is denoted by $\lambda$.

  No built-in booleans or numbers; everything is encoded.

• Pure lambda-calculus enriched with booleans and naturals is denoted by $\lambda \text{𝐍𝐁}$.

  Has primitive $\text{true}$, $\text{false}$, numeric literals, $\text{succ}$, $\text{pred}$, $\text{iszero}$, etc. (as in the earlier arithmetic language in Chapter 3. Untyped arithmetic expressions).

• In $\lambda \text{𝐍𝐁}$, there are effectively two versions of booleans and numbers:

  • Real (primitive) values

  • Encoded (Church) values

    Conversions:

  • Church boolean \to primitive boolean: $\text{realbool}=\lambda b.b\text{true}\text{false}$.

  • Primitive boolean \to Church boolean: $\text{churchbool}=\lambda b.\text{if}b\text{then}\text{tru}\text{else}\text{fls}$.

Why primitive values help: evaluation order & call by value ​

• We use call by value (CBV):

  • Do not reduce under lambdas.

  • Only reduce a redex when its argument is already a value.

• Example: successor of a Church numeral

  • We expect: $\text{scc}{c}_1\to c_2$

  • But in CBV we actually get a \lambda-term that is extensionally equal to $c_2$, but not syntactically the same; some computation is "stuck under a \lambda" and cannot be reduced further under CBV.

  • So $\text{scc}{c}_1$ is behaviorally equivalent to $c_2$ (they act the same when given $s$ and $z$), but not literally the same normal form.

• Example: multiplication

  • $\text{times}{c}_2{c}_2$ does not reduce to $c_4$ under CBV; it reduces to a large lambda-term with a lot of latent computation.

  • We can still check behavior by:

    • Comparing at the Church level:

      $\text{equal}{c}_4(\text{times}{c}_2{c}_2)\to \text{tru}$

    • Or more conveniently, converting to a primitive number:

      $\text{realnat}(\text{times}{c}_2{c}_2)\to 4$

  • Applying $\text{realnat}$ "finishes" the computation, because it supplies the missing arguments ($\text{succ}$ and $0$) and forces all remaining \beta-reductions.

Therefore:

• Encodings show that pure $\lambda$ is expressive enough.

• Primitives + conversions in $\lambda \text{𝐍𝐁}$ make examples and reasoning under call-by-value much easier to see and check.

Recursion ​

• Some terms never reach a normal form; they are said to diverge.

• The classic divergent/big omega combinator:

  $$\mathrm{\Omega }=(\lambda x.xx)(\lambda x.xx)$$

  • This term has exactly one redex; reducing it just gives back the same term $\omega$ again, so evaluation loops forever.

  • Any term with no normal form (like $\mathrm{\Omega }$) is said to diverge.

• The omega combinator has a useful generalization called the fixed-point combinator.

  • The call-by-name version is called the Y-combinator.

  • The call-by-value version is called the Z-combinator.

• The fixed-point combinator $\text{fix}$ is used to specify recursive definitions in the untyped \lambda-calculus:

  $$\text{fix}=\lambda f.(\lambda x.f(\lambda y.xxy))(\lambda x.f(\lambda y.xxy))$$

  • $\text{fix}f$ gives you a term $h$ such that, operationally,

    $$\text{fix}f\approx f(\text{fix}f)$$

    so $f$ receives a copy of its own result as an argument.

  • How to derive the call-by-value fixed-point combinator: (Friedman and Felleisen, 1996, Chapter 9).

• There is also a simpler call-by-name fixed-point combinator:

  $$Y=\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$$

  but:

  • $Y$ diverges under call-by-value.

  • This is because CBV tries to evaluate $xx$ too eagerly.

    -> It is not usable as-is in the CBV setting.

• Using $\text{fix}$ to define recursive functions

  We want recursive definitions of the form:

  • Informal recursive style:

    $$h=⟨\text{body containing }h⟩$$

  • To encode this in \lambda-calculus:

    1. First define a non-recursive generator:

       $$g=\lambda f.⟨\text{body containing }f⟩$$

    2. Then define the recursive function as:

       $$h=\text{fix}g$$

  • Operational idea:

    • $\text{fix}g$ expands to something like $g(\text{fix}g)$.

    • Everywhere $f$ appears in the body of $g$, it is effectively unrolled with another copy of the recursive function.

      -> Each recursive call "unrolls" one more copy of the body.

• Example: $\text{factorial}$ with Church numerals

  $$g=\lambda \text{fct}.\lambda n.\text{if }\text{realeq}n{c}_0\text{ then }{c}_1\text{ else }\text{times}n(\text{fct}(\text{prd}n))\text{factorial}=\text{fix}g$$

  • The $\text{fix}$ machinery ensures that each time $\text{fct}$ is applied.

    -> $\text{fct}$ effectively behaves like factorial itself.

    -> The definition is unrolled one step at a time.

  • Conceptually, $\text{fct}$ is a self-replicator:

    Applying $\text{fct}n$ feeds $\text{fct}$ and $n$ back into $g$.

    -> Producing another expanded copy of the recursive body, with new $\text{fct}$s ready to continue the process.

Exercise 5.2.9 Why did we use a primitive $\text{if}$ in the definition of $g$, instead of the Church-boolean $\text{test}$ function on Church booleans? Show how to define the $\text{factorial}$ function in terms of $\text{test}$ rather than $\text{if}$.

Exercise 5.2.10 Define a function $\text{churchnat}$ that converts a primitive natural number into the corresponding Church numeral.

Exercise 5.2.11 Use $\text{fix}$ and the encoding of lists from Exercise 5.2.8 to write a function that sums lists of Church numerals.

Representation ​

• What does it mean that Church numerals "represent" ordinary numbers?

• Ordinary naturals (as in $\lambda \text{𝐍𝐁}$):

  • A constant: $0$.

  • Operations:

    • $\text{succ}$: numbers $\to$ numbers.

    • $\text{pred}$: numbers $\to$ numbers.

    • $\text{iszero}$: numbers $\to$ booleans.

  • Their behavior is fixed by evaluation rules (e.g. $\text{succ}2=3$, $\text{iszero}0=\text{true}$).

• Church encoding idea: represent all of these as lambda-terms.

  • Zero: $c_0=\lambda s.\lambda z.z$

    • Other behaviorally equivalent (non-canonical) terms (e.g. $\text{lambdas}.\text{lambdaz}.(\text{lambdax}.x)z$) also count as representations of 0.

  • Successor/predecessor:

    • $\text{scc}$ represents $\text{succ}$: if $t$ represents $n$, then $\text{scc}t$ evaluates to a representation of $n+1$.

    • $\text{prd}$ represents $\text{pred}$: if $t$ represents $n$, then $\text{prd}t$ evaluates to a representation of $\max (n-1,0)$.

  • Zero test: $\text{iszro}$ represents $\text{iszero}$:

    • If $t$ represents 0, $\text{iszro}t$ evaluates to $\text{true}$.

    • If $t$ represents any $n\ne 0$, $\text{iszro}t$ evaluates to $\text{false}$.

• Representation correctness (observational view):

  • Take any program that:

    • Uses primitive numbers and operations ($0$, $\text{succ}$, $\text{pred}$, $\text{iszero}$, \ldots)

    • Produces a boolean result.

  • Replace all numbers and arithmetic operations with their Church encodings ($c_0$, $\text{scc}$, $\text{prd}$, $\text{iszro}$, \ldots).

  • After evaluation, the final boolean result is the same.

  • Therefore, no observable difference: Church numerals and primitive naturals behave the same from the program's point of view.

Formalities ​

Syntax ​

• The usual \lambda-calculus grammar (e.g. $t::=x|\text{lambdax}.t|tt$) is shorthand for an inductively defined set of abstract syntax trees.

• Terms:

  • Fix a countable set of variable names $V$.

  • The set of terms $T$ is the smallest set such that:

    1. $x\in T\text{for every }x\in V$.

    2. $\text{if }{t}_1\in T\text{ and }x\in V,\text{ then }\lambda x.t_1\in T$.

    3. $\text{if }{t}_1\in T\text{ and }{t}_2\in T,\text{ then }{t}_1{t}_2\in T$.

• Free variables ($\text{FV}$)

  • $\text{FV}(t)$ = set of variables that occur free in term $t$.

  • Rules:

    1. $\text{FV}(x)=x$.

    2. $\text{FV}(\lambda x.t_1)=\text{FV}(t_1)\setminus x$.

    3. $\text{FV}(t_1{t}_2)=\text{FV}(t_1)\cup \text{FV}(t_2)$.

Exercise 5.3.3 Give a careful proof that $|\text{FV}(t)|\le \text{size}(t)$ for every term $t$.

Substitution ​

• Throughout, two definitions of substitution are used:

  • The compact and intuitive definition shown before: $[x\to s]$, optimized for examples and in mathematical definitions and proofs.

  • Another developed in Chapter 6, is notationally heavier, depending on an alternative "de Bruijn presentation" of terms in which named variables are replaced by numeric indices, but is more convenient for the concrete ML implementations.

• Goal: define substitution $[x\mapsto s]t$ in the \lambda-calculus correctly (capture-avoiding).

Naive substitution (wrong #1) ​

• Defined structurally on term $t$:

  • $[x\mapsto s]x=s$.

  • $[x\mapsto s]y=y\text{if }x\ne y$

  • $[x\mapsto s](\lambda y.t_1)=\lambda y.[x\mapsto s]t_1$

  • $[x\mapsto s](t_1{t}_2)=([x\mapsto s]t_1)([x\mapsto s]t_2)$

• Problem: does not distinguish free vs bound occurrences of $x$.

  Example: $[x\mapsto y](\lambda x.x)=\lambda x.y$

  -> This conflicts with the basic intuition about functional abstractions that the names of bound variables do not matter: The identity function is exactly the same whether we write it $\text{lambdax}.x$ or $\text{lambday}.y$ or $\lambda \text{franz}.\text{franz}$. If these do not behave exactly the same under substitution, then they will not behave the same under reduction either, which seems wrong.

• Mistake: No distinction between free occurrences of a variable (which should get replaced during substitution) and bound ones, which should not.

Improved substitution (wrong #2) - stop at binder with the same name ​

• Modify abstraction case to not substitute under a binder with the same name:

  • $[x\mapsto s]x=s$

  • $[x\mapsto s]y=y\text{if }y\ne x$

  • $$[x\mapsto s](\lambda y.t_1)=\{\begin{array}{cc}\lambda y.t_1& \text{if }y=x\\ \lambda y.[x\mapsto s]t_1& \text{if }y\ne x\end{array}$$

  • $[x\mapsto s](t_1{t}_2)=([x\mapsto s]t_1)([x\mapsto s]t_2)$

• Fixes earlier issue, but introduces variable capture:

  Example: $[x\mapsto z](\lambda z.x)=\lambda z.z$

Variable capture & capture-avoiding substitution ​

• Variable capture: a free variable in $s$ becomes bound after substitution into $t$.

• To avoid this, in the abstraction case we must ensure the bound variable $y$:

  • is not $x$, and

  • does not occur free in $s$.

• Capture-avoiding substitution:

  • $[x\mapsto s]x=s$

  • $[x\mapsto s]y=y\text{if }y\ne x$

  • $$[x\mapsto s](\lambda y.t_1)=\{\begin{array}{cc}\lambda y.t_1& \text{if }y=x\\ \lambda y.[x\mapsto s]t_1& \text{if }y\ne x\text{ and }y\notin FV(s)\end{array}$$

  • $[x\mapsto s](t_1{t}_2)=([x\mapsto s]t_1)([x\mapsto s]t_2)$

• The above definition is partial: if $y\ne x$ but $y\in \text{FV}(s)$, no clause applies.

  -> Work with terms "up to renaming bound variables".

Alpha-conversion ​

• \alpha-conversion: Consistent renaming of a bound variable - $\text{lambday}.xy\equiv \text{lambdaw}.xw$.

• Convention: Terms that differ only by renaming bound variables are interchangeable - We work "up to \alpha-conversion".

• If substitution would be undefined because $y\in \text{FV}(s)$, we rename the bound variable first.

  Example:

  $[x\mapsto yz](\lambda y.xy)$

  • First rename: $\text{lambday}.xy$ \to $\text{lambdaw}.xw$

  • Then: $[x\mapsto yz](\lambda w.xw)=\lambda w.(yzw)$

Final capture-avoiding substitution definition ​

• Using the \alpha-conversion convention, we assume the binder $y$ is always chosen fresh (\neq $x$ and not free in $s$), so we can drop the special case:

  • $[x\mapsto s]x=s$

  • $[x\mapsto s]y=y\text{if }y\ne x$

  • $[x\mapsto s](\lambda y.t_1)=\lambda y.[x\mapsto s]t_1\text{if }y\ne x\text{ and }y\notin \text{FV}(s)$

  • $[x\mapsto s](t_1{t}_2)=([x\mapsto s]t_1)([x\mapsto s]t_2)$

• This is the standard capture-avoiding substitution used in \lambda-calculus proofs and definitions.

Operational semantics (lambda calculus) ​

The untyped lambda calculus \lambda

• Values are exactly lambda-abstractions:

  • $v::=\lambda x.t$

  • Evaluation stops when it reaches a $\lambda$; arbitrary $\lambda$-terms can be values.

• Small-step rules (call-by-value application)

  1. E-AppAbs - computation rule

  2. E-App1 ****(reduce the function part first) - congruence rule

  3. E-App2 (then reduce the argument) - congruence rule

• How metavariables enforce evaluation order

  • $v_2$ in E-AppAbs: must be a value, so \beta-reduction only fires when the argument is fully evaluated.

  • $t_1$ in E-App1: any term; we reduce the function position first while it can step.

  • $v$ in E-App2: the left side must already be a value, so we only start reducing the argument after the function is done.

  • Combined, these rules enforce call-by-value, left-to-right:

    1. Reduce $t_1$ to a value (E-App1).

    2. Reduce $t_2$ to a value (E-App2).

    3. Apply \beta (E-AppAbs).

• Special property of the pure \lambda-calculus

  • Since only \lambda-abstractions are values, once $t_1$ has been reduced to a value (by E-App1), it must be a $\text{lambdax}.t$.

  • This breaks once we enrich the language (e.g. add primitive booleans, numbers), where values include more forms than just \lambda-abstractions.

Exercise 5.3.6 Adapt these rules to describe the other three strategies for evaluation-full beta-reduction, normal-order, and lazy evaluation.

Exercise 5.3.7 Exercise 3.5.16 gave an alternative presentation of the operational semantics of booleans and arithmetic expressions in which stuck terms are defined to evaluate to a special constant wrong. Extend this semantics to $\lambda \text{𝐍𝐁}$.

Exercise 5.3.8 Exercise 4.2.2 introduced a "big-step" style of evaluation for arithmetic expressions, where the basic evaluation relation is "term $t$ evaluates to final result $v$." Show how to formulate the evaluation rules for lambda-terms in the big-step style.