Infelizmente, há muitas coisas acontecendo aqui. Então, é fácil misturar as coisas. O uso de "completo" em "total plenitude" e "abstração total" refere-se a idéias completamente diferentes de plenitude. Mas há também alguma conexão vaga entre eles. Então, essa será uma resposta complicada.
Completude total : "Som e completação" é uma propriedade que você deseja que uma lógica tradicional tenha com relação à sua semântica. Solidez significa que tudo o que você pode provar na lógica é verdadeiro no modelo semântico. Completude significa que tudo o que é verdadeiro no modelo semântico é comprovável na lógica. Dizemos que uma lógica é sólida e completa para um modelo semântico específico. Quando chegamos à lógica construtiva, como a teoria do tipo Martin-Lof ou a lógica linear, nos preocupamos não apenas com a comprovação das fórmulas, mas também com as provas. Uma fórmula comprovável pode ter muitas provas e uma lógica construtiva deseja mantê-las separadas. Portanto, uma semântica para uma lógica construtiva envolve especificar não apenas se uma fórmula é verdadeira, mas também alguma noção semântica abstrata de "prova" ("evidência") para sua verdade. Abramsky e colegas cunharam o termo "plenitude total" para significar que as provas na lógica podem expressar todas as provas semânticas no modelo. Portanto, "completo" se refere a provas aqui. Uma lógica "completa" pode provar tudo o que precisa. Uma lógica "totalmente completa" possui todas as provas de que precisa. Portanto, "completude total" significa "completude construtiva" ou "completude de prova". Isso não tem nada a ver com abstração completa.
Abstração completa : "Adequado e totalmente abstrato" é uma propriedade que você deseja para o modelo semântico de uma linguagem de programação. (Observe a primeira diferença: agora estamos lidando com as propriedades do modelo semântico, não as propriedades da linguagem!) Adequação significa que, sempre que dois termos têm o mesmo significado no modelo semântico, eles são observacionalmente equivalentes na linguagem de programação (com relação a alguma noção de execução). Abstração completa significa que, se dois termos são observacionalmente equivalentes, eles têm o mesmo significado no modelo semântico. Essas idéias podem estar relacionadas à solidez e integridade, mas de uma maneira um tanto artificial. Se pensarmos no modelo semântico de uma linguagem de programação como uma "lógica" ou um "método de prova" para falar sobre equivalência observacional, adequação significa que esse método de prova é sólido; abstração completa significa que esse método de prova está completo. Não há noção de "plenitude total" aqui, porque ninguém ainda produziu um modelo semântico que represente ummétodo de prova. (Mas, tal coisa é teoricamente possível, e um dia desses alguém poderá fazê-lo.)
No seu caso, você está interessado em traduções e não em modelos semânticos. As propriedades de adequação e abstração total podem ser estendidas para lidar com traduções da seguinte maneira. Você pensa na língua-alvo como seu "modelo semântico", isto é, um formalismo que você entende completamente. Nesse caso, você tem alguma noção de equivalência para isso. Então, dizemos que a tradução é adequada se, sempre que as traduções de dois programas de origem forem equivalentes no idioma de destino, elas forem observacionalmente equivalentes no idioma de origem. Dizemos que é totalmente abstrato se, sempre que dois programas de origem são observacionalmente equivalentes no idioma de origem, suas traduções são equivalentes no idioma de destino.
Na realidade, não conheço nenhum idioma de destino que realmente "entendamos". Tudo o que sabemos é outra noção de equivalência observacional para a língua-alvo. Nesse caso, a tradução é adequada se a equivalência observacional das traduções no idioma de destino implica equivalência observacional no idioma de origem.
A tradução é totalmente abstrata se a equivalência observacional dos termos no idioma de origem implicar a equivalência observacional das traduções no idioma de destino.
M ≅ N ⟹ τ ( M ≅
τ(M)≅τ(N)⟹M≅N
Alguns autores consideram "tradução totalmente abstrata" para significar a combinação dessas duas propriedades:
M ≅ NM≅N⟹τ(M)≅τ(N)
M≅N⟺τ(M)≅τ(N)
Egger e cols. Parecem estender da mesma forma a idéia de completude total às traduções. Em sua configuração, fórmulas são tipos e provas são termos. A tradução deles traduz tanto tipos quanto termos. Eles chamam sua tradução totalmente concluída se a tradução de um tipo tem apenas os termos que são obtidos por traduzir os termos originais do tipo A .
∀ N : τ ( A ) .AA
∀N:τ(A).∃M:A.τ(M)=N
Agora, a vaga conexão entre a plenitude total e a abstração total. Provar que um modelo semântico ou uma tradução é totalmente abstrato geralmente envolve alguma definibilidade. Isso ocorre porque nossos idiomas são geralmente de ordem superior. Portanto, se o modelo semântico ou a linguagem de destino tiver muitos "contextos", ele será capaz de cutucar nossos termos ou significados semânticos de maneiras indesejáveis e estragar sua equivalência. "Maneiras indesejáveis" significa que a própria linguagem de programação não pode cutucá-las. Portanto, para obter abstração completa, precisamos garantir que os "contextos" disponíveis no modelo semântico ou no idioma de destino sejam provenientes dos que estão no idioma de origem de alguma forma. Observe que isso se refere à propriedade completa.
Por que queremos essas propriedades? Tem nadaa ver com compiladores! Queremos essas propriedades para afirmar que o idioma de origem é incorporado ao idioma de destino. Se estivermos satisfeitos com um idioma de destino específico (como sendo limpo, compreensível, de alguma forma fundamental ou dado por Deus), então, se o idioma de origem se incorporar a ele, podemos afirmar que não há nada novo no idioma de origem. É apenas um fragmento da língua-alvo que conhecemos e amamos. É apenas açúcar sintático. Portanto, as traduções totalmente abstratas são dadas pelas pessoas para estabelecer que os idiomas-alvo específicos são ótimos. Às vezes, eles também são dados por pessoas que têm uma linguagem grande ou complicada para lidar. Portanto, em vez de definir uma semântica diretamente, eles a traduzem para uma linguagem principal e, em seguida, fornecem a semântica para a linguagem principal. Por exemplo, o relatório Haskell faz isso. Mas a abstração completa dessas traduções raramente é comprovada porque os idiomas de origem são grandes e complicados. As pessoas acreditam que a tradução é boa.
Mais uma vez, isso não tem nada a ver com compiladores. Compiladores raramente são adequados ou totalmente abstratos. E eles não precisam ser! Tudo o que um compilador precisa fazer é preservar o comportamento de execução de programas completos. O idioma de destino de um compilador geralmente é enorme, o que significa que ele tem muitos contextos que podem atrapalhar a equivalência. Portanto, programas equivalentes no idioma de origem quase nunca são equivalentes ao contexto quando compilados.
Resumo: integralidade completa significa que a função de interpretação não é apenas completa, mas também adjetiva nos programas. A abstração completa não requer requisitos de sujidade.
ContextosΓ no idioma de origem para contextos
[[ Γ ]] no idioma de destino.
Programas em contextoY ⊢ P: α para programas em contexto [[ Γ ]] ⊢ [[ P]] : [[ α ]] .
Em uma interpretação categórica, os dois primeiros mapas colapsam em um. A função de interpretação pode ter várias propriedades, por exemplo, pode ser de composição, preservar terminação ou ... Abstração completa é uma dessas propriedades. Lembre-se de que a abstração completa de[[ . ]]
significa que
para todosP, Q . Aqui≅S is the
chosen notion of typed program equivalence for the source
language while ≅T plays that role for the target language. More precisely, because we are in a typed setting,
Now full abstraction does not imply that[[.]]
is surjective on types, contexts or programs in context.
Full completeness means that the map[[.]] is (complete and) surjective on
programs in context for all definable contexts and definable types,
i.e. any program [[Γ]]⊢Q:[[α]] in the target
language is the denotation of some Γ⊢P:α in the
source language, i.e. Q=[[P]] . Note that this does not
require [[.]] to be surjective on types and contexts, because
that property rarely holds in the interpretations we are
typically interested in.
fonte