O problema da parada é decidível para programas puros em um computador ideal?

É bastante simples entender por que o problema da parada é indecidível para programas impuros (ou seja, aqueles que têm E / S e / ou estados dependentes do estado global da máquina); mas intuitivamente, parece que a interrupção de um programa puro em um computador ideal seria decidida por, por exemplo, análise estática.

Este é realmente o caso? Caso contrário, quais são alguns contra-exemplos ou documentos que refutam essa reivindicação?

Aqui está uma prova de indecidibilidade por redução do problema da parada.

Redução: Dada uma máquina e uma entrada x , construa uma nova Máquina de Turing H que não leia nenhuma entrada, mas grava M e x na fita e simula M em x até M parar.$M$$x$$H$$M$$x$$M$$x$$M$

O comportamento desta nova máquina é independente da fita de entrada; portanto, é uma máquina de Turing pura, na qual apenas a análise estática é aplicável. Se a análise estática fosse suficiente, poderia mostrar se H para , o que mostraria se M para x , o que resolveria o problema de parada de máquinas impuras, que sabemos ser indecidíveis e, portanto, seu problema também é indecidível.$H$$H$$M$$x$

Não, não é e, além disso, não depende de E / S.

Contra-exemplo simples: escreva um programa para encontrar um número ímpar perfeito (este é um problema em aberto: ainda não sabemos se existe algum) - ele não recebe nenhuma entrada e não executa tarefas impuras ; pode parar quando encontra um ou pode funcionar infinitamente (no caso de esse número não existir). Agora, se a análise estática fosse poderosa o suficiente para determinar o caso de parada, ela seria usada para responder a essa (e muitas outras perguntas), onde parar significaria a existência positiva de um número assim e não parar significaria que não existe esse número, mas infelizmente a análise estática não é tão poderoso.

A prova clássica por diagonalização é uma máquina pura , não apenas uma máquina de Turing pura, mas também não depende de "problemas em aberto".

Por exemplo, uma máquina de Turing que executa a Conjectura de Collatz tem um status de interrupção desconhecido, mas que depende de nossa ignorância sobre a Conjectura de Collatz, um dia poderíamos provar que Collatz estava certo e então poderíamos decidir o status de parada da conjectura (Para algumas entradas, não para ou sempre pára).

Portanto, a Conjectura Collatz já pode responder à sua pergunta (pelo menos temporariamente), mas depende de algo que não sabemos . Em vez disso, a prova clássica é um problema resolvido: já sabemos que isso é indecidível .

Apenas para constar, a prova padrão da indecidibilidade do problema de parada se baseia na mesma idéia que o quines: que é possível escrever um programa cujo subdomínio é avaliado segundo o código fonte de todo o programa. Então, se houvesse uma função haltsque, dado o código-fonte de um programa, retornasse True se esse programa interrompesse todas as entradas e False caso contrário, este seria um programa legal:

prog() = if halts "prog" then prog() else ()

onde "prog"haveria alguma expressão avaliada no código-fonte prog; no entanto, você pode ver rapidamente queprog para (para todas as entradas) se não parar, o que é uma contradição. Nada nesta prova depende de E / S de forma alguma (você precisa de E / S para escrever um quine?).

A propósito, você pode procurar em "E / S baseada em diálogo" para obter mais evidências de que a E / S é totalmente irrelevante para o seu problema (basicamente, programas que executam E / S podem ser reduzidos a programas que recebem entrada como argumentos funcionais (explícitos) e retornam a saída como resultados adicionais (explícitos) em uma linguagem lenta). Infelizmente, não consigo encontrar uma página razoável e sem preconceitos (ou pró-diálogo) na Web no momento.