Prova informal de um problema insolúvel (com código!)

Chris Wilson está apresentando programação funcional em Ruby . Veja o Tweet que gerou esta postagem aqui . Seus slides (possivelmente revisados ​​desde este post) me fizeram pensar: como alguém pode descrever o Entscheidungsproblem da forma mais simples possível com um exercício de programação?

Entscheidungsproblem, a definição de

Entscheidungsproblem em alemão significa “problema de decisão”; David Hilbert (indiscutivelmente o matemático alemão mais influente do final do século 19 e início do século 20) apresentou o problema como um desafio para seus formidáveis ​​colegas em todo o mundo. O objetivo é implementar um algoritmo que nos diga se uma afirmação matemática específica tem uma prova ou não. No código, isso significa o código que decide se o código é avaliado com 100% de previsibilidade.

O (pseudo) código

/* GoLang */

type FormalLanguage interface{
  Description() rules // describes the language
  Statements() statements // statements of the language
}

func Provable( input FormalLanguage ) output bool {
  // impossible to write algorithm mapping a boolean to each statement
  // of the language
  // the best implementation probably should cause a kernel panic
}

/* Ruby */

module HigherOrderLogic
  def self.provable? statement
    // impossible to write algorithm which returns
    // true iff the statement is provable
    // when correct it should always returns nil!!!
  end
end

A Prova (Informal)

Digamos que tenhamos essa função. Gostaríamos de implementá-lo onde seria mais útil – provavelmente como parte de um algoritmo de otimização (em uma linguagem compilada), como parte do interpretador (em uma linguagem dinâmica), ou talvez como uma ferramenta de meta-teste.

Vamos colocá-lo para trabalhar na cadeia de ferramentas de teste. A função / método “comprovável” poderia informar ao conjunto de testes se a expectativa seria atendida ou não. Uma maneira de fazer isso seria tomando a base de código inteira como uma descrição e um caso de teste como uma instrução. Os resultados de aprovação / reprovação são os óbvios.

Agora, em linguagem comum, o que significa quando um caso de teste retorna “verdadeiro”? Normalmente, atende a alguma expectativa. O que significa quando uma expectativa é atendida? Corresponde a alguns requisitos!

Se escrevêssemos um código que “sabe” como criar expectativas a partir dos requisitos e também “saiba” se atende a essas expectativas com alguma base de código, os testes e a programação seriam redundantes (ou seriam automatizados no sentido de que o código se atualizaria de acordo com os requisitos e expectativas derivadas).

Se chegarmos a este ponto, implementaríamos os algoritmos Entscheidungsproblem para nosso código primeiro ou escreveríamos o código? Se implementarmos os algoritmos, presumimos que já sabemos como o código se parece … e nosso grande objetivo não é alcançado (pontos bônus: por quê?) Se escrevermos o código, então nossa implementação do Entscheidungsproblem é suscetível às menores alterações na base de código (pontos de bônus: por quê?)

Portanto, qualquer implementação do Entscheidungsproblem será insuficiente.