What is syntax?

I’m in the middle of confronting my lack of knowledge about denotational semantics. One of the things that has confused me for so long about denotational semantics, which I didn’t even realize was confusing me, was the use of the word “syntax” (and, consequently, “semantics”).

For context, the contents of this note will be obvious to perhaps half of programming languages (PL) researchers. Perhaps half enter PL through math. That is not how I entered PL. I entered PL through software engineering. I was very interested in building beautiful software and systems; I still am. Until recently, I ran my own cloud infrastructure—mail, calendars, reminders, contacts, file syncing, remote git syncing. I still run some of it. I run secondary spam filtering over university email for people in my department, because out department’s email system is garbage. I am way better at building systems and writing software than math, but I’m interested in PL and logic and math nonetheless. Unfortunately, I lack lot of background and constantly struggle with a huge part, perhaps half, of PL research. The most advanced math course I took was Calculus 1. (well, I took a graduate recursion theory course too, but I think I passed that course because it was a grad course, not because I did well.)

So when I hear “syntax”, I think “oh sure. I know what that is. It’s the grammar of a programming language. The string, or more often the tree structure, used to represent the program text.”. And that led me to misunderstand half of programming languages research.

The First Meaning of Syntax

Syntax has two meanings in programming languages, and both meanings can frequently be found in the same paper.

The first meaning is the one I gave above. I could give a definition of the syntax (in the first sense) of the lambda-calculus as follows.

e ::= x | (lambda (x) e) | (e e)

Ah. Beautiful syntax.

If we were following a standard text, such as Harper’s Practical Foundation for Programming Languages (2nd ed), we might next define the “semantics” of this “syntax”. We might define the “static semantics”, i.e., the type system or binding rules, then the “dynamic semantics”, i.e., the rules governing the evaluation behaviour of the syntax. For example, I might write the following small-step operational semantics.

((lambda (x) e) e') -> e[x := e']

Ah. Beautiful semantics.

Except, everything I wrote above, reduction rule included, is also syntax and not semantics.

Historical Interlude

The words “syntax” and “semantics” come from mathematical logic.

In that context, “syntax” describes sentences, statements, symbols, formulas, etc, without respect to any meaning. You can write down a logical formula say as "∀ X.P(X, A)" (where “A” is a logical constant, “X” is a variable, “P” is a proposition), and it has no meaning; it’s mere syntax. It might be true, or might be false, depending on its interpretation of “P”, “A”, and "∀". I could say that it means “all leaves are green”, which would be false. A more relevant example for PL might be the syntax ((lambda (x) x+1) 2) = 3, which I would certainly like to be true, but it very much depends on what I mean. If + means string append as in JavaScript, then the statement is false since ''.concat(1, 2) = '12'. Wikipedia is a good start for trying to understand this history of the word “syntax”: https://en.wikipedia.org/wiki/Syntax_(logic)

By contrast, in that same context, “semantics” is the means by which syntax is given an interpretation. Perhaps the most widely used approach to providing an interpretation of syntax is model theory, which I never learned. In model theory, we start with a “syntax” (or “theory”). This theory is a collection of constants, function symbols, and predicate symbols. A model then is a map from the uninterpreted syntax to some interpretation that preserves relationships. I’ll say more of this in a later post, but for now, consider the following example. I might provide a model of our earlier example that interprets + as ''.concat, and = is mapped to, say ===. This preserves relationships, if all my constants are mapped to strings. Wikipedia is a good source for this history too: https://en.wikipedia.org/wiki/Semantics_of_logic.

When Semantics is the Syntax

What’s interesting about this history is how it was adopted in programming languages, and evolved in two different ways. On the one hand, a programming language grammar is syntax, in the sense of being uninterpreted statements. That syntax can be given a semantics, an interpretation, by using operation semantics (this is the sense in which operational semantics is a semantics). The operational semantics provides an interpretation to our grammar.

But, in another sense, the grammar, typing rules, and evaluation rules (the “syntax”, “static semantics”, and “dynamic semantics”) are mere syntax, in the older logical sense. They are a theory, in the model-theoretic sense. To see why, we must understand what the earlier example ((lambda (x) x+1) 2) = 3 means. Or in fact, realize that it doesn’t mean anything at all.

To write this down is to write down a proposition about the grammar: that one piece of the grammar is equal to another. Except I didn’t write a proposition that the two were equal. I wrote the uninterpreted proposition symbol =, the syntax =, next to two pieces of uninterpreted grammar, two other pieces of syntax. Every syntactic judgment about our grammar is itself syntax, in the model theoretic sense. At least, this is true if we follow the tradition of writing them down synthetically, axiomatically, about the grammar, as is done in standard programming languages textbooks such as Types and Programming Languages or Practical Foundations for Programming Languages.

In this view, the typing rules and reduction relations are syntax. This is a bizarre perspective from a software engineering perspective, but makes sense from the mathematical logic perspective.

With this perspective, it might make sense to call “operational semantics” “syntactic semantics”, or to imagine a tower of syntax and semantics where one level’s semantics become the next level’s syntax. This view finally helped me make sense of why we call “syntactic logical relations” syntactic, when they are clearly semantics. (A problem I danced around in my previous post on logical relations.)

This perspective is also useful, for two reasons. The first is that reasoning purely syntactically, while very general, prevents you from importing any other reasoning principles from any other domain. By viewing the typing system as syntax, and then building a model of it (and by necessity, the programming language terms) in, say, set theory, we can import all set-theoretic reasoning in our attempts to reason about our type system. But more than that, we can reinterpret the syntax freely, to prove general results. While I might have written a type system using syntax that looks like numbers, I could build a model that interprets that type system as over strings, and know that actually the entire system is safe for strings, too. Appropriately generalized, I wouldn’t need to do any additional proofs.

Unfortunately, this double meaning of the word syntax seems to be completely taken for granted by some. nLab is a good example of this. To quote from the introduction to the nLab model theory page:

On the one hand, there is syntax. On the other hand, there is semantics. Model theory is (roughly) about the relations between the two: model theory studies classes of models of theories, hence classes of “mathematical structures”.

What’s most interesting about this quote isn’t what it says, but what it links to. The link for “syntax” is to the page on the internal logic of a category. From the software perspective, this is not syntax, but semantics. How on earth could it be syntax? The link for “semantics” is to the page on structure, the idea of equipping a category with a particular functor. How on earth is that any more semantics than the original abstract nonsense version of syntax?

Before I understood “syntax”, I couldn’t make any sense of that, but now I’m beginning to understand. The internal logic of a category in some sense must be able to express the grammar of a language, and the judgments of a language, but in a purely syntactic way—in the same way that when I write down the grammar and typing rules of a language, I don’t refer to any interpretation of those symbols beyond the way I combine them on the page. Then the semantics or structure is a the particular functor over that category, providing an interpretation, a semantics, of that original category (the syntax).

Anyway, now I think I’m ready to understand what a model is.