Solucionando o Insolucionavel (Solving the Unsolvabe)

Fonte aqui

Autoria de Moshe Y. Vardi

Communications of the ACM
Vol. 54 No. 7, Page 5
10.1145/1965724.1965725 

Em 16 de junho de 1902, o filósofo britânico Bertand Russel enviou uma carta a Gottlob Frege, um lógico alemão, na qual ele argumento, por usar o que se tornou conhecido por "Paradoxo de Russel", que o sistema lógco de Frege era inconsistente. A carta lançou uma "Crise Fundamental" na matemática, engatilhando uma procura quase angustiante por fundações apropriadas para Matemática. Em 1921, David Hilbert, o preeminete matemático alemão, lançou um programa de pesquisa objetivando eliminar "as questões fundamentais de uma vez por todas". O Programa de Hilbert falhou;em 1931, o lógico austríaco Kurt Goedel provou dois teoremas de incompletude que provaram a futilidade do Programa de Hilbert.

Um elemento no Programa de Hilbert era a mecanização da Matemática. "Uma vez que um formalismo lógico for estabelecido, algupem pode esperar que um tratamento de fórmulas lógicas sistemático, ou pode-se dizer computacional, é possivel, o que poderia de certa forma corresponder à teoria das equações em Álgebra." Em 1928, Hilbert e Ackerman apresentaram o "Entscheidungsproblem" (Problema da Decisão), que perguntava se há um algoritmo para verificar se uma dada fórmula lógica (em lógica de primeira ordem) é válida, isto é, necessariamente com valor-verdade verdadeiro. Em 1936-1937, Alonzo Church, um lógico americano, e Alan Turing, um lógico britânico, provaram independentemente que o problema da Decisão para lógica de primeira ordem é insolucionavel; não há algoritmo que possa verificar a validade de fórmulas lógicas. O Teorema de Church-turing pode ser visto como o nascimento da Ciência da Computação teórica. Para resolver o problema, Church e Turing introduziram modelos computacionais, funções recursivas e máquinas de Turing, respectivamente, e provaram que o Problema da Parada - verificar se uma função recursiva ou máquina de Turing produz uma saída para uma entrada fornecida - é insolucionável.

A insolucionabilidade do Problema da Parada, provado justamente enquanto Konrad Zuse na Alemanha e John Atanasoff e Clifford Berry nos EUA estavam embarcando na construção de seus computadores digitais - o Z3 e o Computador Atanasoff-Berry - singificou que a Ciência da Computação nasceu com um conhecimento da limitação inerente da computação mecânica. Enqaunto Hilbert acreditava que "todo problema matemático é necessariamente capaz de uma solução estrita", nós sabemos que o insolucionavel é uma barreira que não pode ser quebrada. Quando eu encontrei a insolucionabilidade na condição de um estudante recém formado, isso parecia pra mim um muro intransponivel. Muito da minha pesquisa com o passar dos anos foi dedicado a delinear as fronteiras entre o solucionavel e o insolucionavel.

É bem notavel, no entanto, que a edição de maio de 2011 do Communications incluiu um artigo de Byron Cook, Andreas Podelski e Andrey Rybalchenko entitulado "Proving Program Termination" (Provando Término de Programas, pg. 88), no qual eles argumentam que "em contraste com a crença popular, provar o término de programas não é sempre impossivel". Com certeza eles entenderam errado! O Problema da Parada (término é o mesmo que parada) é insolucionavel! Com certeza Cook et al. não reivindicam terem resolvido o Problema da Parada. O que eles descrevem no artigo é um novo método para provar o término de programas. O método em si não tem garantia de término - se tivesse, isto contradiria o Teorema de Church-Turing. O que Cook et al. ilustram é que o método é notavelmente effetivo na prática e pode dar conta de um grande número de programas reais. De fato, uma ferramenta de software chamada Terminator, usada para implementar seu método, tem sido capaz de encontrar alguns erros de término muito sutis em programas da Microsoft.

Eu acredito que este progresso notavel em provar o término de programas  nos força a reconsiderar o significado de insolucionabilidade. Em meu editorial de novembro/2010, "On P, NP, and Computational Complexity" (Sobre Complexidade Computacional, P e NP), apontei que problemas NP-completos, tais como a Satisfabilidade Booleana, não parecem tão intrataveis hoje como pareciam no início da década de 80, com solucionadores (solvers) SAT industriais mostrando desempenho impressinavel na prática. "Proving Program Termination" mostra que programas insolucionaveis podem não ser tão insolucionaveis quanto pensávamos. Na teoria, insolucionabilidade realmente impõe uma barreira rígida em computabilidade, mas é menos claro o quão significante esta barreira é na prática. Ao contrário do Problema de Collatz, descrito no artigo de Cook et al., a maioria dos programas reais, se eles (não) terminam*, o fazem por razões simples, porque programadores nunca concebem os motivos sofisticados e profundos para término. Assim não deveria ser chocante que uam ferramenta como Terminator possa provar término para tais programas.

Por último, desenvolvimento de software é uma atividade de engenharia, não uma atividade matemática. Design de engenharia e técnicas de análise não fornecem garantia matemática, fornecem confiança. Não precisamos resolver o Problema da Parada, nós só precisamos estar aptos para raciocinar com sucesso sobre término de programas reais. É hora de desistir da nossa "fobia de insolucionabilidade". É hora de resolver o insoluvel.

Do autor do blog: este texto achei bom demais para deixar apenas no lugar onde estava. Agradeço a Mr. Yardi pela autoria, ao Prof. Lamb pela divulgação, e aqui deixo meu pedido pra que parem de pensar apenas de maneira a ver limites. Se há limite de ferramentas para um determinado problema, é hora de ver novos usos para as ferramentas que temos. As definições servem para organizar, e os limites dados a ela são, na maioria, para restringir um domínio de problema ou imagem de solução. Com já dizem por aí: "era impossivel até que alguém que não sabia foi lá e fez".

O (não*) deixei aqui por achar que houve erro na redação original do texto, mas deixo a intepretação para vocês e concluam se é necessário ou não. Caso queiram alguma coisa de links relacionados, podem deixar nos comentários que tentarei colocar algo sobre alguma coisa do que foi citado no texto.