Différence entre la sémantique opérationnelle à petite et à grande étape

28

Quelle est la différence fondamentale entre la sémantique opérationnelle à petite et à grande étape?

J'ai du mal à comprendre ce que c'est et la motivation pour avoir les deux.

Simon Morgan
la source
1
L'article de Wikipedia sur la sémantique opérationnelle semble prometteur ... jusqu'à ce que l'on se rende compte que la somme totale des informations dans la section "Sémantique à grands pas" est "Cette section nécessite une expansion. (Février 2011)."
David Richerby
1
Quelle est votre source d'apprentissage? Que contient-il en la matière? Qu'est-ce que tu penses? Astuce: quelle est la sémantique des grands pas x = 0; while ( true ) { x = x + 1; }?
Raphael
@Raphael Je lis Comprendre le calcul . Je pense que l'approche à petite étape consiste à réduire une expression en sous-expressions jusqu'à ce qu'elle ne puisse plus être réduite, puis à évaluer cela. La grande étape semble être d'évaluer immédiatement les choses, mais je n'ai pas vraiment de différence intéressante entre les deux méthodes, car elles semblent toutes deux concerner l'exploration de constructions de niveau supérieur.
Simon Morgan
La grande étape consiste à explorer des constructions de niveau supérieur en évaluant les sous-constructions et à petite étape en réduisant une construction plus grande, encore une fois, en ses sous-constructions.
Simon Morgan

Réponses:

32

La sémantique à petits pas définit une méthode pour évaluer les expressions une étape de calcul à la fois. Formellement parlant, une sémantique à petits pas pour un langage d'expression E est une relation →:E×E appelée relation de réduction . La sémantique à petits pas décrit en détail ce qui arrive à une expression. Il est capable de rendre compte avec précision même des programmes sans terminaison, avec une chaîne infinie e0e1e2 . Un programme de fin est un programme tel que e0e1vse termine par une valeur v telle que eE,ve .

À l'autre extrémité du spectre se trouve la sémantique dénotationnelle . La sémantique dénotationnelle attribue un «sens» à chaque expression. C'est une fonction des expressions aux dénotations: ( est appelé le domaine). L'espace des dénotations peut être complètement indépendant de l'espace syntaxique, par exemple pourrait être des expressions évaluées à un nombre et pourrait être un ensemble de nombres comme ou .D E D N R[[]]:EDDEDNR

La sémantique à grands pas est un peu au milieu. Une sémantique grands pas sur un langage d'expression et un ensemble de valeurs est une relation . Il relie une expression à sa valeur (éventuellement plusieurs valeurs si le langage n'est pas déterministe). Souvent, une valeur spéciale est utilisée pour les expressions sans terminaison.V : E × V EV⇓:E×V

Alors pourquoi avons-nous ces trois notions? Toutes ces notions peuvent se modéliser, mais le modèle ajoute un certain degré de complexité.

  • Étant donné une sémantique à petits pas , vous pouvez définir une sémantique à grands pas correspondante qui relie chaque expression à sa valeur (ou valeurs, si la réduction n'est pas déterministe): existe une chaîne et ne peut pas réduire davantage. Notez qu'en général, vous ne pouvez pas reconstruire la sémantique à petits pas à partir de la sémantique à grands pas. Par exemple, toutes les expressions sans terminaison ne peuvent pas être distinguées sous la sémantique à grand pas.e v e e 1v vevee1vv
  • Étant donné une sémantique grands pas , vous pouvez dire que c'est une sémantique petite étape sur . Ce n'est pas particulièrement utile.E V⇓:E×VEV
  • Étant donné une sémantique à petits pas , vous pouvez définir une sémantique dénotationnelle correspondante où la dénotation d'une expression est l'ensemble des chaînes de réduction à partir de celle-ci. Cela satisfait la définition formelle, mais ce n'est pas particulièrement utile, car cela ajoute une surcharge théorique d'ensemble aux objets qui sont plus faciles à raisonner en regardant directement la syntaxe.
  • Étant donné une sémantique dénotationnelle , vous pouvez définir une sémantique à petits pas en ajoutant toutes les dénotations possibles en tant que valeurs dans le langage. Cela nécessite de créer des valeurs qui ne font pas partie de la syntaxe que le programmeur peut écrire, ce qui signifie que certains résultats intéressants doivent indiquer «pour tous les programmes que le programmeur peut écrire» plutôt que «pour tous les programmes». Celui-ci n'est donc pas très utile non plus.[[]]
  • Étant donné une sémantique à grand pas , vous pouvez définir une sémantique dénotationnelle correspondante où le domaine est l'ensemble d'ensembles de valeurs: [ . Si la sémantique à grands pas est déterministe (chaque expression se réduit à une seule valeur), vous pouvez définir une sémantique dénotationnelle plus simple où le domaine est l'ensemble de valeurs.[[e]]={vev}
  • Inversement, étant donné une sémantique dénotationnelle , vous pouvez définir une sémantique à grand pas E [[[]] . Encore une fois, celui-ci est un peu inutile.E[[]]

Du point de vue opérationnel, la sémantique à petits pas correspond à regarder chaque opération effectuée par un interprète de la langue. La sémantique à grands pas ne regarde que la valeur résultante. La sémantique dénotationnelle examine une interprétation mathématique qui peut ou non avoir quelque chose à voir avec ce qui se passe sur un ordinateur.

La sémantique à petits pas est la plus évidente. Il fournit clairement des informations utiles sur les programmes non terminés. Plus généralement, il fournit des informations détaillées sur le comportement du programme.

La sémantique dénotationnelle transforme les constructions syntaxiques en objets mathématiques arbitraires; il peut exprimer tout ce que les scientifiques veulent (vous pouvez définir la dénotation d'une expression comme étant toutes les chaînes de réduction possibles), mais au prix d'ajouter un niveau de complexité. Il est utilisé lorsque nous voulons faire abstraction de certains détails tels que la façon exacte dont l'expression est évaluée.

La sémantique à grands pas est au milieu: elle résume les détails de l'évaluation mais conserve la nature syntaxique du résultat. Habituellement, le concept est utilisé lorsqu'il existe une sémantique sous-jacente à petits pas, comme un moyen d'exprimer de manière concise « »Comme« e e n(e1,,en),ee1en and e,eneeen". Dans de telles constructions, alors que les concepts sont très différents (l'un nous permet de parler des étapes de calcul individuelles et des programmes non terminés, l'autre pas), les définitions seront très similaires, car dans ce cas les règles qui définissent le la sémantique à grands pas est fondamentalement de la forme «si et… et e n v et v est une valeur alors e 1v ».e1e2envve1v

Gilles 'SO- arrête d'être méchant'
la source
J'apprends aussi cela, mais j'ai un problème avec quelque chose que vous avez dit dans votre réponse que j'aimerais que vous clarifiiez. Vous avez dit que "la sémantique à grands pas est un peu au milieu." Cependant, le petit pas ne serait-il pas réellement le modèle «intermédiaire»? Considérez les expressions: A: ((5 + 7) + 3) B: ((5 + 5) + 5) C: ((1 + 2) + 1) D: ((2 + 1) + 1) La dénotation classerait même C et D avec des valeurs différentes (éventuellement "C" et "D"), et les grands pas les classeraient tous les deux comme "4" et les deux A et B comme "15" Cependant, les petits pas vous donneraient "(12 + 3) "et" (10 + 5) "pour A et B, et" (3 + 1) "pour C et D.
Timothy Swan
@TimothySwan En supposant que vous vouliez définir l'évaluation arithmétique habituelle, une sémantique dénotationnelle ne distinguerait pas C et D. Une sémantique à petits pas définirait une chaîne de réduction comme . Une sémantique à grands pas serait très similaire à une sémantique dénotationnelle: ( ( 2 + 1 ) + 1 ) 3 vs [((2+1)+1)3+14((2+1)+1)3 . Le 4 de la sémantique à grands pas est celui de la syntaxe du langage tandis que le 4 de la sémantique dénotationnelle est celui de la métathéorie, mais la distinction n'est pas visible ou importante dans cet exemple simple. [[((2+1)+1)]]=444
Gilles 'SO- arrête d'être méchant'
Ainsi, lorsque vous avez dit: «La sémantique dénotationnelle attribue un« sens »à chaque expression. vous ne vouliez pas dire identifier de manière unique les expressions elles-mêmes, mais une sorte de signification indépendante de l'évaluation? Pouvez-vous fournir un exemple simple qui montre clairement la différence entre la sémantique à grands pas et la sémantique dénotationnelle? De plus, veuillez expliquer 3dans ((2+1)+1)⇓3Je suppose que «dénotation» est une valeur finale, mais dans quel cas «grand pas» ne correspondrait-il pas nécessairement directement à cela? La différence a-t-elle quelque chose à voir avec le contexte, comme (a + 1)selon l'environnement qui en contient a?
Timothy Swan
@TimothySwan Tant qu'il n'y a pas d'effets secondaires, pas de non-déterminisme et pas de fonctions, la sémantique dénotationnelle d'une expression est la valeur à laquelle elle évalue. Le non-déterminisme est un bon moyen d'illustrer la différence entre grand pas et dénotation: la dénotation d'une expression serait l'ensemble des valeurs qu'elle peut avoir: , alors qu'une sémantique à grands pas aurait plusieurs jugements admissibles: r a n d ( 1 .. n ) 1 et r a n d ( 1 .. n ) 2 et ...C'était une faute de frappe. [[rand(1..n)]]={1,2,,n}rand(1..n)1rand(1..n)23
Gilles 'SO- arrête d'être méchant'