Semântica codificação - Semantics encoding

A codificação semântica é uma tradução entre linguagens formais . Para os programadores, a forma mais familiar de codificação é a compilação de uma linguagem de programação em código de máquina ou byte-code. A conversão entre formatos de documento também são formas de codificação. Compilação de TeX ou LaTeX documentos para PostScript também são comumente encontrados processos de codificação. Alguns pré-processadores de alto nível, como OCaml 's camlp4 também envolvem a codificação de uma linguagem de programação para outra.

Formalmente, uma codificação de uma linguagem de A para B é uma linguagem de mapeamento de todos os termos de A para B. Se houver uma satisfatória codificação de A para B, B é considerado , pelo menos, tão potente (ou , pelo menos, como expressivo ) como A.

propriedades

Uma noção informal de tradução não é suficiente para ajudar a determinar a expressividade de línguas, uma vez que permite codificações triviais, como o mapeamento de todos os elementos de A para o mesmo elemento de B. Portanto, é necessário determinar a definição de um "bom o suficiente" encoding . Esta noção varia de acordo com a aplicação.

Comumente, uma codificação é esperado para preservar um número de propriedades. ${\ Displaystyle [\ cdot]: A \ B} longrightarrow$

Preservação de composições

solidez: Para cada operador n-ário de A, existe um operador n-ário de B tal que ${\ Displaystyle op_ {A}}$ ${\ Displaystyle op_ {B}}$; ${\ Displaystyle \ forall T_ {A} ^ {1}, T_ {A} ^ {2}, \ pontos, T_ {A} ^ {n}, [op_ {A} (T_ {A} ^ {1}, T_ {A} ^ {2}, \ cdots, T_ {A} ^ {n})] = op_ {B} ([T_ {A} ^ {1}], [T_ {A} ^ {2}], \ cdots, [T_ {A} ^ {n}])}$
plenitude: Para cada operador n-ário de A, existe um operador n-ário de B tal que ${\ Displaystyle op_ {A}}$ ${\ Displaystyle op_ {B}}$; ${\ Displaystyle \ forall T_ {B} ^ {1}, T_ {B} ^ {2}, \ pontos, T_ {B} ^ {n}, \ existe T_ {A} ^ {1}, \ pontos, T_ {A} ^ {n}, op_ {B} (T_ {B} ^ {1}, \ cdots, T_ {B} ^ {N}) = [op_ {A} (T_ {A} ^ {1}, T_ {A} ^ {2}, \ cdots, T_ {A} ^ {n})]}$

(Nota: na medida em que o autor está ciente, este critério de completude nunca é utilizado.)

Preservação das composições é útil na medida em que garante que os componentes podem ser analisados separadamente ou em conjunto, sem "quebrar" qualquer propriedade interessante. Em particular, no caso de compilações, este solidez garante a possibilidade de prosseguir com a compilação separada de componentes, enquanto integridade garante a possibilidade de de-compilação.

Preservação de reduções

Isso pressupõe a existência de uma noção de redução em ambos linguagem A e linguagem B. Normalmente, no caso de uma linguagem de programação, a redução é a relação que modela a execução de um programa.

Nós escrevemos para um passo de redução e para qualquer número de passos de redução. ${\ Displaystyle \ longrightarrow}$ ${\ Displaystyle \ longrightarrow ^ {*}}$

solidez: Para cada termos de linguagem A, se depois . ${\ Displaystyle T_ {A} ^ {1}, {A} T_ ^ {2}}$ ${\ Displaystyle T_ {A} ^ {1} \ longrightarrow ^ {*} T_ {A} ^ {2}}$ ${\ Displaystyle [T_ {A} ^ {1}] \ longrightarrow ^ {*} [T_ {A} ^ {2}]}$
plenitude: Para cada termo da língua A e cada termos da linguagem B, se então existe algum tal que . ${\ Displaystyle T_ {A} ^ {1}}$ ${\ Displaystyle T_ {B} ^ {2}}$ ${\ Displaystyle [T_ {A} ^ {1}] \ longrightarrow ^ {*} T_ {B} ^ {2}}$ ${\ Displaystyle T_ {A} ^ {2}}$ ${\ Displaystyle T_ {B} ^ {2} = [T_ {A} ^ {2}]}$

Esta preservação garante que ambas as línguas se comportam da mesma maneira. Solidez garante que todos os comportamentos possíveis são preservados enquanto garantias integralidade que nenhum comportamento é adicionado pela codificação. Em particular, no caso de compilação de uma linguagem de programação, correcção e completude em conjunto significa que o programa compilado se comporta de acordo com a semântica de alto nível da linguagem de programação.

Preservação de terminação

Isso também pressupõe a existência de uma noção de redução em ambos linguagem A e linguagem B.

solidez: para qualquer termo , se todas as reduções de convergir, então todas as reduções de convergir. ${\ Displaystyle T_ {A}}$ ${\ Displaystyle T_ {A}}$ ${\ Displaystyle [T_ {A}]}$
plenitude: para qualquer termo , se todas as reduções de convergir, então todas as reduções de convergir. ${\ Displaystyle [T_ {A}]}$ ${\ Displaystyle [T_ {A}]}$ ${\ Displaystyle T_ {A}}$

No caso de compilação de uma linguagem de programação, solidez garante que a compilação não introduz não-terminação, como loops infinitos ou recursions intermináveis. A propriedade de completude é útil quando a linguagem B é usado para estudar ou testar um programa escrito em linguagem A, possivelmente por extrair partes fundamentais do código: se este estudo ou teste prova que o programa termina em B, então ele também termina em A.

Preservação de observações

Isso pressupõe a existência de uma noção de observação em ambos linguagem A e linguagem B. Em linguagens de programação, observáveis típicos são resultados de entradas e saídas, por oposição à computação puro. Em uma linguagem de descrição, como HTML , um observável típico é o resultado de renderização de páginas.

solidez: para cada observável em termos de A, existe um observável de termos de B tal que para qualquer termo com observável , tem observável . ${\ Displaystyle obs_ {A}}$ ${\ Displaystyle obs_ {B}}$ ${\ Displaystyle T_ {A}}$ ${\ Displaystyle obs_ {A}}$ ${\ Displaystyle [T_ {A}]}$ ${\ Displaystyle obs_ {B}}$
plenitude: para cada observável em termos de A, existe um observável em termos de B tal que para qualquer termo com observável , tem observável . ${\ Displaystyle obs_ {A}}$ ${\ Displaystyle obs_ {B}}$ ${\ Displaystyle [T_ {A}]}$ ${\ Displaystyle obs_ {B}}$ ${\ Displaystyle T_ {A}}$ ${\ Displaystyle obs_ {A}}$

Preservação de simulações

Isso pressupõe a existência de noção de simulação em ambos linguagem A e linguagem B. Em linguagens de programação, um programa simula outro se ele pode executar as mesmas tarefas (observáveis) e possivelmente alguns outros. As simulações são utilizados tipicamente para descrever optimizações de tempo de compilação.

solidez: para cada termos , se simula então simula . ${\ Displaystyle T_ {A} ^ {1}, {A} T_ ^ {2}}$ ${\ Displaystyle T_ {A} ^ {2}}$ ${\ Displaystyle T_ {A} ^ {1}}$ ${\ Displaystyle [T_ {A} ^ {2}]}$ ${\ Displaystyle [T_ {A} ^ {1}]}$
plenitude: para cada termos , se simula então simula . ${\ Displaystyle T_ {A} ^ {1}, {A} T_ ^ {2}}$ ${\ Displaystyle [T_ {A} ^ {2}]}$ ${\ Displaystyle [T_ {A} ^ {1}]}$ ${\ Displaystyle T_ {A} ^ {2}}$ ${\ Displaystyle T_ {A} ^ {1}}$

Preservação de simulações é uma propriedade muito mais forte do que a preservação de observações, que ela implica. Por sua vez, é mais fraca do que uma propriedade de preservação da bisimulations . Como em casos anteriores, solidez é importante para a compilação, enquanto completude é útil para testar ou provar propriedades.

Preservação de equivalências

Isso pressupõe a existência de uma noção de equivalência em ambos linguagem A e linguagem B. Normalmente, isso pode ser uma noção de igualdade de dados estruturados ou uma noção de sintaticamente diferentes programas ainda semanticamente idênticos, como congruência estrutural ou equivalência estrutural.

solidez: Se dois termos e são equivalentes em A, em seguida, e são equivalentes em B. ${\ Displaystyle T_ {A} ^ {1}}$ ${\ Displaystyle T_ {A} ^ {2}}$ ${\ Displaystyle [T_ {A} ^ {1}]}$ ${\ Displaystyle [T_ {A} ^ {2}]}$
plenitude: Se dois termos e são equivalentes em B, em seguida, e são equivalentes em A. ${\ Displaystyle [T_ {A} ^ {1}]}$ ${\ Displaystyle [T_ {A} ^ {2}]}$ ${\ Displaystyle T_ {A} ^ {1}}$ ${\ Displaystyle T_ {A} ^ {2}}$

Preservação de distribuição

Isso pressupõe a existência de uma noção de distribuição em ambos linguagem A e linguagem B. Normalmente, para a compilação de programas distribuídos escritos em Agudo , JoCaml ou E, isso significa distribuição de processos e dados entre vários computadores ou CPUs.

solidez: se um prazo é a composição de dois agentes em seguida, deve ser a composição de dois agentes . ${\ Displaystyle T_ {A}}$ ${\ Displaystyle T_ {A} ^ {1} ~ | ~ T_ {A} ^ {2}}$ ${\ Displaystyle [T_ {A}]}$ ${\ Displaystyle [T_ {A} ^ {1}] ~ | ~ [T_ {A} ^ {2}]}$
plenitude: se um prazo é a composição de dois agentes em seguida, deve ser a composição de dois agentes de tal forma que e . ${\ Displaystyle [T_ {A}]}$ ${\ Displaystyle T_ {B} ^ {1} ~ | ~ T_ {B} ^ {2}}$ ${\ Displaystyle T_ {B}}$ ${\ Displaystyle T_ {A} ^ {1} ~ | ~ T_ {A} ^ {2}}$ ${\ Displaystyle [T_ {A} ^ {1}] = T_ {B} ^ {1}}$ ${\ Displaystyle [T_ {A} ^ {2}] = T_ {B} ^ {2}}$