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

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?

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

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

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.

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.