Exemplo de um algoritmo que não possui uma prova de correção

Nós temos a lógica Hoare. Por que ainda é possível que um algoritmo esteja correto, mas não há provas de que esteja correto? Suponha que o algoritmo seja expresso em C. Em seguida, podemos argumentar passo a passo que ele está fazendo o que deveria fazer.

Então, minha pergunta é:

Dê-me um exemplo de um algoritmo correto, mas que não possui uma prova de correção.

Edição: Eu acho que um pouco de fundo pode ajudar a esclarecer onde estou indo. Deixe-me citar Scott Aaronson:

Desde a década de 1970, especula-se que P NP possa ser independente (isto é, nem provável nem refutável) dos sistemas de axioma padrão da matemática, como a teoria dos conjuntos de Zermelo-Fraenkel. Para ser claro, isso significaria que tanto$\ne$

1. não existe um algoritmo de tempo polinomial para problemas completos de NP, mas nunca podemos provar isso (pelo menos não em nossos sistemas formais usuais), ou então

2. um algoritmo de tempo polinomial para problemas NP-completos faz existir, mas de qualquer nunca podemos provar que ele funciona, ou nunca podemos provar que ele pára em tempo polinomial.

Estou me referindo à segunda possibilidade. Como Aaronson pode listá-lo com tanta confiança como uma possibilidade, acho que deve haver um exemplo existente do tipo 2. É por isso que estou fazendo essa pergunta. Mas parece que uma resposta rápida e clara não está à vista.

Aqui está um algoritmo para a função de identidade:

• Entrada: $n$
• Verifique se o º cadeia binária codifica uma prova de 0 > 1 em ZFC, e se assim for, a saída n + $n$$0 > 1$$n+1$
• Caso contrário, a saída $n$

A maioria das pessoas suspeita que esse algoritmo calcule a função de identidade, mas não sabemos e não podemos prová-lo na estrutura de matemática comumente aceita, o ZFC .

A maioria dos algoritmos não foi provada correta na lógica Hoare. A principal razão é que essas provas de correção são extremamente caras a partir de janeiro de 2017, provavelmente por várias ordens de grandeza em comparação com a 'mera' programação. Há muito trabalho em andamento para reduzir esse custo pela automação, mas é uma luta árdua.

Outra razão pela qual um algoritmo pode não ter uma prova de correção, e mais relevante na prática do que os fenômenos de incompletude mencionados por Yuval e chi, é que talvez não saibamos o que é essa especificação. Este problema tem duas dimensões.

• Os clientes não sabem o que querem. Esse é um problema bem conhecido na engenharia de software, e os engenheiros de software desenvolveram muitas abordagens para lidar com isso.

• $n$variando acima dos números naturais, e os adversários são máquinas de Turing com probabilidade probabilística polinomial. De acordo com o meu conhecimento (corrija-me se estiver errado), existe uma incompatibilidade entre teoria e prática, e algoritmos concretos como AES e SHA256 não estão completamente dentro do alcance dessas especificações teóricas. Eu não acho que exista uma especificação completa para tais algoritmos, portanto, não podemos, em princípio, verificá-los no sentido, por exemplo, da lógica Hoare.

$P(n)$$P(0)$$P(1)$$P(2)$$\forall n\in \mathbb{N}.\ P(n)$

$M$$n$$P(n)$$M$$\forall n.\ P(n)$$M$$\forall n.\ P(n)$

Problema: Imprima "Sim" se todo número par ≥ 4 for a soma de dois números primos e "Não" se houver um número par ≥ 4 que não seja a soma de dois números primos.

Algoritmo: Imprimir "Sim"

A maioria das pessoas pensa que o algoritmo está correto. Não há nenhuma prova conhecida, e é bem possível que não é nenhuma prova.

Qualquer algoritmo que esteja correto, mas não sabemos quanto tempo leva para executar, pode ser transformado em um algoritmo que pára em um período de tempo garantido, mas não temos certeza se está correto.

$n$$n+1$$0$$\log(n)^2$$0$$\sqrt{n}$

$P=NP$