Semântica denotacional - Denotational semantics

Na ciência da computação , a semântica denotacional (inicialmente conhecida como semântica matemática ou semântica de Scott – Strachey ) é uma abordagem de formalizar os significados das linguagens de programação por meio da construção de objetos matemáticos (chamados denotações ) que descrevem os significados das expressões das linguagens. Outras abordagens que fornecem semântica formal de linguagens de programação incluem semântica axiomática e semântica operacional .

Em termos gerais, a semântica denotacional está preocupada em encontrar objetos matemáticos chamados domínios que representam o que os programas fazem. Por exemplo, programas (ou frases de programa) podem ser representados por funções parciais ou por jogos entre o ambiente e o sistema.

Um princípio importante da semântica denotacional é que a semântica deve ser composicional : a denotação de uma frase de programa deve ser construída a partir das denotações de suas subfrases .

Desenvolvimento histórico

A semântica denotacional originou-se no trabalho de Christopher Strachey e Dana Scott publicado no início dos anos 1970. Conforme desenvolvida originalmente por Strachey e Scott, a semântica denotacional fornecia o significado de um programa de computador como uma função que mapeia a entrada em saída. Para dar significado a programas definidos recursivamente , Scott propôs trabalhar com funções contínuas entre domínios , especificamente pedidos parciais completos . Conforme descrito abaixo, o trabalho continuou na investigação da semântica denotacional apropriada para aspectos das linguagens de programação, como sequencialidade, simultaneidade , não determinismo e estado local .

A semântica denotacional foi desenvolvida para linguagens de programação modernas que usam recursos como simultaneidade e exceções , por exemplo, ML concorrente , CSP e Haskell . A semântica dessas linguagens é composicional, no sentido de que o significado de uma frase depende dos significados de suas subfrases. Por exemplo, o significado da expressão aplicativa f (E1, E2) é definido em termos de semântica de suas subfrases f, E1 e E2. Em uma linguagem de programação moderna, E1 e E2 podem ser avaliados simultaneamente e a execução de um deles pode afetar o outro, interagindo por meio de objetos compartilhados, fazendo com que seus significados sejam definidos em termos um do outro. Além disso, E1 ou E2 podem lançar uma exceção que pode encerrar a execução do outro. As seções abaixo descrevem casos especiais da semântica dessas linguagens de programação modernas.

Significados de programas recursivos

A semântica denotacional é atribuída a uma frase de programa como uma função de um ambiente (mantendo os valores atuais de suas variáveis ​​livres) para sua denotação. Por exemplo, a frase n*mproduz uma denotação quando fornecida com um ambiente que possui ligação para suas duas variáveis ​​livres: ne m. Se no ambiente ntiver o valor 3 e mtiver o valor 5, a denotação será 15.

Uma função pode ser representada como um conjunto de pares ordenados de argumentos e valores de resultados correspondentes. Por exemplo, o conjunto {(0,1), (4,3)} denota uma função com resultado 1 para o argumento 0, resultado 3 para o argumento 4 e indefinido caso contrário.

O problema a ser resolvido é fornecer significados para programas recursivos que são definidos em termos de si mesmos, como a definição da função fatorial como

int factorial(int n) { if (n == 0) then return 1; else return n * factorial(n-1); }

Uma solução é construir os significados por aproximação. A função fatorial é uma função total de ℕ a ℕ (definida em qualquer lugar em seu domínio), mas nós a modelamos como uma função parcial . No início, começamos com a função vazia (um conjunto vazio). A seguir, adicionamos o par ordenado (0,1) à função para resultar em outra função parcial que se aproxima melhor da função fatorial. Depois, adicionamos outro par ordenado (1,1) para criar uma aproximação ainda melhor.

É instrutivo pensar nessa cadeia de iteração para uma "função fatorial parcial" F como F 0 , F 1 , F 2 , ... onde F n indica F aplicado n vezes .

  • F 0 ({}) é a função parcial totalmente indefinida, representada como o conjunto {};
  • F 1 ({}) é a função parcial representada como o conjunto {(0,1)}: é definida em 0, como 1, e indefinida em outro lugar;
  • F 5 ({}) é a função parcial representada como o conjunto {(0,1), (1,1), (2,2), (3,6), (4,24)}: é definida por argumentos 0,1,2,3,4.

Este processo iterativo constrói uma sequência de funções parciais de ℕ a ℕ. As funções parciais formam uma ordem parcial completa da cadeia usando ⊆ como a ordem. Além disso, esse processo iterativo de melhores aproximações da função fatorial forma um mapeamento expansivo (também chamado de progressivo) porque cada um usa ⊆ como ordenação. Portanto, por um teorema de ponto fixo (especificamente teorema de Bourbaki-Witt ), existe um ponto fixo para este processo iterativo.

Neste caso, o ponto fixo é o menor limite superior desta cadeia, que é a factorialfunção completa , que pode ser expressa como o limite direto

Aqui, o símbolo "⊔" é a junção direcionada (de conjuntos direcionados ), significando "limite superior mínimo". A junção direcionada é essencialmente a junção de conjuntos direcionados.

Semântica denotacional de programas não determinísticos

O conceito de domínios de poder foi desenvolvido para dar uma semântica denotacional a programas sequenciais não determinísticos. Escrevendo P para um construtor poder-domínio, o domínio P ( D ) é o domínio de cálculos não-determinística do tipo indicado por D .

Existem dificuldades com justiça e falta de limites em modelos teóricos de domínio de não-determinismo.

Semântica denotacional de simultaneidade

Muitos pesquisadores argumentaram que os modelos teóricos de domínio dados acima não são suficientes para o caso mais geral de computação concorrente . Por esta razão, vários novos modelos foram introduzidos. No início dos anos 1980, as pessoas começaram a usar o estilo de semântica denotacional para fornecer semântica para linguagens concorrentes. Os exemplos incluem o trabalho de Will Clinger com o modelo de ator ; O trabalho de Glynn Winskel com estruturas de eventos e redes de petri ; e o trabalho de Francez, Hoare, Lehmann e de Roever (1979) sobre a semântica de traços para CSP. Todas essas linhas de investigação permanecem sob investigação (ver, por exemplo, os vários modelos denotacionais para CSP).

Recentemente, Winskel e outros propuseram a categoria de profuncionadores como uma teoria de domínio para concorrência.

Semântica denotacional de estado

O estado (como um heap) e os recursos imperativos simples podem ser modelados diretamente na semântica denotacional descrita acima. Todos os livros abaixo contêm os detalhes. A ideia principal é considerar um comando como uma função parcial em algum domínio de estados. O significado de " x:=3" é então a função que leva um estado para o estado com 3atribuído a x. O operador de sequenciamento " ;" é denotado pela composição de funções. As construções de ponto fixo são então usadas para fornecer uma semântica às construções de loop, como " while".

As coisas se tornam mais difíceis na modelagem de programas com variáveis ​​locais. Uma abordagem é não trabalhar mais com domínios, mas, em vez disso, interpretar tipos como functores de alguma categoria de mundos para uma categoria de domínios. Os programas são então denotados por funções contínuas naturais entre esses functores.

Denotações de tipos de dados

Muitas linguagens de programação permitem que os usuários definam tipos de dados recursivos . Por exemplo, o tipo de listas de números pode ser especificado por

datatype list = Cons of nat * list | Empty

Esta seção trata apenas das estruturas de dados funcionais que não podem ser alteradas. Linguagens de programação imperativas convencionais normalmente permitiriam que os elementos de uma lista recursiva fossem alterados.

Para outro exemplo: o tipo de denotações do cálculo lambda não tipado é

datatype D = D of (D  D)

O problema de resolver equações de domínio está relacionado a encontrar domínios que modelem esses tipos de tipos de dados. Uma abordagem, grosso modo, é considerar a coleção de todos os domínios como um domínio em si e, em seguida, resolver a definição recursiva lá. Os livros abaixo fornecem mais detalhes.

Tipos de dados polimórficos são tipos de dados definidos com um parâmetro. Por exemplo, o tipo de α lists é definido por

datatype α list = Cons of α * α list | Empty

As listas de números naturais, então, são do tipo nat list, enquanto as listas de strings são do tipo string list.

Alguns pesquisadores desenvolveram modelos teóricos de domínio de polimorfismo. Outros pesquisadores também modelaram o polimorfismo paramétrico dentro de teorias de conjuntos construtivos. Os detalhes são encontrados nos livros listados abaixo.

Uma área de pesquisa recente envolveu a semântica denotacional para linguagens de programação baseadas em objetos e classes.

Semântica denotacional para programas de complexidade restrita

Seguindo o desenvolvimento das linguagens de programação baseadas na lógica linear , a semântica denotacional foi dada às linguagens para uso linear (ver, por exemplo , redes de prova , espaços de coerência ) e também complexidade de tempo polinomial.

Semântica denotacional de sequencialidade

O problema de abstração completa para a linguagem de programação sequencial PCF foi, por muito tempo, uma grande questão em aberto na semântica denotacional. A dificuldade com o PCF é que é uma linguagem muito sequencial. Por exemplo, não há como definir a função paralela ou no PCF. É por esse motivo que a abordagem usando domínios, conforme apresentada acima, produz uma semântica denotacional que não é totalmente abstrata.

Essa questão aberta foi resolvida principalmente na década de 1990 com o desenvolvimento da semântica de jogos e também com técnicas envolvendo relações lógicas . Para obter mais detalhes, consulte a página sobre PCF.

Semântica denotacional como tradução fonte-a-fonte

Muitas vezes é útil traduzir uma linguagem de programação para outra. Por exemplo, uma linguagem de programação simultânea pode ser traduzida em um cálculo de processo ; uma linguagem de programação de alto nível pode ser traduzida em código de bytes. (Na verdade, a semântica denotacional convencional pode ser vista como a interpretação das linguagens de programação na linguagem interna da categoria de domínios.)

Nesse contexto, noções de semântica denotacional, como abstração completa, ajudam a satisfazer as preocupações de segurança.

Abstração

Freqüentemente, é considerado importante conectar a semântica denotacional com a semântica operacional . Isso é especialmente importante quando a semântica denotacional é bastante matemática e abstrata, e a semântica operacional é mais concreta ou mais próxima das intuições computacionais. As seguintes propriedades de uma semântica denotacional são frequentemente interessantes.

  1. Independência de sintaxe : as denotações de programas não devem envolver a sintaxe do idioma de origem.
  2. Adequação (ou integridade) : Todos os programas distintos observáveis têm denotações distintas;
  3. Abstração completa : Todos os programas observacionalmente equivalentes têm denotações iguais.

Para a semântica no estilo tradicional, adequação e abstração completa podem ser entendidas aproximadamente como o requisito de que "a equivalência operacional coincide com a igualdade denotacional". Para a semântica denotacional em modelos mais intensionais, como o modelo de ator e cálculos de processo , existem diferentes noções de equivalência dentro de cada modelo e, portanto, os conceitos de adequação e de abstração total são uma questão de debate e mais difíceis de definir. Além disso, a estrutura matemática da semântica operacional e da semântica denotacional pode se tornar muito próxima.

Propriedades adicionais desejáveis ​​que podemos desejar manter entre a semântica operacional e denotacional são:

  1. Construtivismo : o construtivismo se preocupa em saber se os elementos do domínio podem ser mostrados por métodos construtivos.
  2. Independência da semântica denotacional e operacional : A semântica denotacional deve ser formalizada usando estruturas matemáticas que são independentes da semântica operacional de uma linguagem de programação; No entanto, os conceitos subjacentes podem estar intimamente relacionados. Consulte a seção sobre composição abaixo.
  3. Completude completa ou definibilidade : Cada morphism do modelo semântico deve ser a denotação de um programa.

Composicionalidade

Um aspecto importante da semântica denotacional das linguagens de programação é a composicionalidade, pela qual a denotação de um programa é construída a partir da denotação de suas partes. Por exemplo, considere a expressão "7 + 4". A composicionalidade, neste caso, é fornecer um significado para "7 + 4" em termos dos significados de "7", "4" e "+".

Uma semântica denotacional básica na teoria do domínio é composicional porque é dada da seguinte maneira. Começamos considerando fragmentos de programa, ou seja, programas com variáveis ​​livres. Um contexto de digitação atribui um tipo a cada variável livre. Por exemplo, na expressão ( x + y ) pode ser considerado num contexto tipagem ( x : nat, y : nat). Agora fornecemos uma semântica denotacional para fragmentos de programa, usando o seguinte esquema.

  1. Começamos descrevendo o significado dos tipos de nossa linguagem: o significado de cada tipo deve ser um domínio. Escrevemos 〚τ〛 para o domínio denotando o tipo τ. Por exemplo, o significado do tipo natdeve ser o domínio dos números naturais: nat〚〛 = ℕ .
  2. Do significado dos tipos, derivamos um significado para contextos de digitação. Montamos [ x 1 : τ 1 , ..., x n : τ n = = [τ 1 = × ... × [τ n =. Por exemplo, [ x : nat, y : nat= = ℕ × ℕ . Como um caso especial, o significado do contexto de digitação vazio, sem variáveis, é o domínio com um elemento, denotado 1.
  3. Finalmente, devemos dar um significado a cada fragmento de programa no contexto de digitação. Suponha que P seja um fragmento de programa do tipo σ, no contexto de digitação Γ, freqüentemente escrito Γ⊢ P : σ. Então, o significado deste programa no contexto de digitação deve ser uma função contínua 〚Γ⊢ P : σ〛: 〚Γ〛 → 〚σ〛. Por exemplo, [⊢7: nat=: 1 → ℕ é a função constantemente "7", enquanto que [ X : nat, Y : natx + y : nat=: ℕ × ℕ → ℕ é a função que adiciona dois números .

Agora, o significado da expressão composto (7 + 4) é determinada pela composição das três funções [⊢7: nat=: 1 ℕ → , [⊢4: nat=: 1 ℕ → , e [ x : nat, y : natx + y : nat〛: ℕ × ℕ → ℕ .

Na verdade, este é um esquema geral para semântica denotacional composicional. Não há nada específico sobre domínios e funções contínuas aqui. Em vez disso, pode-se trabalhar com uma categoria diferente . Por exemplo, na semântica dos jogos, a categoria dos jogos tem os jogos como objetos e as estratégias como morfismos: podemos interpretar os tipos como jogos e os programas como estratégias. Para uma linguagem simples sem recursão geral, podemos nos contentar com a categoria de conjuntos e funções . Para uma linguagem com efeitos colaterais, podemos trabalhar na categoria Kleisli para uma mônada. Para uma linguagem com estado, podemos trabalhar em uma categoria de functor . Milner defendeu a modelagem de localização e interação trabalhando em uma categoria com interfaces como objetos e bigrafos como morfismos.

Semântica versus implementação

De acordo com Dana Scott (1980):

Não é necessário que a semântica determine uma implementação, mas deve fornecer critérios para mostrar que uma implementação está correta.

De acordo com Clinger (1981):

Normalmente, entretanto, a semântica formal de uma linguagem de programação sequencial convencional pode ser interpretada para fornecer uma implementação (ineficiente) da linguagem. Uma semântica formal nem sempre precisa fornecer tal implementação, entretanto, e acreditar que a semântica deve fornecer uma implementação leva à confusão sobre a semântica formal de linguagens concorrentes. Essa confusão é dolorosamente evidente quando se diz que a presença de não-determinismo ilimitado na semântica de uma linguagem de programação implica que a linguagem de programação não pode ser implementada.

Conexões com outras áreas da ciência da computação

Alguns trabalhos em semântica denotacional interpretaram os tipos como domínios no sentido da teoria dos domínios, o que pode ser visto como um ramo da teoria dos modelos , levando a conexões com a teoria dos tipos e a teoria das categorias . Dentro da ciência da computação, existem conexões com interpretação abstrata , verificação de programa e verificação de modelo .

Referências

Leitura adicional

Livros didáticos
Notas de aula
Outras referências

links externos