Reading programming language papers: the notation, from sets to inference rules

This series follows the course Foundations of Programming Languages in my MSc in Software Engineering at FCUL, taught by Prof. Vasco T. Vasconcelos. It’s built on three books: Benjamin C. Pierce’s Types and Programming Languages (TAPL, MIT Press, 2002), Advanced Topics in Types and Programming Languages (MIT Press, 2005), edited by Pierce, and Session Types (Cambridge University Press, 2025) by Simon J. Gay and Vasco T. Vasconcelos himself. The goals:

• understand the fundamental abstractions of programming languages, as opposed to how a particular language happens to implement them;
• reason formally about the properties of a language;
• get comfortable with advanced ideas: linearity, traces, ownership and borrowing, and session types;
• see them at work in real languages like Rust and Go.

If that sounds far from day-to-day work, it isn’t. Every time TypeScript refuses to compile, a linter flags code that can never run, or Rust’s borrow checker stops you, you’re watching these ideas at work. This series is about how those tools can know what they know.

Before any of that, the notation. Programming language theory is written in a compact mathematical style that looks intimidating until you know about a dozen conventions. This post collects them in one place, with a tiny example language, so the rest of the series can just use them.

Sets, briefly#

Almost everything is a set, and a few symbols carry most of the weight:

The fancy $\T$ (a calligraphic T) is the set of terms: every well-formed expression of the language.

Terms, and a tiny language#

A term is a piece of syntax: a program, or part of one. To keep things small, take a language with just booleans and a conditional:

$t$::=terms|$\mathsf{true}$constant true|$\mathsf{false}$constant false|$\mathsf{if}\ t\ \mathsf{then}\ t\ \mathsf{else}\ t$conditional

This is a grammar in BNF style. Read ::= as “can be” and | as “or”: a term is true, or false, or if followed by three terms. So $\ite{\ttrue}{\tfalse}{\ttrue}$ is a term, and so is $\ite{(\ite{\tfalse}{\ttrue}{\tfalse})}{\ttrue}{\tfalse}$.

Metavariables#

The $t$ in the grammar is not part of the language. It’s a metavariable: a placeholder that stands for any term, used to talk about the language. When a rule says $\ite{\ttrue}{t_2}{t_3}$, the $t_2$ and $t_3$ can be replaced by any terms at all. Subscripts and primes ($t_1$, $t_2$, $t'$) just give different placeholders different names.

This two-level view is the first thing to get used to: there’s the object language (the language we study, with its true, if…) and the metalanguage (the maths we use to describe it, with its $\in$, $t_1$, and so on).

Three ways to define a set of terms#

A grammar is a convenient shorthand. Underneath, there are three precise definitions of the same set, and each one is handy for a different kind of argument.

1. Inductively: the smallest closed set#

The clauses say what must be in the set. “Smallest” says that nothing else is. Without it, a set that also contained, say, the number 42 would satisfy the clauses too. With it, every term got into $\T$ because a clause put it there, and that’s what lets us prove things aren’t terms.

2. With inference rules#

The same definition, written as inference rules, the notation used for nearly everything in the course:

(T-True)

axiom, by T-True:$\ttrue \in \T$

(T-False)

axiom, by T-False:$\tfalse \in \T$

$t_1 \in \T$

$t_2 \in \T$

$t_3 \in \T$

(T-If)

therefore, by T-If:$\ite{t_1}{t_2}{t_3} \in \T$

An inference rule reads: if everything above the line holds, then what’s below the line holds.

• The statements above the line are the premises.
• The statement below it is the conclusion.
• The label on the side is the rule’s name, so a proof can say which rule it used.

A statement like $t \in \T$, the kind of thing rules prove, is called a judgement.

Axioms and rules

An axiom is a rule with no premises: its conclusion holds unconditionally, so there’s nothing above its bar. T-True and T-False are axioms: $\ttrue$ is a term, full stop. T-If is not: it only concludes that a conditional is a term once you’ve shown its three parts are.

The distinction matters because every proof has to bottom out somewhere, and it always bottoms out in axioms.

Rules are schemas

A rule with metavariables is really a schema: a template for infinitely many concrete rules, one for each way to fill in $t_1$, $t_2$ and $t_3$. T-If with $t_1 = \ttrue$, $t_2 = \tfalse$, $t_3 = \ttrue$ is one instance; with other terms, another. When we use a rule, we always use an instance of it.

Derivations

A derivation is a tree of rule instances: each node is the conclusion of a rule whose premises are the nodes above it, and every leaf is an axiom. A term is in $\T$ exactly when there’s a finite derivation that ends with it.

(T-False)

axiom, by T-False:$\tfalse \in \T$

(T-True)

axiom, by T-True:$\ttrue \in \T$

(T-False)

axiom, by T-False:$\tfalse \in \T$

(T-If)

therefore, by T-If:$\ite{\tfalse}{\ttrue}{\tfalse} \in \T$

(T-True)

axiom, by T-True:$\ttrue \in \T$

(T-False)

axiom, by T-False:$\tfalse \in \T$

(T-If)

therefore, by T-If:$\ite{(\ite{\tfalse}{\ttrue}{\tfalse})}{\ttrue}{\tfalse} \in \T$

Read it from the bottom up to see why the term is a term, or from the top down to see how it’s built. Either way, the leaves are all axioms.

3. Concretely: building the set in layers#

The third definition mentions neither “smallest” nor rules. It builds the set up in stages, starting from nothing:

$$\begin{aligned} S_0 &= \emptyset \\ S_{i+1} &= \{\ttrue, \tfalse\} \cup \{\, \ite{t_1}{t_2}{t_3} \mid t_1, t_2, t_3 \in S_i \,\} \\ S &= \textstyle\bigcup_i S_i \end{aligned}$$

• $S_1 = \{\ttrue, \tfalse\}$: only the constants, since $S_0$ is empty.
• $S_2$ adds every conditional built from constants, like $\ite{\ttrue}{\tfalse}{\ttrue}$: eight of them.
• $S_3$ adds conditionals whose parts come from $S_2$, and so on.

Each stage contains the one before, every term appears at some finite stage, and $S$ collects them all. It’s a standard result that this gives exactly the same set: $\T = S$ (TAPL, Proposition 3.2.6, proves it for a slightly bigger language).

This view is the most down-to-earth of the three. It also tells you when a term appears: at the stage equal to its depth. $\ttrue$ has depth 1 and appears in $S_1$; a conditional of constants has depth 2 and appears in $S_2$.

Which one to use when#

Evaluation: rules about a relation#

Syntax says which terms exist. Semantics says what they mean. The style used in this course is operational semantics: define how a term runs, one small step at a time.

The judgement is now $t \eval t'$, read ”$t$ evaluates to $t'$ in one step”. It’s a relation between terms: a set of pairs, defined, again, by inference rules.

(E-IfTrue)

axiom, by E-IfTrue:$\ite{\ttrue}{t_2}{t_3} \eval t_2$

(E-IfFalse)

axiom, by E-IfFalse:$\ite{\tfalse}{t_2}{t_3} \eval t_3$

$t_1 \eval t_1'$

(E-If)

therefore, by E-If:$\ite{t_1}{t_2}{t_3} \eval \ite{t_1'}{t_2}{t_3}$

The same vocabulary applies. E-IfTrue and E-IfFalse are axioms: they fire whenever the condition is a literal boolean. E-If is a rule with one premise: to step a conditional whose condition isn’t a value yet, step the condition first.

The rules come in two flavours worth naming:

• Computation rules do the actual work: E-IfTrue and E-IfFalse replace a conditional by one of its branches.
• Congruence rules say where to work next: E-If steps inside the condition.

Values, normal forms and stuck terms#

• A value is a finished result: here, $\ttrue$ and $\tfalse$.
• A normal form is a term that no rule can step.
• A term is stuck if it’s a normal form but not a value. This tiny language has none, but add numbers and $\ite{0}{\ttrue}{\tfalse}$ gets stuck: no rule knows what to do with a condition that’s a number. Stuck terms are the language’s runtime errors, and ruling them out before running anything is what type systems are for.

$t \evals t'$ (with a star) is the multi-step relation: zero or more steps. Evaluating a program means following $\eval$ until you reach a normal form.

Proving things about all terms#

The last idea to have in hand is structural induction. Because every term is built from smaller terms by the rules, to prove a property $P$ holds for every term it’s enough to show:

• $P$ holds for the axioms’ terms (here, $\ttrue$ and $\tfalse$), and
• whenever $P$ holds for $t_1$, $t_2$ and $t_3$, it holds for $\ite{t_1}{t_2}{t_3}$.

It’s ordinary induction on numbers, generalised to trees, and it works for exactly the reason “smallest” works: there’s no other way for a term to exist. Most proofs in the course have this shape, and the next post has a first one.

Glossary#

Next in the series: the first exercise sheet, on TAPL’s arithmetic expressions, where all of this gets used.