Como os efeitos colaterais são tratados na semântica?

Na seção "Introdução às linguagens de programação" de Anthony Aaby , sobre Semântica , ele faz a seguinte observação:

Grande parte do trabalho na semântica das linguagens de programação é motivada pelos problemas encontrados na tentativa de construir e entender programas imperativos - programas com comandos de atribuição. Como o comando de atribuição reatribui valores às variáveis, a atribuição pode ter efeitos inesperados em partes distantes do programa.

Isso me parece uma admissão notável, que permitir efeitos colaterais motivaria grande parte do trabalho em semântica.

Como a existência de efeitos colaterais em uma linguagem de programação afeta a capacidade de mapear um programa para um modelo computacional? Existem abordagens para gerenciar o estado que podem melhorar esse processo e ainda permitir efeitos colaterais?

Com base na resposta de Charles, a principal dificuldade na teoria das linguagens de programação é que a noção natural de equivalência de programas geralmente não é uma igualdade estrita, nem na semântica matemática mais direta que você pode fornecer, nem no modelo de máquina subjacente. Por exemplo, considere o seguinte bit de código semelhante ao Java:

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

Portanto, este programa cria um objeto e o nomeia x, depois cria um segundo objeto chamado y e continua executando mais um código. Agora, suponha que um programador decida inverter a ordem de alocação desses dois objetos:

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

Agora, faça a pergunta: essa refatoração muda o comportamento do programa? Por um lado, na máquina subjacente, x e y serão alocados em locais diferentes nas duas execuções do programa. Portanto, nesse sentido, o programa se comporta de maneira diferente.

Porém, em uma linguagem semelhante a Java, você só pode testar referências de igualdade e não de ordem, portanto, essa é uma diferença que o "um pouco mais de código" não pode observar . Como resultado, a maioria dos programadores espera que a reversão da ordem não faça diferença para a resposta final, e a maioria dos criadores de compiladores espera poder realizar reordenamentos e otimizações com base nisso. (Por outro lado, em uma linguagem C, você pode comparar indicadores para pedidos, convertendo-os em números inteiros primeiro e, portanto, essa reordenação não preserva necessariamente o comportamento observável.)

Uma das questões centrais da semântica é responder à questão de quando dois programas são notavelmente equivalentes. Como nossa noção de observação depende dos recursos da linguagem de programação, terminamos com uma definição como "dois programas são equivalentes quando nenhum programa cliente pode calcular respostas diferentes com base no recebimento desses programas como entradas". A quantificação de todos os programas clientes é o que dificulta essa pergunta - parece que você acaba dizendo algo sobre todos os programas possíveis para dizer algo sobre dois trechos de código específicos.

O truque da semântica denotacional é fornecer uma interpretação matemática que permita evitar essa quantificação universal - você diz que o significado de um pedaço de código é algum valor matemático e as compara verificando se são matematicamente iguais ou não. É local (isto é, composicional) e não envolve quantificação sobre todos os possíveis clientes. (Você precisa mostrar que a semântica denotacional implica equivalência contextual para que seja correta, é claro. Quando está completa - quando a igualdade denotacional é exatamente igual à equivalência contextual, dizemos que a semântica é "totalmente abstrata".)

Mas significa que você precisa garantir que a semântica denotacional valide essas equivalências. Portanto, para este exemplo, se você deseja fornecer uma semântica denotacional para essa linguagem semelhante a Java, é necessário garantir não apenas que chamar new pegue um monte e devolva um novo heap com o objeto recém-criado, mas que o significado do programa é invariável mesmo em todas as permutações do heap de entrada. Isso pode envolver estruturas matemáticas bastante complexas (por exemplo, nesse caso, trabalhar em uma categoria que garante que tudo funcione com um grupo de permutação adequado).

É claro que existem maneiras de lidar com efeitos na semântica (denotacional). Por exemplo, podemos usar a idéia de Eugenio Moggi de que efeitos computacionais são mônadas (essa idéia também foi usada no design de Haskell). Um dos problemas com isso é que as mônadas são difíceis de combinar. Gordon Plotkin e John Power sugeriram um refinamento das mônadas de Moggi às teorias de Lawvere , ou teorias algébricas, como também são chamadas, que englobam efeitos algébricos (os efeitos mais comuns são algébricos, como estado, E / S, não determinismo, mas continuações são não). Para um tratamento abrangente, consulte a tese de Matija Pretnar .

Também devo mencionar a possível semântica de mundos para o estado local, desenvolvida por Frank Oles e John Reynolds (desculpe, não consigo encontrar um link melhor, esse material é de 1982), que antecede as mônadas de Moggi. Eles usaram categorias de presheaves para fornecer uma semântica de uma linguagem semelhante ao algol que modelou corretamente muitos aspectos do estado local (mas não todos, acho que o modelo permitiu o snapback, mas talvez minha memória me sirva errado).

Matthias Felleisen apresentou uma solução convincente para o problema dos efeitos colaterais na semântica em sua série "Teorias sintáticas de controle e estado".

Essa linha de trabalho resultou na máquina CESK, uma estrutura de máquina abstrata simples capaz de modelar de forma concisa linguagens funcionais, orientadas a objetos, imperativas e até lógicas. A estrutura CESK lida com não apenas efeitos colaterais, mas também construções de controle "complexas", como exceções, continuações, preguiça e até threads.

A máquina CESK, e a semântica operacional em pequenos passos de maneira mais ampla, são o padrão de fato na teoria da linguagem de programação há cerca de duas décadas.

Em resumo, uma máquina CESK é uma máquina de etapas pequenas com quatro componentes para descrever cada estado da máquina: a cadeia de controle (uma generalização do contador de programas), o ambiente, uma loja (também chamada heap) e a continuação atual.

O ambiente mapeia variáveis ​​para endereços; a loja mapeia os endereços para valores.

Isso torna fácil modelar variáveis ​​mutáveis: basta alterar o valor em seu endereço.

Também facilita a modelagem de ponteiros e alocação dinâmica: basta criar endereços de loja com valores de primeira classe.

De maneira semelhante, continuações de primeira classe resultam em torná-las valores endereçáveis.

Como a existência de efeitos colaterais em uma linguagem de programação afeta a capacidade de mapear um programa para um modelo computacional?

Isso não dificulta necessariamente, mas impõe restrições à maneira como a semântica de expressões maiores pode ser construída a partir de expressões menores. Ele pode interagir muito mal com outras construções de programação, por exemplo, se alguém quiser fornecer uma semântica denotacional no estilo Scott para uma linguagem que permita atribuir funções de ordem superior a referências globais.

Não são apenas os efeitos colaterais, como o estado, que causam o problema. Linguagens imperativas simples, como a linguagem de comando guardada de Dijkstra, têm esses tipos de efeitos colaterais e têm boa semântica. Surgem problemas com extensões do cálculo lambda com o tipo de semântica operacional esperada das linguagens de programação, mesmo na ausência de efeitos colaterais: o mais antigo, o PCF de Plotkin, recebeu modelos denotacionais relativamente cedo, mas a semântica não era totalmente abstrata, o que significa que a semântica denotacional era excessivamente geral, não correspondendo exatamente à sua semântica operacional. O PCF finalmente recebeu uma semântica denotacional totalmente abstrata no final dos anos 80 com a semântica de jogos, que não é de todo a semântica da teoria da ordem de Scott. A simultaneidade ainda não recebeu um tratamento denotacional totalmente adequado.

Muitos questionam a importância desse tipo de semântica. Sempre podemos fornecer algum tipo de semântica operacional, mesmo que essa "semântica" seja apenas a fonte do programa e os nomes de algumas máquinas que compilaram e executam o programa: por esse motivo, Strachey condenou a semântica operacional. Mas a semântica de operação estrutural de Plotkin mostrou como a semântica operacional pode ser separada dos modelos de máquina, e o trabalho de Pitt mostrou como essa semântica pode suportar raciocínio semelhante sobre programas e linguagens de programação à semântica denotacional. Assim, a semântica operacional é uma alternativa viável à semântica denotacional e foi aplicada com sucesso a um número substancial de linguagens de programação, como o ML padrão.

Existem abordagens para gerenciar o estado que podem melhorar esse processo enquanto ainda permitem efeitos colaterais?

Até certo ponto, as dificuldades de fornecer semântica correspondem à dificuldade de fornecer linguagens de programação poderosas que se comportam da maneira que se esperaria. As decisões de design com motivação pragmática - como evitar o uso do estado global juntamente com a simultaneidade, geralmente por meio da simultaneidade de passagem de mensagens - facilitam o fornecimento de semântica.