Chapter 2

The Language of Terms

Before a kernel can check anything, it needs a precise language of terms. Ours has five kinds of term, and that is enough to express propositional logic with quantification over propositions. This chapter fixes the grammar, the notational conventions used for the rest of the book, and the Rust type that represents terms.

Five kinds of terms

The core language is a small dependent type theory. Its terms are generated by the grammar

t, A, B \;::=\; \Sort{u} \;\mid\; x \;\mid\; \tPi{x}{A}{B} \;\mid\; \tLam{x}{A}{t} \;\mid\; t\;s

where $u$ is a natural number and $x$ is a variable name. Each form has a role.

$\Sort{u}$ is a universe: a type whose elements are themselves types. The number $u$ is its level. $\Sort{0}$ is the universe of propositions. Chapter 13 explains why there is a whole hierarchy rather than a single universe.
$x$ is a variable. Its meaning comes from the context in which it appears, either a $\lambda$ or $\Pi$ binder enclosing it or an assumption in the typing context.
$\tPi{x}{A}{B}$ is a $\Pi$ -type, the dependent function type from Chapter 1. It is the type of functions that take an $x : A$ and return something of type $B$ , where $B$ may mention $x$ .
$\tLam{x}{A}{t}$ is a $\lambda$ -abstraction, a function that takes an argument $x$ of type $A$ and returns $t$ .
$t\;s$ is application of $t$ to $s$ .

The grammar makes no distinction between types and terms. The proposition $\tPi{P}{\Sort{0}}{P \to P}$ and its proof $\tLam{P}{\Sort{0}}{\tLam{p}{P}{p}}$ are both terms built from the same five constructors:

\underbrace{\tLam{P}{\Sort{0}}{\tLam{p}{P}{p}}}_{\text{proof}} \quad : \quad \underbrace{\tPi{P}{\Sort{0}}{P \to P}}_{\text{proposition, the type of the proof}}.

The same two terms, seen as trees, make the shared grammar visible. Every node is one of the five constructors; the name on a $\Pi$ or $\lambda$ node is the variable it binds. Click a node to see the subterm it stands for, or type another term.

Whether a term is a valid type is not a syntactic property. It is decided by the type checker: a term is a type exactly when its own type is a universe (Chapter 5).

Conventions

The book uses the following letters consistently.

Letters	Stand for
$s, t, a, b, f$ and $A, B, C, T$ (possibly primed or subscripted)	terms
$x, y, z$ and any name bound by $\Pi$ or $\lambda$	variable names
$u, v, w$	universe levels
$\Gamma$	typing contexts (Chapter 3)
$\Sigma$	the signature of constants (Chapter 7)

Three abbreviations keep terms readable.

Arrows. When $B$ does not mention $x$ , we write $A \to B$ for $\tPi{x}{A}{B}$ . Ordinary function types are thus a special case of dependent function types, and implication is a special case of universal quantification. In the implementation the binder of an arrow is the reserved name _.

Associativity. Application associates to the left and arrows to the right:

f\;a\;b \;=\; (f\;a)\;b, \qquad A \to B \to C \;=\; A \to (B \to C).

Currying. A function of two arguments is a function that takes the first argument and returns a function waiting for the second. For example, $\tLam{a}{A}{\tLam{b}{B}{a}}$ has type $A \to B \to A$ , and applying it to $x : A$ and $y : B$ is written

(\tLam{a}{A}{\tLam{b}{B}{a}})\;x\;y \;=\; ((\tLam{a}{A}{\tLam{b}{B}{a}})\;x)\;y.

The two associativity conventions are designed to fit together: a curried function of type $A \to B \to C$ applied as $f\;a\;b$ needs no parentheses on either side.

Binding and scope

In $\tLam{x}{A}{t}$ and $\tPi{x}{A}{B}$ , the variable $x$ is bound, and its scope is the body $t$ or $B$ . The annotation $A$ is outside the scope: in $\tLam{x}{x}{x}$ the $x$ in the annotation refers to something outside the term, while the $x$ in the body refers to the argument. A variable occurrence that is not inside the scope of a binder for it is free. For example, in $\tLam{x}{P}{f\;x\;y}$ the variables $P$ , $f$ , and $y$ are free and $x$ is bound.

Two facts about bound variables matter throughout the book, and both are formalized in Chapter 11.

The name of a bound variable carries no meaning: $\tLam{x}{A}{x}$ and $\tLam{y}{A}{y}$ are the same function. Terms that differ only in the names of bound variables are called alpha-equivalent, and a kernel must treat them as equal.
Replacing a variable by a term, which the typing rules and computation both require, must not accidentally bring a free variable under a binder of the same name. Getting this right is called capture-avoiding substitution.

Both facts are easy to state and both have caused real bugs in real proof checkers, which is why they get their own chapter.

In the code

Terms are the Rust enum Term in src/term.rs. There is one variant per kind of term, plus the constants of Part II.

#[derive(Clone, Debug, PartialEq, Eq)]
pub enum Term {
    Sort(u64),                          // Sort u
    Var(String),                        // x        (local, bound or in the context)
    Const(String),                      // c        (global, from the signature)
    Pi(String, Box<Term>, Box<Term>),   // Pi (x : A). B
    Lam(String, Box<Term>, Box<Term>),  // fun (x : A). b
    App(Box<Term>, Box<Term>),          // f a
}

Variables are represented by their names as strings, and binders store the bound name. This is the most direct representation and the easiest to read; it is also the one that makes the naming problems of Chapter 11 unavoidable, which is deliberate, because the point of the book is to see those problems and solve them.

The same file provides small constructor functions so that terms can be written without nested Box::new calls: var("x"), const_term("Nat"), app(f, a), pi("x", a, b), lam("x", a, b), and arrow(a, b), which builds pi("_", a, b). Three helpers encode the conventions of this chapter directly.

/// f a_1 ... a_n   (left-associated application)
pub fn apps(f: Term, args: impl IntoIterator<Item = Term>) -> Term {
    args.into_iter().fold(f, app)
}

/// Pi (x_1 : A_1) ... Pi (x_k : A_k). tail   (a telescope of binders)
pub fn telescope(binders: &[(String, Term)], tail: Term) -> Term {
    binders.iter().rev().fold(tail, |body, (name, ty)| pi(name, ty.clone(), body))
}

/// Decomposes t into its spine: a head that is not an application, and its arguments.
/// f a b  becomes  (f, [a, b]);  a non-application becomes  (t, []).
pub fn spine(t: &Term) -> (Term, Vec<Term>) {
    match t {
        Term::App(f, a) => {
            let (head, mut args) = spine(f);
            args.push((**a).clone());
            (head, args)
        }
        _ => (t.clone(), vec![]),
    }
}

apps and spine are inverses of each other: apps(h, args) builds the left-nested application $h\;a_1 \cdots a_n$ , and spine takes it apart again. The spine view is how the reduction engine of Chapter 12 looks at a term, so get comfortable with it now. The nested term $((f\;a)\;b)\;c$ has head $f$ and arguments $[a, b, c]$ ; walking down the function side of each application reaches the head, and the arguments collected on the way, read from the inside out, are in the right order.

The surface syntax of the .leanmini scripts used throughout the book writes the same terms as Sort 0, forall (x : A), B, A -> B, fun (x : A) => b, and juxtaposition for application. Appendix E gives the full grammar.

Exercises

Write the proposition "for all propositions $P$ and $Q$ , $P$ implies $Q$ implies $P$ " as a term, and give a proof term for it.

Solution

The proposition is $\tPi{P}{\Sort{0}}{\tPi{Q}{\Sort{0}}{P \to Q \to P}}$ , which unfolds to $\tPi{P}{\Sort{0}}{\tPi{Q}{\Sort{0}}{\tPi{\_}{P}{\tPi{\_}{Q}{P}}}}$ . A proof is $\tLam{P}{\Sort{0}}{\tLam{Q}{\Sort{0}}{\tLam{p}{P}{\tLam{q}{Q}{p}}}}$ . In leanmini syntax:

goal forall (P : Sort 0), forall (Q : Sort 0), P -> Q -> P
exact fun (P : Sort 0) => fun (Q : Sort 0) => fun (p : P) => fun (q : Q) => p
qed

Fully parenthesize $f\;a\;(g\;b)\;c$ and $A \to (B \to C) \to D$ , then give the spine of the first term.

Solution

$f\;a\;(g\;b)\;c = ((f\;a)\;(g\;b))\;c$ , with head $f$ and arguments $[a,\; g\;b,\; c]$ . Note that $g\;b$ stays a single argument because of the parentheses. $A \to (B \to C) \to D = A \to ((B \to C) \to D)$ , which is $\tPi{\_}{A}{\tPi{\_}{(\tPi{\_}{B}{C})}{D}}$ .

In $\tLam{x}{A}{\tLam{y}{x}{\tLam{x}{\Sort{0}}{y}}}$ , which occurrences of $x$ refer to which binder? Which variables are free?

Solution

The $x$ in the annotation of $y$ refers to the outer binder $\lambda(x : A)$ , because the inner $\lambda(x : \Sort{0})$ has not been entered yet. The innermost $x$ is bound by the inner binder but never used. The only free variable is $A$ . This term reappears in Chapter 11, where it breaks a type checker that handles shadowing carelessly.

What to remember

Terms are universes $\Sort{u}$ , variables, $\Pi$ -types, $\lambda$ -abstractions, and applications. Types and terms share one grammar.
$A \to B$ abbreviates a $\Pi$ -type whose body ignores its variable. Application is left-associative, arrows are right-associative, and functions are curried.
Bound variable names are arbitrary, and substitution must avoid capture. Both are handled in Chapter 11.
In Rust, Term is an enum with one variant per form, and spine/apps convert between nested applications and a head with an argument list.