L11) Au-delà des trois sémantiques

Traduction, processus et algèbre

Dans L5, nous avons décrit trois façons de donner du sens à un programme : opérationnelle, dénotationnelle, axiomatique. Mais le monde réel a besoin de plus. Comment donner un sens à un compilateur ? À deux processus qui s’exécutent en parallèle ? À un type de données défini par ses équations ? Trois familles de sémantiques répondent à ces questions — et elles sont loin d’être exotiques.

Où se situe cet article ?

Cet article prolonge la trilogie sémantique de la série L :

Opérationnelle : « comment ça s’exécute » — approfondie dans L6) SOS
Dénotationnelle : « quelle fonction mathématique ça calcule » — approfondie dans L7) Sémantique dénotationnelle
Axiomatique : « quelles propriétés ça garantit » — approfondie dans L8) Sémantique axiomatique

L5 à L8 ont couvert les trois piliers historiques. Mais dans la pratique, de nombreux systèmes ne rentrent pas bien dans ces trois cadres : les compilateurs définissent le sens d’un langage en le traduisant vers un autre ; les systèmes concurrents (serveurs web, orchestres, réseaux) ont besoin d’outils pour raisonner sur le parallélisme ; et les types abstraits de données se décrivent naturellement par des équations algébriques.

L11 explore ces trois extensions. Chacune répond à une question que les trois sémantiques classiques laissent ouverte.

Pourquoi c’est important ?

Chaque compilateur est une sémantique traductionnelle incarnée. Quand vous écrivez du TypeScript, son sens est ce en quoi il se compile (JavaScript). Quand BP2SC traduit une grammaire BP3 en patterns SuperCollider, il définit une sémantique traductionnelle pour BP3.
Les systèmes concurrents sont partout : chaque serveur web, chaque interface réactive, chaque partition orchestrale implique des processus qui s’exécutent en parallèle et se synchronisent. La sémantique de processus fournit le vocabulaire pour en parler rigoureusement.
Les types abstraits de données (piles, files, dictionnaires) sont omniprésents en programmation. La sémantique algébrique donne un cadre pour les spécifier par leurs propriétés, indépendamment de toute implémentation.

Ce ne sont pas des curiosités académiques. Ce sont les outils que les informaticiens utilisent vraiment — souvent sans savoir qu’ils font de la sémantique.

L’idée en une phrase

Au-delà des trois sémantiques classiques, on peut donner du sens à un programme par ce en quoi on le traduit (sémantique traductionnelle), par ses interactions avec d’autres processus (sémantique de processus), ou par les équations que ses opérations satisfont (sémantique algébrique).

La sémantique traductionnelle

Le sens par la traduction

L’idée fondatrice est désarmante de simplicité : le sens d’un programme P, c’est le sens de sa traduction T(P).

On ne définit pas directement ce que P « signifie ». On le traduit vers un langage cible dont la sémantique est déjà connue, et on dit : « le sens de P est le sens de T(P) dans le langage cible. »

Analogie :

Imaginez un poème en japonais. Vous ne parlez pas japonais, mais vous avez une traduction en français. Pour vous, le sens du poème japonais est sa traduction française. Bien sûr, quelque chose se perd peut-être en traduction — et c’est exactement le type de question que la sémantique traductionnelle force à poser : la traduction préserve-t-elle tout le sens ?

C’est exactement ce que fait un compilateur. TypeScript n’a pas de sémantique formelle indépendante ; son sens est défini par sa compilation vers JavaScript. Le langage C, dans la pratique, est défini par ce que GCC ou Clang en font. Chaque transpileur (compilateur source-à-source, qui traduit un langage de haut niveau vers un autre langage de haut niveau, par opposition à un compilateur classique qui cible du code machine), chaque compilateur, chaque traducteur est une sémantique traductionnelle.

La différence avec les autres sémantiques est structurelle : la sémantique opérationnelle dit « voici les pas d’exécution », la dénotationnelle dit « voici la fonction calculée », l’axiomatique dit « voici les propriétés garanties ». La sémantique traductionnelle dit : « voici un programme équivalent dans un autre langage — allez demander à ce langage ce que ça veut dire. »

C’est une définition indirecte, et elle soulève immédiatement une question : le langage cible a-t-il lui-même une sémantique bien définie ? Si oui, la chaîne est solide. Si non, on construit sur du sable.

Décryptage :

Le terme technique est translational semantics en anglais. On parle aussi parfois de compilational semantics quand la traduction est une compilation. Le point clé : la sémantique est indirecte — elle passe par un intermédiaire. Cette indirection n’est pas un défaut : c’est exactement ce que font tous les compilateurs en pratique.

Le diagramme de Morris (1973)

En 1973, James Morris a formalisé l’idée avec un diagramme devenu classique :

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

Décryptage :

La flèche du haut (compile) traduit le programme source en programme cible

Les flèches verticales (meaning_S, meaning_T) donnent la sémantique de chaque programme dans son langage respectif

La double ligne du bas ( ==== ) affirme que les deux valeurs sémantiques sont équivalentes

Ce diagramme doit commuter : que l’on passe par le chemin « compiler puis interpréter le cible » ou par le chemin « interpréter directement le source », on doit obtenir le même résultat. Un compilateur correct est un compilateur qui fait commuter ce diagramme.

C’est un test puissant. Si votre compilateur produit un programme cible dont le comportement diffère de ce que le programme source est censé faire, le diagramme ne commute pas : le compilateur est incorrect.

Le projet CompCert (Leroy, 2006) a réussi l’exploit de prouver formellement en Coq (un assistant de preuve : un logiciel qui vérifie mécaniquement que chaque étape d’un raisonnement mathématique est correcte, éliminant toute possibilité d’erreur humaine dans la démonstration) que le diagramme de Morris commute pour un compilateur C complet. C’est l’une des plus grandes réalisations de la vérification formelle appliquée : un compilateur dont chaque passe de traduction est mathématiquement garantie de préserver le sens du programme source.

Transducteurs : les machines qui traduisent

Si la sémantique traductionnelle est « le sens par la traduction », une question naturelle se pose : quelles machines effectuent cette traduction ? La théorie des transducteurs y répond.

Transducteurs à états finis (Finite State Transducers, FST) :
Un FST lit un mot d’entrée et produit un mot de sortie, lettre par lettre. C’est un automate fini enrichi d’une sortie : à chaque transition, il consomme un symbole d’entrée et émet un symbole de sortie.

Les FST sont utilisés en traitement du langage naturel (morphologie, phonologie) et en synthèse vocale. Mais ils sont trop faibles pour la compilation : ils ne gèrent pas les structures récursives (parenthèses imbriquées, blocs emboîtés). Un FST ne peut pas « compter » les niveaux d’imbrication — exactement la même limitation que les langages réguliers par rapport aux langages hors-contexte (cf. la hiérarchie de Chomsky dans L1).

Transducteurs d’arbres (tree transducers) :
Un programme n’est pas une chaîne de caractères — c’est un arbre (l’AST, abstract syntax tree). Les transducteurs d’arbres transforment un arbre en un autre arbre, noeud par noeud. C’est exactement ce que fait un compilateur : il prend l’AST du programme source et produit l’AST du programme cible.

Il existe une hiérarchie de puissance :

FST  ⊂  top-down tree  ⊂  macro tree transducers

FST : chaîne vers chaîne, pas de récursion
Transducteurs d’arbres descendants (top-down) : traitent l’arbre de la racine vers les feuilles, un noeud à la fois
Macro tree transducers : peuvent accumuler des paramètres pendant la descente, ce qui les rend assez puissants pour modéliser la plupart des passes de compilation réelles

Décryptage :

Pourquoi les arbres ? Parce que la traduction d’un if-then-else ne dépend pas seulement des mots-clés — elle dépend de la structure : le then est un sous-arbre, le else en est un autre. Un transducteur d’arbre capture naturellement cette structure hiérarchique.

Un mot sur l’Action Semantics (Mosses, 1992) :

Peter Mosses a poussé l’idée traductionnelle plus loin avec l’Action Semantics. Au lieu de traduire un programme vers un langage cible existant, on le traduit vers un langage intermédiaire universel composé d' »actions » : giving (produire une valeur), binding (lier un nom), storing (modifier la mémoire), communicating (envoyer un message). Ces actions se composent avec des combinateurs modulaires. L’avantage : ajouter une nouvelle construction au langage source ne force pas à réécrire les règles existantes. C’est la sémantique traductionnelle la plus modulaire qui existe.

Application : BP2SC, le premier transpileur musical formalisé

Le projet BP2SC traduit des grammaires BP3 (notation musicale formelle) en patterns SuperCollider (langage de synthèse sonore). C’est un cas concret de sémantique traductionnelle :

Source : l’AST d’une grammaire BP3 (25 types de noeuds : Sequence, Polymetric, Sound, Duration, etc.)
Cible : des expressions SuperCollider (Pbind, Pseq, Ppar, etc.)
Règles de traduction : chaque type de noeud a une règle qui le transforme en son équivalent SuperCollider

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

Le diagramme de Morris s’applique directement : une grammaire BP3 et le pattern SuperCollider qu’elle produit doivent donner la « même musique ».

Mais il y a un problème fondamental : SuperCollider n’a pas de spécification formelle. La sémantique du langage cible est définie par son implémentation (l’interpréteur sclang), pas par un document mathématique. Le diagramme ne peut commuter que conditionnellement — sous l’hypothèse que l’interpréteur SuperCollider fait ce qu’on croit qu’il fait.

Décryptage :

C’est un problème courant en pratique. La sémantique traductionnelle de TypeScript repose sur la sémantique de JavaScript, qui est elle-même définie par la spécification ECMAScript — un document de 800 pages. Mais pour BP2SC, il n’existe aucune spécification équivalente pour SuperCollider. La correction du transpileur est donc relative à l’implémentation, pas à une spécification. Avant BP2SC, aucun langage de notation musicale n’avait reçu de sémantique traductionnelle formalisée.

La sémantique de processus

Le sens par la concurrence

Les trois sémantiques classiques (et même la sémantique traductionnelle) supposent un monde séquentiel : un programme, une exécution, pas à pas. Mais le monde réel est concurrent. Un serveur web traite des centaines de requêtes en parallèle. Un orchestre de 80 musiciens joue simultanément. Un système d’exploitation gère des dizaines de processus qui partagent des ressources.

La sémantique de processus (process semantics) modélise les programmes comme des processus qui communiquent. Le sens d’un système n’est pas ce qu’il calcule, mais comment ses composants interagissent.

Analogie :

Imaginez un orchestre. Chaque musicien est un processus : il suit sa partition de manière autonome. Mais à certains moments — les temps forts, les reprises, les cadences — les musiciens doivent se synchroniser. Le chef d’orchestre est un canal de communication. Le sens de la symphonie n’est pas dans les partitions individuelles, mais dans l’interaction entre tous les musiciens.

CCS (Milner, 1980)

Le Calculus of Communicating Systems (CCS), inventé par Robin Milner, est le premier formalisme majeur pour les processus concurrents.

Les ingrédients de base :

Processus : entités qui effectuent des actions
Actions : a, b, c… (actions observables) et tau (action interne, invisible)
Composition parallèle P | Q : P et Q s’exécutent en même temps
Restriction (new a) P : l’action a est privée à P (invisible de l’extérieur)
Choix P + Q : le processus choisit entre se comporter comme P ou comme Q

Exemple : la machine à café

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

Décryptage :

Machine : attend une pièce (coin), sert un café (coffee), puis recommence

User : insère une pièce, prend un café, s’arrête (nil)

System : les deux en parallèle — ils se synchronisent sur coin et coffee

Le point . signifie « puis » (séquencement)

Lecture : La machine et l’utilisateur interagissent via les actions partagées coin et coffee. L’utilisateur insère une pièce, la machine la reçoit ; la machine sert un café, l’utilisateur le prend. L’interaction est la sémantique.

Le CCS a une élégance minimaliste : avec seulement cinq opérateurs (préfixe, choix, parallèle, restriction, renommage), on peut modéliser une variété surprenante de systèmes concurrents.

Le CCS a sa propre sémantique opérationnelle (des règles SOS — Structural Operational Semantics, sémantique opérationnelle structurelle — comme dans L6). Par exemple, la règle de synchronisation :

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

Décryptage :

Quand P peut effectuer l’action a et Q peut effectuer l’action complémentaire a̅ (la « réception » de a), les deux processus se synchronisent. L’action résultante est tau — invisible de l’extérieur. C’est un rendez-vous privé entre P et Q. Cette règle est au coeur de toute communication inter-processus en CCS.

Robin Milner a reçu le prix Turing en 1991, en grande partie pour le CCS et ses développements ultérieurs (le pi-calcul (pi-calculus), une extension du CCS qui ajoute la mobilité des canaux de communication — les processus peuvent s’échanger des canaux, pas seulement des messages).

CSP (Hoare, 1985)

Communicating Sequential Processes (CSP), créé par Tony Hoare (le même que la logique de Hoare de L8), est l’autre grand formalisme de la concurrence.

Différence clé avec CCS : en CSP, la synchronisation se fait sur des événements partagés. Si deux processus proposent tous les deux l’événement a, ils doivent le réaliser ensemble — c’est une synchronisation obligatoire. En CCS, la synchronisation est asymétrique (action/co-action) ; en CSP, elle est symétrique (même événement des deux côtés).

CSP a eu un impact industriel considérable : il est utilisé pour vérifier les protocoles de sécurité (TLS, Kerberos), la conception de circuits intégrés, et les systèmes embarqués critiques. L’outil FDR (Failures-Divergences Refinement) permet de vérifier automatiquement qu’un système CSP satisfait sa spécification.

CSP propose trois modèles sémantiques de richesse croissante :

Modèle	Ce qu’il capture	Exemple
Traces	Les séquences d’événements possibles	`{<coin, coffee>, <coin>}`
Échecs (failures)	Les traces + les événements refusés	Distingue un processus bloqué d’un processus qui attend
Échecs-divergences	+ les comportements divergents (boucles infinies)	Détecte les livelocks (blocages actifs : le système tourne en boucle sans jamais progresser)

Décryptage :

Pourquoi trois modèles ? Parce que les traces seules ne suffisent pas à distinguer tous les systèmes. Deux distributeurs qui acceptent les mêmes séquences de pièces et de cafés pourraient se comporter différemment en cas de panne : l’un refuse votre pièce (il est bloqué), l’autre l’accepte et boucle indéfiniment sans servir de café (il diverge). Le modèle des échecs distingue le premier cas ; celui des échecs-divergences distingue le second.

Exemple musical : deux musiciens qui se synchronisent

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

Les deux instruments jouent en parallèle mais se synchronisent sur l’événement downbeat (le temps fort). Entre les temps forts, chacun joue de manière indépendante. C’est exactement le mécanisme de la musique d’ensemble.

Décryptage :

La notation [| {downbeat} |] est l’opérateur de parallélisme alphabétisé de CSP : les deux processus se synchronisent uniquement sur les événements listés dans l’ensemble (ici, {downbeat}). Pour tous les autres événements (melody, chords), chaque processus avance à son rythme. C’est un modèle remarquablement fidèle de ce qui se passe dans un duo musical réel.

Bisimulation : quand deux systèmes se comportent pareil

Une question fondamentale en sémantique de processus : quand peut-on dire que deux systèmes sont équivalents ?

La réponse naïve serait : « quand ils produisent les mêmes séquences d’événements » (équivalence de traces). Mais c’est insuffisant.

Contre-exemple :

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

P : insérez une pièce, puis choisissez entre café et thé
Q : choisissez entre (insérer une pièce puis café) et (insérer une pièce puis thé)

Les deux ont les mêmes traces : {<coin, coffee>, <coin, tea>}. Mais ils sont différents ! Avec P, après avoir inséré la pièce, vous avez encore le choix. Avec Q, le choix a déjà été fait avant l’insertion.

La bisimulation capture cette différence. Deux processus P et Q sont bisimilaires si un observateur externe ne peut les distinguer à aucun moment de l’interaction — pas seulement en regardant les traces complètes, mais aussi la structure de branchement à chaque étape.

Formellement, une bisimulation est une relation R entre processus telle que si (P, Q) appartient à R :

si P peut faire l’action a et devenir P’, alors Q peut faire a et devenir Q’, avec (P’, Q’) dans R
et réciproquement (si Q peut faire a…)

Décryptage :

La bisimulation est plus fine que l’équivalence de traces : elle prend en compte quand les choix sont faits, pas seulement quels résultats sont possibles. Dans l’exemple ci-dessus, P et Q sont trace-équivalents mais pas bisimilaires. Cette distinction a des conséquences pratiques : si vous remplacez un composant P par un composant Q dans un système, et que P et Q ne sont que trace-équivalents (pas bisimilaires), le système global peut se comporter différemment.

Application : la polymétrie comme processus parallèles

En BP3, la construction {voice1, voice2} place deux voix en parallèle. C’est exactement une composition parallèle au sens du CCS ou du CSP :

V1 | V2

Les voix s’exécutent de manière indépendante mais se synchronisent aux frontières de mesure (ou à d’autres points de rendez-vous définis par la grammaire).

En CSP, cela s’exprimerait :

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

Chaque voix peut avoir un nombre de notes différent entre les barres de mesure — c’est la polymétrie. La synchronisation sur barline force les deux voix à se retrouver aux mêmes points structurels, tout en conservant leur indépendance rythmique entre ces points.

Décryptage :

Mark Ross (1995) a proposé MWSCCS (Meije Weighted Synchronous CCS), une extension du CCS avec des poids, pour modéliser la performance musicale. Dans ce cadre, chaque musicien est un processus CCS, les synchronisations représentent les points d’ensemble (temps forts, cadences), et les poids modélisent les nuances dynamiques. La polymétrie de BP3 se prête naturellement à cette modélisation : chaque voix polymétrée est un processus qui émet des événements musicaux (notes, silences) et se synchronise avec les autres voix aux points structurels.

La sémantique algébrique

Le sens par les équations

La sémantique algébrique (algebraic semantics) adopte une perspective radicalement différente : le sens d’un programme — ou d’un type de données — est donné par les équations que ses opérations satisfont.

L’idée fondatrice, due à Goguen, Thatcher, Wagner et Wright (1977), est de voir un AST (abstract syntax tree) comme une algèbre initiale. Dans cette vision, la syntaxe est une algèbre (les constructeurs de l’AST sont les opérations), et la sémantique est l’unique homomorphisme de cette algèbre initiale vers un domaine d’interprétation.

Décryptage :

Un homomorphisme est une fonction qui préserve la structure. Si l’AST dit « addition de 3 et 5 », l’homomorphisme vers les entiers donne 3 + 5 = 8. Si l’AST dit « séquence de do et ré », l’homomorphisme vers les événements MIDI donne la séquence de notes correspondante. Le fait que cet homomorphisme soit unique (grâce à l’initialité) garantit qu’il n’y a qu’une seule façon de donner du sens à chaque programme — ce qui est exactement ce qu’on veut d’une sémantique.

Exemple concret : une pile (stack) peut être spécifiée par des équations algébriques :

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

Ces deux équations sont la sémantique de la pile. On ne dit rien sur l’implémentation (tableau ? liste chaînée ? mémoire contiguë ?). On dit uniquement : push puis pop redonne la pile d’origine, et top après push donne l’élément empilé. Toute implémentation qui satisfait ces équations est correcte.

Ce cadre a un lien direct avec BP3. Les homomorphismes de BP3 (master/slave, les constructions _ho(), _se(), _al()) transforment un objet musical en un autre tout en préservant certaines propriétés structurelles. La sémantique algébrique fournit le vocabulaire pour formaliser cette idée : chaque homomorphisme BP3 est un morphisme d’algèbre, et la correction de la transformation se vérifie par les propriétés algébriques préservées.

Décryptage :

La sémantique algébrique est particulièrement adaptée aux langages déclaratifs (ceux qui décrivent ce que l’on veut obtenir, sans spécifier comment l’obtenir — comme SQL pour les bases de données, ou les grammaires BP3 qui décrivent une structure musicale sans détailler les pas d’exécution). Elle est en revanche moins naturelle pour les langages impératifs (ceux qui décrivent une suite d’instructions pas à pas, comme C ou Python), car ces langages reposent sur des effets de bord — des modifications de l’état du programme (écrire dans une variable, afficher à l’écran, envoyer un message réseau) qui ne se laissent pas facilement capturer par de simples équations.

En résumé : si votre système se définit bien par « faire X puis défaire X redonne l’état initial » (comme pop(push(x, s)) = s), la sémantique algébrique excelle. Si votre système dépend de quand et dans quel ordre les choses se passent, les sémantiques opérationnelle ou dénotationnelle sont plus adaptées.

Tableau comparatif : les six sémantiques

Sémantique	Question posée	Méthode	Concept clé	Exemple de système
Opérationnelle	Comment ça s’exécute ?	Règles de transition	Configuration, pas d’exécution	Interpréteurs, débogueurs
Dénotationnelle	Quelle fonction ça calcule ?	Fonctions mathématiques	Point fixe, domaine	Optimiseurs, prouveurs d’équivalence
Axiomatique	Qu’est-ce que ça garantit ?	Pré/postconditions	Triplet de Hoare, invariant	Vérification formelle, contrats
Traductionnelle	En quoi ça se traduit ?	Compilation / traduction	Diagramme commutatif	Compilateurs, transpileurs (BP2SC)
De processus	Comment ça interagit ?	Algèbre de processus	Bisimulation, composition parallèle	Protocoles réseau, musique parallèle
Algébrique	Quelles équations ça satisfait ?	Algèbre initiale	Homomorphisme	Types abstraits, spécification

Décryptage :

Ces six sémantiques ne sont pas en compétition — elles éclairent des facettes différentes. Un même système peut être étudié sous plusieurs angles : BP3 a une sémantique opérationnelle (les règles SOS de L6), une sémantique traductionnelle (BP2SC), et ses homomorphismes relèvent de la sémantique algébrique. Le choix dépend de la question posée.

Les six sémantiques sont-elles indépendantes ?

Non. Elles forment un réseau de relations formelles, pas un catalogue de méthodes isolées. Voici les connexions principales :

                    Opérationnelle
                   (comment ça tourne)
                    /       |       \
          [SOS]   /  [adéq] |        \ [SOS]
                 /          |         \
         Processus    Dénotationnelle   Traductionnelle
        (interactions)  (quelle fct)    (en quoi ça compile)
                 \          |         /
        [traces]  \  [init] |        / [cible]
                   \        |       /
                    Algébrique    Axiomatique
                   (équations)   (propriétés)

Les liens formels :

Opérationnelle ↔ Dénotationnelle — le théorème d’adéquation. Si deux programmes ont la même dénotation (la même fonction mathématique), ils ont le même comportement opérationnel (les mêmes pas d’exécution mènent au même résultat). Ce théorème garantit que la vue « abstraite » (dénotationnelle) et la vue « concrète » (opérationnelle) sont cohérentes. La question inverse — la full abstraction (est-ce que la sémantique dénotationnelle distingue exactement les mêmes programmes que l’opérationnelle, ni plus ni moins ?) — est un problème ouvert célèbre, résolu pour certains langages seulement.

Traductionnelle → Opérationnelle — la correction de la compilation. Le diagramme de Morris (vu plus haut) formalise cette relation : compiler puis exécuter le cible doit donner le même résultat qu’exécuter directement le source. La sémantique traductionnelle repose sur la sémantique du langage cible — qui peut être opérationnelle, dénotationnelle, ou elle-même traductionnelle (on peut chaîner les traductions : BP3 → SuperCollider → code audio).

Processus → Opérationnelle — les règles SOS. Les algèbres de processus (CCS, CSP) utilisent des règles SOS (sémantique opérationnelle structurelle, voir L6) pour définir leurs transitions. La bisimulation est ensuite définie sur ce système de transitions. En ce sens, la sémantique de processus est construite au-dessus de l’opérationnelle.

Algébrique ↔ Dénotationnelle — l’homomorphisme initial. L’homomorphisme unique depuis l’algèbre initiale (l’AST) vers un domaine d’interprétation est une sémantique dénotationnelle. Les deux approches convergent : définir le sens par une fonction mathématique (dénotationnelle) ou par l’unique morphisme depuis la syntaxe (algébrique) revient souvent au même.

Axiomatique ↔ Opérationnelle — la correction des règles. Les triplets de Hoare {P} C {Q} (voir L8) sont prouvés corrects par rapport à la sémantique opérationnelle : si {P} C {Q} est valide, alors toute exécution de C commençant dans un état satisfaisant P termine dans un état satisfaisant Q. L’axiomatique abstrait le comportement opérationnel en propriétés vérifiables.

Décryptage :

Ce réseau de relations signifie qu’on ne choisit pas une sémantique « au hasard » — chaque approche éclaire une facette, et les théorèmes de connexion garantissent la cohérence entre les facettes. Pour BP3 par exemple : les règles SOS de L6 définissent l’opérationnelle, BP2SC définit la traductionnelle, et le théorème qu’on voudrait prouver (mais qui bute sur l’absence de spécification formelle de SuperCollider — voir C5) est précisément la correction de compilation : que le diagramme de Morris commute pour BP2SC.

Ce qu’il faut retenir

Les trois sémantiques classiques ne couvrent pas tout. La traduction, la concurrence et les types abstraits demandent des outils spécifiques que l’opérationnelle, la dénotationnelle et l’axiomatique ne fournissent pas directement.
La sémantique traductionnelle définit le sens d’un programme par sa traduction vers un langage cible. Tout compilateur est une sémantique traductionnelle — y compris GCC, javac, tsc, et BP2SC.
Le diagramme de Morris formalise la correction d’un compilateur : le diagramme doit commuter (interpréter le source = compiler puis interpréter le cible). CompCert a prouvé cette commutation pour un compilateur C complet.
Les transducteurs d’arbres sont les machines qui réalisent la traduction : ils transforment l’AST source en AST cible, noeud par noeud, et forment la base théorique de la compilation.
La sémantique de processus (CCS, CSP) modélise les programmes comme des processus qui communiquent. Le sens est dans l’interaction, pas dans le calcul isolé.
La bisimulation est le bon critère d’équivalence entre processus : plus fin que l’équivalence de traces, il capture la structure de branchement (quand les choix sont faits, pas seulement quels résultats sont possibles).
La sémantique algébrique donne du sens par les équations. Les AST sont des algèbres initiales, et la sémantique est l’unique homomorphisme vers un domaine d’interprétation.
Ces six sémantiques sont interconnectées : la traductionnelle repose sur la sémantique du langage cible, la sémantique de processus utilise des règles SOS, et l’algébrique rejoint la dénotationnelle via les homomorphismes.
BP2SC illustre concrètement la sémantique traductionnelle : le sens d’une grammaire BP3 est le pattern SuperCollider qu’elle produit — le premier cas de sémantique traductionnelle formalisée pour un langage de notation musicale.

Pour aller plus loin

Morris, J.H. (1973). « Types are not sets. » POPL ’73 (Symposium on Principles of Programming Languages). — Introduit le diagramme commutatif qui formalise la correction des compilateurs.
Milner, R. (1989). Communication and Concurrency. Prentice Hall. — Présentation complète du CCS, des bisimulations et de l’algèbre de processus. Le livre de référence.
Hoare, C.A.R. (1985). Communicating Sequential Processes. Prentice Hall. — Le texte fondateur du CSP, disponible gratuitement en ligne. Élégant et lisible.
Mosses, P.D. (1992). Action Semantics. Cambridge University Press. — Une sémantique traductionnelle modulaire où les programmes sont traduits en « actions » composables. Résout le problème de modularité des sémantiques dénotationnelles.
Goguen, J.A., Thatcher, J.W., Wagner, E.G., Wright, J.B. (1977). « Initial algebra semantics and continuous algebras. » JACM (Journal of the ACM) 24(1). — Le texte fondateur de la sémantique algébrique.
Aho, A.V., Sethi, R., Ullman, J.D. (1986). Compilers: Principles, Techniques, and Tools (le « Dragon Book »). — Le traitement classique de la compilation comme traduction, avec les transducteurs d’arbres.
Ross, M. (1995). « A Formal Computational Model of Music Performance. » — Application de MWSCCS (CCS pondéré) à la modélisation de la performance musicale.

Glossaire

Algèbre initiale : algèbre dont il existe un unique homomorphisme vers toute autre algèbre de même signature. L’AST d’un langage est une algèbre initiale : il existe une seule façon de l’interpréter dans un domaine sémantique donné.
Bisimulation : relation entre deux processus telle qu’à chaque étape, toute action de l’un peut être imitée par l’autre, et réciproquement. Plus fine que l’équivalence de traces : elle prend en compte la structure de branchement.
CCS (Calculus of Communicating Systems) : algèbre de processus introduite par Robin Milner (1980). Opérateurs : préfixe (a.P), choix (P + Q), parallèle (P | Q), restriction ((new a) P).
Composition parallèle : opérateur P | Q qui exécute P et Q simultanément. Les processus peuvent se synchroniser sur des actions communes.
Correction du compilateur : propriété qui affirme que la compilation préserve le sens. Formellement : le diagramme de Morris commute.
CSP (Communicating Sequential Processes) : algèbre de processus introduite par Tony Hoare (1985). Synchronisation sur événements partagés, avec trois niveaux sémantiques (traces, échecs, échecs-divergences).
Diagramme commutatif : diagramme où tous les chemins entre deux points donnent le même résultat. Pour un compilateur : interpréter le source = compiler puis interpréter le cible.
Homomorphisme : fonction entre deux structures algébriques qui préserve les opérations. Si f est un homomorphisme, alors f(a + b) = f(a) + f(b).
Processus : en algèbre de processus, entité qui effectue des actions et peut interagir avec d’autres processus. Un processus est défini par son comportement observable.
Sémantique traductionnelle (translational semantics) : sémantique qui définit le sens d’un programme par sa traduction vers un langage cible. Le sens de P est le sens de T(P) dans le langage cible.
Trace : séquence d’événements observables produite par un processus. L’ensemble des traces d’un processus est le modèle sémantique le plus simple en CSP.
Transducteur : machine qui transforme une entrée en une sortie. Un FST transforme des chaînes ; un transducteur d’arbre transforme des arbres (AST). Les compilateurs sont des transducteurs d’arbres.

Prérequis : Les trois sémantiques, SOS, Sémantique axiomatique (pour le contexte CSP/Hoare)
Temps de lecture : 15 min
Tags : #semantique-traductionnelle #semantique-processus #algebre-processus #bisimulation #compilation

Article précédent : L8) Sémantique axiomatique
Série L : pour l’application à BP3, voir B7) Le transpileur BP2SC (sémantique traductionnelle en action)