Syntax and Semantics

A programming language is described in two parts. Its syntax fixes what counts as a program: the rules that decide whether a string of characters is one at all. Its semantics gives each program a meaning: what it computes, and how. The two are separable: one meaning can be given more than one syntax, and one syntax more than one meaning. For example x / y in one language divides the values as integers and in another as reals. Similarly, within a single language x + y may add two numbers or concatenate two strings depending on what values x and y store.

When you have a bug in your program, it is either a syntax error — an error caused by misspelling your program: an unmatched parenthesis, a misspelled keyword, an unknown language construct — or a logical error: one that results in a program that behaves in an unexpected or inconsistent way. Syntax errors are typically trivial to detect and relatively easy to fix. Logic errors are harder: the program runs, but does the wrong thing, often in subtle ways. Much of what programmers spend their time on (i.e., testing, debugging, verification) is closing the gap between the program written and the program intended, and all of it rests on being able to say precisely what a program means. That meaning is the focus of this book.

Syntax: what counts as a program

A language’s syntax is the set of rules that decide which strings of characters are programs and what structure each one has: characters grouped into tokens, tokens assembled into a tree. Those rules are given by a grammar — a finite set of productions a mechanical procedure can check a candidate program against, and the same productions a parser follows to recover a program’s structure. Whether a string is a legal program is, once the grammar is fixed, a question with a definite answer.

Two layers hide inside the word syntax. The concrete syntax is the text as written — every parenthesis, the choice of && over and, the whitespace, the fact that multiplication binds tighter than addition. The abstract syntax is the structure that remains once those surface choices have done their one job of disambiguating: a tree commonly referred to as the abstract syntax tree (AST), which records only how the pieces of a program fit together.

The gap between the concrete and abstract syntax is easiest to see by holding the abstract structure fixed, while varying how that structure is concretely written. These three expressions are spelled by different rules:

x + y          (+ x y)          x y +

The first is infix, an operator written between its operands, the arrangement most languages inherit from arithmetic. The second is prefix, the operator first, as in Lisp, where every call takes this parenthesized form. The third is postfix, the operator last, as in the input to a reverse-Polish calculator. Three concrete syntaxes — yet a parser for any of them produces the same abstract structure, an addition with x and y beneath it, and an evaluator handed that structure cannot tell which spelling it came from. The surface can be redrawn without disturbing what is underneath, which is why this book starts at the AST: the structure is where meaning will be assigned, and the AST is the form the rest of the book works on.

In the decade preceding ALGOL 60, a programming language’s syntax was described the same way as a natural language: in prose, with examples, but ultimately determined by the programs its compiler accepted. The ALGOL 60 report gave the language’s syntax in a formal notation instead — now called Backus–Naur Form — precise enough that whether a string is a legal program became a mechanical question the report itself settled, ahead of and independent of any compiler. Backus had introduced the notation a year earlier for ALGOL 58, whose own report still described its syntax in prose; the 1960 report is where a formal grammar became the definition. Syntax has had a clean formal footing ever since.

Semantics: what a program means

Once a string counts as a program, the question becomes what that program means. Previously, we framed meaning as a mapping from a piece of syntax to a mathematical object — the value an expression evaluates to, or a coarser object such as its type. Formally, that mapping is called the semantics of the programming language. A semantics falls into one of two kinds, based on whether the meaning it assigns can be determined without ever running the program.

A semantics is static when the meaning it assigns can be determined by inspecting the program’s text alone, without ever running it. For example, determining whether every identifier a program uses is declared and in scope at each of its uses is a static question (cf. Part III) that can be answered without ever running the program on any inputs. Similarly, type checking is normally a static check (cf. Part VI): whether an operation is applied to a value of the right kind. Consider writing a program where a number is added to a function. A parser would happily parse the expression x + f, because at the time of parsing both x and f are simply names. Type checking, however, would determine that x is a name representing an integer and f is a function, and thus be able to reject the expression x + f as nonsense.

A semantics is dynamic when the meaning it assigns can only be determined by executing the program. The quintessential dynamic semantics is the concrete semantics: it traces how concrete inputs flow through the program to produce its concrete outputs. The interpreter you build throughout this book, beginning in Part II, computes exactly this, one construct at a time. When we ask what a program means, we typically mean its concrete semantics. A program can pass every static check and still not be the program we intended — i.e., the program can be well-formed, well-scoped, well-typed, and still compute the wrong answer. Static semantics is useful for confirming a program is well-behaved (as prescribed by the static check), whereas dynamic semantics describes its actual observed behavior.

A notation for meaning

ALGOL 60 gave a program’s syntax a formal notation, but its meaning was still written informally, in prose. The written description of the program’s semantics was ambiguous and allows multiple interpretations and open questions about how a program should behave. For example, should an operand short-circuit and not evaluate the right-hand operand when the left-hand one already decides the result? Does an assignment produce a value, and if so which one? Since prose can leave such questions open, two reasonable implementors can read the same description and produce two disagreeing implementations.

Over the years and decades since ALGOL 60, several notations were developed to give a program’s meaning unambiguously (cf. Program semantics). For evaluating expressions, this book uses the following notation

$$\rho ⊢e\Downarrow v$$

which can be read as in the environment $\rho$, the expression $e$ evaluates to the value $v$. The environment $\rho$ supplies the value of every name in scope, so a variable can be looked up (cf. Part III). The meaning of an expression is given by rules that tell us how to derive the meaning of an expression from the evaluation of the expression’s sub-expressions. Below we show three example rules in turn. The first rule says that the literal $0$ evaluates to itself — as does every literal — regardless of the environment.

$$\frac{}{\rho ⊢0\Downarrow 0}(\text{E-Lit})$$

The next rule states that the variable $x$ evaluates to the value $v$ assuming that in the environment $\rho$ the variable $x$ is bound to the value $v$.

$$\frac{\rho (x)=v}{\rho ⊢x\Downarrow v}(\text{E-Var})$$

The final rule states that the sum of two expressions is simply the sum of the evaluation of each of those expressions.

$$\frac{\rho ⊢e_1\Downarrow v_1\rho ⊢e_2\Downarrow v_2}{\rho ⊢e_1+e_2\Downarrow v_1+v_2}(\text{E-Add})$$

This style of writing rules has deep roots in logic and computer science: that the fact below the line is true exactly when every assumption above the line is true. This style of rules dates back to Gentzen’s work in the 1930s on logic, and it’s been used by computer scientists to define how a program executes since Plotkin in 1981 (operational semantics) and Kahn in 1987 (big-step semantics). Throughout this book, we develop these rules into a full account of Bridger’s concrete semantics.

Does the spelling matter?

How a program is spelled shapes how easily it can be read, written, and understood. Over the years, concrete forms have converged on shared expectations about meaning: a for loop is read as iterating over a collection, x := e as updating the value a variable holds, infix + as arithmetic. A reader draws on those expectations from the spelling alone, before working through what any rule says. The surface governs what a language makes easy to express and easy to grasp, and a form that cuts against a reader’s expectations misleads about as readily as a poor name.

This book starts past that point, at the abstract syntax — not because spelling is a cosmetic detail, but because this book’s subject is meaning, and meaning is assigned to a program’s structure rather than its surface syntax. How a language chooses its surface, and how that choice shapes the programs people actually write, is a real question with a study of its own; this book simply begins where meaning does.

Further reading

Giving meaning a formal footing: after BNF gave syntax a formal definition, doing the same for meaning took most of the following decade and produced several styles at once. Glynn Winskel’s The Formal Semantics of Programming Languages: An Introduction (MIT Press, 1993) is an accessible book-length review of those semantics, building each from small example languages. C. A. R. Hoare’s “An Axiomatic Basis for Computer Programming” (1969) is the primary source for one of those styles, reasoning about what a program establishes rather than tracing what it does; the operational style the rule above is written in is developed further in Program semantics.

Whether notation shapes thought: Kenneth Iverson’s Turing Award lecture “Notation as a Tool of Thought” (1980) argues the design-space question from the side that says syntax is far from cosmetic — that a well-chosen notation does part of a programmer’s reasoning for them, using the array notation of APL to make the case.

Concept checks