Chapter 3: Lambda Calculus

New files

• src/names.rs
• src/normal.rs

Changed files

• src/eval.rs
• src/ast.rs
• src/lexer.rs
• src/lib.rs
• src/main.rs

Motivation

Our calculator can name a number. What if we could name a computation and use it with different inputs? That’s a function, and adding functions takes us a surprisingly long way. With just lambdas and application we can express the pure untyped lambda calculus. Even data can be represented by functions, as we’ll see with Church encodings (Pierce 2002). That’s a remarkable amount of expressive power for two pieces of syntax!

There are a couple of details we need to get right. If two variables are both called x, how do we know which one a function means? And when we call a function, should we evaluate its argument first? We’ll build substitution and closures ourselves so we can see the answers, rather than quietly borrowing Rust’s answers.

The Language, Now

Programs remain single expressions. Lambdas have one parameter, application associates left, and booleans control an if expression. Comparisons are integer operations. There are no type annotations yet.

let twice = \f -> \x -> f (f x) in twice (\x -> x + 1) 0

A closure remembers the bindings present where its lambda was evaluated. In let x = 1 in let f = \y -> x + y in let x = 100 in f 2, the result is 3. Using the caller’s binding of x instead would give dynamic scope.

Theory

The Untyped Grammar

The pure untyped lambda calculus has just three forms. An expression is a variable, an application, or an abstraction. Read each vertical bar as “or”.

$$\begin{array}{rlrl}e& =x& & \text{variable}\\ & \mid e_1{e}_2& & \text{application}\\ & \mid \lambda x.e& & \text{abstraction}\end{array}$$

That’s the whole calculus! Our little language adds a few conveniences so we can experiment without encoding every number and boolean as a function.

$$\begin{array}{rlrl}e& =\cdots & & \text{the three forms above}\\ & \mid n& & \text{integer literal}\\ & \mid \text{True}\mid \text{False}& & \text{boolean literal}\\ & \mid \text{let}x=e_1\text{in}{e}_2& & \text{local binding}\\ & \mid \text{if}{e}_1\text{then}{e}_2\text{else}{e}_3& & \text{conditional}\\ & \mid -e& & \text{integer negation}\\ & \mid e_{1}op{e}_2& & \text{binary operation}\end{array}$$

Here $n$ is an integer and $op$ is one of +, -, *, /, ==, <, or <=. Parentheses group expressions without adding a tree node. The parser also has an Error placeholder for recovery, which isn’t a form of an accepted program. “Untyped” means we have no static type checker yet, not that every combination of these forms makes sense at runtime.

Reduction and Evaluation

Calling a lambda means replacing its parameter with the supplied argument. This step is called beta reduction. For \x -> x + 1 applied to 41, we replace x and get 41 + 1. So far, so good. The subtlety begins when names repeat. We replace only free occurrences of the parameter in the body, and rename an inner binder if it would capture a free name from the argument. We’ll work through exactly that mistake below (Pierce 2002).

Evaluation order decides which reduction we do next. Normal order takes the leftmost outermost reducible expression, and our full reducer also continues under lambdas. Call-by-value first evaluates the function and its argument, then enters the body. A lambda itself is already a value.

The difference becomes visible when a function ignores an argument that would run forever. Normal order can skip that argument. Call-by-value gets stuck trying to compute it. The Y combinator gives us a particularly striking example. It computes factorial under normal order but exhausts our strict evaluator’s fuel. Running out of fuel means we’ve reached our experiment’s limit, not that we’ve proved the computation will never finish.

Why De Bruijn Indices?

Names help us read programs, but their spelling is incidental to binding. \x -> x and \answer -> answer describe the same function. We call them alpha-equivalent. Renaming a bound variable consistently changes nothing. Comparing their syntax trees directly, however, finds different strings. A compiler that rewrites named terms must keep distinguishing harmless renaming from a change in which binder an occurrence refers to.

Consider this reduction of an open term, where y is free:

(\x -> \y -> x) y

Replacing x with y mechanically gives \y -> y. That is wrong. The function should return the free y supplied as its argument, regardless of its own parameter. Rename the inner parameter first:

(\x -> \z -> x) y
→ \z -> y

This is the capture problem our substitution function must solve. De Bruijn indices give binding a representation that does not depend on fresh spellings. Replace each bound occurrence with its distance to its binder, counting from zero. Count enclosing binders, not application nodes or source lines.

We write λ. body for an unnamed lambda in the examples below. Its numbers are variable indices, not integer literals. This is explanatory notation, not input syntax for the chapter’s parser.

For a longer example, walk into \f -> \x -> f (f x). Entering the first lambda pushes f onto a scope stack. Entering the second pushes x:

scope, nearest first:  [x, f]
index:                  0  1

f (f x)                 1 (1 0)
\f -> \x -> f (f x)     λ. λ. 1 (1 0)

Both occurrences of f have index 1. Application adds no binder, so entering (f x) does not change either index. Renaming the parameters to g and seed produces exactly the same indexed tree. Alpha-equivalence has become ordinary structural equality (Pierce 2002). This is useful in our printer tests. A parse–print–parse round trip should preserve binding even if names change.

An open term still needs a way to represent free variables. Our Term type keeps them as Free(name), separate from Bound(index). Thus \x -> x y becomes Lam(App(Bound(0), Free("y"))). A non-recursive let introduces a binder only in its body. In let x = x in x, the right-hand x is free and the final x is bound:

Let(Free("x"), Bound(0))

Indices make renaming simple, but moving terms across binders still requires care. Inside \a -> (\x -> \b -> x) a, the argument a has index 0 at its original location. After reduction the result is \a -> \b -> a, where the same occurrence needs index 1. Copying the old zero would accidentally select b. An evaluator that substitutes directly into indexed terms needs shifting: adjust references to surrounding binders when a term moves into or out of a scope, while leaving its internally bound references alone.

Here we use indices for conversion and comparison. The normal-order reducer still substitutes in the named tree, and the strict evaluator uses closures. That keeps each example focused. Later Fun passes use unique names so their dumps remain readable. Nameless terms are a useful tool for understanding binding, not a requirement for every compiler IR.

S, K, and I: Functions Without Binders

A combinator is a lambda term with no free variables. It needs no bindings from its surroundings. Three small combinators are enough to express the functions of the pure untyped lambda calculus:

I = \x -> x
K = \x -> \y -> x
S = \f -> \g -> \x -> f x (g x)

These capital letters are mathematical names. The executable tests use lowercase s, k, and i as ordinary local bindings. Applications associate left, so S f g a means ((S f) g) a. Each reduction rule needs all its displayed arguments before it can fire.

I and K are easy to picture. S explains how an application can depend on a shared input. Given f, g, and a, compute f a and g a, then apply the first result to the second. The parentheses in f a (g a) matter.

Try choosing K for both functions:

S K K a
→ K a (K a)        apply the S rule
→ a                apply the K rule

So S K K behaves as I. That’s a beautiful little result. We can build identity out of two operations that, at first glance, don’t look much like identity at all. S and K suffice, though keeping I around makes expressions easier to read. Try the chapter’s s k k (i 42) example and follow the reductions.

Why should these particular operations eliminate lambdas? For a body t, write [x]t for a combinator expression that accepts x and produces t. Once inner lambdas have been translated, there are three cases:

[x]x       = I
[x]t       = K t                  when x is not free in t
[x](p q)   = S ([x]p) ([x]q)       otherwise

If the body is the parameter itself, return it. If the body ignores the parameter, use K to discard it. Otherwise the body is an application, and S passes the parameter to both translated children. This procedure is called bracket abstraction. Work from the innermost lambda outward. Translating a closed pure lambda term eventually leaves only combinators and applications.

For example, remove the binder from \x -> f x, treating f as a free name:

[x](f x)
= S ([x]f) ([x]x)
= S (K f) I

Check the result by giving it an argument:

S (K f) I a
→ (K f a) (I a)
→ f (I a)
→ f a

The occurrence of x has disappeared. The free f remains, as it should. De Bruijn indices retain binders and encode their references as distances. Bracket abstraction removes the binders and expresses their work as application. This gives us a small example of compilation between two representations of the same computation.

There is a catch, and it is the same evaluation-order question we started with. Normal order reduces K 42 omega to 42 even if omega runs forever. Our strict evaluator tries to compute omega before entering K’s body, so it never gets that far. These combinator equations describe rewriting in the pure calculus. They don’t let a strict compiler discard arbitrary computations. We’ll use SKI to understand binding and reduction, while Fun’s back end will use closures. Closures also spare us the large application trees that a simple combinator translation can produce.

Implementation

ast.rs adds lambdas, application, booleans, and conditionals. Its printer uses precedence contexts and adds parentheses only where required to retain the tree. The parser gives application higher precedence than arithmetic:

Application: Expr = {
    <a:Application> <b:Atom> => {
        let (start, end) = (a.span.start, b.span.end);
        Expr::new(Kind::App(Box::new(a), Box::new(b)), start, end)
    },
    Atom,
};

names.rs computes free variables and performs capture-avoiding substitution. The helper below handles a binder. The recursive substitution handles each term form. Fresh names avoid both free and bound names in the original body and the replacement, preventing a new name from colliding with an inner lambda.

#![allow(unused)]
fn main() {
fn binder(
    name: &str,
    body: &Expr,
    target: &str,
    value: &Expr,
) -> (String, Expr) {
    if name == target {
        return (name.to_owned(), body.clone());
    }
    let mut name = name.to_owned();
    let mut body = body.clone();
    if free(value).contains(&name) && free(&body).contains(target) {
        let mut used = BTreeSet::from([target.to_owned()]);
        all_names(&body, &mut used);
        all_names(value, &mut used);
        let mut fresh = format!("{name}'");
        while used.contains(&fresh) {
            fresh.push('\'');
        }
        let variable = Expr::new(Kind::Var(fresh.clone()), 0, 0);
        body = substitute(&body, &name, &variable);
        name = fresh;
    }
    (name, substitute(&body, target, value))
}
}

The same module converts a named term to indices. A stack holds names from the outermost to the innermost scope. A let right-hand side is converted before its binder is pushed. That binder belongs only to the body.

#![allow(unused)]
fn main() {
/// Bound names are distances to binders; free names remain explicit.
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum Term {
    Bound(usize),
    Free(String),
    Int(i64),
    Bool(bool),
    Lam(Box<Term>),
    App(Box<Term>, Box<Term>),
    Let(Box<Term>, Box<Term>),
    If(Box<Term>, Box<Term>, Box<Term>),
    Neg(Box<Term>),
    Binary(Op, Box<Term>, Box<Term>),
    Error,
}

/// Convert without substitution; alpha-equivalent expressions have equal terms.
pub fn debruijn(expr: &Expr, bound: &mut Vec<String>) -> Term {
    let mut go = |e: &Expr| Box::new(debruijn(e, bound));
    match &expr.kind {
        Kind::Var(n) => bound
            .iter()
            .rev()
            .position(|x| x == n)
            .map_or_else(|| Term::Free(n.clone()), Term::Bound),
        Kind::Lam(n, a) => {
            bound.push(n.clone());
            let body = debruijn(a, bound);
            bound.pop();
            Term::Lam(Box::new(body))
        }
        Kind::Let(n, a, b) => {
            let value = go(a);
            bound.push(n.clone());
            let body = debruijn(b, bound);
            bound.pop();
            Term::Let(value, Box::new(body))
        }
        Kind::App(a, b) => Term::App(go(a), go(b)),
        Kind::Binary(op, a, b) => Term::Binary(*op, go(a), go(b)),
        Kind::If(c, a, b) => Term::If(go(c), go(a), go(b)),
        Kind::Neg(a) => Term::Neg(go(a)),
        Kind::Int(n) => Term::Int(*n),
        Kind::Bool(b) => Term::Bool(*b),
        Kind::Error => Term::Error,
    }
}
}

normal.rs implements one small step. In the application case it substitutes without first evaluating the argument. If the function is not a lambda, it steps that function first, then the argument when no earlier redex exists.

#![allow(unused)]
fn main() {
Kind::App(function, argument) => {
    if let Kind::Lam(name, body) = &function.kind {
        return Ok(Some(substitute(body, name, argument)));
    }
    if let Some(next) = step(function)? {
        Kind::App(Box::new(next), argument.clone())
    } else if let Some(next) = step(argument)? {
        Kind::App(function.clone(), Box::new(next))
    } else {
        return Ok(None);
    }
}
}

reduce repeatedly calls step with a limit and a callback that displays each term. This reducer can inspect open terms, including irreducible applications. It is a term-rewriting demonstration rather than Fun’s eventual execution engine.

eval.rs instead stores a lambda’s environment in a closure:

#![allow(unused)]
fn main() {
/// Lexical bindings retained by a closure.
pub type Env = Vec<(String, Value)>;

#[derive(Clone, Debug)]
/// Runtime integers, booleans, and code paired with its lexical environment.
pub enum Value {
    Int(i64),
    Bool(bool),
    Closure(String, Rc<Expr>, Rc<Env>),
}
}

The call-by-value application case makes its order explicit:

#![allow(unused)]
fn main() {
Kind::App(function, argument) => {
    let function = evaluate(function, env, fuel)?;
    let argument = evaluate(argument, env, fuel)?;
    if let Value::Closure(name, body, captured) = function {
        let mut local = (*captured).clone();
        local.push((name, argument));
        evaluate(&body, &local, fuel)
    } else {
        Err("expected a function".into())
    }
}
}

The body runs in the captured environment extended with the argument. Each recursive visit consumes fuel. The CLI uses a larger host stack for these tree walkers. Chapter 5 replaces host recursion with an explicit machine. Neither fuel nor a larger stack is a substitute for that transformation.

Running It

$ cd crates/ch03_lambda
$ cargo run -q -- run tests/programs/church.fun
2
$ cargo run -q -- dump --pass=debruijn tests/programs/identity.fun
App(Lam(Bound(0)), Int(42))
$ cargo run -q -- repl
Lambda: :quit, :parse EXPR, :trace EXPR.
lambda> :trace (\x -> x) 42
(\x -> x) 42
42
lambda> :quit

Select normal order with run --engine=normal. Use --fuel=N when experimenting with terms that might not finish. The two engines count different operations, so the same fuel limit needn’t stop them at the same point. Try a function that ignores a failing argument to see why their answers can differ.

Exercises

1. Easy. Convert \x -> \y -> y x to de Bruijn indices by hand.
2. Medium. Substitute the free name y for x in \y -> \y' -> x y. Check the result’s free variables.
3. Medium. Translate \x -> x x by bracket abstraction, then apply the result to I. Compare its reduction with the lambda term.
4. Medium. Trace K I a b and explain which argument is discarded.
5. Hard. Construct a fixed-point combinator suitable for call-by-value and compare its trace with Y.

Further Reading

Pierce treats substitution, reduction, and nameless terms (Pierce 2002). Felleisen and Friedman introduce the abstract-machine setting that we return to in Chapter 5 (Felleisen and Friedman 1986).