L6) SOS pour les nuls

comprendre la sémantique opérationnelle structurelle

Comment décrire précisément ce que fait un programme, étape par étape, sans ambiguïté ? La sémantique opérationnelle structurelle (SOS) répond à cette question avec une élégance mathématique qui a révolutionné la définition des langages de programmation.

Où se situe la SOS ?

Dans L5, nous avons vu trois façons de donner du sens à un programme :

Opérationnelle : « comment ça s’exécute » ← c’est le sujet de cet article
Dénotationnelle : « quelle fonction mathématique ça calcule »
Axiomatique : « quelles propriétés ça garantit »

La SOS (Structural Operational Semantics) est le formalisme le plus répandu de la sémantique opérationnelle. Inventée par Gordon Plotkin en 1981, elle est devenue le standard de facto pour définir les langages de programmation. D’autres approches existent au sein de la sémantique opérationnelle (sémantique naturelle de Kahn, machines abstraites), mais la SOS domine par sa systématicité. Elle utilise l’L4 (AST, Abstract Syntax Tree, arbre de syntaxe abstraite) comme structure de départ et définit des règles pour le transformer pas à pas.

Pourquoi c’est important ?

Quand on écrit un interpréteur ou un compilateur, on a besoin d’une spécification précise du comportement du langage. « L’instruction if exécute le bloc si la condition est vraie » — c’est vague. Que signifie « vraie » ? Que se passe-t-il exactement ? Dans quel ordre ?

La SOS fournit un cadre rigoureux pour répondre à ces questions. Elle décrit l’exécution comme une série de transitions entre configurations, gouvernées par des règles d’inférence.

Pour le projet BP2SC (transpileur de BP3 vers SuperCollider, voir B7), la SOS est particulièrement pertinente : BP3 (Bol Processor 3, voir I2) est un langage de grammaires avec cinq modes d’exécution — ORD (ordonné), RND (aléatoire pondéré), LIN (linéaire), SUB (substitution complète), SUB1 (substitution unique) —, des flags conditionnels, et des poids stochastiques (probabilités associées aux règles). Spécifier tout cela en prose serait un cauchemar. Avec la SOS, chaque comportement devient une règle formelle, testable et non ambiguë.

L’idée en une phrase

La SOS décrit l’exécution d’un programme comme une séquence de transitions entre configurations, où chaque transition est justifiée par une règle d’inférence.

Les trois ingrédients de la SOS

1. Les configurations

Une configuration capture l’état complet du programme à un instant donné. Elle contient typiquement :

L’expression (ou instruction) en cours d’évaluation
L’environnement (liaisons variables-valeurs)
La mémoire (état des variables mutables)
Éventuellement : le temps, les entrées/sorties, etc.

Notation standard :

⟨e, σ⟩

⟨ et ⟩ : chevrons mathématiques délimitant un tuple (un groupe ordonné d’éléments)
e : l’expression à évaluer
σ (sigma, lettre grecque minuscule) : l’état (environnement + mémoire)

Exemple concret :

⟨x + 1, {x ↦ 5}⟩

Lecture complète : « évaluer l’expression x + 1 dans un état où x vaut 5″.

Décryptage de la notation {x ↦ 5} :

Les accolades {...} représentent un ensemble ou un dictionnaire

La flèche ↦ (lue « est associé à » ou « mappe vers ») indique une correspondance

{x ↦ 5} signifie « un état où la variable x est associée à la valeur 5 »

Un état plus complexe : {x ↦ 5, y ↦ 10, compteur ↦ 0}

2. Les transitions

Une transition représente un pas d’exécution : on passe d’une configuration à une autre.

Notation :

⟨e, σ⟩ ⟹ ⟨e', σ'⟩

Décryptage symbole par symbole :

⟨e, σ⟩ : configuration initiale (expression e dans état σ)

⟹ : flèche de transition (lue « se transforme en » ou « se réduit en »)

⟨e', σ'⟩ : configuration résultante

Le prime (apostrophe ') indique « la nouvelle valeur après transformation »

e' (lu « e prime ») = nouvelle expression

σ' (lu « sigma prime ») = nouvel état

Lecture complète : « la configuration (expression e, état sigma) se réduit en un pas vers (expression e prime, état sigma prime) ».

Deux styles de transitions :

Style	Notation	Signification
Small-step	`⟨e, σ⟩ → ⟨e', σ'⟩`	Un seul pas d’exécution
Big-step	`⟨e, σ⟩ ⇓ v`	Évaluation complète jusqu’à une valeur

Analogie : recette de cuisine

Small-step (petits pas) : comme suivre une recette instruction par instruction. « Casser les œufs » → « battre » → « ajouter la farine » → … → plat final. On voit chaque étape.

Big-step (grands pas) : comme dire directement « cette recette donne un gâteau au chocolat ». On ne voit que le résultat final, pas les étapes intermédiaires.

La flèche ⇓ (lue « s’évalue en » ou « donne ») indique une évaluation complète, tandis que → indique un seul micro-pas.

Le small-step est plus détaillé (on voit chaque micro-étape), le big-step plus compact (on saute directement au résultat).

3. Les règles d’inférence

Une règle d’inférence a la forme :

    prémisse₁    prémisse₂    ...
    ─────────────────────────────── (NomRègle)
              conclusion

Elle se lit : « si toutes les prémisses sont vraies, alors la conclusion est vraie ».

Anatomie d’une règle d’inférence :

Ligne horizontale : sépare les hypothèses (en haut) de la conclusion (en bas). Elle représente l’implication logique « si… alors… ».

Prémisses (au-dessus) : conditions qui doivent être satisfaites pour appliquer la règle. Plusieurs prémisses sont implicitement liées par « et ».

Conclusion (en dessous) : ce qu’on peut affirmer si toutes les prémisses sont vraies.

(NomRègle) : étiquette permettant de référencer cette règle.

Indices (₁, ₂) : indices typographiques pour distinguer les éléments. e₁ se lit « e un » ou « e indice 1 ».

Une règle sans prémisse (rien au-dessus de la barre) est un axiome : elle est toujours applicable.

Exemple — Addition :

    ⟨e₁, σ⟩ ⇓ n₁    ⟨e₂, σ⟩ ⇓ n₂
    ───────────────────────────── (Add)
       ⟨e₁ + e₂, σ⟩ ⇓ n₁ + n₂

Décryptage complet de cette règle :

e₁, e₂ : deux expressions quelconques (variables libres de la règle)

n₁, n₂ : les valeurs numériques résultant de l’évaluation

σ : l’état (le même pour les deux sous-expressions)

⇓ : « s’évalue complètement en »

Le + à gauche du ⇓ est l’opérateur syntaxique (dans le programme)

Le + à droite du ⇓ est l’addition mathématique (sur les nombres)

Lecture en français : « Si l’expression e1 s’évalue en n1 dans l’état sigma, ET si l’expression e2 s’évalue en n2 dans ce même état sigma, ALORS l’expression e1 + e2 s’évalue en la somme n1 + n2. »

Expliquons pas à pas

Exemple 1 : Un mini-langage d’expressions

Définissons la SOS d’un langage ultra-simple avec des nombres et des additions et des multiplications.

Syntaxe :

e ::= n | e + e | e * e

Comment lire cette notation BNF (Backus-Naur Form) :

e : nom de la catégorie syntaxique (ici, « expression »)

::= : « est défini comme » ou « peut être »

| : « ou » (séparateur d’alternatives)

n : un nombre littéral (1, 42, -7…)

e + e : une addition de deux expressions

e * e : une multiplication de deux expressions

Lecture : « Une expression (e) est soit un nombre (n), soit une addition (e + e), soit une multiplication (e * e). »
La définition est récursive : une expression peut contenir d’autres expressions.

Configurations :

⟨e⟩  (pas d'état, expressions pures)

Règles (big-step) :

    ───────── (Num)
    ⟨n⟩ ⇓ n


    ⟨e₁⟩ ⇓ n₁    ⟨e₂⟩ ⇓ n₂
    ─────────────────────── (Add)
       ⟨e₁ + e₂⟩ ⇓ n₁ + n₂


    ⟨e₁⟩ ⇓ n₁    ⟨e₂⟩ ⇓ n₂
    ─────────────────────── (Mul)
       ⟨e₁ * e₂⟩ ⇓ n₁ × n₂

Dérivation de (2 + 3) * 4 :

        ⟨2⟩ ⇓ 2    ⟨3⟩ ⇓ 3
        ─────────────────── (Add)
           ⟨2 + 3⟩ ⇓ 5            ⟨4⟩ ⇓ 4
        ─────────────────────────────────── (Mul)
                ⟨(2 + 3) * 4⟩ ⇓ 20

On construit un arbre de dérivation : chaque noeud est une application de règle, les feuilles sont des axiomes (règles sans prémisse comme (Num)).

Application à BP3

La SOS est l’outil idéal pour formaliser les mécanismes de BP3 : cinq modes d’exécution (ORD, RND, LIN, SUB, SUB1), flags conditionnels, poids décrémentaux. Chaque comportement devient une règle d’inférence précise, testable et non ambiguë.

Cette application est détaillée dans la série B :

B3 — Règles de dérivation — formalisation SOS des cinq modes
B4 — Flags et poids décrémentaux — mécanismes transversaux (Flag-Cond, Weight-Dec)
B7 — De BP3 à SuperCollider — traduction des règles SOS en patterns SuperCollider

Structure d’une spécification SOS complète

Une spécification SOS complète pour n’importe quel langage comprend cinq composants :

1. Syntaxe abstraite

La grammaire du langage, typiquement en BNF ou EBNF (Extended BNF, voir L3) :

Programme ::= Instruction+
Instruction ::= Affectation | Boucle | Condition
Expression ::= Nombre | Variable | Expression Op Expression

2. Domaines sémantiques

Les ensembles mathématiques utilisés :

Valeur = Int | Bool | ...
État = Variable → Valeur

3. Configurations

L’état complet du programme à un instant donné :

C = ⟨instruction, état⟩
C_final quand l'instruction est complètement évaluée

4. Relation de transition

⟹ ⊆ C × C

Décryptage : Cette notation mathématique signifie :

⟹ est la relation de transition (l’ensemble de toutes les transitions possibles)

⊆ signifie « est un sous-ensemble de » ou « est inclus dans »

C × C est le produit cartésien de C par lui-même : l’ensemble de tous les couples (configuration avant, configuration après)

Lecture : « La relation de transition est un ensemble de paires de configurations »

5. Règles d’inférence

Les règles qui définissent comment passer d’une configuration à une autre (comme celles vues dans les exemples ci-dessus).

En pratique : Pour voir ces cinq composants appliqués à un langage concret (BP3, un langage de grammaires musicales), consultez la série B, en commençant par B3.

Small-step vs Big-step : quel style choisir ?

Aspect	Small-step	Big-step
Granularité	Une micro-étape	Évaluation complète
Non-terminaison	Détectable (pas de transition)	Invisible (règle inapplicable)
Concurrence	Naturel (entrelacement)	Difficile
Implémentation	Proche d’un interpréteur	Proche d’un évaluateur récursif

Le choix dépend du langage :

Small-step est préférable quand le langage a de l’état mutable, des boucles potentiellement infinies, ou du temps qui avance entre les étapes.
Big-step est plus concis pour les langages purement fonctionnels sans effets de bord.

Propriétés des règles SOS

Les règles SOS bien conçues ont plusieurs propriétés importantes :

Déterminisme (ou non)

Règle déterministe : pour une configuration donnée, au plus une règle s’applique.

Règle non-déterministe : plusieurs règles peuvent s’appliquer (choix libre ou probabiliste).

Un langage peut mélanger les deux : certaines constructions sont déterministes, d’autres introduisent du non-déterminisme (choix, concurrence, stochasticité).

Progression

Propriété de progression : si une configuration n’est pas finale, au moins une règle s’applique.

Sans cette propriété, un programme peut « se bloquer » dans un état non final — un signe d’erreur dans la spécification ou dans le programme.

Terminaison

Question : la dérivation atteint-elle toujours une configuration finale ?

La SOS ne garantit pas la terminaison. Une définition récursive sans condition d’arrêt boucle indéfiniment. C’est au concepteur du langage ou du programme de l’assurer, par exemple en introduisant des compteurs, des conditions de terminaison, ou des mécanismes comme les poids décrémentaux (voir B4).

Confluence

Propriété de confluence : si plusieurs chemins de dérivation sont possibles, ils mènent tous au même résultat final.

Un langage non-déterministe n’est généralement pas confluent : deux exécutions peuvent produire des résultats différents. Selon le contexte, la non-confluence peut être une propriété voulue (concurrence, stochasticité) ou un défaut à corriger.

Ce qu’il faut retenir

Configuration : état complet du programme (expression + environnement + mémoire).
Transition : un pas d’exécution, noté ⟨e, σ⟩ ⟹ ⟨e', σ'⟩.
Règle d’inférence : « si les prémisses sont vraies, la conclusion est vraie ». Prémisses au-dessus, conclusion en dessous.
Compositionnalité : le comportement d’une expression composée dépend du comportement de ses sous-expressions.
Small-step vs big-step : deux styles complémentaires — le small-step pour les détails, le big-step pour la concision.
Propriétés clés : déterminisme, progression, terminaison, confluence — à vérifier pour toute spécification SOS.

Pour aller plus loin

Article fondateur : Plotkin, G. (2004). « A Structural Approach to Operational Semantics ». JLAP.
Livre accessible : Pierce, B. Types and Programming Languages, chapitre 3 — SOS pour un langage simple
Tutoriel pratique : Nielson & Nielson, Semantics with Applications, chapitre 2
Dans cette série : L5 pour le cadre général
Application à BP3 : B3, B4

Glossaire

Axiome : règle d’inférence sans prémisse (conclusion toujours vraie). Exemple : ⟨n⟩ ⇓ n est un axiome car un nombre s’évalue toujours en lui-même.
Big-step : sémantique où une transition (notée ⇓) évalue complètement une expression jusqu’à sa valeur finale.
BNF (Backus-Naur Form) : notation pour décrire la syntaxe d’un langage. e ::= n | e + e signifie « e est soit n, soit e + e ».
Concaténation : mise bout à bout de chaînes. Notée · (point médian). "abc" · "def" = "abcdef".
Configuration : état instantané du programme, noté ⟨e, σ⟩. Contient l’expression en cours et l’état mémoire.
Dérivation : arbre de preuves montrant comment une transition est justifiée par les règles.
Non-terminal : symbole qui peut être réécrit selon les règles de la grammaire. Opposé de terminal.
Prémisse : condition requise pour appliquer une règle (au-dessus de la barre horizontale).
Prime : apostrophe (') indiquant « la nouvelle valeur ». σ' = « sigma prime » = nouvel état.
Produit cartésien : A × B = ensemble de tous les couples (a, b) avec a dans A et b dans B.
Règle d’inférence : schéma logique de la forme « prémisses impliquent conclusion », séparées par une barre horizontale.
Small-step : sémantique où chaque transition (notée →) représente un seul pas d’exécution.
SOS : Structural Operational Semantics — cadre formel introduit par Plotkin en 1981 pour définir les langages de programmation.
Stochastique : qui suit une distribution de probabilité. Un système stochastique peut produire des résultats différents à chaque exécution.
Terminal : symbole qui ne peut plus être réécrit (feuille de la dérivation). Exemple : un nombre, un mot-clé du langage.
Σ (sigma majuscule) : symbole de sommation. Σwᵢ = w₁ + w₂ + … + wₙ.

Prérequis : L5, L4
Temps de lecture : 12 min
Tags : #SOS #semantique-operationnelle #regles-inference #formalisme

Prochain article : L7 — Sémantique dénotationnelle — quand un programme devient une fonction mathématique