Comment les effets secondaires sont-ils gérés en sémantique?

19

Dans la section "Introduction aux langages de programmation" d' Anthony Aaby sur la sémantique , il fait l'observation suivante:

Une grande partie du travail dans la sémantique des langages de programmation est motivée par les problèmes rencontrés pour essayer de construire et de comprendre des programmes impératifs - des programmes avec des commandes d'affectation. Étant donné que la commande d'affectation réaffecte des valeurs aux variables, l'affectation peut avoir des effets inattendus dans des parties distantes du programme.

Cela me semble être un aveu remarquable, à savoir que permettre des effets secondaires motiverait une grande partie du travail en sémantique.

Comment l'existence d' effets secondaires dans un langage de programmation affecte-t-elle la capacité de mapper un programme sur un modèle informatique? Existe-t-il des approches de gestion de l'état qui peuvent améliorer ce processus tout en permettant des effets secondaires?

Shane
la source
Cela devrait-il être étiqueté comme une question douce? Comme «une grande partie du travail en sémantique [...] est motivée par [les effets secondaires]», vous ne pouvez certainement pas vous attendre à une réponse courte et rigoureuse.
Radu GRIGore
1
@Radu: Sur MO, ce serait probablement tagué [vue d'ensemble], qui ne sont généralement pas [soft-question] ou CW là-bas.
Charles Stewart
La balise big-picture est encore meilleure. Je l'ai oublié.
Radu GRIGore
Bonne suggestion; J'ai ajouté le tag.
Shane

Réponses:

18

En s'appuyant sur la réponse de Charles, la principale difficulté de la théorie des langages de programmation est que la notion naturelle d'équivalence des programmes n'est généralement pas une stricte égalité, ni dans la sémantique mathématique la plus simple que vous pouvez donner, ni dans le modèle de machine sous-jacent. Par exemple, considérez le bit suivant de code de type Java:

Object x = new Object();
Object y = new Object();
... some more code ...

Donc, ce programme crée un objet et le nomme x, puis crée un deuxième objet nommé y, puis continue d'exécuter un peu plus de code. Supposons maintenant qu'un programmeur décide de retourner l'ordre d'allocation de ces deux objets:

Object y = new Object();
Object x = new Object();
... some more code ...

Maintenant, posez la question: cette refactorisation change-t-elle le comportement du programme? D'une part, sur la machine sous-jacente, x et y seront alloués à des emplacements différents dans les deux exécutions du programme. Donc, dans ce sens, le programme se comporte différemment.

Mais dans un langage de type Java, vous ne pouvez tester les références que pour leur égalité, et non pour leur ordre, c'est donc une différence que le «code plus» ne peut pas observer . Par conséquent, la plupart des programmeurs s'attendront à ce que l'annulation de l'ordre ne change rien à la réponse finale, et la plupart des rédacteurs du compilateur s'attendent à pouvoir effectuer des réorganisations et des optimisations sur cette base. (D'autre part, dans un C-comme la langue, vous pouvez comparer les pointeurs pour la commande, en les jetant aux entiers d' abord, et donc ce ne réordonnancement pas préserve nécessairement le comportement observable.)

L'une des questions centrales de la sémantique est de répondre à la question de savoir quand deux programmes sont observablement équivalents. Puisque notre notion d'observation dépend des caractéristiques du langage de programmation, nous nous retrouvons avec une définition comme «deux programmes sont équivalents quand aucun programme client ne peut calculer des réponses différentes en fonction de la réception de ces programmes en entrée». La quantification sur tous les programmes clients est ce qui rend cette question difficile - il semble que vous ayez à dire quelque chose sur tous les programmes clients possibles pour dire quelque chose sur deux morceaux de code particuliers.

L'astuce avec la sémantique dénotationnelle est de donner une interprétation mathématique qui vous permet d'éviter cette quantification universelle - vous dites que la signification d'un morceau de code est une valeur mathématique, et vous les comparez en vérifiant si elles sont mathématiquement égales ou ne pas. Ceci est local (c'est-à-dire compositionnel) et n'implique pas de quantification sur tous les clients possibles. (Vous devez montrer que la sémantique dénotationnelle implique une équivalence contextuelle pour qu'elle soit saine, bien sûr. Quand elle est complète - lorsque l'égalité dénotationnelle est exactement la même que l'équivalence contextuelle, nous disons que la sémantique est "entièrement abstraite".)

Mais cela signifie que vous devez vous assurer que la sémantique dénotationnelle valide ces équivalences. Donc, pour cet exemple, si vous vouliez donner une sémantique dénotationnelle pour ce langage de type Java, vous devez vous assurer non seulement que l'appel de new prend un tas et vous donne un nouveau tas avec l'objet nouvellement créé, mais que la signification du programme est invariant même sous toutes les permutations du tas d'entrée. Cela peut impliquer des structures mathématiques assez complexes (par exemple, dans ce cas, travailler dans une catégorie qui garantit que tout fonctionne modulo un groupe de permutation approprié).

Neel Krishnaswami
la source
"deux programmes sont équivalents quand aucun programme client ne peut calculer des réponses différentes en fonction de la réception de ces programmes en entrée." Je suis confus par cela. Si vous avez un programme X et un programme client Y, je suppose que Y 'appelle en' X. Mais alors vous semblez dire que Y lit le texte de X en entrée , auquel cas j'appellerais à peine Y un «client» de X. Pourriez-vous clarifier?
Radu GRIGore
1
Par "client de X", je veux dire la même chose que "contexte de programme", qui est juste un "programme plus grand qui contient X comme sous-terme".
Neel Krishnaswami
Donc, vous utilisez «X est un client de Y» de manière interchangeable avec «X lit Y comme entrée» parce que vous pensez à X comme un lambda appliqué à Y? C'est logique, mais c'est un peu tordu quand vous parlez de Java. :)
Radu GRIGore
1
@RaduGRIGore: le contexte du programme signifie autre chose. Vous lisez correctement le message, mais si X lit le code source de Y en entrée (c'est ainsi que j'interprète le message), vous pouvez distinguer tous les deux programmes syntaxiquement différents; au lieu de cela, si Y est une fonction lambda sur X, vous pouvez distinguer trop peu de programmes. Le commentaire de Neel sur le «contexte de programme» est la définition correcte: un contexte de programme Y est un programme avec un trou dans son AST, où vous pouvez placer (de manière significative) deux fragments de programme différents X1 et X2.
Blaisorblade
@NeelKrishnaswami: pourriez-vous peut-être clarifier ce que vous voulez dire dans le post? Vous pouvez simplement continuer à utiliser votre exemple et parler d'un programme où vous pouvez insérer l'un ou l'autre fragment.
Blaisorblade
12

Il existe bien sûr des moyens de gérer les effets en sémantique (dénotationnelle). Par exemple, nous pouvons utiliser l' idée d' Eugenio Moggi selon laquelle les effets de calcul sont des monades (cette idée a également été utilisée dans la conception de Haskell). L'un des problèmes avec cela est que les monades sont difficiles à combiner. Gordon Plotkin et John Power ont suggéré un raffinement des monades de Moggi aux théories de Lawvere , ou théories algébriques comme on les appelle également, qui englobe les effets algébriques (les effets les plus courants sont algébriques, tels que l'état, les E / S, le non-déterminisme, mais les suites sont ne pas). Pour un traitement complet, voir la thèse de Matija Pretnar .

Je dois également mentionner la sémantique des mondes possibles pour l'État local, développée par Frank Oles et John Reynolds (désolé, je ne peux pas trouver un meilleur lien, ce truc date de 1982), qui est antérieure aux monades de Moggi. Ils ont utilisé des catégories de pré-faisceaux pour fournir une sémantique d'un langage semblable à un algol qui a correctement modélisé de nombreux aspects de l'état local (mais pas tous, je pense que le modèle permettait le snapback, mais ma mémoire me sert peut-être mal).

Andrej Bauer
la source
1
Oui, la sémantique de la catégorie foncteur n'a pas validé toutes les équivalences de Meyer-Sieber. Peter O'Hearn et Robert Tennant ont développé une version paramétrique de la sémantique de la catégorie foncteur au milieu des années 90 qui (IIRC) a obtenu tous les exemples Meyer-Sieber, mais je ne sais pas si elle était entièrement abstraite ou non.
Neel Krishnaswami
Le modèle O'Hearn et Tennent n'est pas entièrement abstrait. Cela est discuté dans le document lui-même. Mais le raffinement par O'Hearn et Reynolds utilisant le calcul lambda linéaire est entièrement abstrait jusqu'au second ordre. Il casse pour le troisième ordre, des exemples étant les équivalences étudiées par Ahmed, Dreyer, Birkedal et al.
Uday Reddy
12

Matthias Felleisen a présenté une solution convaincante au problème des effets secondaires en sémantique dans sa série sur les "Théories syntaxiques du contrôle et de l'état".

Cette ligne de travail a abouti à la machine CESK, un cadre de machine abstraite simple capable de modéliser de manière concise des langages fonctionnels, orientés objet, impératifs et même logiques. Le framework CESK gère non seulement les effets secondaires, mais aussi les constructions de contrôle "complexes" comme les exceptions, les continuations, la paresse et même les threads.

La machine CESK, et la sémantique opérationnelle à petite échelle plus largement, sont la norme de facto dans la théorie des langages de programmation depuis environ deux décennies.

En bref, une machine CESK est une machine à petite étape avec quatre composants pour décrire chaque état de la machine: la chaîne de contrôle (une généralisation du compteur de programme), l'environnement, un magasin (également appelé tas) et la continuation actuelle.

L'environnement mappe les variables aux adresses; le magasin mappe les adresses aux valeurs.

Il est donc simple de modéliser des variables mutables: il suffit de changer la valeur à son adresse.

Il facilite également la modélisation des pointeurs et l'allocation dynamique: il suffit de faire des adresses de magasin des valeurs de première classe.

De la même manière, les suites de première classe résultent de leur transformation en valeurs adressables.

Matt pourrait
la source
6

Comment l'existence d'effets secondaires dans un langage de programmation affecte-t-elle la capacité de mapper un programme à un modèle informatique?

Cela ne rend pas nécessairement la tâche difficile, mais elle impose des restrictions sur la façon dont la sémantique d'expressions plus grandes peut être construite à partir d'expressions plus petites. Il peut très mal interagir avec certaines autres constructions de programmation, par exemple, si l'on veut donner une sémantique dénotationnelle de style Scott pour un langage permettant l'attribution de fonctions d'ordre supérieur à des références globales.

Ce ne sont pas simplement les effets secondaires comme l'état qui causent le problème. Des langages impératifs simples tels que le langage de commande gardé de Dijkstra ont ce genre d'effets secondaires et ont une belle sémantique. Des problèmes surviennent avec les extensions du lambda-calcul avec le type de sémantique opérationnelle attendue des langages de programmation même en l'absence d'effets secondaires: le premier, le PCF de Plotkin, a reçu des modèles de dénotation relativement tôt, mais la sémantique n'était pas entièrement abstraite, ce qui signifie que la sémantique dénotationnelle était trop générale, ne correspondant pas exactement à leur sémantique opérationnelle. PCF a finalement reçu une sémantique dénotationnelle entièrement abstraite à la fin des années 1980 avec une sémantique de jeu, ce qui n'est pas du tout comme la sémantique de la théorie des ordres de Scott. La concurrence n'a toujours pas reçu un traitement de dénotation entièrement adéquat.

Beaucoup remettent en question l'importance de ce type de sémantique. Nous pouvons toujours fournir une sorte de sémantique opérationnelle, même si cette "sémantique" n'est que la source du programme et les noms de certaines machines qui ont compilé et exécuté le programme: pour cette raison Strachey a condamné la sémantique opérationnelle. Mais la sémantique d'opération structurelle de Plotkin a montré comment la sémantique opérationnelle peut être séparée des modèles de machine, et le travail de Pitt a montré comment une telle sémantique peut prendre en charge un raisonnement similaire sur les programmes et les langages de programmation à la sémantique dénotationnelle. Ainsi, la sémantique opérationnelle est une alternative viable à la sémantique dénotationnelle et a été appliquée avec succès à un nombre important de langages de programmation tels que Standard ML.

Existe-t-il des approches de gestion de l'état qui peuvent améliorer ce processus tout en permettant des effets secondaires?

Dans une certaine mesure, les difficultés à fournir la sémantique correspondent à la difficulté de fournir des langages de programmation puissants qui se comportent de la manière attendue. Des décisions de conception motivées de manière pragmatique - telles que le fait d'éviter l'utilisation de l'état global avec la concurrence, généralement par le biais de la concurrence par transmission de messages - facilitent la fourniture de sémantique.

Charles Stewart
la source
Le PCF de Scott n'a pas d'état et n'est pas non plus celui de Scott, n'est-ce pas? Voir en.wikipedia.org/wiki/…
Andrej Bauer
@Andrej: Euh, tout à fait, étant donné que Luke Ong a supervisé mon D.Phil, je ne devrais pas faire cette erreur. J'ai posté un résumé teaser du PCF de Milner et du LCF de Scott qui est plus ... succint que celui de WP en tant qu'histoire LtU: lambda-the-ultimate.org/node/2196 Il me semble que vous pourriez avoir accès au Scott disparu (1969) manuscrit ...
Charles Stewart
Ce serait le PCF de Plotkin, je pense :-) Je peux essayer de me procurer le manuscrit, mais je ne l'ai pas.
Andrej Bauer
Mais le fait demeure que PCF n'a pas d'État. Quelle "raison" dites-vous que Strachey condamne la sémantique opérationnelle? Ce n'était pas évident pour moi. Le dernier paragraphe contredit ce que vous avez dit plus tôt, à savoir, les commandes gardées ont une belle sémantique mais pas PCF!
Uday Reddy
@Andrej, Uday: J'ai corrigé mon message, moins de trois ans plus tard.
Charles Stewart