Qual é o objetivo por trás da interpretação abstrata em linguagens de programação?

Agora estou tentando entender melhor o que é "interpretação abstrata" em linguagens de programação. Encontrei um bom capítulo de livro que explica a idéia de estender o domínio com um elemento menos fixo, os quatro axiomas que produzem um ponto fixo para uma função contínua, e assim por diante. Entendo esses detalhes técnicos (embora não tenha muita certeza do que é a "interpretação abstrata" exatamente referente a todo esse esquema).

O que não tenho certeza é o que motiva o uso da interpretação abstrata? É apenas identificar pontos fixos para funções computáveis? A principal motivação advém da recursão na maioria das linguagens de programação?

Também ficaria feliz em ter uma visão geral de alto nível, que é tecnicamente profunda o suficiente para alguém formado em ciência da computação. Acho a página da Wikipedia bastante perturbadora.

A interpretação abstrata é um conceito muito geral e, dependendo de quem você perguntar, receberá explicações diferentes porque conceitos versáteis admitem múltiplas perspectivas. A visão nesta resposta é minha e eu não assumiria que é geral.

Dureza computacional como motivação

Vamos começar com problemas de decisão, cujas soluções têm uma estrutura como esta:

Geralmente, existe um limite inferior rígido de NP no procedimento. A verificação das propriedades semânticas dos programas é ainda indecidível. O que podemos fazer?

Vamos fazer duas observações. Primeiro, às vezes podemos resolver instâncias de problemas específicas, mesmo que não possamos resolver o problema geral. Segundo, aplicativos como a otimização do compilador toleram a aproximação, pois um compilador que elimina algumas, mas nem todas as fontes de ineficiência é útil. Para tornar essa intuição precisa, devemos responder:

1. O que significa formalmente resolver algumas, mas nem todas as instâncias de problemas?
2. Qual é a solução aproximada para um problema de decisão?

Resumo Interpretação Ideia 1: Alterar a declaração do problema

Para mim, uma das principais idéias da interpretação abstrata é alterar a formulação do problema para que, em vez de pedir uma resposta Sim / Não , solicitemos uma resposta Sim / Não / Talvez .

Como conseqüência, todo problema tem uma solução trivial e constante de tempo (saída Talvez ). Agora podemos mudar nossa atenção para derivar um procedimento que nem sempre produz o Talvez . Para retornar às perguntas acima, uma solução que funciona para algumas instâncias de problemas é aquela que retorna Talvez em problemas que não pode resolver. Além disso, Talvez seja uma aproximação de Sim e Não, porque não temos certeza de qual é a resposta.

Essa ideia não se restringe a problemas de decisão. Considere estes problemas relacionados aos programas.

1. Quais linhas de código no programa estão inoperantes (nunca serão executadas)?
2. Quais variáveis ​​no programa têm valores constantes?
3. Quais asserções no programa são violadas?

Em todas essas situações, podemos passar de uma solução exata para uma aproximada, considerando soluções com alguma incerteza.

1. O que é um conjunto de linhas de código que está morto?
2. O que é um conjunto de variáveis ​​no programa que possuem valores constantes?
3. O que é um conjunto de asserções no programa que não é violado?

Os conjuntos produzidos não precisam ser os maiores. Essa idéia é extremamente geral e se aplica a problemas que pouco têm a ver com a análise do programa.

1. $m$$n$$[a,b]$
2. $m$$n$$k$
3. Em vez de solicitar as atribuições satisfatórias para uma fórmula, podemos solicitar um conjunto que contenha as atribuições satisfatórias.

Observe que não apenas mudamos o problema, mas também o generalizamos estritamente, porque uma solução para o problema original ainda é uma solução para o problema modificado. A grande questão não respondida agora é: Como podemos encontrar uma solução aproximada?

Resumo Interpretação da Idéia 2: Caracterização de Ponto Fixo das Soluções Originais

$t$$s$$\mathit{Reach}(s)$$s$$t$$\mathit{Reach}(s)$

$X = \{s\} \cup \{ w ~|~ v \text{ is in } X \text{ and } (v,w) \text{ is an edge}\}$

$n$$n$$s$

A caracterização do ponto fixo é uma decisão de design. Existem muitas caracterizações diferentes de um conjunto de soluções. Cada um deles pode ter vantagens diferentes. No caso de linguagens de programação, temos mais estrutura do que apenas lidar com um gráfico. As equações de ponto fixo com as quais nos preocupamos podem ser definidas por indução na estrutura do programa de entrada. Essa ideia não é específica para programas. Ao aplicar a interpretação abstrata a elementos de uma linguagem estruturada, como gramática, fórmula lógica, programa, expressão aritmética, etc., podemos definir pontos fixos por indução na estrutura de algum objeto sintático.

Ao fornecer essa caracterização de ponto fixo, estamos comprometidos com uma maneira específica de soluções de computação. Na verdade, não calcularemos esse ponto fixo porque é pelo menos tão difícil quanto resolver o problema original, o que nos leva ao próximo passo.

Resumo Interpretação da Idéia 3: Aproximação de Ponto Fixo

$F$$L$$G$$M$$M$$L$$M$$L$

$L$$M$$F$$G$

Você pode achar a intuição por trás da transferência de ponto fixo perspicaz. Podemos pensar em um ponto fixo como o limite de uma cadeia (possivelmente transfinita) de elementos. O cálculo de soluções aproximadas equivale a aproximar esse limite, o que podemos fazer aproximando elementos da cadeia.

$s$$t$$s$$t$

Resumo Interpretação da Idéia 4: Algoritmos de Aproximação de Ponto Fixo

Tudo visto até agora tem sido um resultado matemático da existência. O passo final é calcular a aproximação. Quando a rede de aproximações é finita (ou se a condição da cadeia ascendente / descendente for atendida), podemos usar um procedimento iterativo simples. Se a rede é infinita, um procedimento iterativo pode não ser suficiente, embora a computação de um ponto fixo ainda possa ser decidida. Nessa situação, muitas técnicas são usadas para aproximar ainda mais a solução ou pular para uma solução exata mais rapidamente que um algoritmo de iteração ingênuo. No contexto da computação de uma solução, você ouve termos como ampliação , restrição , iteração de estratégia , aceleração etc.

Sumário

Na minha opinião, a interpretação abstrata fornece uma base matemática para a noção de abstração da mesma maneira que a lógica matemática fornece uma base matemática para o raciocínio. As soluções para muitos problemas com os quais nos preocupamos têm caracterizações como pontos fixos. Essa observação não se restringe a problemas de linguagem de programação e mesmo a ciência da computação. Soluções aproximadas podem ser caracterizadas como aproximações de pontos fixos e são computadas com algoritmos especializados. Essas caracterizações e algoritmos explorarão a estrutura da instância do problema. No caso de programas, essa estrutura é dada pela sintaxe da linguagem.

Computar aproximações para problemas que não possuem uma métrica natural é uma arte constantemente desenvolvida e refinada pelos profissionais. A interpretação abstrata é uma teoria matemática para a ciência por trás desta arte.

Referências Existem vários bons tutoriais sobre interpretação abstrata que você pode ler.

1. Uma introdução casual à Interpretação Abstrata , Patrick Cousot (trabalho conjunto com Radhia Cousot), Workshop sobre Biologia de Sistemas e Métodos Formais (SBFM'12)
2. Uma introdução suave à verificação formal de sistemas de computador por interpretação abstrata , Patrick e Radhia Cousot, Marktoberdorf Summer School 2010.
3. Aula 13: Abstração Parte I , Patrick Cousot, Interpretação abstrata, Curso MIT.
4. Introdução à Interpretação Abstrata , Samson Abramsky e Chris Hankin, Interpretação Abstrata de Linguagens Declarativas, 1987.
5. Interpretação abstrata e aplicação a programas lógicos , Patrick e Radhia Cousot, 1992. As duas primeiras seções têm uma visão geral geral de alto nível, com vários exemplos.

Concordo que muitas vezes é difícil extrair o ponto principal de todos esses detalhes. (De fato, meu grande problema com todos os tratamentos de interpretação abstrata que já vi é que eles apresentam tantas máquinas sem motivá-las.)

Aqui está como eu penso sobre isso:

A interpretação abstrata está executando programas, aproximadamente, em grandes conjuntos de entradas de uma só vez.

Isso não cobre tudo, mas sustenta-se bem em geral.

O exemplo canônico é avaliar expressões aritméticas para determinar o sinal do resultado. Você pode imaginar uma máquina hipotética, infinitamente rápida, capaz de avaliar uma expressão em cada entrada positiva e retornar o conjunto de resultados. Se você tivesse um desses, em princípio, poderia determinar coisas como "este programa retorna números positivos quando recebe números positivos".

Mas é claro que você realmente não tem essa máquina. Você está preso na vida real, então você deve fazer a mesma coisa simbolicamente , o que pode dar respostas exatas às vezes, mas geralmente falha, ou aproximadamente , de uma maneira que sempre retorna respostas, mas elas podem não ser exatas. O último é o que a interpretação abstrata faz.

$\{neg,zero,pos\}$$\{\{...,-2,-1\},\{0\},\{1,2,...\}\}$

$add : pos \times pos \to pos$

$add : pos \times pos \to pos$$add(a,b)$$a$$b$$pos \times neg \to (pos \sqcup zero \sqcup neg)$$\sqcup$

$\sqcap$$\sqsubseteq$

Quando você quiser provar que sua interpretação abstrata é a mais rígida possível, você precisará de uma conexão de Galois para formalizar essa correspondência. Apenas ter um garante que, para qualquer conjunto concreto, exista um conjunto abstrato mais rígido.

$\bot$

IOW, o que você identificou como a motivação para a interpretação abstrata é realmente a motivação para o mecanismo necessário para fazer a interpretação abstrata em linguagens equivalentes a Turing. A motivação real é útil resumir o comportamento dos programas, executando-os em várias entradas de uma só vez.