O que constitui semântica denotacional?

Em um encadeamento diferente , Andrej Bauer definiu a semântica denotacional como:

o significado de um programa é uma função dos significados de suas partes.

O que me incomoda nessa definição é que ela não parece destacar o que é comumente considerado como semântica denotacional do que é comumente considerado como semântica não denotacional, ou seja, semântica operacional estrutural .

Mais precisamente, o principal ingrediente aqui é modularidade , ou composicionalidade , da semântica, ou, de maneira diferente, o fato de que eles são definidos de acordo com a estrutura abstrata do programa.

Como a maioria das semânticas formais hoje em dia tende a ser estrutural, essa é a definição necessária?

Então, minha pergunta é: o que é semântica denotacional?

A distinção que eu pessoalmente faço entre semântica denotacional e operacional é algo como isto:

• a semântica denotacional é matemática e equacional. Os detalhes da redução importam menos do que o resultado final, que é um valor atemporal em algum espaço matemático.
• a semântica operacional é algorítmica. Ela se desdobra em etapas individuais no tempo. O processo faz parte do significado e o resultado final é apenas uma etapa distinta desse processo.

Às vezes, a diferença pode ser bastante sutil, e pode ser difícil dizer se é apenas uma diferença de estilo ou substância.

No entanto, podemos ver como a definição composicional de Andrej segue mais naturalmente da definição denotacional e também podemos facilmente imaginar uma semântica não confluente e não composicional que ainda atende à definição operacional.

Se eu fosse adivinhar o que Dana Scott diria, ele provavelmente diria que a semântica denotacional é composicional (como o que afirmei) e que o significado de um programa deve ser um objeto matemático genuíno, não uma entidade sintática ou formalista. Obviamente, essa visão exige que se diferencie entre manipulação formal de sintaxe e matemática "verdadeira". Esta é necessariamente uma distinção não matemática.

Como uma reflexão tardia, presumivelmente, seria desejável que o significado fosse adequado no sentido de que dois programas observacionalmente diferentes não recebem o mesmo significado. Certamente, a adequação desse tipo depende do que se admite como "observação".

Sob essa visão, pode-se argumentar que a semântica operacional estrutural não é semântica denotacional porque iguala o significado de uma entidade sintática a outra entidade sintática (um valor ou uma sequência de redução).

Concordo que a identificação de A. Bauer da semântica denotacional com a composicionalidade (em Livros sobre semântica da linguagem de programação ) realmente não caracteriza bem o que tradicionalmente se entende por semântica denotacional, uma vez que a semântica claramente operacional e a lógica do programa (semântica axiomatics) são composicionais .

Eu sugeriria que o termo seja melhor entendido sócio-historicamente, como se referindo livremente a uma certa tradição teórica (iniciada a sério quando Scott produziu um modelo teórico de rede do cálculo lambda não tipado) com certas ferramentas preferidas (teoria da ordem, teoremas do ponto de fixação) , topologia, teoria das categorias) e idiomas de destino preferidos (puramente funcionais e seqüenciais). Eu imagino que - além do puro interesse intelectual - a semântica denotacional foi inventada principalmente porque:

1. Costumava ser difícil argumentar sobre semântica operacional.

2. Costumava ser difícil dar semântica axiomantica a linguagens não triviais.

$\pi$

Então, em resumo, eu argumentaria que o termo "semântica denotacional" se tornou menos preciso e, portanto, menos útil. Pode ser útil para a comunidade semântica convergir para uma melhor terminologia.

Estou feliz com a resposta de Adrej, mas gostaria de me aprofundar mais.

Para começar, a semântica denotacional quer dizer algo como "o significado dessa notação é esse". Um semanticista real gostaria de imaginar que os significados são o que existem em nossa mente e as notações são apenas uma maneira de expressar esses significados. O requisito de que a semântica denotacional deve ser de composição segue isso. Se os significados são primários e as notações secundárias, então não temos escolha a não ser definir os significados de notações maiores como funções dos significados de seus constituintes.

Se aceitarmos esse ponto de vista, uma boa semântica denotacional precisará capturar os significados que presumimos ter em nossa mente. Qualquer semântica de composição não seria necessariamente adequada. Se eu chegar a uma definição semântica composicional e ninguém concordar que ela declare qualquer significado que eles tenham em mente, será de pouca utilidade. A semântica de jogos atualmente está nessa situação. É uma definição de composição e tecnicamente bastante forte, mas poucas pessoas concordam que isso tenha algo a ver com os significados que eles têm em mente.

Dito isto, qualquer definição de composição tem várias vantagens técnicas. Podemos usá-lo para verificar equivalências ou outras propriedades por indução na sintaxe dos termos. Podemos usá-lo para verificar a solidez dos sistemas de prova, novamente por indução na sintaxe dos termos. Podemos verificar a correção dos compiladores ou técnicas de análise de programas (que, por sua natureza, são definidas por indução na sintaxe). Uma definição semântica totalmente abstrata tem vantagens ainda mais técnicas. Você pode usá-lo para mostrar que dois programas são não equivalentes, o que você não pode fazer com nenhuma semântica composicional arbitrária. Uma definição semântica totalmente definível é ainda melhor. Aqui, os domínios semânticos têm exatamente o que você pode expressar na linguagem de programação (com algumas ressalvas). Portanto, você pode enumerar os valores nos domínios para ver quais valores existem, o que seria difícil de fazer com as notações sintáticas. Por todas essas razões, a semântica dos jogos é brilhante.

No entanto, as definições semânticas composicionais têm perdido sua vantagem ao longo dos anos. Robin Milner e Andy Pitts desenvolveram várias técnicas de " raciocínio operacional ", que funcionam puramente na sintaxe, mas usam a semântica operacional sempre que necessário para falar sobre comportamento. Essas técnicas operacionais de raciocínio são de baixa tecnologia. Sem matemática sofisticada. Não há objetos infinitos. Podemos ensiná-los a estudantes de graduação e qualquer pessoa pode usá-los. Portanto, muitas pessoas fazem a pergunta por que precisamos de semântica denotacional. (Martin Berger provavelmente está neste campo.)

Pessoalmente, não tenho nenhum problema em ter muitas ferramentas em minha caixa de ferramentas. Técnicas denotacionais podem ter uma pontuação melhor para alguns problemas e técnicas operacionais para outros. Os pesquisadores que desenvolvem a teoria podem estar melhor sintonizados em uma abordagem ou outra. Com bastante frequência, podemos desenvolver os insights em uma abordagem e transferi-los para a outra. (Muito do trabalho de Andy Pitts é desse tipo. A parametridade relacional foi desenvolvida no cenário denotacional, mas ele é capaz de descobrir como reafirmar isso como raciocínio operacional. Quando olho para ele, digo "uau, eu nunca teria pensei que isso seria possível. "A lógica de separação também está indo nessa direção. Steve Brookes deu uma prova de integridade de 60 páginas para a lógica de separação simultânea usando semântica denotacional.

As abordagens operacionais também têm uma pontuação brilhante quando as linguagens de programação ficam muito sofisticadas, com todos os tipos de tipos de ordem superior em loop. Podemos não ter idéia de como modelar essas coisas matematicamente. Ou, os modelos matemáticos padrão podem se tornar inconsistentes sob o estresse da malha. (Por exemplo, consulte "O polimorfismo não é teórico-definido" por Reynolds.) Abordagens operacionais que funcionam puramente na sintaxe podem perfeitamente evitar todos esses problemas matemáticos.

Outra abordagem intermediária entre as abordagens operacional e denotacional é a capacidade de realização . Em vez de trabalhar com termos sintáticos, como nas abordagens operacionais, passamos a denotar parte, usando alguma outra forma de representantes matemáticos. Esses representantes podem não se qualificar como "significados" denotacionais reais, mas seriam pelo menos um pouco mais abstratos do que termos sintáticos. Por exemplo, para o cálculo lambda polimórfico, podemos primeiro atribuir significados a termos não digitados (em alguns modelos do cálculo lambda não digitado) e depois usá-los como representantes ('realizadores') para fazer alguma forma de "raciocínio operacional" de maneira ligeiramente nível mais abstrato.

Portanto, que haja uma concorrência saudável entre as abordagens denotacional, operacional e de realização. Não há mal nenhum.

Por outro lado, também pode haver alguma competição "prejudicial" crescendo entre as diferentes abordagens. As pessoas que trabalham com uma abordagem podem estar tão intimamente ligadas a ela que podem não entender o objetivo das outras abordagens. Idealmente, todos devemos estar cientes dos pontos fortes e fracos das diferentes abordagens e desenvolver uma atitude científica em relação a elas, mesmo que não sejam nossos favoritos individuais.

[Mais uma resposta. Provavelmente não é legal acumular várias respostas. Mas, ei, isso é um problema profundo.]

Eu disse que concordei com a resposta de Andrej, mas parece que não concordo totalmente. Há uma diferença.

Eu disse que uma semântica denotacional tem que dizer "o significado dessa notação é isso". O que eu quis dizer é que as notações devem ter significados atribuídos, que são alguma forma de entidades conceituais , não algumas outras notações. Por outro lado, Andrej também exigiu, parafraseando Scott, que os significados devessem ser objetos "matemáticos". Não acredito que o bit matemático seja necessário.

Por exemplo, seria perfeitamente bom, do meu ponto de vista, que significados de notações fossem processos físicos. Depois de todos os programas de computador pisarem no seu carro, pilote aviões, jogue bombas e o que não. Estes são processos físicos, não elementos em algum espaço matemático. Você não pode soltar uma bomba, ver se ela mata alguém e levá-la de volta se não. Programas de computador não podem fazer isso. Mas funções matemáticas podem. (Eles são chamados de operações de "snapback".) Portanto, não está claro que funções matemáticas tenham bons significados para programas de computador.

Por outro lado, ainda não sabemos como falar sobre processos físicos de maneira abstrata. Portanto, podemos de fato usar alguma descrição matemática de processos para articular nossas idéias. Mas essas descrições matemáticas seriam apenas isso, "descrições". Eles não são significados. Os significados reais seriam apenas os processos físicos que imaginamos conceitualmente.

Em seu discurso de aceitação do prêmio SIGPLAN (que deve estar no youtube em breve), Hoare disse que o ACP usou uma "abordagem algébrica", o CSP usou uma "abordagem denotacional" e o CCS usou uma "abordagem operacional" para descrever processos. Ohad e eu estávamos sentados juntos na sessão, nos entreolhamos e dissemos "isso é realmente interessante". Portanto, há muito espaço conceitual aqui que está sendo explorado. Penso que muitos dos trabalhos posteriores de Scott, em sistemas de vizinhança e sistemas de informação etc., foram de fato um esforço para explicar funções como "processos" de alguma forma. A geometria de interação de Girard e a semântica dos jogos posteriores também são esforços para explicar funções como processos. Eu diria que o desenvolvimento de uma sólida teoria de processos poderia ser a grande contribuição que a Ciência da Computação poderia dar à matemática do século XXI. Eu não aceitaria a crença de que a matemática tem todas as respostas e devemos tentar reduzir os fenômenos computacionais a conceitos matemáticos para entendê-los.

O que me surpreende é como lindamente a ocultação de informações funciona em cálculos estatais (programação imperativa e cálculo de processos), enquanto é desajeitada e complicada em formalismos matemáticos / funcionais. Sim, temos parametridade relacional e isso nos permite contornar muito bem as limitações dos formalismos matemáticos. Mas isso não corresponde à simplicidade e elegância da programação imperativa. Portanto, não acredito que os formalismos matemáticos sejam a resposta certa, embora eu admita que eles sejam a melhor resposta que temos no momento. Mas devemos continuar procurando. Existe uma boa teoria dos processos por aí que derrota a matemática tradicional.

[Espero que esta seja minha última resposta a esta pergunta!]

A pergunta original de Ohad era sobre como a semântica denotacional difere da semântica operacional estrutural. Ele achava que os dois eram de composição. Na verdade, isso é falso. A semântica operacional estrutural é dada como sequências de etapas. Cada passo é expresso em termos de composição (e é notável que Plotkin faça a descoberta de que isso é possível!), Mas todo o comportamento não é definido em termos de composição. Aqui está o que Plotkin diz em sua introdução ao artigo da SOS [ênfase adicionada]:

Na semântica denotacional, segue-se um ideal de composicionalidade, onde o significado de uma frase composta é dado em função do significado de suas partes. No caso da semântica operacional, considera-se o comportamento de uma frase de programa, que é apenas a coleção das transições que ela pode fazer. Esse comportamento, no entanto, não é composicional quando pensado como uma função das frases do programa. No entanto, as regras dão estruturalmente, isto é, primitivo recursivamente, na sintaxe; ...

O fato de cada etapa ser expressa em termos de composição não significa que todo o comportamento seja expresso em termos de composição.

Há um belo artigo de Carl Gunter chamado Forms of Semantic Specification , no qual os diferentes métodos de especificação de semântica são comparados e contrastados. Grande parte desse material também é reproduzida no primeiro capítulo de seu texto "Semântica das linguagens de programação". Espero que isso esclareça a imagem.

Outra palavra sobre "semântica operacional". Nos primeiros dias, o termo "operacional" era usado para se referir a qualquer definição semântica que se referia às etapas detalhadas da avaliação. Os semanticistas denotacionais e os proponentes axiomáticos desprezavam a semântica "operacional", considerando-a como de baixo nível e orientada à máquina. Eu acho que isso foi realmente baseado na crença de que descrições de nível superior eram possíveis. Essas crenças foram destruídas assim que consideraram simultaneidade. Os processos de Bakker e Zucker e a semântica denotacional da simultaneidade têm estas passagens interessantes:

Usaremos a metodologia da semântica denotacional . "Denotacional" deve ser contrastado aqui com "operacional": a idéia principal da primeira abordagem é que expressões em uma linguagem de programação denotam valores em domínios matemáticos equipados com uma estrutura apropriada, enquanto que, na última, as operações prescritas pelas construções de linguagem são modelado por etapas executadas por alguma máquina abstrata adequada ....

O modelo matemático contém várias noções que, embora em estilo denotacional, são operacionais em espírito [grifo nosso]. Isso inclui o recurso "histórico" da noção de processo em si e o uso dos chamados movimentos silenciosos ao lidar com sincronização e recursão.

Aqui vemos os autores lutando com as duas noções de "operacional", uma a noção técnica - comportamento expresso usando manipulações sintáticas, e a outra, a noção conceitual - de baixo nível e detalhamento. O crédito é amplamente atribuído a Plotkin e Milner por reabilitar a semântica "operacional", tornando-a o mais alto nível possível e mostrando que ela pode ser elegante e perspicaz.

Apesar de tudo isso, a noção operacional de processo ainda é bastante diferente da noção denotacional de processo, a última desenvolvida por De Bakker e Hoare e suas equipes. E acho que há muita coisa misteriosa e bonita no conceito de processo denotacional que ainda deve ser entendido.

Essa resposta adicional é para ampliar o ponto em que modelos semânticos denotacionais são projetados para "explicar" fenômenos computacionais. Vou dar uma série de exemplos da semântica de linguagens de programação imperativas (também chamadas de linguagens "tipo Algol").

Primeiro, houve o modelo semântico formulado por Scott e Strachey. (Cf. Gordon: Descrição denotacional de linguagens de programação - o meu favorito de todos os tempos ou o livro de Winskel.) Esse modelo postula que existe um estado global , composto pelo estado de todos os locais alocados por um programa. Todo comando é interpretado como algum tipo de função de estados globais para estados globais.

Reynolds disse que não modelou a disciplina de pilha de variáveis ​​locais. Quando um escopo local é inserido, suas variáveis ​​são alocadas e desalocadas quando o escopo é encerrado. Basicamente, esta é a pergunta "em que sentido as variáveis ​​locais são locais?" Como a semântica captura a localidade? Para explicar isso, ele inventou um modelo de categoria de functor. (Cf. Reynolds: A Essência de Algol e Tennent: Semântica de linguagens de programação).

A Tennent queria modelar os princípios de raciocínio formulados na Specification Logic de Reynolds (uma extensão da Hoare Logic para procedimentos de ordem superior). A lógica tem idéias como cálculos de expressão (somente leitura), não interferência entre cálculos de comando e de expressão e alguns princípios de raciocínio de abstração de dados. Ele refinou o modelo de categoria de functor de Reynolds para encontrar um novo. Isso se chama modelo SASL, também abordado no livro da Tennent.

Meyer e Sieber, e também O'Hearn e Tennent, observaram que nenhum desses modelos ainda capturava completamente a localidade das variáveis ​​locais. Quando duas implementações de um tipo de dado abstrato ou de uma classe diferem em suas variáveis ​​locais, mas as manipulam de maneiras que têm o mesmo comportamento quando vistas de fora, elas são observacionalmente equivalentes. A semântica denotacional deve igualá-los. Para modelar isso, O'Hearn e Tennent adicionaram parametridade relacional a uma variante do modelo de categoria de funções de Reynolds.

Quando analisei o problema ao mesmo tempo, não acreditei na abordagem da categoria functor. Eu também pensei que era excessivamente técnico e acreditava que deveria haver um modelo mais simples. Isso me levou a inventar o modelo "Estado global considerado desnecessário", que é mais ou menos como um modelo de rastreamento de CSP, mas para uma linguagem de ordem superior. Como um bônus adicional, este modelo também capturou a irreversibilidade da mudança de estado, que não estava presente nos modelos anteriores.

Meu modelo só funcionava para uma sub-linguagem bem-comportada de Algol, chamada Controle Sintático de Interferência . Abramsky e McCusker estenderam meu modelo usando idéias de semântica de jogos para que ele funcionasse para o Algol completo. Portanto, o modelo deles explica os mesmos fenômenos que o meu, mas para a linguagem maior.

Em cada caso, podemos demonstrar que os novos modelos capturam equivalências observacionais (ou outras formas de fórmulas lógicas) exibindo os fenômenos computacionais mencionados, que não foram validados pelos modelos anteriores. Portanto, há um sentido muito preciso no qual esses modelos estão "explicando" fenômenos computacionais.

[Todo o trabalho que mencionei aqui pode ser encontrado nos volumes "Linguol-like Languages": link e link ]