O problema da parada em poema

"No general procedure for bug checks succeeds.
Now, I won’t just assert that, I’ll show where it leads:
I will prove that although you might work till you drop,
you cannot tell if computation will stop."

Algo bem interessante com que eu me deparei recentemente foi uma "demonstração poética" da indecidibilidade do problema da parada — confira na íntegra aqui. Futuramente devo abordar o assunto com mais detalhes, mas por enquanto decidi arriscar e traduzir o poema para português, assim os menos experientes em inglês podem ler também.

A parábola da perscrutação da parada

Uma demonstração da indecidibilidade do problema da parada, por Geoffrey K. Pullum.

(Escola de Filosofia, Psicologia e Linguística, Universidade de Edinburgh).

Um detector de loops é uma ilusão irreal.

E não apenas digo, provarei tal:

Você pode até tentar, trabalhar até cansar,

mas não poderá dizer se o programa irá parar.

Imagine um certo procedimento P,

que em cada chamada permite a você ver

se o procedimento lido, não importa a sua cara,

define um fluxo¹ que em algum momento para.

Ponha no programa os dados importantes.

P faz seu serviço, e após alguns instantes,

(em tempo finito) conclui então

se um loop infinito ocorre ou não.

Se não há nenhum loop, P exibe "Legal".

Quer dizer que o fluxo para, como é usual.

Mas se for detectado o mal irrefreável,

então P exclama "Loop!" - desastre inevitável.

A verdade é que P não pode nem existir,

porque se eu o escrevesse e começasse a agir,

poderia ocasionar algo bem imprudente,

que ignora a lógica e bagunça sua mente.

Meu esquema é simples, um rápido truque.
Definirei um procedimento chamado Q,
que usará as previsões de parada de P
para alimentar um terrível fuzuê.

Seja A um programa qualquer fornecido,
em primeiro lugar faço Q dar ouvido
aos resultados de P, que informa de fato
o comportamento de A, sendo exato².

Se P exibe "Loop!", Q vai logo parar.
Mas do contrário, Q tratará de retornar,
e começar novamente, em um ciclo contínuo,
até o fim do universo em caos repentino.

Mas Q não ficaria isolado na vida;
reservo ao seu futuro outra coisa ainda.
Ao ler o seu código, ele fará o quê?
Qual é o comportamento de Q lido por Q?

Se P  disser "Loop!", Q vai logo parar;
mas P não poderia nunca falhar!
E se Q vai parar, então P diz "Legal",
que faz Q entrar em loop - desastre astral!

Independente de P, Q sempre estará à frente:
Q é esperto e faz P parecer que mente.
Diga o que quiser, P não chega nem perto:
P é certo em falso, e falso em certo!

Eu criei um paradoxo, como se vê -
bastou eu usar o hipotético P.
Ao propor esse P, você caiu da escada;
a pretensão o levou à minha emboscada.

E aonde esse argumento pretende chegar?
Sei que você sabe, não preciso falar.
Um reductio³: Não pode haver algo tão mágico
quanto um procedimento como P, ilógico.

Você nunca encontrará meios mecânicos gerais
que prevejam ações de programas, aliás;
é algo que não pode ser feito. Programadores
estão a sós. Malditos computadores!

Notas da tradução

¹ O fluxo refere-se ao program counter, o "fluxo lógico" do programa. Mais detalhes nesta introdução à lógica de programação.

² Ou seja, Q faz uma chamada a P usando A como argumento.

³ Reductio ad absurdum: consiste em assumir uma premissa e chegar a um resultado contraditório. Conclui-se então que a premissa deve estar errada.