Existe uma noção sensata de um algoritmo de aproximação para um problema indecidível?

48

Certos problemas são conhecidos por serem indecidíveis, mas, no entanto, é possível progredir na solução deles. Por exemplo, o problema de parada é indecidível, mas é possível progredir na criação de ferramentas para detectar possíveis loops infinitos em seu código. Os problemas de lado a lado são muitas vezes indecidíveis (por exemplo, esse poliomino telha algum retângulo?), Mas novamente é possível avançar o estado da arte nesta área.

O que me pergunto é se existe algum método teórico decente para medir o progresso na solução de problemas indecidíveis, que se assemelha ao aparato teórico desenvolvido para medir o progresso em problemas difíceis de NP. Ou parece que estamos presos a avaliações ad hoc de "eu sei o progresso quando vejo" de quanto avanços específicos avançam nossa compreensão de problemas indecidíveis?

Edit : Enquanto penso sobre esta questão, ocorre-me que talvez a complexidade parametrizada possa ser relevante aqui. Um problema indecidível pode se tornar decidível se introduzirmos um parâmetro e fixarmos o valor do parâmetro. Não tenho certeza se essa observação é de alguma utilidade.

Timothy Chow
fonte
3
.. lembra-me da teoria da interpretação abstrata.
Jagadish
11
[Juntamente com o comentário de Jagadish]: Você pode dar uma olhada no curso 16.399 do MIT : Interpretação abstrata . Especialmente, a Aula 3 pode ser útil para o seu caso.
MS Dousti
6
A medida óbvia da qual você provavelmente não vai gostar é simplesmente pedir várias soluções parciais de acordo com seus domínios (isto é, o conjunto de entradas nas quais elas funcionam). Para que você gostaria de usar a medida?
Andrej Bauer
3
@ Andrej: Deixe-me responder sua pergunta indiretamente. No campo dos problemas difíceis de NP, às vezes temos resultados muito bons da forma: "Essa e tal proporção de aproximação é alcançável e qualquer melhoria adicional é impossível, a menos que P = NP". Ser capaz de provar resultados análogos para problemas indecidíveis interessantes seria bom. Isso nos daria uma noção de se existe alguma barreira intrínseca ao progresso adicional.
Timothy Chow
propor um conceito de "quasialgorithms" com algumas pesquisas na área
vzn

Respostas:

30

No caso do problema de parada, a resposta é "ainda não". A razão é que o método lógico padrão para caracterizar o quão difícil é a prova de término de um programa (por exemplo, análise ordinal) tende a perder muita estrutura combinatória e / ou teórica dos números.

ω

Isso significa que não há uma relação clara entre a força teórica da prova da metalógica na qual você mostra a terminação (isso é muito importante na teoria da reescrita, por exemplo) e as funções que técnicas como a síntese da função de classificação podem mostrar a terminação para .

Para o cálculo lambda, temos uma caracterização precisa da terminação em termos de tipabilidade: um termo lambda está fortemente normalizando se e somente se for tipificável na disciplina do tipo de interseção. Obviamente, isso significa que a inferência de tipo completa para tipos de interseção é impossível, mas também pode fornecer uma maneira de comparar algoritmos de inferência parcial.

Neel Krishnaswami
fonte
6

De uma conversa memorável de uma pessoa que implementou um algoritmo que resolve um problema indecidível: "São necessários 2-3 segundos para todas as entradas que eu tentei".

Sariel Har-Peled
fonte
2

Isso está respondendo mais ao título da pergunta do que ao seu conteúdo, mas você também pode considerar "aproximações" do problema de parada como algoritmos que fornecerão uma resposta correta em quase todos os programas.

A noção de "quase todos" programas só faz sentido se o seu modelo de computação é ideal (no mesmo sentido que para a complexidade de Kolmogorov ), para evitar situações em que a maioria dos seus programas é trivial.

Mn<nϵϵp>0

ρnρn<n

Ted
fonte