1. Lambda Calculus Basics: Syntax and Variables

Contents

Working System

This chapter works in the untyped lambda calculus, represented as a Python AST (Var, Lam, App).

1. Lambda Calculus Basics: Syntax and Variables#

Goal. Build a precise reading of lambda terms, then implement a small Python representation to experiment with free and bound variables.

You will learn

  • The grammar of lambda terms

  • How to read and parenthesize terms

  • Free and bound variables

  • Alpha-renaming as a safe change of bound variable names

Roadmap#

  1. Define the syntax of lambda terms and the standard parenthesization conventions.

  2. Implement an AST (Var, Lam, App) and a readable printer show.

  3. Define and compute free variables.

  4. Implement alpha-renaming and test it on shadowing/capture examples.

Definition (Lambda Terms)

A term is built from three constructors.

  1. A variable: x

  2. An abstraction: λx. t

  3. An application: t u

Definition (Precedence and Associativity)

We use two conventions.

  1. Application associates to the left: t u v means (t u) v.

  2. Abstraction extends to the right: λx. t u means λx. (t u).

Example

λx. x (λy. y) means λx. (x (λy. y)), while (λx. x) (λy. y) applies the identity function to itself.

We’ll implement a small abstract syntax tree (AST) and some helper functions to reason about variables.

from dataclasses import dataclass
from typing import Set, Union

@dataclass(frozen=True)
class Var:
    name: str

@dataclass(frozen=True)
class Lam:
    param: str
    body: "Term"

@dataclass(frozen=True)
class App:
    fn: "Term"
    arg: "Term"

Term = Union[Var, Lam, App]

def show(t: Term) -> str:
    if isinstance(t, Var):
        return t.name
    if isinstance(t, Lam):
        return f"(λ{t.param}. {show(t.body)})"
    if isinstance(t, App):
        return f"({show(t.fn)} {show(t.arg)})"
    raise TypeError("Unknown term")

def free_vars(t: Term) -> Set[str]:
    if isinstance(t, Var):
        return {t.name}
    if isinstance(t, Lam):
        return free_vars(t.body) - {t.param}
    if isinstance(t, App):
        return free_vars(t.fn) | free_vars(t.arg)
    raise TypeError("Unknown term")

Example

Let t = (λx. x) (λy. y).

  • The function and argument are both abstractions.

  • No variables are free.

t = App(Lam("x", Var("x")), Lam("y", Var("y")))
print(show(t))
print(free_vars(t))

((λx. x) (λy. y))
set()

Definition (Free vs. Bound)

A variable occurrence is bound if it lies inside the scope of a matching λx. It is free otherwise.

Free variables act like parameters from the outside world.

Definition (Alpha-Renaming)

Alpha-renaming changes the name of a bound variable, keeping the term’s meaning the same.

Example: λx. x is alpha-equivalent to λz. z.

We will implement a safe bound-variable rename inside a lambda body.

Rules:

  • Do not rename inside an inner lambda that binds the same variable (shadowing).

  • The target binder must be fresh in the body to avoid capture.

  • If the requested name is not fresh, we automatically generate a fresh variant.

def all_vars(t: Term) -> Set[str]:
    if isinstance(t, Var):
        return {t.name}
    if isinstance(t, Lam):
        return {t.param} | all_vars(t.body)
    if isinstance(t, App):
        return all_vars(t.fn) | all_vars(t.arg)
    raise TypeError("Unknown term")

def fresh_var(used: Set[str], hint: str = "x") -> str:
    i = 0
    while True:
        candidate = f"{hint}{i}"
        if candidate not in used:
            return candidate
        i += 1

def rename_bound(body: Term, old: str, new: str) -> Term:
    if isinstance(body, Var):
        return Var(new) if body.name == old else body
    if isinstance(body, App):
        return App(rename_bound(body.fn, old, new), rename_bound(body.arg, old, new))
    if isinstance(body, Lam):
        if body.param == old:
            # Shadowing: stop here
            return body
        return Lam(body.param, rename_bound(body.body, old, new))
    raise TypeError("Unknown term")

def alpha_rename(lam_term: Lam, new_param: str) -> Lam:
    if new_param == lam_term.param:
        return lam_term
    used = all_vars(lam_term.body) | {lam_term.param}
    target = new_param if new_param not in used else fresh_var(used | {new_param}, new_param)
    return Lam(target, rename_bound(lam_term.body, lam_term.param, target))

Example

Alpha-renaming changes bound names but keeps meaning.

term = Lam("x", App(Var("x"), Var("y")))
renamed = alpha_rename(term, "z")
print(show(term))
print(show(renamed))

# Requesting binder "y" would capture free y; alpha_rename makes it fresh automatically.
capture_sensitive = Lam("x", App(Var("x"), Var("y")))
print(show(alpha_rename(capture_sensitive, "y")))

(λx. (x y))
(λz. (z y))
(λy0. (y0 y))

Exercise

  1. Compute the free variables of λx. (x (y z)).

  2. Alpha-rename the outer binder in λx. (λx. x) x to w. Which occurrences of x should change?

  3. Give a term where renaming a binder to a free variable name would change meaning (capture). What does a capture-avoiding alpha-rename do instead?

  4. For each term, compute the set of free variables: (a) λx. λy. x y, (b) λx. y x, © (λx. x) y. See solution: Exercise 1 (Lambda Basics)

Summary#

  • Lambda terms are built from variables, abstractions, and applications.

  • Parenthesization conventions matter: application is left-associative; abstraction extends to the right.

  • Free variables are computed structurally; bound variables are those introduced by a surrounding binder.

  • Alpha-renaming changes only a chosen binder and the occurrences it binds (shadowing stops renaming).

  • Capture-avoiding alpha-renaming never turns a free variable into a bound one.

  • Operationally: edit a term in the code cells and re-run free_vars(...) and show(...) to see how binding changes.

  • Next: capture-avoiding substitution and beta-reduction (Chapter 2).

Contents