L11) Beyond the Three Semantics

Translation, Process, and Algebra

In L5, we described three ways to give meaning to a program: operational, denotational, axiomatic. But the real world needs more. How do you give meaning to a compiler? To two processes running in parallel? To a data type defined by its equations? Three families of semantics answer these questions — and they are far from exotic.

Where does this article fit in?

This article extends the semantic trilogy of the L series:

Operational: “how it executes” — explored in L6
Denotational: “what mathematical function it computes” — explored in L7
Axiomatic: “what properties it guarantees” — explored in L8

L5 to L8 covered the three historical pillars. But in practice, many systems don’t fit well into these three frameworks: compilers define the meaning of a language by translating it into another; concurrent systems (web servers, orchestras, networks) need tools to reason about parallelism; and abstract data types are naturally described by algebraic equations.

L11 explores these three extensions. Each answers a question that classical semantics leave open.

Why is this important?

Every compiler is an embodied translational semantics. When you write TypeScript, its meaning is what it compiles into (JavaScript). When BP2SC translates a BP3 grammar into SuperCollider patterns, it defines a translational semantics for BP3.
Concurrent systems are everywhere: every web server, every reactive interface, every orchestral score involves processes running in parallel and synchronizing. Process semantics provides the vocabulary to talk about them rigorously.
Abstract data types (stacks, queues, dictionaries) are ubiquitous in programming. Algebraic semantics provides a framework for specifying them by their properties, independently of any implementation.

These are not academic curiosities. These are the tools that computer scientists really use — often without knowing they are doing semantics.

The idea in one sentence

Beyond the three classical semantics, a program can be given meaning by what it translates into (translational semantics), by its interactions with other processes (process semantics), or by the equations its operations satisfy (algebraic semantics).

Translational Semantics

Meaning by Translation

The foundational idea is disarmingly simple: the meaning of a program P is the meaning of its translation T(P).

We don’t directly define what P “means”. We translate it into a target language whose semantics are already known, and we say: “the meaning of P is the meaning of T(P) in the target language.”

Analogy:

Imagine a poem in Japanese. You don’t speak Japanese, but you have a French translation. For you, the meaning of the Japanese poem is its French translation. Of course, something might be lost in translation — and that’s exactly the type of question that translational semantics forces us to ask: does the translation preserve all the meaning?

This is exactly what a compiler does. TypeScript does not have an independent formal semantics; its meaning is defined by its compilation to JavaScript. The C language, in practice, is defined by what GCC or Clang do with it. Every transpiler (source-to-source compiler, which translates a high-level language into another high-level language, as opposed to a classic compiler that targets machine code), every compiler, every translator is a translational semantics.

The difference with other semantics is structural: operational semantics says “here are the execution steps”, denotational says “here is the function computed”, axiomatic says “here are the guaranteed properties”. Translational semantics says: “here is an equivalent program in another language — go ask that language what it means.”

It’s an indirect definition, and it immediately raises a question: does the target language itself have a well-defined semantics? If so, the chain is solid. If not, we are building on sand.

Deciphering:

The technical term is translational semantics. We also sometimes speak of compilational semantics when the translation is a compilation. The key point: the semantics is indirect — it goes through an intermediary. This indirection is not a flaw: it’s exactly what all compilers do in practice.

The Morris Diagram (1973)

In 1973, James Morris formalized the idea with a classic diagram:

Source ── compile ──> Target
  |                     |
  | meaning_S           | meaning_T
  v                     v
Value_S ============ Value_T

Deciphering:

The top arrow (compile) translates the source program into the target program

The vertical arrows (meaning_S, meaning_T) give the semantics of each program in its respective language

The double line at the bottom ( ==== ) asserts that the two semantic values are equivalent

This diagram must commute: whether one takes the path “compile then interpret the target” or the path “interpret the source directly”, the same result must be obtained. A correct compiler is a compiler that makes this diagram commute.

This is a powerful test. If your compiler produces a target program whose behavior differs from what the source program is supposed to do, the diagram does not commute: the compiler is incorrect.

The CompCert project (Leroy, 2006) achieved the feat of formally proving in Coq (a proof assistant: software that mechanically verifies that each step of a mathematical reasoning is correct, eliminating any possibility of human error in the demonstration) that the Morris diagram commutes for a complete C compiler. This is one of the greatest achievements of applied formal verification: a compiler whose every translation pass is mathematically guaranteed to preserve the meaning of the source program.

Transducers: The Machines That Translate

If translational semantics is “meaning by translation”, a natural question arises: what machines perform this translation? The theory of transducers answers this.

Finite State Transducers (FST):
An FST reads an input word and produces an output word, letter by letter. It’s a finite automaton enriched with an output: at each transition, it consumes an input symbol and emits an output symbol.

FSTs are used in natural language processing (morphology, phonology) and speech synthesis. But they are too weak for compilation: they don’t handle recursive structures (nested parentheses, nested blocks). An FST cannot “count” nesting levels — exactly the same limitation as regular languages compared to context-free languages (cf. Chomsky hierarchy in L1).

Tree transducers:
A program is not a string of characters — it’s a tree (the AST, abstract syntax tree). Tree transducers transform one tree into another tree, node by node. This is exactly what a compiler does: it takes the AST of the source program and produces the AST of the target program.

There is a hierarchy of power:

FST  ⊂  top-down tree  ⊂  macro tree transducers

FST: string to string, no recursion
Top-down tree transducers: process the tree from root to leaves, one node at a time
Macro tree transducers: can accumulate parameters during the descent, making them powerful enough to model most real compilation passes

Deciphering:

Why trees? Because the translation of an if-then-else does not depend only on keywords — it depends on the structure: the then is a subtree, the else is another. A tree transducer naturally captures this hierarchical structure.

A word on Action Semantics (Mosses, 1992):

Peter Mosses pushed the translational idea further with Action Semantics. Instead of translating a program into an existing target language, it is translated into a universal intermediate language composed of “actions”: giving (producing a value), binding (linking a name), storing (modifying memory), communicating (sending a message). These actions are composed with modular combinators. The advantage: adding a new construct to the source language does not force rewriting existing rules. It is the most modular translational semantics available.

Application: BP2SC, the first formalized musical transpiler

The BP2SC project translates BP3 grammars (formal musical notation) into SuperCollider patterns (sound synthesis language). This is a concrete case of translational semantics:

Source: the AST of a BP3 grammar (25 node types: Sequence, Polymetric, Sound, Duration, etc.)
Target: SuperCollider expressions (Pbind, Pseq, Ppar, etc.)
Translation rules: each node type has a rule that transforms it into its SuperCollider equivalent

BP3 AST ── translate ──> SC Pattern
  |                         |
  | meaning_BP3             | meaning_SC
  v                         v
Musical structure ====== Sound output

The Morris diagram applies directly: a BP3 grammar and the SuperCollider pattern it produces must yield the “same music”.

But there is a fundamental problem: SuperCollider has no formal specification. The semantics of the target language is defined by its implementation (the sclang interpreter), not by a mathematical document. The diagram can only commute conditionally — assuming that the SuperCollider interpreter does what we believe it does.

Deciphering:

This is a common problem in practice. TypeScript’s translational semantics relies on JavaScript’s semantics, which is itself defined by the ECMAScript specification — an 800-page document. But for BP2SC, no equivalent specification exists for SuperCollider. The correctness of the transpiler is therefore relative to the implementation, not to a specification. Before BP2SC, no musical notation language had received a formalized translational semantics.

Process Semantics

Meaning by Concurrency

The three classical semantics (and even translational semantics) assume a sequential world: one program, one execution, step by step. But the real world is concurrent. A web server handles hundreds of requests in parallel. An orchestra of 80 musicians plays simultaneously. An operating system manages dozens of processes that share resources.

Process semantics models programs as communicating processes. The meaning of a system is not what it computes, but how its components interact.

Analogy:

Imagine an orchestra. Each musician is a process: they follow their score autonomously. But at certain moments — downbeats, repeats, cadences — the musicians must synchronize. The conductor is a communication channel. The meaning of the symphony is not in the individual scores, but in the interaction between all musicians.

CCS (Milner, 1980)

The Calculus of Communicating Systems (CCS), invented by Robin Milner, is the first major formalism for concurrent processes.

Basic ingredients:

Processes: entities that perform actions
Actions: a, b, c… (observable actions) and tau (internal, invisible action)
Parallel composition P | Q: P and Q execute at the same time
Restriction (new a) P: action a is private to P (invisible from outside)
Choice P + Q: the process chooses between behaving like P or like Q

Example: the coffee machine

Machine = coin . coffee . Machine
User    = coin . coffee . nil
System  = Machine | User

Deciphering:

Machine: waits for a coin (coin), serves coffee (coffee), then restarts

User: inserts a coin, takes coffee, stops (nil)

System: both in parallel — they synchronize on coin and coffee

The dot . means “then” (sequencing)

Reading: The machine and the user interact via the shared actions coin and coffee. The user inserts a coin, the machine receives it; the machine serves coffee, the user takes it. The interaction is the semantics.

CCS has a minimalist elegance: with only five operators (prefix, choice, parallel, restriction, renaming), a surprising variety of concurrent systems can be modeled.

CCS has its own operational semantics (SOS rules — Structural Operational Semantics, as in L6). For example, the synchronization rule:

  P ──a──> P'    Q ──a̅──> Q'
────────────────────────────── (Com)
     P | Q ──tau──> P' | Q'

Deciphering:

When P can perform action a and Q can perform the complementary action a̅ (the “reception” of a), the two processes synchronize. The resulting action is tau — invisible from the outside. This is a private rendezvous between P and Q. This rule is at the heart of all inter-process communication in CCS.

Robin Milner received the Turing Award in 1991, largely for CCS and its subsequent developments (the pi-calculus, an extension of CCS that adds mobility of communication channels — processes can exchange channels, not just messages).

CSP (Hoare, 1985)

Communicating Sequential Processes (CSP), created by Tony Hoare (the same as Hoare logic from [[L8_Semantique_Axiomatique|L8)]), is the other major formalism for concurrency.

Key difference with CCS: in CSP, synchronization occurs on shared events. If two processes both propose event a, they must perform it together — it’s a mandatory synchronization. In CCS, synchronization is asymmetric (action/co-action); in CSP, it’s symmetric (same event on both sides).

CSP has had a considerable industrial impact: it is used to verify security protocols (TLS, Kerberos), integrated circuit design, and critical embedded systems. The FDR tool (Failures-Divergences Refinement) automatically verifies that a CSP system satisfies its specification.

CSP offers three semantic models of increasing richness:

Model	What it captures	Example
Traces	Possible sequences of events	`{<coin, coffee>, <coin>}`
Failures	Traces + refused events	Distinguishes a blocked process from a waiting process
Failures-Divergences	+ divergent behaviors (infinite loops)	Detects livelocks (active blockages: the system loops indefinitely without ever progressing)

Deciphering:

Why three models? Because traces alone are not enough to distinguish all systems. Two vending machines that accept the same sequences of coins and coffees might behave differently in case of failure: one refuses your coin (it’s blocked), the other accepts it and loops indefinitely without serving coffee (it diverges). The failures model distinguishes the first case; the failures-divergences model distinguishes the second.

Musical example: two musicians synchronizing

Violin = downbeat . melody . Violin
Piano  = downbeat . chords . Piano
Duo    = Violin [| {downbeat} |] Piano

The two instruments play in parallel but synchronize on the downbeat event. Between downbeats, each plays independently. This is exactly the mechanism of ensemble music.

Deciphering:

The notation [| {downbeat} |] is CSP’s alphabetized parallelism operator: the two processes synchronize only on the events listed in the set (here, {downbeat}). For all other events (melody, chords), each process advances at its own pace. This is a remarkably faithful model of what happens in a real musical duo.

Bisimulation: When Two Systems Behave the Same

A fundamental question in process semantics: when can we say that two systems are equivalent?

The naive answer would be: “when they produce the same sequences of events” (trace equivalence). But this is insufficient.

Counter-example:

P = coin . (coffee + tea)
Q = (coin . coffee) + (coin . tea)

P: insert a coin, then choose between coffee and tea
Q: choose between (insert a coin then coffee) and (insert a coin then tea)

Both have the same traces: {<coin, coffee>, <coin, tea>}. But they are different! With P, after inserting the coin, you still have a choice. With Q, the choice has already been made before insertion.

Bisimulation captures this difference. Two processes P and Q are bisimilar if an external observer cannot distinguish them at any point of interaction — not just by looking at the complete traces, but also the branching structure at each step.

Formally, a bisimulation is a relation R between processes such that if (P, Q) belongs to R:

if P can perform action a and become P’, then Q can perform a and become Q’, with (P’, Q’) in R
and vice versa (if Q can perform a…)

Deciphering:

Bisimulation is finer than trace equivalence: it takes into account when choices are made, not just what results are possible. In the example above, P and Q are trace-equivalent but not bisimilar. This distinction has practical consequences: if you replace a component P with a component Q in a system, and P and Q are only trace-equivalent (not bisimilar), the overall system may behave differently.

Application: Polymetry as Parallel Processes

In BP3, the {voice1, voice2} construct places two voices in parallel. This is exactly a parallel composition in the sense of CCS or CSP:

V1 | V2

The voices execute independently but synchronize at measure boundaries (or other rendezvous points defined by the grammar).

In CSP, this would be expressed as:

Voice1 = note_do . note_re . note_mi . barline . Voice1
Voice2 = note_sol . note_la . barline . Voice2
Piece  = Voice1 [| {barline} |] Voice2

Each voice can have a different number of notes between measure bars — this is polymetry. Synchronization on barline forces the two voices to meet at the same structural points, while maintaining their rhythmic independence between these points.

Deciphering:

Mark Ross (1995) proposed MWSCCS (Meije Weighted Synchronous CCS), an extension of CCS with weights, to model musical performance. In this framework, each musician is a CCS process, synchronizations represent ensemble points (downbeats, cadences), and weights model dynamic nuances. BP3 polymetry naturally lends itself to this modeling: each polymetric voice is a process that emits musical events (notes, rests) and synchronizes with other voices at structural points.

Algebraic Semantics

Meaning by Equations

Algebraic semantics adopts a radically different perspective: the meaning of a program — or a data type — is given by the equations that its operations satisfy.

The foundational idea, due to Goguen, Thatcher, Wagner, and Wright (1977), is to view an AST (abstract syntax tree) as an initial algebra. In this view, syntax is an algebra (the AST constructors are the operations), and semantics is the unique homomorphism from this initial algebra to an interpretation domain.

Deciphering:

A homomorphism is a function that preserves structure. If the AST says “addition of 3 and 5”, the homomorphism to integers gives 3 + 5 = 8. If the AST says “sequence of C and D”, the homomorphism to MIDI events gives the corresponding note sequence. The fact that this homomorphism is unique (thanks to initiality) guarantees that there is only one way to give meaning to each program — which is exactly what we want from a semantics.

Concrete example: a stack can be specified by algebraic equations:

pop(push(x, s)) = s
top(push(x, s)) = x

These two equations are the semantics of the stack. Nothing is said about the implementation (array? linked list? contiguous memory?). It only states: push then pop restores the original stack, and top after push gives the pushed element. Any implementation that satisfies these equations is correct.

This framework has a direct link with BP3. BP3 homomorphisms (master/slave, the _ho(), _se(), _al() constructs) transform one musical object into another while preserving certain structural properties. Algebraic semantics provides the vocabulary to formalize this idea: each BP3 homomorphism is an algebra morphism, and the correctness of the transformation is verified by the preserved algebraic properties.

Deciphering:

Algebraic semantics is particularly well-suited for declarative languages (those that describe what is to be achieved, without specifying how to achieve it — like SQL for databases, or BP3 grammars that describe a musical structure without detailing execution steps). It is, however, less natural for imperative languages (those that describe a sequence of step-by-step instructions, like C or Python), because these languages rely on side effects — modifications to the program’s state (writing to a variable, displaying on screen, sending a network message) that are not easily captured by simple equations.

In summary: if your system is well-defined by “doing X then undoing X restores the initial state” (like pop(push(x, s)) = s), algebraic semantics excels. If your system depends on when and in what order things happen, operational or denotational semantics are more appropriate.

Comparative Table: The Six Semantics

Semantics	Question asked	Method	Key concept	Example system
Operational	How does it execute?	Transition rules	Configuration, execution step	Interpreters, debuggers
Denotational	What function does it compute?	Mathematical functions	Fixed point, domain	Optimizers, equivalence provers
Axiomatic	What does it guarantee?	Pre/postconditions	Hoare triple, invariant	Formal verification, contracts
Translational	What does it translate into?	Compilation / translation	Commutative diagram	Compilers, transpilers (BP2SC)
Process	How does it interact?	Process algebra	Bisimulation, parallel composition	Network protocols, parallel music
Algebraic	What equations does it satisfy?	Initial algebra	Homomorphism	Abstract types, specification

Deciphering:

These six semantics are not in competition — they illuminate different facets. The same system can be studied from multiple angles: BP3 has an operational semantics (the SOS rules from L6), a translational semantics (BP2SC), and its homomorphisms fall under algebraic semantics. The choice depends on the question asked.

Are the six semantics independent?

No. They form a network of formal relations, not a catalog of isolated methods. Here are the main connections:

                    Operational
                   (how it runs)
                    /       |       \
          [SOS]   /  [adequacy] |        \ [SOS]
                 /          |         \
         Process    Denotational   Translational
        (interactions)  (what fct)    (what it compiles to)
                 \          |         /
        [traces]  \  [initial] |        / [target]
                   \        |       /
                    Algebraic    Axiomatic
                   (equations)   (properties)

Formal links:

Operational ↔ Denotational — the adequacy theorem. If two programs have the same denotation (the same mathematical function), they have the same operational behavior (the same execution steps lead to the same result). This theorem guarantees that the “abstract” (denotational) view and the “concrete” (operational) view are consistent. The inverse question — full abstraction (does denotational semantics distinguish exactly the same programs as operational, no more, no less?) — is a famous open problem, solved for some languages only.

Translational → Operational — compiler correctness. The Morris diagram (seen above) formalizes this relationship: compiling then executing the target must yield the same result as executing the source directly. Translational semantics relies on the semantics of the target language — which can be operational, denotational, or itself translational (translations can be chained: BP3 → SuperCollider → audio code).

Process → Operational — SOS rules. Process algebras (CCS, CSP) use SOS rules (structural operational semantics, see L6) to define their transitions. Bisimulation is then defined on top of this transition system. In this sense, process semantics is built above operational semantics.

Algebraic ↔ Denotational — the initial homomorphism. The unique homomorphism from the initial algebra (the AST) to an interpretation domain is a denotational semantics. The two approaches converge: defining meaning by a mathematical function (denotational) or by the unique morphism from the syntax (algebraic) often amounts to the same thing.

Axiomatic ↔ Operational — correctness of rules. Hoare triples {P} C {Q} ( see [[L8_Semantique_Axiomatique|L8)] ) are proven correct with respect to operational semantics: if {P} C {Q} is valid, then any execution of C starting in a state satisfying P terminates in a state satisfying Q. Axiomatic semantics abstracts operational behavior into verifiable properties.

Deciphering:

This network of relations means that one does not choose a semantics “at random” — each approach illuminates a facet, and connection theorems guarantee consistency between the facets. For BP3, for example: the SOS rules from L6 define the operational semantics, BP2SC defines the translational semantics, and the theorem we would like to prove (but which runs into the absence of a formal specification for SuperCollider — see C5) is precisely compiler correctness: that the Morris diagram commutes for BP2SC.

Key Takeaways

The three classical semantics don’t cover everything. Translation, concurrency, and abstract types require specific tools that operational, denotational, and axiomatic semantics do not directly provide.
Translational semantics defines the meaning of a program by its translation into a target language. Every compiler is a translational semantics — including GCC, javac, tsc, and BP2SC.
The Morris diagram formalizes compiler correctness: the diagram must commute (interpret the source = compile then interpret the target). CompCert proved this commutation for a complete C compiler.
Tree transducers are the machines that perform translation: they transform the source AST into the target AST, node by node, and form the theoretical basis of compilation.
Process semantics (CCS, CSP) models programs as communicating processes. Meaning lies in interaction, not in isolated computation.
Bisimulation is the correct criterion for equivalence between processes: finer than trace equivalence, it captures the branching structure (when choices are made, not just what results are possible).
Algebraic semantics gives meaning through equations. ASTs are initial algebras, and semantics is the unique homomorphism to an interpretation domain.
These six semantics are interconnected: translational relies on the target language’s semantics, process semantics uses SOS rules, and algebraic semantics joins denotational via homomorphisms.
BP2SC concretely illustrates translational semantics: the meaning of a BP3 grammar is the SuperCollider pattern it produces — the first case of formalized translational semantics for a musical notation language.

Glossary

Initial algebra: an algebra from which there is a unique homomorphism to any other algebra of the same signature. A language’s AST is an initial algebra: there is only one way to interpret it in a given semantic domain.
Bisimulation: a relation between two processes such that at each step, any action of one can be mimicked by the other, and vice versa. Finer than trace equivalence: it takes into account the branching structure.
CCS (Calculus of Communicating Systems): process algebra introduced by Robin Milner (1980). Operators: prefix (a.P), choice (P + Q), parallel (P | Q), restriction ((new a) P).
Parallel composition: operator P | Q that executes P and Q simultaneously. Processes can synchronize on common actions.
Compiler correctness: property stating that compilation preserves meaning. Formally: the Morris diagram commutes.
CSP (Communicating Sequential Processes): process algebra introduced by Tony Hoare (1985). Synchronization on shared events, with three semantic levels (traces, failures, failures-divergences).
Commutative diagram: a diagram where all paths between two points yield the same result. For a compiler: interpret the source = compile then interpret the target.
Homomorphism: a function between two algebraic structures that preserves operations. If f is a homomorphism, then f(a + b) = f(a) + f(b).
Process: in process algebra, an entity that performs actions and can interact with other processes. A process is defined by its observable behavior.
Translational semantics: semantics that defines the meaning of a program by its translation into a target language. The meaning of P is the meaning of T(P) in the target language.
Trace: a sequence of observable events produced by a process. The set of traces of a process is the simplest semantic model in CSP.
Transducer: a machine that transforms an input into an output. An FST transforms strings; a tree transducer transforms trees (ASTs). Compilers are tree transducers.

Prerequisites: L5, L6, L8 (for CSP/Hoare context)
Reading time: 15 min
Tags: #translational-semantics #process-semantics #process-algebra #bisimulation #compilation

Previous article: L8
Series L: for application to BP3, see B7 (translational semantics in action)