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

45

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?

Ohad Kammar
la source
4
Le sens peut être donné sous plusieurs formes: conditions pré-post, fonctionnement d'une machine abstraite, d'une entité mathématique, d'une stratégie de jeu. Dans toutes les approches modernes, ces significations sont données en fonction de la signification des parties.
Ohad Kammar
1
La question de l'existence de initié l'étude de la théorie de domaine. Il découle de l'approche dénotationnelle, mais ne le définit pas (par exemple, le langage en question peut même ne pas avoir d'espaces de fonction). En ce qui concerne la modularité, comme je l’ai dit ci-dessus, chaque approche moderne de la sémantique a fondamentalement une compositionnalité appropriée. [DD]D
Ohad Kammar
10
[DD]=D λλ
2
[DD]=DλD[DD]D
1
Je ne suis pas sûr que cela aide, mais je vois le travail "actuel" en sémantique dénotationnelle est "la compilation du langage en une catégorie" - en effet, vous pouvez écrire une sémantique en terme d'objets mathématiques connus sans insister sur la structure de la une description juste des exemples spécifiques que j'ai rencontrés.
Gasche

Réponses:

30

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.

Marc Hamann
la source
Le traitement de la non-terminaison est un bon exemple de la différence algorithmique vs mathématique. La dénotation d'une boucle est en bas, mais à cause du problème d'arrêt, il est indécidable de savoir si la dénotation d'un programme arbitraire est en bas. Dans la sémantique à petites étapes, vous pouvez plutôt observer des étapes de réduction, mais la théorie n'a pas de valeur "inférieure". L’indécidabilité et la non-disparition passent à la métathéorie: ce qui est indécidable, c’est de savoir si une séquence de réduction se termine. De même, dans la sémantique à grands pas, il est indécidable de savoir s'il existe une dérivation.
Blaisorblade
23

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).

Andrej Bauer
la source
3
De temps en temps, on me dit que les systèmes de transition ne sont pas aussi mathématiques que des domaines, des treillis ou des ordres. Je trouve cette vue déroutante. Tout peut être exprimé dans la théorie des ensembles ZFC.
Martin Berger
1
Considérer avec quelle précision une sémantique donnée peut modéliser un phénomène informatique est une approche plus intéressante et dépend en fait de manière cruciale de la notion d'observation choisie. L'un des principaux avantages de la sémantique opérationnelle (par exemple, la théorie des processus) est précisément que les notions d'observation naturelles sont beaucoup plus faciles à définir par rapport à la sémantique de la théorie de l'ordre.
Martin Berger
3
@Marc: Je suis d'accord avec vous pour dire que les méthodes opérationnelles ne modélisent pas le calcul en tant que fonction. Mais je ne vois pas pourquoi cela rend les approches théoriques de l'ordre "plus mathématiques". Les mathématiques influencées par la physique, telles que les équations différentielles, modélisent les évaluations de certains systèmes dans le temps. L'approche entrée-sortie utilise elle-même une structure temporelle rudimentaire, à savoir que la sortie n'est pas disponible avant l'entrée.
Martin Berger
2
@Martin: Les mathématiciens se plaignent souvent que ce que font les physiciens n'est pas une vraie mathématique non plus. ;-) La physique est juste une science plus confortablement établie pour le moment. TCS est encore relativement le nouveau venu sur le bloc. Je pense que le SDC ne devrait pas s'inquiéter de rendre les gens heureux dans une discipline différente (peu importe combien nous l'aimons personnellement); nous avons notre propre mojo sur le pouce (tout comme les physiciens).
Marc Hamann
2
@Marc: les ordures arbitraires peuvent être exprimées en ZFC, ce n'est donc pas un critère important. La sémantique dans laquelle les "fonctions" d'un langage de programmation sont interprétées comme des fonctions au sens mathématique présente au moins deux avantages. Premièrement, cela correspond bien à la façon dont les gens perçoivent les fonctions dans un langage de programmation. Deuxièmement, les fonctions sont des objets mathématiques familiers. Il existe donc de nombreuses machines que l’on peut utiliser. Bien entendu, les systèmes de transition ont aussi leur utilité.
Andrej Bauer
19

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.

π

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.

Martin Berger
la source
1
Pour récapituler mon dernier post, une "sémantique dénotationnelle" doit dire, "le sens de cette notation est celui". La sémantique "opérationnelle" et la sémantique "axiomatique" ne sont pas des définitions sémantiques de ce type. Il est trompeur de les faire paraître ainsi. Notez également que ce qu'on appelle "l'approche opérationnelle" est une approche de raisonnement sur les programmes. Ce n'est pas une sémantique opérationnelle. L'approche opérationnelle et l'approche axiomatique peuvent se substituer aux applications d'ingénierie de la sémantique dénotationnelle. Mais ils ne deviennent pas une sémantique dénotationnelle.
Uday Reddy
LπL
1
@Martin. Pourquoi assigner des processus de manière compositionnelle n'est pas dénotationnel. Cela pourrait être le cas si vous convainciez tous que les processus sont une théorie fondamentale au même titre que la théorie des ensembles et qu'il ne faut pas en demander la sémantique. Je comprends le point de vue selon lequel il pourrait exister un langage de base modélisant les calculs avec état. Peut-être qu'un jour un calcul de processus, sous une forme ou une autre, sera accepté comme base. Mais je ne pense pas que nous sommes encore là.
Uday Reddy le
1
@MartinBerger C'est le seul que j'ai jamais appris, mais j'ai du mal à vous fournir une bonne référence tout de suite. Par exemple, "Enfin sans étiquette, partiellement évalué" ( citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.99.9287 ) utilise "fold", "composition" et "primitive récursive" dans l'intro comme synonymes évidents (mais cela n'est pas beaucoup discuté dans le journal, c'est pris pour acquis). Viceversa, il semblerait que ce soit un sujet de débat en philosophie, si l'on doit faire confiance à Wikipedia ici: en.wikipedia.org/wiki/Principle_of_compositionality#Critiques
Blaisorblade
1
@Blaisorblade Quand j'étais doctorant, je me suis socialisé avec des sémantistes dénotants, parce que j'étais censé travailler sur la sémantique dénotationnelle. Je leur ai toujours demandé quelle était la sémantique dénotationnelle, s'ils pouvaient me donner une définition abstraite, mais je n'ai eu que des réponses évasives ou vagues telles que "la sémantique dénotationnelle est une sémantique mathématique", voir également l'explication de A. Bauer. Je ne pense pas que le concept soit bien défini. Je ne vois pas non plus pourquoi le fait d'exiger, par exemple, la récursivité primitive est suffisamment contraignant, car le pouvoir de la récursivité primitive dépend de ce qui est disponible: (suite)
Martin Berger
16

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.

Uday Reddy
la source
Une solution constructive à ce problème pourrait consister à trouver des traductions entre les différentes approches.
Martin Berger
1
Notez que je n'ai aucun problème avec la sémantique dénotationnelle conventionnelle en tant qu'outil dans la boîte à outils. Je trouve simplement que les suggestions implicites ou explicites selon lesquelles il est préférable qu'elles soient en quelque sorte problématiques et sans justification cohérente.
Martin Berger
Je mettrais en place les volumes "Algollike Languages" ( eecs.qmul.ac.uk/~ohearn/Algol/algol.html ) édités par Peter O'Hearn et Bob Tennent comme un modèle de bonne pratique. Ils comprennent des articles sur la "sémantique dénotationnelle conventionnelle" (Strachey, Reynolds, Tennent, Meyer et al), ainsi que la sémantique dénotationnelle "non conventionnelle" (mine, Abramsky & McCusker, Brookes) et les approches opérationnelles (Andy Pitts, Felleisen). Incidemment, deux articles de Reynolds dans les volumes (Logique de spécification et Contrôle syntaxique de l’interférence) étaient "axiomatiques" lorsqu’ils ont été écrits!
Uday Reddy
1
En ce qui concerne la saine concurrence, l’un des problèmes clés est qu’il existe tellement d’approches, de formalismes, de chercheurs et de documents qu’il est difficile de suivre l’évolution. En tant que communauté de recherche, il pourrait être utile de déployer des efforts soutenus pour synthétiser et unifier les approches existantes.
Martin Berger
2
@MartinBerger, un point de départ que je connais bien est l'article de Patrick Cousot intitulé "Conception constructive d'une hiérarchie de sémantique", qui montre qu'un très large éventail de modèles sémantiques, notamment les systèmes de transition, la sémantique axiomatique et les modèles dénotationnels, peut être associé à l'aide d'adjonctions, donc considéré comme différentes abstractions.
Vijay D
12

[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.

Uday Reddy
la source
10

[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.

Uday Reddy
la source
Désolé de ne pas répondre à la demande de chat. Je suis très occupé pour les deux prochaines semaines. Merci d'avoir écrit ça! C'est la première réponse technique sur la page que je comprends.
Vijay D
Je saisis peut-être cette occasion pour mettre sur pied une école spécialisée en informatique théorique dans notre école supérieure du Midlands , qui est destinée à résoudre tous ces problèmes. Il est ouvert à tous les doctorants, de partout dans le monde.
Uday Reddy
9

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 ]

Uday Reddy
la source