Tales - On denotational, operational and axiomatic semantics

The notion of the syntax of a programming language is usually well-understood: it’s essentially the grammar, the rules for writing “correct” sentences within this language. Amusingly, the way people usually describe semantics is much less clear, for example:

In programming language theory, semantics is the rigorous mathematical study of the meaning of programming languages. Semantics assigns computational meaning to valid strings in a programming language syntax. It is closely related to, and often crosses over with, the semantics of mathematical proofs.

Semantics describes the processes a computer follows when executing a program in that specific language. This can be done by describing the relationship between the input and output of a program, or giving an explanation of how the program will be executed on a certain platform, thereby creating a model of computation.

– Wikipédia entry for Semantics (computer science), 2024-07-14

I think¹ it’s safe to say that the core idea behind semantics is to connect the syntax of a program with some abstract ideas: we would describe equally the semantics of a natural language, where we’d try to connect symbols to ideas. Now, if we want to reach anything meaningful through this connection, we want to be rigorous, formal, and so the connection, and the abstract ideas must be mathematically sound.

This – mathematically connecting (the syntax) of a program with some mathematical objects – is called “denotational semantics”.

Then, there are two common special cases of denotational semantics:

Operational semantics, where we create a link between (the syntax of) a program and some algorithmic formalism;
Axiomatic semantics, where we create a link between (the syntax of) a program and some logical formalism;

One is finally left but to wonder as to why things are usually presented so confusingly. It seems that it’s merely because of the historical development of the subject: different people pushed things in different directions, aimed at different goals; each found in their own direction different tools and results, and progressively segmented the domain between operational/denotational/axiomatic.

So conceptually, denotational semantics is the real deal, and the other two are mere instances.

Denotational semantics aims at connecting (the syntax of) a program with “arbitrary” abstract mathematical objects; this allows to study the “meaning” of a program in a very general way;
Operational semantics aims at describing in particular the execution of a program; this is useful e.g. to implement compilers, or to teach programming, where you need to understand how each instruction will affect the hardware; we (ideally) connect here (the syntax of) a program to a mathematical modelling of the execution hardware;
Axiomatic semantics aims at evaluating the correctness of a program; we connect (the syntax of) a program to a logical system.

Note: Of course in the case of operational semantics, if you consider the case of teaching programming or writing compilers, you don’t always have a strict, precise mathematical model of the hardware, and things are a bit looser. Still rigorous though. But it’s a good enough approximation, especially in the context where semantics is discussed in terms of “operational/denotational/axiomatic semantics.”

The essence of what I am presenting in this short note seems to be confirmed by the second part of this reddit comment; feel free to correct me. ↩︎

Comments

By email, at mathieu.bivert chez: