L5) The Three Semantics

Giving Meaning to Formal Languages

When we say that a program “does something,” what exactly do we mean? That it executes step by step? That it computes a mathematical function? Or that it adheres to certain properties?

Where does this article fit in?

This article is part of the Formal Languages (L) series. After syntax (CFG L2, EBNF L3, AST L4), it addresses the meaning of formal languages through three approaches. Article L6 delves deeper into the operational approach applied to BP3.

Why is this important?

Imagine you need to explain what a program does. You could:

Simulate its execution step by step, like a debugger
Describe the function it computes, from inputs to outputs
List the properties it guarantees, such as “it never divides by zero”

These three approaches correspond to three families of formal semantics: operational, denotational, and axiomatic. Each answers different questions and adapts to different contexts.

For the BP2SC project (BP3-to-SuperCollider, see I2 and I3) — a transpiler (source-to-source code translator) that converts BP3 musical grammars (the Bol Processor language) into SuperCollider patterns (generative motifs) (sound synthesis environment) — understanding these distinctions is crucial. How do you specify that a stochastic rule (with random, probabilistic behavior) “does what it’s supposed to” when its result changes with each execution? Operational semantics gives us the answer.

The idea in one sentence

The three formal semantics describe the meaning of a program in three complementary ways: by its execution (operational), by the function it computes (denotational), or by the properties it verifies (axiomatic).

Let’s explain step by step

Example 1: A coffee machine

Let’s take a concrete example before addressing music: an automatic coffee machine.

What is a mathematical function?

A function is a relation that associates exactly one output with each input. For example, the “double” function associates each number with its double: double(3) = 6, double(5) = 10. In computer science, a program is often seen as a function: it takes inputs (data) and produces outputs (results).

Operational Semantics — “How it works”

We describe the system’s transitions:

Initial state: (waiting, 0€)

Insert 1€:     (waiting, 0€) → (waiting, 1€)
Insert 1€:     (waiting, 1€) → (ready, 2€)
Press coffee:  (ready, 2€)   → (dispensing, 0€)
Coffee served: (dispensing, 0€) → (waiting, 0€)

This is a mechanistic description: we see exactly what happens at each step.

Denotational Semantics — “What function”

We describe what the system computes:

machine : (money, button) → (coffee | nothing)

machine(2€, coffee) = coffee
machine(1€, coffee) = nothing
machine(2€, tea)    = tea

How to read the · (double brackets) notation?

The double brackets X are read as “the denotation of X” or “what X means mathematically.” This is the standard notation in formal semantics. Here, machine means “the mathematical function that the machine represents.” The expression machine(2€, coffee) = coffee is read as: “the function denoted by the machine, applied to inputs 2€ and coffee, yields coffee as output.”

We ignore the “how” to focus on the input-output relationship.

Axiomatic Semantics — “What guarantees”

We describe the system’s invariants:

{money ≥ 2€ ∧ button = coffee}
  press
{coffee_dispensed = true ∧ money = 0€}

What is a Hoare triple?

A Hoare triple is a notation invented by British logician Tony Hoare in 1969 to formally reason about programs. It is the foundation of Hoare logic, used to prove that a program does what it is supposed to do.

The triple has the form {P} C {Q} where:

{P} is the precondition (what must be true before)

C is the command or program

{Q} is the postcondition (what will be true after)

How to read a Hoare triple {P} C {Q}?

This notation reads: “if property P is true before executing C, then property Q will be true after.” The curly braces {...} enclose assertions (statements about the program’s state). Here:

{money ≥ 2€ ∧ button = coffee} is the precondition: what must be true before

press is the action (or command)

{coffee_dispensed = true ∧ money = 0€} is the postcondition: what is guaranteed after

The symbol ∧ means “and” (logical conjunction)

We prove that if certain conditions are met before, others will be met after.

Example 2: A BP3 musical grammar

Now let’s move on to algorithmic music. Here is a simple BP3 rule:

RND[2]
<3> Motif --> do ré mi
<2> Motif --> fa sol la

RND[2] indicates a random derivation mode with 2 rules. The weights <3> and <2> (see B4) determine the probability of each alternative. This grammar says: “Motif can become either do ré mi (weight 3, or 60% chance), or fa sol la (weight 2, or 40%)”.

Operational Semantics — BP3’s SOS rules

What is SOS?

SOS (Structural Operational Semantics) is a formalism invented by Gordon Plotkin in 1981 to precisely describe how a program executes step by step.

The idea: we define inference rules that describe how the program’s state evolves at each step. Each rule has the form:
    conditions (what must be true)
    ─────────────────────────────────
    conclusion (what happens then)

It’s like a recipe: “if you are in this situation, here’s what happens next.”

We define configurations and transitions:

Configuration C = (σ, φ, t)
- σ (sigma) : string of symbols (e.g., "S Motif Motif")
- φ (phi) : state of flags (e.g., {Ideas: 20})
- t : current time

Transition for RND mode:
                    random choice among applicable rules
    ────────────────────────────────────────────────────────
    (σ₁ · Motif · σ₂, φ, t) ⟹ (σ₁ · "do ré mi" · σ₂, φ, t')

How to read the notation ⟨e, σ⟩ ⟹ ⟨e', σ'⟩?

This notation describes a transition (an execution step):

⟨ and ⟩ are angle brackets that enclose a configuration (a snapshot of the program’s state)

e is the expression or string currently being processed

σ (sigma) represents the state: memory, variables, flags…

⟹ (double arrow) means “transforms into” or “reduces to”

e' and σ' (with prime) represent the new values after the execution step

The symbol · represents string concatenation (joining end-to-end)

Full reading: “the configuration (expression e with state σ) transforms into (expression e’ with state σ’)”.

Each derivation is a sequence of transitions. At each step, an applicable rule is chosen and applied.

Denotational Semantics — How to formalize randomness?

At first glance, one might think that randomness poses a problem: what is “the function” computed by a random grammar, if the output changes with each execution?

In fact, mathematics handles this situation very well. Probabilistic semantics (a field established since the 1980s) defines the meaning of a stochastic program not as a single value, but as a probability distribution over the possible values.

Motif = { "do ré mi" ↦ 3/5, "fa sol la" ↦ 2/5 }

This notation reads: “the denotation of Motif is a distribution where do ré mi has a probability of 3/5 and fa sol la has a probability of 2/5″.

This is not a hack

Probabilistic semantics is mathematically rigorous. It uses measure theory and probability spaces. Entire languages (like probabilistic programming languages for machine learning) are formalized this way.

For BP3, however, operational semantics is preferred because it is closer to the implementation: it concretely describes how the generator chooses a rule at each step, rather than reasoning about abstract distributions.

Axiomatic Semantics — Musical invariants

We could specify properties:

{weight(rule1) > 0 ∧ weight(rule2) > 0}
  derive(Motif)
{result ∈ {"do ré mi", "fa sol la"}}

Or more musical properties:

{mode = RND}
  derive_n_times(Motif, 1000)
{frequency("do ré mi") ≈ 0.6 ± 0.05}

Comparative table: when to use which?

Criterion	Operational	Denotational	Axiomatic
Question	How does it execute?	What function does it compute?	What properties does it guarantee?
Perspective	Implementer	Mathematician	Verifier
Formalism	Transition rules	Functions, domains	Pre/post-conditions
Notation	`⟨e, σ⟩ ⟹ ⟨e', σ'⟩`	`e : D → D'`	`{P} C {Q}`
Strengths	Close to code, testable	Compositional*, abstract	Allows proof

\ Compositional means that the meaning of a whole depends only on the meaning of its parts. Like a recipe: the taste of the final dish depends on the taste of each ingredient combined according to the steps.*
| Weaknesses | Verbose, low-level | Difficult for effects | Requires annotations |
| Ideal for | Interpreters, debuggers | Optimization, equivalence | Verification, contracts |

The three approaches in practice

When to choose operational?

You are implementing an interpreter (program that executes code directly) or a compiler (program that translates code into another form)
The language has side effects (state, inputs/outputs)
You want to specify the exact step-by-step behavior
BP2SC Example: SOS rules define how to derive a grammar

When to choose denotational?

You want to reason about program equivalence
The language is purely functional
You are looking to optimize (two programs = same function = can substitute)
Example: proving that Pseq([a,b,c], 1) and Pseq([a], 1) ++ Pseq([b,c], 1) are equivalent in SuperCollider (Pseq = pattern sequence, ++ = concatenation)

When to choose axiomatic?

You want to prove that a program is correct
You use formal verification tools
You specify contracts (preconditions/postconditions)
Example: verifying that a BP3 grammar always terminates

The case of BP3: why operational dominates

BP3 is a language of stochastic grammars. Its characteristics make operational semantics particularly suitable:

Mutable state: flags (conditional flags, see B4) like /Ideas=20/ modify the global state
Stochasticity: weights (<3>, <2>, see B4) introduce randomness
Decremental weights: <50-12> changes with each use
Time: notes have durations, time advances

Operational semantics captures all of this naturally via configurations (σ, φ, t) and transition rules.

Denotational semantics, on the other hand, would have to model:

Probability distributions (not simple values)
State transformations (monads in theory)
Continuous time

What is a monad?

A monad is a mathematical structure that allows encapsulating “effects” (randomness, state, errors, inputs/outputs) within a purely functional framework. Imagine a box that contains not only a value but also a “recipe” for managing side effects. In Haskell, for example, IO Int is a monad that represents “a computation that performs input/output and returns an integer.” For BP3, we would need a monad combining probabilities AND mutable state.

This is feasible but much more complex.

A bit of history: where do these three approaches come from?

Operational semantics (1960s-80s)

The idea of describing a language by its execution rules dates back to the first interpreters. But it was Gordon Plotkin who, in 1981, formalized the approach with SOS (Structural Operational Semantics). His key idea: to structure the rules in a compositional way — the behavior of a composite expression depends on the behavior of its parts.

Before Plotkin, definitions were often ad hoc, difficult to compare between languages. With SOS, we have a unified, reusable, and mathematically rigorous framework.

Denotational semantics (1960s-70s)

Developed primarily by Dana Scott and Christopher Strachey at Oxford, this approach sought to give a mathematical meaning to programs, independently of any machine. The idea: a program is a function, period.

The main challenge was to give meaning to loops and recursion. Scott introduced domain theory to solve this problem — a contribution that earned him the Turing Award in 1976.

What is domain theory?

It is a branch of mathematics that provides a framework for talking about “partially defined values” and “computations that may not terminate.” It defines structures (called domains) where one can give meaning to circular definitions like f(x) = f(x) + 1. Without this theory, it would be impossible to mathematically define what a while loop or a recursive function means.

Axiomatic semantics (1960s-70s)

C.A.R. Hoare published his foundational paper “An Axiomatic Basis for Computer Programming” in 1969. His idea: instead of describing what a program does, describe what it guarantees. The famous “Hoare triples” {P} C {Q} were born.

This approach gave rise to the entire field of formal verification: mathematically proving that a program is correct. Tools like Coq and Isabelle (formal proof assistants) or modern static analyzers are its direct descendants.

Combinations and hybrids

In practice, approaches are often combined:

Operational + axiomatic semantics

One can define a Hoare logic on top of an operational semantics. Hoare’s rules state: “if SOS guarantees such a transition, then such a postcondition is true.”

This is the basis of most verification tools: they use operational semantics as a foundation and build axiomatic proofs on top of it.

Operational-denotational correspondence

An important result in language theory is the correspondence between semantics: proving that ⟨e, σ⟩ ⇓ v (operational; ⇓ means “evaluates to”) if and only if e(σ) = v (denotational).

This correspondence ensures that the two viewpoints are consistent — one describes the “how,” the other the “what,” but they agree on the final result.

The particular case of algorithmic music

For BP3 and algorithmic music in general, these three semantics offer complementary perspectives:

Operational: how the grammar is derived, step by step, to produce a sequence of notes. This is what the BP3 engine does.

Denotational: what probability distribution over possible pieces is generated. Useful for musicological analysis (which motifs are more frequent?).

Axiomatic: what musical constraints are respected (tessitura — the range of playable notes —, valid rhythm, no forbidden dissonances…). Useful for computer-assisted composition.

The BP2SC transpiler (see B7) focuses on the operational aspect: it translates derivation rules into SuperCollider patterns that reproduce the same behavior.

Key takeaways

Operational semantics: describes how a program executes, step by step. Ideal for interpreters and stateful languages.
Denotational semantics: describes what function a program computes. Ideal for mathematical reasoning and optimization.
Axiomatic semantics: describes what properties a program guarantees. Ideal for formal verification.
Complementarity: these three approaches are not mutually exclusive. Operational can be used for implementation, denotational for optimization, and axiomatic for verification.
BP3 and operational: for stochastic grammars with state like BP3, operational semantics (SOS) is the most natural and practical approach.

Glossary

Compositionality: property whereby the meaning of a composite expression depends only on the meaning of its components. Example: the meaning of “2 + 3” depends only on the meaning of “2”, “3”, and “+”.
Configuration: complete state of a program at a given instant (expression to evaluate + environment + memory). Notated ⟨e, σ⟩ where e is the expression and σ is the state.
Semantic domain: mathematical set in which programs are interpreted (integers, functions, distributions…).
Mathematical function: relation that associates exactly one element from a starting set (domain) with each element from a target set (codomain). Example: f(x) = x + 1 associates each integer with its successor.
Invariant: property that remains true throughout execution.
Monad: mathematical structure allowing the encapsulation of effects (state, randomness, errors) within a functional framework. Used to model programs with side effects in denotational semantics.
· notation: double brackets meaning “the denotation of” or “the mathematical meaning of”. e is read “the denotation of e”.
Fixed point: value x such that f(x) = x. Example: 0 is a fixed point of f(x) = x², because f(0) = 0. In semantics, used to define loops and recursion.
Postcondition: property guaranteed after the execution of an instruction.
Precondition: property required before the execution of an instruction.
Inference rule: schema of the form “if these premises are true, then this conclusion is true”.
Semantics: formal study of the meaning of programs.
Stochasticity: random or probabilistic nature of a process. A stochastic system can produce different results with each execution.
Domain theory: branch of mathematics providing the necessary structures (ordered domains) to define the semantics of loops and recursion.
Transition: passage from one configuration to another during execution. Notated ⟨e, σ⟩ ⟹ ⟨e', σ'⟩.
Hoare triple: notation {P} C {Q} meaning “if P is true before C, then Q is true after”.

Prerequisite: L2 — Context-Free Grammars
Reading time: 10 min
Tags: #semantics #formalism #language-theory #verification

Next articles:

L6 — SOS for Dummies — Structural Operational Semantics
L7 — Denotational Semantics — when a program becomes a function
L8 — Axiomatic Semantics — proving program correctness