-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 O Teorema da Parada, prova a indecidibilidade, para qualquer programa. É um teorema. O Teorema de Goedel não é "meramente" matemático. É um teorema! "Meramente" matemático é um termo novo para mim. Não sei o que significa. Nem vou lhe pedir para explicar.
A referência a Goedel foi para lembrar da incompletude de sistemas formais. Uma linguagem de programação é um sistema formal. Logo, a linguagem de programação é incompleta. Portanto, cuidado quando usá-la. A aritmética (ou a matemática) é incompleta, portanto, cuidado ao usá-la. O Teorema da Parada, não me parece ser de Turing (Turing, provou que ele não tem solução). Turing provou usando sua máquina (a famosa máquina de Turing, importantíssima para os teóricos de complexidade de algorítmos). Mostrou, na realidade que não se pode criar um procedimento efetivo (do ponto de vista da Tese de Church). Provado, ele passou de uma conjectura, para teorema. Qual a visão prática de Goedel e Turing x o Teorema da Parada? Nenhum progamador sério, pequeno, grande ou em equipe irá desenvolver programas achando que ele estará correto. Um bom programador, pratica a humildade, claro. E, leva em conta alguns colorários: C1. Programar é difícil. C2. Programar é uma arte. C3. Não é possível desenvolver procedimentos automáticos para provar que um programa está correto. (Os grandes "players" não são malucos. Portanto, não gastam dinheiro procurando por isso. O que eles devem ter é algo que indique com grande chance, que um programa "pode" estar correto. Ou alguma ferramenta parecida.) ... Cn. Outros. Um pequeno programa é uma exceção. Algum programa (como esse que você falou, talvez), com o espírito acadêmico (principalmente), pode tratar exceções. O que não deixa de ter validade empírica, mesmo sabendo da existência do Teorema da Parada. Assim como Pitagoras, que achou a nossa conhecida solução para a**2 + b**2 = c**2. Você iria tentar resolver a**n + b**n = c**n, para n=3, sabendo que existe um Teorema (provado, em 1965) dizendo que qualquer equação dessas para n >= 3, não tem solução? Não fiz a abordagem com o objetivo de criar um debate acadêmico. Somente para responder ao Davi. []s, Julião Jean Everson Martina escreveu: > Voce está misturando completamente as coisas. Os Teoremas de > imcompletude de Goedel não tem nada a ver com a história. Na verdade a > aplicação de Goedel é meramente matemática e em computação sua > aplicação é restrita teorema de parada de Touring. Mas o teorema de > parada também não se aplica nesse caso porque ele só trata se > programas com entrada nula tem ou não parada, o que não quer dizer que > todos os programas não tem parada. Existem programas que tem sim > parada garantida (estão corretos), por exemplo o Hello World que você > mencionou > > Eu conheço (pessoalmente) o pessoal de New South Wales e o projeto > prova a decidibilidade de todas as entradas de todas as rotinas > implementadas pelo micro-kernel de forma indutiva. Voce pode verificar > a prova você mesmo, usando o Isabelle. > > Pra finalizar, se o que você escreveu fosse verdade, a Intel, a > Nvidia, a Microsoft, a NSA americana e muitos outros players enormes > do mercado não poderiam usar usar provadores de teoremas pra garantir > decidibilidade. > > Nas boas escolas de computação hoje, se ensina, além de lógica, também > semântica e provadores de teoremas. Pena que o Brasil está anos atras > em métodos formais aplicados. > > > Jean -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.2.2 (MingW32) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iD8DBQFK5N/j0m/vNWbSX14RAufMAKCbQ0poH+CZyo5iA/QdfIer4mZL1ACgrbQM 8N7TnXBFgPK1RvFijiD5n8g= =wcYB -----END PGP SIGNATURE----- ------------------------- Histórico: http://www.fug.com.br/historico/html/freebsd/ Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd