Qu'est-ce qui constitue la sémantique dénotationnelle?

Sur un fil différent , Andrej Bauer a défini la sémantique dénotationnelle comme suit:

la signification d'un programme est fonction de la signification de ses parties.

Ce qui me dérange dans cette définition, c'est qu'elle ne semble pas distinguer ce qu'on appelle communément la sémantique dénotationnelle de ce qu'on appelle communément la sémantique non dénotationnelle, à savoir la sémantique opérationnelle structurelle .

Plus précisément, l'ingrédient clé ici est la modularité , ou compositionalité , de la sémantique, ou autrement dit, le fait qu'elles sont définies en fonction de la structure abstraite du programme.

Comme la plupart des sémantiques formelles (toutes?) Ont tendance à être structurelles, est-ce la définition requise?

Ma question est donc la suivante: qu’est-ce que la sémantique dénotationnelle?

La distinction que je fais personnellement entre la sémantique dénotationnelle et opérationnelle ressemble à ceci:

• la sémantique dénotationnelle est mathématique et équationnelle. Les détails de la réduction importent moins que le résultat final, ce qui est une valeur intemporelle dans un espace mathématique.
• la sémantique opérationnelle est algorithmique. Il se déroule par étapes individuelles dans le temps. Le processus fait partie du sens, et le résultat final n’est qu’une étape distinguée de ce processus.

La différence peut parfois être assez subtile et il peut être difficile de dire si c'est simplement une différence de style ou de substance.

Cependant, nous pouvons voir comment la définition compositionnelle d'Andrej découle plus naturellement de la définition dénotationnelle, et nous pouvons également facilement imaginer une sémantique non confluente, non compositionnelle qui répond toujours à la définition opérationnelle.

Si je devais deviner ce que Dana Scott dirait, il dirait probablement que la sémantique dénotationnelle est compositionnelle (comme ce que j'ai affirmé) et que la signification d'un programme doit être un véritable objet mathématique, et non une entité syntaxique ou formaliste. Bien entendu, une telle vision nécessite de distinguer la manipulation formelle de la syntaxe des "vraies" mathématiques. Ceci est nécessairement une distinction non mathématique.

Après coup, on voudrait probablement que le sens soit adéquat en ce sens que deux programmes différents sur le plan de l’observation ne reçoivent pas le même sens. Bien entendu, une telle adéquation dépend de ce que l’on appelle «observation».

Selon ce point de vue, on pourrait faire valoir que la sémantique opérationnelle structurelle n'est pas une sémantique dénotationnelle, car elle assimile la signification d'une entité syntaxique à une autre entité syntaxique (une valeur ou une séquence de réduction).

Je conviens que l'identification par A. Bauer de la sémantique dénotationnelle avec la compositionnalité (dans Books on Programming sémantique des langages de programmation ) ne caractérise pas vraiment ce que l'on entend traditionnellement par sémantique dénotationnelle, car la sémantique clairement opérationnelle ainsi que la logique de programme (sémantique axiomatique) sont compositionnelles. .

Je pense que le terme est mieux compris du point de vue socio-historique, car il renvoie vaguement à une certaine tradition théorique (commencée sérieusement lorsque Scott produisit un modèle théorique sur réseau du lambda-calcul non typé) avec certains outils préférés (théorie de l'ordre, théorèmes du point fixe). , topologie, théorie des catégories) et les langues cibles préférées (purement fonctionnelles et séquentielles). J'imagine que - hormis l'intérêt intellectuel pur - la sémantique dénotationnelle a été principalement inventée pour les raisons suivantes:

1. Auparavant, il était difficile de raisonner sur la sémantique opérationnelle.

2. Auparavant, il était difficile de donner une sémantique axiomantique à des langages non triviaux.

$\pi$

Donc, en résumé, je dirais que le terme "sémantique dénotationnelle" est devenu moins précis et donc moins utile. Il pourrait être utile que la communauté sémantique converge vers une meilleure terminologie.

Je suis content de la réponse d'Adrej, mais j'aimerais approfondir davantage.

Pour commencer, la sémantique dénotationnelle veut dire quelque chose comme "le sens de cette notation est que". Un vrai sémanticiste voudrait imaginer que les significations sont ce qui existe dans notre esprit et que les notations ne sont qu'un moyen d’exprimer ces significations. Il en découle l'exigence selon laquelle la sémantique dénotationnelle doit être compositionnelle. Si les significations sont primaires et les notations secondaires, nous n'avons pas d'autre choix que de définir les significations des plus grandes notations en tant que fonctions des significations de leurs constituants.

Si nous acceptons ce point de vue, une bonne sémantique dénotationnelle doit capturer les significations que nous supposons avoir dans notre esprit. Toute sémantique de composition ne conviendrait pas nécessairement. Si je propose une définition sémantique compositionnelle et que personne ne s'accorde pour dire que cela indique le sens qu'ils ont en tête, alors cela ne sert à rien. La sémantique des jeux est actuellement dans cette situation. C'est une définition de la composition et techniquement assez forte, mais très peu de gens s'accordent pour dire que cela a quelque chose à voir avec les significations qu'ils ont à l'esprit.

Cela dit, toute définition de la composition présente divers avantages techniques. Nous pouvons l'utiliser pour vérifier des équivalences ou d'autres propriétés par induction sur la syntaxe des termes. Nous pouvons l'utiliser pour vérifier la validité des systèmes de preuve, encore une fois par induction sur la syntaxe des termes. Nous pouvons vérifier l'exactitude des compilateurs ou des techniques d'analyse de programme (qui, de par leur nature, sont définies par induction sur la syntaxe). Une définition sémantique totalement abstraite présente des avantages encore plus techniques. Vous pouvez l'utiliser pour montrer que deux programmes ne sont pas équivalents, ce que vous ne pouvez pas faire avec une sémantique de composition arbitraire. Une définition sémantique entièrement définissable est encore meilleure. Ici, les domaines sémantiques ont exactement ce que vous pouvez exprimer dans le langage de programmation (avec quelques réserves). Vous pouvez donc énumérer les valeurs dans les domaines pour voir quelles sont les valeurs, ce qui serait difficile à faire avec les notations syntaxiques. Sur tous ces terrains, la sémantique des jeux marque des points.

Cependant, les définitions sémantiques compositionnelles ont perdu leur avantage au fil des ans. Robin Milner et Andy Pitts ont mis au point un certain nombre de techniques de " raisonnement opérationnel ", qui fonctionnent uniquement sur la syntaxe, mais utilisent la sémantique opérationnelle chaque fois que cela est nécessaire pour parler du comportement. Ces techniques de raisonnement opérationnel sont peu techniques. Pas de mathématiques sophistiquées. Pas d'objets infinis. Nous pouvons leur apprendre aux étudiants de premier cycle et n'importe qui peut les utiliser. Ainsi, beaucoup de gens se demandent pourquoi nous avons besoin de la sémantique dénotationnelle. (Martin Berger est probablement dans ce camp.)

Personnellement, je n'ai aucun problème à avoir beaucoup d'outils dans ma boîte à outils. Les techniques de dénotation peuvent donner de meilleurs résultats pour certains problèmes et les techniques opérationnelles pour d'autres. Les chercheurs qui développent la théorie pourraient être mieux adaptés à l'une ou l'autre approche. Assez souvent, nous pouvons développer les connaissances dans une approche et transférer ces informations dans une autre approche. (Une grande partie du travail d’Andy Pitts est de ce type. La paramétrie relationnelle s’est développée dans un contexte dénotationnel, mais il est capable de trouver un moyen de le reformuler en tant que raisonnement opérationnel. Quand je le regarde, je dis pensait que cela serait possible. "La logique de séparation va également dans ce sens. Steve Brookes a donné une preuve de fiabilité de 60 pages pour la logique de séparation simultanée en utilisant une sémantique dénotationnelle.

Les approches opérationnelles se démarquent également lorsque les langages de programmation deviennent très sophistiqués, avec toutes sortes de types à ordre élevé en boucle. Nous ne savons peut-être pas comment modéliser de telles choses mathématiquement. Ou bien, les modèles mathématiques standard pourraient s’avérer incohérents sous l’effet du rebondissement. (Par exemple, voir "Le polymorphisme n’est pas une théorie des ensembles" de Reynolds.) Des approches opérationnelles qui fonctionnent uniquement sur la syntaxe peuvent parfaitement contourner tous ces problèmes mathématiques.

Une autre approche intermédiaire entre les approches opérationnelles et dénotatives est la réalisabilité . Au lieu de travailler avec des termes syntaxiques comme dans les approches opérationnelles, nous allons en partie dénotationnel en utilisant une autre forme de représentants mathématiques. Ces représentants ne sont peut-être pas qualifiés de "significations" dénotatives réelles, mais ils seraient au moins un peu plus abstraits que les termes syntaxiques. Par exemple, pour le calcul lambda polymorphe, nous pouvons d’abord donner une signification aux termes non typés (dans un modèle du calcul lambda non typé), puis les utiliser comme représentants ("réalisateurs") pour effectuer une forme de "raisonnement opérationnel" légèrement niveau plus abstrait.

Alors, faisons en sorte que la concurrence entre les approches dénotationnelle, opérationnelle et de réalisabilité soit saine. Il n'y a pas de mal.

D'autre part, il pourrait également y avoir une concurrence "malsaine" entre les différentes approches. Les personnes qui utilisent une approche peuvent être si intimement liées qu’elles ne voient peut-être pas l’intérêt des autres approches. Idéalement, nous devrions tous être conscients des forces et des faiblesses des différentes approches et développer une attitude scientifique à leur égard, même si elles ne sont pas nos préférées.

[Une réponse de plus. Il n’est probablement pas cool d’empiler plusieurs réponses. Mais, hé, c’est un problème grave.]

J'ai dit que j'étais d'accord avec la réponse d'Andrej, mais il semble que je ne suis pas entièrement d'accord. Il existe une différence.

J'ai dit qu'une sémantique dénotationnelle doit dire "le sens de cette notation est que". Ce que je voulais dire, c'est qu'il faut attribuer aux notations des significations, qui sont une forme d' entités conceptuelles , et non d'autres notations. En revanche, Andrej a également exigé, en paraphrasant Scott, que les significations soient des objets "mathématiques". Je ne crois pas que le bit mathématique est nécessaire.

Par exemple, il serait tout à fait correct, de mon point de vue, que les significations des notations soient des processus physiques. Après que tous les programmes informatiques freinent dans votre voiture, pilotent des avions, larguent des bombes, etc. Ce sont des processus physiques, pas des éléments dans un espace mathématique. Vous ne pouvez pas larguer une bombe, voir si elle tue quelqu'un, et la reprendre si elle ne le fait pas. Les programmes informatiques ne peuvent pas faire cela. Mais les fonctions mathématiques peuvent. (On les appelle opérations de "snapback".) Donc, il n’est pas du tout clair que les fonctions mathématiques donneront un bon sens aux programmes informatiques.

D'autre part, nous ne savons pas encore comment parler des processus physiques de manière abstraite. Nous pourrions donc utiliser une description mathématique des processus afin d’articuler nos idées. Mais ces descriptions mathématiques ne seraient que cela, des "descriptions". Ce ne sont pas des significations. Les véritables significations seraient simplement les processus physiques que nous imaginons conceptuellement.

Dans son discours de remerciement pour le prix SIGPLAN (qui devrait être sur youtube prochainement), Hoare a déclaré que ACP utilisait une "approche algébrique", que CSP utilisait une "approche dénotative" et que CCS utilisait une "approche opérationnelle" pour décrire ses processus. Ohad et moi étions assis ensemble pendant la séance, nous nous sommes regardés et nous nous sommes dit "c'est vraiment intéressant". Il y a donc beaucoup d'espace conceptuel à explorer. Je pense que beaucoup des travaux ultérieurs de Scott, sur les systèmes de voisinage et les systèmes d’information, etc., visaient bien à expliquer les fonctions en tant que "processus". La géométrie de l'interaction de Girard et la sémantique des derniers jeux sont également des efforts pour expliquer les fonctions en tant que processus. Je dirais que le développement d’une théorie solide des processus pourrait être la grande contribution que l’informatique pourrait apporter aux mathématiques du XXIe siècle. Je n'accepterais pas de croire que les mathématiques ont toutes les réponses et que nous devrions essayer de réduire les phénomènes informatiques aux concepts mathématiques afin de les comprendre.

Ce qui me surprend, c’est combien la dissimulation d’informations fonctionne à merveille dans les calculs avec état (programmation impérative ainsi que dans les calculs de processus), alors qu’elle est maladroite et compliquée dans les formalismes mathématique / fonctionnel. Oui, nous avons la paramétrie relationnelle, et cela nous permet de contourner très bien les limites des formalismes mathématiques. Mais cela ne correspond pas à la simplicité et à l'élégance d'une programmation impérative. Donc, je ne crois pas que les formalismes mathématiques soient la bonne réponse, bien que je reconnaisse qu’ils sont la meilleure réponse que nous ayons à l’heure actuelle. Mais nous devrions continuer à chercher. Il existe une belle théorie des processus qui battront les mathématiques traditionnelles haut la main.

[J'espère que ceci est ma dernière réponse à cette question!]

La question initiale de Ohad portait sur les différences entre la sémantique dénotationnelle et la sémantique opérationnelle structurelle. Il pensait que les deux étaient compositionnels. En fait, c'est faux. La sémantique opérationnelle structurelle est donnée sous forme de séquences d'étapes. Chaque étape est exprimée de manière compositionnelle (et il est remarquable de la part de Plotkin de faire la découverte que cela est possible!), Mais l'ensemble du comportement n'est pas défini de manière compositionnelle. Voici ce que Plotkin dit dans son introduction à l'article SOS [italique ajouté]:

En sémantique dénotationnelle, on suit un idéal de compositionnalité, où le sens d'une phrase composée est donné en fonction du sens de ses parties. Dans le cas de la sémantique opérationnelle, on considère le comportement d'une phrase de programme, qui est simplement l'ensemble des transitions qu'il peut effectuer. Ce comportement n’est toutefois pas compositionnel au regard des expressions de programme. Cependant, les règles le donnent structurellement, c'est-à-dire primitivement récursif, dans la syntaxe; ...

Le fait que chaque étape soit exprimée de manière compositionnelle ne signifie pas que tout le comportement est exprimé de manière compositionnelle.

Il existe un bel article de Carl Gunter intitulé Formes de spécification sémantique , dans lequel les différentes méthodes de spécification de la sémantique sont comparées et comparées. Une grande partie de ce matériel est également reproduite dans le premier chapitre de son texte "Sémantique des langages de programmation". Cela devrait, espérons-le, clarifier la situation.

Un autre mot sur la "sémantique opérationnelle". Dans les premiers temps, le terme "opérationnel" était utilisé pour désigner toute définition sémantique faisant référence à des étapes d'évaluation détaillées. Les sémantistes dénotationnels et les partisans axiomatiques ont méprisé la sémantique «opérationnelle», la considérant comme étant de bas niveau et orientée machine. Je pense que cela était vraiment basé sur leur conviction que des descriptions de niveau supérieur étaient possibles. Ces croyances ont été brisées dès qu'ils ont considéré la concurrence. Les processus et la sémantique dénotationnelle de la simultanéité de Bakker et Zucker contiennent ces passages intéressants:

Nous utiliserons la méthodologie de la sémantique dénotationnelle . Le terme "dénotationnel" doit être comparé ici avec le terme "opérationnel": L'idée principale de la première approche est que les expressions dans une langue de programmation désignent des valeurs dans des domaines mathématiques dotés d'une structure appropriée, tandis que dans la dernière, les opérations prescrites par les constructions de langage sont les suivantes: modélisé par étapes effectuées par une machine abstraite appropriée ....

Le modèle mathématique contient diverses notions qui, bien que de style dénotationnel, sont opérationnelles dans l’esprit [soulignement ajouté]. Celles-ci incluent la fonction "historique" de la notion de processus elle-même et l'utilisation de mouvements dits silencieux dans le traitement de la synchronisation et de la récursion.

Nous voyons ici les auteurs aux prises avec les deux notions "opérationnelles", l'une technique - le comportement exprimé à l'aide de manipulations syntaxiques, et l'autre, la notion conceptuelle - de bas niveau et détaillée. Le mérite revient en grande partie à Plotkin et à Milner pour la réhabilitation de la sémantique "opérationnelle", en la rendant le plus haut niveau possible et en montrant qu'elle pourrait être élégante et perspicace.

Malgré tout, la notion opérationnelle de processus est encore assez différente de la notion dénotée de processus, cette dernière ayant été développée à la fois par De Bakker et Hoare et leurs équipes. Et, je pense qu'il y a beaucoup de choses mystérieuses et belles dans le concept de processus dénotationnel qui doit encore être compris.

Cette réponse supplémentaire est destinée à amplifier le fait que les modèles sémantiques dénotationnels sont conçus pour "expliquer" les phénomènes de calcul. Je donnerai une série d’exemples tirés de la sémantique des langages de programmation impératifs (également appelés langages "de type Algol").

Il y a d'abord eu le modèle sémantique élaboré par Scott et Strachey. (Cf. Gordon: Description dénotative des langages de programmation - mon livre préféré ou le livre de Winskel.) Ce modèle postule qu'il existe un état global , constitué de l'état de tous les emplacements alloués par un programme. Chaque commande est interprétée comme une sorte de fonction d'états globaux en états globaux.

Reynolds a déclaré qu'il ne modélisait pas la discipline de pile des variables locales. Lorsqu'une étendue locale est entrée, ses variables sont allouées et elles sont désallouées lors de la sortie de l'étendue. Fondamentalement, telle est la question "dans quel sens les variables locales sont-elles locales?" Comment la sémantique capture-elle la localité? Pour expliquer cela, il a inventé un modèle de catégorie foncteur. (Cf. Reynolds: L'essence d'Algol et Tennent: Sémantique des langages de programmation).

Tennent souhaitait modéliser les principes de raisonnement formulés dans la spécification logique de Reynolds (une extension de la logique de Hoare pour les procédures d'ordre supérieur). La logique contient des idées telles que les calculs de type expression (lecture seule), la non-interférence entre les calculs de type commande et ceux de type expression, ainsi que certains principes de raisonnement sur l'abstraction de données. Il a affiné le modèle de la catégorie de foncteur de Reynolds pour en trouver un nouveau. Cela s'appelle le modèle "SASL", également couvert dans le livre de Tennent.

Meyer et Sieber, ainsi que O'Hearn et Tennent, ont noté qu'aucun de ces modèles ne capturait encore pleinement la localité des variables locales. Lorsque deux implémentations d'un type de données abstrait ou d'une classe diffèrent par leurs variables locales mais les manipulent d'une manière qui a le même comportement lorsqu'elles sont vues de l'extérieur, elles sont équivalentes en termes d'observation. La sémantique dénotationnelle devrait les assimiler. Pour modéliser cela, O'Hearn et Tennent ont ajouté la paramétrie relationnelle à une variante du modèle de la catégorie des foncteurs de Reynolds.

Lorsque j’ai examiné le problème au même moment, j’ai renoncé à l’approche de la catégorie des foncteurs. Je pensais aussi que c'était trop technique et je pensais qu'il devait y avoir un modèle plus simple. Cela m'a amené à inventer le modèle "État global considéré comme inutile", qui ressemble plutôt à un modèle de traces CSP, mais pour un langage d'ordre supérieur. En prime, ce modèle a également capturé l' irréversibilité du changement d'état, qui n'était pas présente dans les modèles précédents.

Mon modèle ne fonctionnait que pour une sous-langue bien pensée d'Algol, appelée Contrôle syntaxique de l'interférence . Abramsky et McCusker ont étendu mon modèle en utilisant des idées de sémantique de jeux afin qu’il puisse fonctionner à plein Algol. Ainsi, leur modèle explique les mêmes phénomènes que le mien, mais pour le langage plus large.

Dans chaque cas, nous sommes en mesure de démontrer que les nouveaux modèles capturent des équivalences d’observation (ou d’autres formes de formules logiques) présentant les phénomènes informatiques mentionnés, qui n’avaient pas été validées par les modèles précédents. Il existe donc un sens très précis dans lequel ces modèles "expliquent" les phénomènes de calcul.

[Tous les travaux que je viens de mentionner se trouvent dans les volumes "Algol-like Languages": link and link ]