Qual a diferença entre computação e matemática?
A resposta para essa questão é derivada do nascimento da computação.
O Programa de Hilbert foi um ambicioso projeto de David Hilbert no início do século XX para fundamentar toda a matemática, que bem na sua base é apenas crença, isto é, "axiomas". Ele tinha quatro principais objetivos:
Objetivos Principais do programa Hilbert
- Formalização: Escrever toda a matemática em uma única linguagem formal precisa.
- Completude: Provar que todas as afirmações matemáticas verdadeiras poderiam ser provadas dentro do sistema.
- Consistência: Provar que o sistema não geraria contradições, usando raciocínio "finitista" (com objetos finitos).
- Decidibilidade: Criar um método para determinar a verdade ou falsidade de qualquer proposição matemática.
O triste para o Hilbert, é que a realidade costuma ser muito dura com os sonhadores, e ocorreu uma ruptura.
A ruptura (Gödel e Turing)
Teoremas de Gödel (1931): Mostraram que sistemas axiomáticos poderosos (como os da matemática) são inerentemente incompletos e não podem provar sua própria consistência, invalidando o objetivo de completude (2) e consistência (3) na matemática.
Teoremas de Turing (1936): Provaram que não existe um algoritmo geral para decidir a verdade de todas as afirmações matemáticas (notadamente o problema de parada), invalidando o objetivo de decidibilidade (4) na matemática.
Um corolário importante é que uma formalização única para a matemática é impossível sem a completude, consistência e decidibilidade, mas demonstrar isso está fora do escopo desta postagem. Interessantes considerações são feitas em Has incorrect notation ever led to a mistaken proof?
A notação como escrevemos em postagem anterior, é de extrema importância.
A matemática, enquanto disciplina unificada, compartilha axiomas e lógicas fundamentais, mas sua aplicação prática é fragmentada por notações que evoluíram organicamente, muitas vezes criando bolsões de conhecimento "incompatíveis". Muitos gostariam de descrever as diversas "matemáticas" como diferentes perspectivas/dialetos da mesma "linguagem universal", em vez de disciplinas fundamentalmente separadas. A questão é que como provado por Gödel e Turing, essa "linguagem universal" não pode existir.
Em outras palavras, a computação nasce da negação da matemática como sonhada na época (anos 1930), e da prova dos principais objetivos de Hilbert serem impossíveis para a matemática.
Mas algo pode cumprir esses quatro objetivos de Hilbert? Sim, esse algo é a computação.
Uma das sementes da computação é a prova de completude de Gödel, ela prova que um algoritmo computacional pode ser completo, principalmente por seu escopo (ao contrário da matemática) ser muito limitado.
Outra é a tese de Church–Turing, reforçada por diversos estudos e contribuições. Todas essas contribuições envolvem provas de que os modelos são computacionalmente equivalentes à máquina de Turing; diz-se que tais modelos são Turing completos. Como todas essas diferentes tentativas de formalizar o conceito de "calculabilidade / computabilidade efetiva" produziram resultados equivalentes, geralmente se assume que a tese de Church-Turing está correta. De fato, Gödel (1936) propôs algo mais forte do que isso; ele observou que havia algo de "absoluto" no conceito. O relevante para esta postagem, é que não apenas que um algoritmo computacional pode ter parada, mas podemos provar se ele termina ou não, cumprindo o conceito de decidibilidade de Hilbert.
A consolidação da computação veio com a prova de corretude, ela estabelece que um algoritmo produz a saída correta para cada entrada, seguindo sua especificação funcional. Ela difere da fase de testes ao garantir o comportamento do código, dividindo-se em corretude parcial (o resultado está correto se o algoritmo acabar) e corretude total (garante que ele termina e está correto). Corresponde às provas de consistência e completude de Hilbert.
A Lógica de Hoare, proposta por C.A.R. Hoare em 1969, é um sistema formal e axiomático que garante que uma linguagem de programação pode ser expressa numa linguagem formal precisa. Ela é fundamental para a verificação formal de algoritmos e desenvolvimento de softwares seguros.
Esses quatro pontos cardiais definem a separação entre computação e matemática: Formalização, Completude, Consistência e Decidibilidade.
Em linguagem simples, sob essa ótica, computação é o antônimo da matemática.
