Entscheidungsproblem

Em matemática e ciência da computação, o Entscheidungsproblem (pronunciado [ɛntˈʃaɪ̯dʊŋspʁoˌbleːm], alemão para &# 39;problema de decisão') é um desafio lançado por David Hilbert e Wilhelm Ackermann em 1928. O problema pede um algoritmo que considere, como entrada, uma afirmação e responda "Sim" ou "Não" de acordo com se a declaração é universalmente válida, ou seja, válida em toda estrutura que satisfaça os axiomas.

Teorema da completude

Pelo teorema da completude da lógica de primeira ordem, uma afirmação é universalmente válida se e somente se puder ser deduzida dos axiomas, então Entscheidungsproblem também pode ser visto como pedindo um algoritmo para decidir se uma determinada declaração é demonstrável a partir dos axiomas usando as regras da lógica.

Em 1936, Alonzo Church e Alan Turing publicaram artigos independentes mostrando que uma solução geral para o Entscheidungsproblem é impossível, assumindo que a noção intuitiva de "efetivamente calculável" é capturada pelas funções computáveis por uma máquina de Turing (ou equivalentemente, por aquelas exprimíveis no cálculo lambda). Esta suposição é agora conhecida como a tese de Church-Turing.

Histórico do problema

A origem do Entscheidungsproblem remonta a Gottfried Leibniz, que no século XVII, depois de ter construído uma máquina de calcular mecânica de sucesso, sonhava em construir uma máquina que pudesse manipular símbolos para determinar os valores de verdade de declarações matemáticas. Ele percebeu que o primeiro passo teria que ser uma linguagem formal limpa, e muito de seu trabalho subsequente foi direcionado para esse objetivo. Em 1928, David Hilbert e Wilhelm Ackermann colocaram a questão na forma descrita acima.

Na continuação de seu "programa", Hilbert fez três perguntas em uma conferência internacional em 1928, a terceira das quais ficou conhecida como "Hilbert's Entscheidungsproblem". Em 1929, Moses Schönfinkel publicou um artigo sobre casos especiais do problema de decisão, preparado por Paul Bernays.

Ainda em 1930, Hilbert acreditava que não haveria problemas insolúveis.

Resposta negativa

Antes que a pergunta pudesse ser respondida, a noção de "algoritmo" tinha que ser formalmente definido. Isso foi feito por Alonzo Church em 1935 com o conceito de "calculabilidade efetiva" baseado em seu cálculo λ, e por Alan Turing no ano seguinte com seu conceito de máquinas de Turing. Turing reconheceu imediatamente que esses são modelos de computação equivalentes.

A resposta negativa ao Entscheidungsproblem foi então dada por Alonzo Church em 1935–36 ( Teorema de Church) e de forma independente logo depois por Alan Turing em 1936 (prova de Turing). Church provou que não há função computável que decida, para duas expressões de cálculo λ dadas, se elas são equivalentes ou não. Ele se baseou fortemente no trabalho anterior de Stephen Kleene. Turing reduziu a questão da existência de um 'algoritmo' ou 'método geral' capaz de resolver o Entscheidungsproblem para a questão da existência de um 'método geral' que decide se qualquer máquina de Turing pára ou não (o problema da parada). Se 'algoritmo' é entendido como significando um método que pode ser representado como uma máquina de Turing, e com a resposta a esta última questão negativa (em geral), a questão sobre a existência de um algoritmo para o Entscheidungsproblem também deve ser negativo (em geral). Em seu artigo de 1936, Turing diz: "Correspondendo a cada máquina de computação 'isso' construímos uma fórmula 'Un(it)' e mostramos que, se existe um método geral para determinar se 'Un(it)' é demonstrável, então existe um método geral para determinar se 'isso' sempre imprime 0".

O trabalho de Church e Turing foi fortemente influenciado pelo trabalho anterior de Kurt Gödel em seu teorema da incompletude, especialmente pelo método de atribuir números (uma numeração de Gödel) a fórmulas lógicas para reduzir a lógica à aritmética.

O Entscheidungsproblem está relacionado ao décimo problema de Hilbert, que pede um algoritmo para decidir se as equações diofantinas têm solução. A inexistência de tal algoritmo, estabelecida pelo trabalho de Yuri Matiyasevich, Julia Robinson, Martin Davis e Hilary Putnam, com a peça final da prova em 1970, também implica uma resposta negativa ao Entscheidungsproblem.

Algumas teorias de primeira ordem são algoritmicamente decidíveis; exemplos disso incluem a aritmética de Presburger, campos fechados reais e sistemas de tipo estático de muitas linguagens de programação. Entretanto, a teoria geral de primeira ordem dos números naturais expressa nos axiomas de Peano não pode ser decidida com um algoritmo.

Procedimentos práticos de decisão

Ter procedimentos práticos de decisão para classes de fórmulas lógicas é de grande interesse para verificação de programas e verificação de circuitos. As fórmulas lógicas booleanas puras geralmente são decididas usando técnicas de resolução SAT baseadas no algoritmo DPLL. Fórmulas conjuntivas sobre aritmética linear real ou racional podem ser decididas usando o algoritmo simplex, fórmulas em aritmética linear inteira (aritmética de Presburger) podem ser decididas usando o algoritmo de Cooper ou o teste Omega de William Pugh. Fórmulas com negações, conjunções e disjunções combinam as dificuldades do teste de satisfatibilidade com as da decisão de conjunções; eles são geralmente decididos hoje em dia usando técnicas de resolução SMT, que combinam a resolução SAT com procedimentos de decisão para conjunções e técnicas de propagação. A aritmética polinomial real, também conhecida como teoria dos campos reais fechados, é decidível; este é o teorema de Tarski-Seidenberg, que foi implementado em computadores usando a decomposição algébrica cilíndrica.