The Deep Link Equacionando Provas Matemáticas e Programas de Computador | Revista Quanta

Algumas descobertas científicas são importantes porque revelam algo novo – a estrutura de dupla hélice do ADN, por exemplo, ou a existência de buracos negros. No entanto, algumas revelações são profundas porque mostram que dois conceitos antigos, antes considerados distintos, são na verdade os mesmos. Tomemos como exemplo as equações de James Clerk Maxwell que mostram que a eletricidade e o magnetismo são dois aspectos de um único fenômeno, ou a ligação da gravidade com um espaço-tempo curvo na relatividade geral.

A correspondência Curry-Howard faz o mesmo, mas numa escala maior, ligando não apenas conceitos separados dentro de um campo, mas disciplinas inteiras: Ciência da Computação e lógica matemática. Também conhecido como isomorfismo de Curry-Howard (um termo que significa que existe algum tipo de correspondência um-para-um entre duas coisas), estabelece uma ligação entre provas matemáticas e programas de computador.

Dito de forma simples, a correspondência Curry-Howard postula que dois conceitos da ciência da computação (tipos e programas) são equivalentes, respectivamente, a proposições e provas – conceitos da lógica.

Uma ramificação desta correspondência é que a programação – muitas vezes vista como uma arte pessoal – é elevada ao nível idealizado da matemática. Escrever um programa não é apenas “codificar”, torna-se um ato de provar um teorema. Isto formaliza o ato de programar e fornece maneiras de raciocinar matematicamente sobre a correção dos programas.

A correspondência leva o nome dos dois pesquisadores que a descobriram de forma independente. Em 1934, o matemático e lógico Haskell Curry notou uma semelhança entre as funções na matemática e a relação de implicação na lógica, que assume a forma de declarações “se-então” entre duas proposições.

Inspirado pela observação de Curry, o lógico matemático William Alvin Howard descobriu uma ligação mais profunda entre computação e lógica em 1969, mostrando que executar um programa de computador é muito parecido com simplificar uma prova lógica. Quando um programa de computador é executado, cada linha é “avaliada” para produzir uma única saída. Da mesma forma, em uma prova, você começa com declarações complexas que podem ser simplificadas (eliminando etapas redundantes, por exemplo, ou substituindo expressões complexas por outras mais simples) até chegar a uma conclusão – uma declaração mais condensada e sucinta derivada de muitas declarações intermediárias. .

Embora esta descrição transmita um sentido geral da correspondência, para compreendê-la completamente precisamos aprender um pouco mais sobre o que os cientistas da computação chamam de “teoria dos tipos”.

Comecemos com um famoso paradoxo: numa aldeia vive um barbeiro que faz a barba todos os homens que não se barbeiam, e só eles. O barbeiro se barbeia? Se a resposta for sim, então ele não deve se barbear (porque ele só faz a barba de homens que não se barbeiam). Se a resposta for não, então ele deve se barbear (porque ele faz a barba de todos os homens que não se barbeiam). Esta é uma versão informal de um paradoxo que Bertrand Russell descobriu ao tentar estabelecer os fundamentos da matemática usando um conceito chamado conjuntos. Ou seja, é impossível definir um conjunto que contenha todos os conjuntos que não se contêm sem encontrar contradições.

Para evitar esse paradoxo, mostrou Russell, podemos usar “tipos”. Grosso modo, são categorias cujos valores específicos são chamados de objetos. Por exemplo, se existe um tipo chamado “Nat”, que significa números naturais, seus objetos são 1, 2, 3 e assim por diante. Os pesquisadores normalmente usam dois pontos para denotar o tipo de objeto. O número 7, do tipo inteiro, pode ser escrito como “7: Inteiro”. Você pode ter uma função que pega um objeto do tipo A e cospe um objeto do tipo B, ou uma que combina um par de objetos que eram do tipo A e do tipo B em um novo tipo, chamado “A × B”.

Uma forma de resolver o paradoxo, portanto, é hierarquizar esses tipos, de modo que possam conter apenas elementos de “nível inferior” aos deles. Então um tipo não pode conter a si mesmo, o que evita a autorreferencialidade que cria o paradoxo.

No mundo da teoria dos tipos, provar que uma afirmação é verdadeira pode parecer diferente do que estamos acostumados. Se quisermos provar que o inteiro 8 é par, então é uma questão de mostrar que 8 é de fato um objeto de um tipo específico chamado “Par”, onde a regra para pertinência é ser divisível por 2. Depois de verificar que 8 é divisível por 2, podemos concluir que 8 é de fato um “habitante” do tipo Even.

Curry e Howard mostraram que os tipos são fundamentalmente equivalentes às proposições lógicas. Quando uma função “habita” um tipo — isto é, quando você consegue definir com sucesso uma função que é um objeto daquele tipo — você está efetivamente mostrando que a proposição correspondente é verdadeira. Portanto, funções que recebem uma entrada do tipo A e fornecem uma saída do tipo B, denotada como tipo A → B, devem corresponder a uma implicação: “Se A, então B”. Por exemplo, tomemos a proposição “Se está chovendo, então o chão está molhado”. Na teoria dos tipos, esta proposição seria modelada por uma função do tipo “Raining → GroundIsWet”. As formulações de aparência diferente são, na verdade, matematicamente iguais.

Por mais abstrata que possa parecer essa ligação, ela não só mudou a forma como os profissionais da matemática e da ciência da computação pensam sobre o seu trabalho, mas também levou a diversas aplicações práticas em ambos os campos. Para a ciência da computação, fornece uma base teórica para a verificação de software, o processo de garantir a correção do software. Ao enquadrar os comportamentos desejados em termos de proposições lógicas, os programadores podem provar matematicamente que um programa se comporta conforme o esperado. Ele também fornece uma base teórica sólida para projetar linguagens de programação funcionais mais poderosas.

E para a matemática, a correspondência levou ao nascimento de assistentes de prova, também chamados de provadores de teoremas interativos. São ferramentas de software que auxiliam na construção de provas formais, como Coq e Lean. No Coq, cada etapa da prova é essencialmente um programa, e a validade da prova é verificada com algoritmos de verificação de tipo. Os matemáticos também têm usado assistentes de prova - notadamente, o provador do teorema lean — formalizar a matemática, o que envolve a representação de conceitos, teoremas e provas matemáticas num formato rigoroso e verificável por computador. Isso permite que a linguagem, por vezes informal, da matemática seja verificada por computadores.

Os pesquisadores ainda estão explorando as consequências dessa ligação entre matemática e programação. A correspondência Curry-Howard original funde a programação com um tipo de lógica chamada lógica intuicionista, mas acontece que mais tipos de lógica também poderiam ser passíveis de tais unificações.

“O que aconteceu no século desde a descoberta de Curry é que continuamos descobrindo cada vez mais casos em que 'o sistema lógico X corresponde ao sistema computacional Y'”, disse Michael Clarkson, cientista da computação da Universidade Cornell. Os pesquisadores já conectaram a programação a outros tipos de lógica, como a lógica linear, que inclui o conceito de “recursos”, e a lógica modal, que trata de conceitos de possibilidade e necessidade.

E embora esta correspondência tenha os nomes de Curry e Howard, eles não são de forma alguma os únicos que a descobriram. Isso atesta a natureza fundamental da correspondência: as pessoas continuam notando isso continuamente. “Parece não ser por acaso que existe uma ligação profunda entre computação e lógica”, disse Clarkson.