L7) Sémantique dénotationnelle

Quand un programme devient une fonction

Et si un programme n’était rien d’autre qu’une fonction mathématique déguisée ? Cette idée audacieuse est au cœur de la sémantique dénotationnelle.

Où se situe cet article ?

Dans L5, nous avons vu trois approches pour donner du sens à un programme. La L6 (SOS, Structural Operational Semantics) décrit comment ça s’exécute. La sémantique dénotationnelle décrit quoi — quelle fonction mathématique le programme calcule. C’est le sujet de cet article.

Pourquoi c’est important ?

La sémantique opérationnelle (SOS) décrit comment un programme s’exécute. C’est précis, utile pour implémenter un interpréteur, mais parfois trop détaillé. On veut savoir ce que fait le programme, pas comment il le fait.

La sémantique dénotationnelle prend le problème sous un autre angle : elle associe à chaque programme une fonction mathématique. Deux programmes sont équivalents si et seulement si ils dénotent la même fonction. C’est une vision plus abstraite, plus mathématique, qui permet de raisonner sur l’équivalence et l’optimisation.

Pour BP3 (Bol Processor 3, un langage de grammaires musicales, voir I2), cette approche est intéressante mais limitée : la stochasticité (comportement régi par des probabilités) et les effets de bord (modifications d’état, entrées/sorties, ou tout ce qui dépasse le simple calcul d’une valeur) compliquent la définition des fonctions. Comprendre pourquoi nous aide à mieux cerner les forces et faiblesses de chaque approche sémantique.

L’idée en une phrase

La sémantique dénotationnelle interprète chaque construction du langage comme une fonction mathématique, transformant la question « que fait ce programme ? » en « quelle fonction est-ce ? »

Expliquons pas à pas

Exemple 1 : Expressions arithmétiques

Commençons par un exemple simple : les expressions arithmétiques.

Syntaxe :

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

Domaine sémantique :

Valeurs = Entiers
Environnement = Variables → Entiers

La fonction de dénotation · :

On définit e comme une fonction qui prend un environnement et retourne un entier.

n : Env → Int
n(ρ) = n

x : Env → Int
x(ρ) = ρ(x)

e₁ + e₂ : Env → Int
e₁ + e₂(ρ) = e₁(ρ) + e₂(ρ)

e₁ * e₂ : Env → Int
e₁ * e₂(ρ) = e₁(ρ) × e₂(ρ)

Décryptage complet de ces notations :

La notation · (doubles crochets) :

Se lit « la dénotation de » ou « la signification mathématique de »

C’est une fonction qui transforme la syntaxe (le texte du programme) en sémantique (sa signification mathématique)

e = « ce que l’expression e signifie vraiment »

La notation Env → Int :

Se lit « fonction de Env vers Int »

Env (Environnement) = l’ensemble des associations variables-valeurs

Int = l’ensemble des entiers

Env → Int = « une fonction qui prend un environnement et retourne un entier »

La lettre ρ (rho) :

Représente un environnement concret (un dictionnaire variable → valeur)

ρ(x) = « la valeur de x dans l’environnement ρ »

Exemple : si ρ = {x ↦ 5, y ↦ 10}, alors ρ(x) = 5

Lecture ligne par ligne :

n(ρ) = n : « la dénotation d’un nombre n, dans n’importe quel environnement, est ce nombre lui-même »

x(ρ) = ρ(x) : « la dénotation d’une variable x est sa valeur dans l’environnement »

e₁ + e₂(ρ) = e₁(ρ) + e₂(ρ) : « la dénotation d’une somme est la somme des dénotations »

Exemple concret :

x + 2 * 3({x ↦ 5})
= x({x ↦ 5}) + 2 * 3({x ↦ 5})
= 5 + (2({x ↦ 5}) × 3({x ↦ 5}))
= 5 + (2 × 3)
= 11

Lecture pas à pas de ce calcul :

On veut la dénotation de x + 2 * 3 dans l’environnement où x vaut 5

Par la règle de l’addition, c’est la somme des dénotations de x et de 2 * 3

La dénotation de x dans {x ↦ 5} est 5

La dénotation de 2 * 3 est 2 fois 3 = 6

Donc le résultat final est 5 + 6 = 11

La dénotation est compositionnelle : la signification d’une expression composée dépend uniquement de la signification de ses sous-expressions.

Pourquoi la compositionnalité est-elle importante ?

Imaginez une recette de cuisine. Si vous savez que « faire une pâte brisée » donne une certaine pâte, et que « faire une garniture aux pommes » donne une certaine garniture, alors vous savez ce que donne « tarte aux pommes = pâte brisée + garniture aux pommes » sans avoir besoin de refaire toute la recette. La compositionnalité permet de raisonner sur les parties pour comprendre le tout.

Exemple 2 : Instructions avec état

Passons aux instructions qui modifient l’état.

Syntaxe :

cmd ::= skip | x := e | cmd ; cmd | if b then cmd else cmd

Domaine sémantique :

Une instruction transforme un état en un autre état :

cmd : État → État

Qu’est-ce qu’un domaine sémantique ?

C’est l’espace mathématique dans lequel « vivent » les significations des programmes. Ici, les instructions sont interprétées comme des transformateurs d’état : des fonctions qui prennent un état (la mémoire avant) et retournent un nouvel état (la mémoire après).

Les fonctions de dénotation :

skip : État → État
skip(σ) = σ

x := e : État → État
x := e(σ) = σ[x ↦ e(σ)]

c₁ ; c₂ : État → État
c₁ ; c₂(σ) = c₂(c₁(σ))

if b then c₁ else c₂ : État → État
if b then c₁ else c₂(σ) =
    si b(σ) = vrai  alors c₁(σ)
    sinon c₂(σ)

Décryptage de chaque règle :

skip(σ) = σ : l’instruction « ne rien faire » renvoie l’état inchangé

x := e(σ) = σ[x ↦ e(σ)] :

L’affectation x := e évalue d’abord e (donnant e(σ))

Puis met à jour l’état : σ[x ↦ v] = « σ où x vaut maintenant v »

Exemple : x := 5({x ↦ 0, y ↦ 10}) = {x ↦ 5, y ↦ 10}

c₁ ; c₂(σ) = c₂(c₁(σ)) :

La séquence « c1 puis c2 » exécute d’abord c1 (obtenant un nouvel état)

Puis exécute c2 dans ce nouvel état

C’est une composition de fonctions : (c₂ ∘ c₁)(σ)

if b then c₁ else c₂ : selon la valeur de b, exécute c1 ou c2

On voit que chaque construction syntaxique a une interprétation fonctionnelle directe.

Le défi des boucles : les points fixes

Les boucles posent un problème subtil. Considérons :

while b do c

Intuitivement, c’est équivalent à :

if b then (c ; while b do c) else skip

Mais cette définition est circulaire : while est défini en termes de lui-même.

Solution : l’équation de point fixe

On cherche une fonction F telle que :

while b do c = F

où F satisfait :

F(σ) = si b(σ) alors F(c(σ)) sinon σ

C’est une équation de point fixe : on cherche F tel que F = G(F) pour un certain opérateur G.

Qu’est-ce qu’un point fixe ? Exemples concrets

Un point fixe d’une fonction f est une valeur x telle que f(x) = x (la fonction « ne bouge pas » cette valeur).

Exemples simples :

Pour f(x) = x², les points fixes sont 0 et 1 (car 0² = 0 et 1² = 1)

Pour f(x) = x + 1, il n’y a pas de point fixe (aucun nombre égale son successeur)

Pour un thermostat réglé à 20°C, la température 20°C est un « point fixe » : le système n’a plus besoin de changer

Pour les boucles :
On cherche une fonction F (le comportement de la boucle) telle que « exécuter la boucle une fois de plus ne change rien ». C’est exactement la définition d’un point fixe appliquée aux fonctions.

Le théorème de Kleene garantit que cette équation a une solution (le plus petit point fixe) sous certaines conditions. C’est la base mathématique de la sémantique des boucles.

Pourquoi « le plus petit » point fixe ?

Il peut y avoir plusieurs points fixes. On choisit le plus petit car il correspond au comportement « minimal » : la boucle fait exactement ce qu’elle doit faire, sans inventer de comportement supplémentaire. Pour une boucle infinie, le plus petit point fixe est la fonction « indéfinie partout » (la boucle ne termine jamais).

Intuition : Le point fixe représente « la limite » de :

0 itérations : skip
1 itération : if b then c else skip
2 itérations : if b then (c; if b then c else skip) else skip
…

Les domaines : la fondation mathématique

Pour que les points fixes existent, on a besoin d’une structure mathématique appropriée. C’est le rôle de la théorie des domaines (domain theory).

Idées clés :

Ordre partiel : les valeurs sont ordonnées par « information ». ⊥ (bottom) représente « pas d’information » ou « non-terminaison ».
Chaînes croissantes : si x₀ ⊑ x₁ ⊑ x₂ ⊑ ..., la suite converge vers une limite.
Fonctions continues : les fonctions qui préservent les limites de chaînes.
Théorème du point fixe : toute fonction continue sur un domaine a un plus petit point fixe.

Décryptage des symboles et concepts :

⊥ (bottom, « fond ») : symbole représentant l’absence d’information ou un calcul qui ne termine pas. C’est « moins » que toute autre valeur.

⊑ (ordre partiel) : se lit « est moins défini que » ou « a moins d’information que ». x ⊑ y signifie « y a au moins autant d’information que x ».

Exemple : ⊥ ⊑ 5 (ne pas terminer a moins d’information que retourner 5)

Chaîne croissante : une suite où chaque élément a « plus d’information » que le précédent

Exemple : ⊥ ⊑ "programme qui termine en 1 itération" ⊑ "programme qui termine en 2 itérations" ⊑ ...

Fonction continue : une fonction qui « préserve les approximations ». Si on approxime de mieux en mieux l’entrée, la sortie s’approxime de mieux en mieux aussi.

En pratique : Ces détails sont importants pour les théoriciens. Pour les praticiens, l’essentiel est que les boucles et la récursion ont une interprétation mathématique bien définie.

Et BP3 dans tout ça ?

BP3 est un cas intéressant pour la sémantique dénotationnelle. Essayons de définir · pour une grammaire BP3.

Premier essai : grammaires déterministes

Pour le mode ORD (ordonné) sans stochasticité :

S : () → String
S() = Tihai Tihai Tihai()
Tihai() = "dha dhin dhin"

Ça fonctionne : chaque non-terminal (symbole qui peut être réécrit selon les règles de la grammaire, voir L1) dénote une chaîne de symboles.

Le problème : la stochasticité

En mode RND (aléatoire pondéré) avec poids (valeurs numériques déterminant la probabilité de sélection d’une règle) :

<3> Tihai → dha dhin dhin
<2> Tihai → fa sol la

Quelle est la dénotation de Tihai ?

Tihai = ???

Ce n’est pas une chaîne unique mais un ensemble de chaînes possibles avec des probabilités. La dénotation devient :

Tihai : () → Distribution(String)
Tihai() = { "dha dhin dhin" ↦ 0.6, "fa sol la" ↦ 0.4 }

C’est possible mais plus complexe. On entre dans le domaine des monades probabilistes.

Qu’est-ce qu’une distribution de probabilité ?

C’est une fonction qui associe à chaque résultat possible sa probabilité d’occurrence. La somme de toutes les probabilités vaut 1 (100%).

Ici, { "dha dhin dhin" ↦ 0.6, "fa sol la" ↦ 0.4 } signifie :

60% de chances d’obtenir « dha dhin dhin »

40% de chances d’obtenir « fa sol la »

(0.6 + 0.4 = 1, la somme fait bien 100%)

Une monade probabiliste est une structure mathématique qui permet de composer de telles distributions. Si A a une certaine distribution et B aussi, comment calculer la distribution de « A puis B » ? La monade répond à cette question.

Le problème : l’état mutable

Les flags BP3 (variables conditionnelles comme /Ideas=20/, voir B4) ajoutent de l’état :

règle avec /Ideas-1/ : État → Distribution(String × État)

Maintenant la dénotation retourne à la fois une chaîne ET un nouvel état. On a besoin de monades d’état combinées avec les distributions.

Le problème : les poids décrémentaux

Avec <50-12> (poids initial 50 décrémenté de 12 à chaque usage, voir B4), les probabilités changent à chaque utilisation :

Tihai après 3 appels ≠ Tihai après 5 appels

La dénotation dépend de l’historique complet des dérivations passées.

Conclusion pour BP3 :

Une sémantique dénotationnelle de BP3 est possible mais requiert :

Monades probabilistes
Monades d’état
Historique des poids

C’est faisable (les chercheurs l’ont fait pour des langages similaires) mais complexe. La sémantique opérationnelle (SOS) est plus directe et plus pratique pour BP3.

Quand la dénotationnelle brille

Malgré ses limites pour BP3, la sémantique dénotationnelle excelle dans certains contextes :

Contexte	Avantage
Langages fonctionnels purs	Pas d’état, pas d’effets : dénotation directe
Preuves d’équivalence	`P₁ ≡ P₂` ssi `P₁ = P₂`
Optimisation	Si `P' = P`, on peut substituer P’ à P
Définition de types	Les types sont des domaines sémantiques
Fondements théoriques	Liens avec logique, topologie, théorie des catégories

Exemple d’équivalence :

x + 0 = x
x * 1 = x
if true then e₁ else e₂ = e₁

Ces équations sont des lois que tout interpréteur doit respecter.

Ce qu’il faut retenir

e = la fonction dénotée par e : notation standard pour « la sémantique de ».
Compositionnalité : la signification d’un tout dépend de la signification de ses parties.
Points fixes : solution mathématique pour définir les boucles et la récursion.
Domaines : structures mathématiques qui garantissent l’existence des points fixes.
Limites pour BP3 : la stochasticité, l’état mutable, et les poids dynamiques rendent la sémantique dénotationnelle complexe. La SOS est plus adaptée.
Forces : preuves d’équivalence, optimisation, fondements théoriques solides.

Pour aller plus loin

Livre fondateur : Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory — le classique historique
Introduction moderne : Winskel, The Formal Semantics of Programming Languages — chapitres 5-8
Monades et effets : Moggi, E. (1991). « Notions of Computation and Monads » — comment traiter les effets en sémantique dénotationnelle
Pour les curieux : Tennent, Semantics of Programming Languages — approche pédagogique

Glossaire

Bottom (⊥) : élément minimal d’un domaine, représentant l’absence d’information ou la non-terminaison. Se prononce « bottom » ou « fond ». Exemple : une boucle infinie a pour dénotation ⊥.
Chaîne croissante : suite d’éléments x₀ ⊑ x₁ ⊑ x₂ ⊑ ... où chaque élément a « plus d’information » que le précédent. Utilisée pour construire les points fixes.
Compositionnalité : propriété selon laquelle la signification d’une expression composée dépend uniquement de la signification de ses composants. Permet de raisonner sur les parties pour comprendre le tout.
Dénotation : la valeur mathématique (fonction, ensemble, etc.) associée à une expression. Notée e pour l’expression e.
Distribution de probabilité : fonction associant à chaque résultat possible sa probabilité. La somme des probabilités vaut 1.
Domaine : structure mathématique avec un ordre partiel (⊑) et des propriétés de complétude ; sert d' »espace de valeurs » pour les programmes.
Domaine sémantique : l’espace mathématique dans lequel on interprète les programmes (entiers, fonctions, états…).
Environnement : dictionnaire associant chaque variable à sa valeur. Noté ρ (rho). Exemple : {x ↦ 5, y ↦ 10}.
Fonction continue : fonction qui préserve les limites de chaînes croissantes. Nécessaire pour l’existence des points fixes.
Monade : structure mathématique qui encapsule les effets (état, non-déterminisme, exceptions, probabilités) dans un cadre fonctionnel.
Monade probabiliste : monade permettant de composer des distributions de probabilité.
Ordre partiel (⊑) : relation « est moins défini que » ou « a moins d’information que ». ⊥ ⊑ x pour tout x.
Point fixe : valeur x telle que f(x) = x. Exemples : 0 et 1 sont points fixes de f(x) = x². Utilisé pour définir les boucles et la récursion.
Théorème de Kleene : garantit que toute fonction continue sur un domaine a un plus petit point fixe, obtenu comme limite d’approximations successives.
Transformateur d’état : fonction de type État → État. Une instruction impérative est vue comme un transformateur d’état.
· (doubles crochets) : notation standard pour « la fonction de dénotation ». e se lit « la dénotation de e » ou « ce que e signifie mathématiquement ».
ρ (rho) : lettre grecque conventionnellement utilisée pour représenter un environnement (dictionnaire variable → valeur).
σ (sigma) : lettre grecque conventionnellement utilisée pour représenter un état (mémoire du programme).

Prérequis : L5
Temps de lecture : 8 min
Tags : #semantique-denotationnelle #fonctions #point-fixe #theorie-domaines

Article précédent : L6 — SOS pour les nuls
Pour la pratique, voir : R1 — Le formalisme BP3