L5) Les trois sémantiques

Donner du sens aux langages formels

Quand on dit qu’un programme « fait quelque chose », que veut-on dire exactement ? Qu’il s’exécute étape par étape ? Qu’il calcule une fonction mathématique ? Ou qu’il respecte certaines propriétés ?

Où se situe cet article ?

Cet article fait partie de la série Langages formels (L). Après la syntaxe (CFG L2, EBNF L3, AST L4), il aborde le sens des langages formels à travers trois approches. L’article L6 approfondit l’approche opérationnelle appliquée à BP3.

Pourquoi c’est important ?

Imaginez que vous devez expliquer ce que fait un programme. Vous pourriez :

Simuler son exécution pas à pas, comme un débogueur
Décrire la fonction qu’il calcule, entrées vers sorties
Lister les propriétés qu’il garantit, comme « il ne divise jamais par zéro »

Ces trois approches correspondent à trois familles de sémantiques formelles : opérationnelle, dénotationnelle, et axiomatique. Chacune répond à des questions différentes et s’adapte à des contextes différents.

Pour le projet BP2SC (BP3-to-SuperCollider, voir I2 et I3) — un transpileur (traducteur de code source à code source) qui convertit des grammaires musicales BP3 (le langage du Bol Processor) en patterns (motifs génératifs) SuperCollider (environnement de synthèse sonore) — comprendre ces distinctions est crucial. Comment spécifier qu’une règle stochastique (à comportement aléatoire, probabiliste) « fait ce qu’il faut » quand son résultat change à chaque exécution ? La sémantique opérationnelle nous donne la réponse.

L’idée en une phrase

Les trois sémantiques formelles décrivent le sens d’un programme de trois manières complémentaires : par son exécution (opérationnelle), par la fonction qu’il calcule (dénotationnelle), ou par les propriétés qu’il vérifie (axiomatique).

Expliquons pas à pas

Exemple 1 : Un distributeur de café

Prenons un exemple concret avant d’aborder la musique : un distributeur automatique de café.

Qu’est-ce qu’une fonction mathématique ?

Une fonction est une relation qui associe à chaque entrée exactement une sortie. Par exemple, la fonction « double » associe à chaque nombre son double : double(3) = 6, double(5) = 10. En informatique, on voit souvent un programme comme une fonction : il prend des entrées (données) et produit des sorties (résultats).

Sémantique opérationnelle — « Comment ça marche »

On décrit les transitions du système :

État initial : (attente, 0€)

Insérer 1€ :     (attente, 0€) → (attente, 1€)
Insérer 1€ :     (attente, 1€) → (prêt, 2€)
Appuyer café :   (prêt, 2€)    → (distribution, 0€)
Café servi :     (distribution, 0€) → (attente, 0€)

C’est une description mécaniste : on voit exactement ce qui se passe à chaque étape.

Sémantique dénotationnelle — « Quelle fonction »

On décrit ce que le système calcule :

distributeur : (argent, bouton) → (café | rien)

distributeur(2€, café) = café
distributeur(1€, café) = rien
distributeur(2€, thé)  = thé

Comment lire la notation · (doubles crochets) ?

Les doubles crochets X se lisent « la dénotation de X » ou « ce que X signifie mathématiquement ». C’est la notation standard en sémantique formelle. Ici, distributeur signifie « la fonction mathématique que représente le distributeur ». L’expression distributeur(2€, café) = café se lit : « la fonction dénotée par le distributeur, appliquée aux entrées 2€ et café, donne café en sortie ».

On ignore le « comment » pour se concentrer sur la relation entrée-sortie.

Sémantique axiomatique — « Quelles garanties »

On décrit les invariants du système :

{argent ≥ 2€ ∧ bouton = café}
  appuyer
{café_distribué = vrai ∧ argent = 0€}

Qu’est-ce qu’un triplet de Hoare ?

Un triplet de Hoare est une notation inventée par le logicien britannique Tony Hoare en 1969 pour raisonner formellement sur les programmes. C’est le fondement de la logique de Hoare, utilisée pour prouver qu’un programme fait ce qu’il est censé faire.

Le triplet a la forme {P} C {Q} où :

{P} est la précondition (ce qui doit être vrai avant)

C est la commande ou le programme

{Q} est la postcondition (ce qui sera vrai après)

Comment lire un triplet de Hoare {P} C {Q} ?

Cette notation se lit : « si la propriété P est vraie avant d’exécuter C, alors la propriété Q sera vraie après ». Les accolades {...} encadrent des assertions (des affirmations sur l’état du programme). Ici :

{argent ≥ 2€ ∧ bouton = café} est la précondition : ce qui doit être vrai avant

appuyer est l’action (ou commande)

{café_distribué = vrai ∧ argent = 0€} est la postcondition : ce qui est garanti après

Le symbole ∧ signifie « et » (conjonction logique)

On prouve que si certaines conditions sont remplies avant, d’autres le seront après.

Exemple 2 : Une grammaire musicale BP3

Passons maintenant à la musique algorithmique. Voici une règle BP3 simple :

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

RND[2] indique un mode de dérivation aléatoire (random) avec 2 règles. Les poids <3> et <2> (voir B4) déterminent la probabilité de chaque alternative. Cette grammaire dit : « Motif peut devenir soit do ré mi (poids 3, soit 60 % de chances), soit fa sol la (poids 2, soit 40 %) ».

Sémantique opérationnelle — Les règles SOS de BP3

Qu’est-ce que SOS ?

SOS (Structural Operational Semantics, sémantique opérationnelle structurelle) est un formalisme inventé par Gordon Plotkin en 1981 pour décrire précisément comment un programme s’exécute pas à pas.

L’idée : on définit des règles d’inférence qui décrivent comment l’état du programme évolue à chaque étape. Chaque règle a la forme :
    conditions (ce qui doit être vrai)
    ─────────────────────────────────
    conclusion (ce qui se passe alors)

C’est comme une recette : « si tu es dans cette situation, voici ce qui se passe ensuite ».

On définit des configurations et des transitions :

Configuration C = (σ, φ, t)
- σ (sigma) : chaîne de symboles (ex: "S Motif Motif")
- φ (phi) : état des flags (ex: {Ideas: 20})
- t : temps courant

Transition pour le mode RND :
                    choix aléatoire parmi règles applicables
    ────────────────────────────────────────────────────────
    (σ₁ · Motif · σ₂, φ, t) ⟹ (σ₁ · "do ré mi" · σ₂, φ, t')

Comment lire la notation ⟨e, σ⟩ ⟹ ⟨e', σ'⟩ ?

Cette notation décrit une transition (un pas d’exécution) :

⟨ et ⟩ sont des chevrons qui encadrent une configuration (un instantané de l’état du programme)

e est l’expression ou la chaîne en cours de traitement

σ (sigma) représente l’état : mémoire, variables, flags…

⟹ (flèche double) signifie « se transforme en » ou « se réduit à »

e' et σ' (avec prime) représentent les nouvelles valeurs après le pas d’exécution

Le symbole · représente la concaténation (mise bout à bout) de chaînes

Lecture complète : « la configuration (expression e avec état σ) se transforme en (expression e’ avec état σ’) ».

Chaque dérivation est une séquence de transitions. À chaque pas, on choisit une règle applicable et on l’applique.

Sémantique dénotationnelle — Comment formaliser l’aléa ?

À première vue, on pourrait croire que l’aléa pose un problème : quelle est « la fonction » calculée par une grammaire aléatoire, si la sortie change à chaque exécution ?

En fait, les mathématiques gèrent très bien cette situation. La sémantique probabiliste (un champ établi depuis les années 1980) définit le sens d’un programme stochastique non pas comme une valeur unique, mais comme une distribution de probabilité sur les valeurs possibles.

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

Cette notation se lit : « la dénotation de Motif est une distribution où do ré mi a une probabilité de 3/5 et fa sol la une probabilité de 2/5″.

Ce n’est pas un bidouillage

La sémantique probabiliste est mathématiquement rigoureuse. Elle utilise la théorie des mesures et des espaces de probabilité. Des langages entiers (comme les langages de programmation probabiliste pour le machine learning) sont formalisés ainsi.

Pour BP3, on privilégie cependant la sémantique opérationnelle car elle est plus proche de l’implémentation : on décrit concrètement comment le générateur choisit une règle à chaque étape, plutôt que de raisonner sur des distributions abstraites.

Sémantique axiomatique — Les invariants musicaux

On pourrait spécifier des propriétés :

{poids(règle1) > 0 ∧ poids(règle2) > 0}
  dériver(Motif)
{résultat ∈ {"do ré mi", "fa sol la"}}

Ou des propriétés plus musicales :

{mode = RND}
  dériver_n_fois(Motif, 1000)
{fréquence("do ré mi") ≈ 0.6 ± 0.05}

Tableau comparatif : quand utiliser laquelle ?

Critère	Opérationnelle	Dénotationnelle	Axiomatique
Question	Comment ça s’exécute ?	Quelle fonction ça calcule ?	Quelles propriétés ça garantit ?
Point de vue	Implémenteur	Mathématicien	Vérificateur
Formalisme	Règles de transition	Fonctions, domaines	Pré/post-conditions
Notation	`⟨e, σ⟩ ⟹ ⟨e', σ'⟩`	`e : D → D'`	`{P} C {Q}`
Forces	Proche du code, testable	Compositionnelle*, abstraite	Permet la preuve

\ Compositionnelle signifie que la signification d’un tout dépend uniquement de la signification de ses parties. Comme une recette : le goût du plat final dépend du goût de chaque ingrédient combiné selon les étapes.*
| Faiblesses | Verbeux, bas niveau | Difficile pour les effets | Demande des annotations |
| Idéal pour | Interpréteurs, débogueurs | Optimisation, équivalence | Vérification, contrats |

Les trois approches en pratique

Quand choisir l’opérationnelle ?

Vous implémentez un interpréteur (programme qui exécute du code directement) ou un compilateur (programme qui traduit du code en une autre forme)
Le langage a des effets de bord (état, entrées/sorties)
Vous voulez spécifier le comportement exact pas à pas
Exemple BP2SC : les règles SOS définissent comment dériver une grammaire

Quand choisir la dénotationnelle ?

Vous voulez raisonner sur l’équivalence de programmes
Le langage est purement fonctionnel
Vous cherchez à optimiser (deux programmes = même fonction = on peut substituer)
Exemple : prouver que Pseq([a,b,c], 1) et Pseq([a], 1) ++ Pseq([b,c], 1) sont équivalents en SuperCollider (Pseq = séquence de patterns, ++ = concaténation)

Quand choisir l’axiomatique ?

Vous voulez prouver qu’un programme est correct
Vous utilisez des outils de vérification formelle
Vous spécifiez des contrats (préconditions/postconditions)
Exemple : vérifier qu’une grammaire BP3 termine toujours

Le cas de BP3 : pourquoi l’opérationnelle domine

BP3 est un langage de grammaires stochastiques. Ses caractéristiques rendent la sémantique opérationnelle particulièrement adaptée :

État mutable : les flags (drapeaux conditionnels, voir B4) comme /Ideas=20/ modifient l’état global
Stochasticité : les poids (<3>, <2>, voir B4) introduisent de l’aléatoire
Poids décrémentaux : <50-12> change à chaque utilisation
Temps : les notes ont des durées, le temps avance

La sémantique opérationnelle capture tout cela naturellement via des configurations (σ, φ, t) et des règles de transition.

La sémantique dénotationnelle, elle, devrait modéliser :

Des distributions de probabilité (pas des valeurs simples)
Des transformations d’état (monades en théorie)
Du temps continu

Qu’est-ce qu’une monade ?

Une monade est une structure mathématique qui permet d’encapsuler des « effets » (aléatoire, état, erreurs, entrées/sorties) dans un cadre purement fonctionnel. Imaginez une boîte qui contient non seulement une valeur, mais aussi une « recette » pour gérer les effets de bord. En Haskell, par exemple, IO Int est une monade qui représente « un calcul qui fait des entrées/sorties et retourne un entier ». Pour BP3, on aurait besoin d’une monade combinant probabilités ET état mutable.

C’est faisable mais beaucoup plus complexe.

Un peu d’histoire : d’où viennent ces trois approches ?

La sémantique opérationnelle (années 1960-80)

L’idée de décrire un langage par ses règles d’exécution remonte aux premiers interpréteurs. Mais c’est Gordon Plotkin qui, en 1981, a formalisé l’approche avec la SOS (Structural Operational Semantics). Son idée clé : structurer les règles de manière compositionnelle — le comportement d’une expression composée dépend du comportement de ses parties.

Avant Plotkin, les définitions étaient souvent ad hoc, difficiles à comparer entre langages. Avec la SOS, on dispose d’un cadre unifié, réutilisable, et mathématiquement rigoureux.

La sémantique dénotationnelle (années 1960-70)

Développée principalement par Dana Scott et Christopher Strachey à Oxford, cette approche cherchait à donner une signification mathématique aux programmes, indépendamment de toute machine. L’idée : un programme est une fonction, point final.

Le défi principal était de donner un sens aux boucles et à la récursion. Scott a introduit la théorie des domaines pour résoudre ce problème — une contribution qui lui a valu le prix Turing en 1976.

Qu’est-ce que la théorie des domaines ?

C’est une branche des mathématiques qui fournit un cadre pour parler de « valeurs partiellement définies » et de « calculs qui peuvent ne pas terminer ». Elle définit des structures (appelées domaines) où l’on peut donner un sens aux définitions circulaires comme f(x) = f(x) + 1. Sans cette théorie, impossible de définir mathématiquement ce que signifie une boucle while ou une fonction récursive.

La sémantique axiomatique (années 1960-70)

C.A.R. Hoare a publié en 1969 son article fondateur « An Axiomatic Basis for Computer Programming ». Son idée : au lieu de décrire ce qu’un programme fait, décrire ce qu’il garantit. Les fameux « triplets de Hoare » {P} C {Q} sont nés.

Cette approche a donné naissance à tout le domaine de la vérification formelle : prouver mathématiquement qu’un programme est correct. Des outils comme Coq et Isabelle (assistants de preuve formelle) ou les analyseurs statiques modernes en sont les héritiers directs.

Combinaisons et hybrides

En pratique, on combine souvent les approches :

Sémantique opérationnelle + axiomatique

On peut définir une logique de Hoare au-dessus d’une sémantique opérationnelle. Les règles de Hoare disent : « si la SOS garantit telle transition, alors telle postcondition est vraie ».

C’est la base de la plupart des outils de vérification : ils utilisent la sémantique opérationnelle comme fondation, et construisent des preuves axiomatiques par-dessus.

Correspondance opérationnelle-dénotationnelle

Un résultat important en théorie des langages est la correspondance entre sémantiques : prouver que ⟨e, σ⟩ ⇓ v (opérationnelle ; ⇓ signifie « s’évalue en ») si et seulement si e(σ) = v (dénotationnelle).

Cette correspondance garantit que les deux points de vue sont cohérents — l’un décrit le « comment », l’autre le « quoi », mais ils s’accordent sur le résultat final.

Le cas particulier de la musique algorithmique

Pour BP3 et la musique algorithmique en général, ces trois sémantiques offrent des perspectives complémentaires :

Opérationnelle : comment la grammaire se dérive, pas à pas, pour produire une séquence de notes. C’est ce que fait le moteur de BP3.

Dénotationnelle : quelle distribution de probabilité sur les morceaux possibles est générée. Utile pour l’analyse musicologique (quels motifs sont plus fréquents ?).

Axiomatique : quelles contraintes musicales sont respectées (tessiture — l’étendue des notes jouables —, rythme valide, pas de dissonances interdites…). Utile pour la composition assistée par ordinateur.

Le transpileur BP2SC (voir B7) se concentre sur l’aspect opérationnel : il traduit les règles de dérivation en patterns SuperCollider qui reproduisent le même comportement.

Ce qu’il faut retenir

Sémantique opérationnelle : décrit comment un programme s’exécute, étape par étape. Idéale pour les interpréteurs et les langages avec état.
Sémantique dénotationnelle : décrit quelle fonction un programme calcule. Idéale pour le raisonnement mathématique et l’optimisation.
Sémantique axiomatique : décrit quelles propriétés un programme garantit. Idéale pour la vérification formelle.
Complémentarité : ces trois approches ne s’excluent pas. On peut utiliser l’opérationnelle pour implémenter, la dénotationnelle pour optimiser, et l’axiomatique pour vérifier.
BP3 et l’opérationnelle : pour les grammaires stochastiques avec état comme BP3, la sémantique opérationnelle (SOS) est l’approche la plus naturelle et la plus pratique.

Pour aller plus loin

Livre de référence : Nielson & Nielson, Semantics with Applications: An Appetizer — introduction accessible aux trois sémantiques
Article fondateur SOS : Plotkin, G. (2004). « The Origins of Structural Operational Semantics »
Hoare Logic : Hoare, C.A.R. (1969). « An Axiomatic Basis for Computer Programming » — article fondateur de la sémantique axiomatique
Articles suivants :

– L6 — SOS : la sémantique opérationnelle structurelle (Plotkin)
– L7 — Sémantique dénotationnelle : programmes comme fonctions (Scott-Strachey)
– L8 — Sémantique axiomatique : prouver la correction (Hoare)

Glossaire

Compositionnalité : propriété selon laquelle la signification d’une expression composée dépend uniquement de la signification de ses composants. Exemple : la signification de « 2 + 3 » ne dépend que de la signification de « 2 », de « 3 » et de « + ».
Configuration : état complet d’un programme à un instant donné (expression à évaluer + environnement + mémoire). Notée ⟨e, σ⟩ où e est l’expression et σ l’état.
Domaine sémantique : ensemble mathématique dans lequel on interprète les programmes (entiers, fonctions, distributions…).
Fonction mathématique : relation qui associe à chaque élément d’un ensemble de départ (domaine) exactement un élément d’un ensemble d’arrivée (codomaine). Exemple : f(x) = x + 1 associe à chaque entier son successeur.
Invariant : propriété qui reste vraie tout au long de l’exécution.
Monade : structure mathématique permettant d’encapsuler des effets (état, aléatoire, erreurs) dans un cadre fonctionnel. Utilisée pour modéliser les programmes avec effets de bord en sémantique dénotationnelle.
Notation · : doubles crochets signifiant « la dénotation de » ou « la signification mathématique de ». e se lit « la dénotation de e ».
Point fixe : valeur x telle que f(x) = x. Exemple : 0 est un point fixe de f(x) = x², car f(0) = 0. En sémantique, utilisé pour définir les boucles et la récursion.
Postcondition : propriété garantie après l’exécution d’une instruction.
Précondition : propriété requise avant l’exécution d’une instruction.
Règle d’inférence : schéma de la forme « si ces prémisses sont vraies, alors cette conclusion est vraie ».
Sémantique : étude formelle du sens des programmes.
Stochasticité : caractère aléatoire ou probabiliste d’un processus. Un système stochastique peut produire des résultats différents à chaque exécution.
Théorie des domaines : branche des mathématiques fournissant les structures (domaines ordonnés) nécessaires pour définir la sémantique des boucles et de la récursion.
Transition : passage d’une configuration à une autre lors de l’exécution. Notée ⟨e, σ⟩ ⟹ ⟨e', σ'⟩.
Triplet de Hoare : notation {P} C {Q} signifiant « si P est vrai avant C, alors Q est vrai après ».

Prérequis : L2 — Grammaires context-free
Temps de lecture : 10 min
Tags : #semantique #formalisme #theorie-langages #verification

Articles suivants :

L6 — SOS pour les nuls — sémantique opérationnelle structurelle
L7 — Sémantique dénotationnelle — quand un programme devient une fonction
L8 — Sémantique axiomatique — prouver qu’un programme est correct