Isomorfismo de Curry-Howard

Uma prova escrita como um programa funcional: a prova de comutatividade da adição de números naturais no assistente de provas Coq. nat_ind está apra indução matemática, eq_ind substitui a igualdade and f_equal toma a mesma função em ambos os lados da igualdade. Teoremas mais atuais são referenciados como mostrado. m = m + 0 and S (m + y) = m + S y.

O isomorfismo de Curry–Howard é uma relação direta entre programas de computador e demonstrações matemáticas. Também conhecido como correspondência de Curry–Howard, correspondência demonstrações-como-programas, e correspondência fórmulas-como-tipos, ele se refere à generalização de uma analogia sintática entre sistemas de lógica formal e cálculos computacionais que foi descoberto pela primeira vez pelo matemático americano Haskell Curry e o lógico William Alvin Howard.

Origem, escopo, e consequências

Em primeiro lugar, a correspondência de Curry-Howard é:

1. A observação em 1934 feita por Curry de que tipos de combinadores poderiam ser vistos como esquemas axiomáticos para a lógica intuicionista implicacional.
2. A observação em 1958 feita por Curry de que certos tipos de sistemas de provas, chamados de sistemas de Hilbert , coincide em algum fragmento com um fragmento tipado de um modelo computacional conhecido como lógica combinatória.

1. A observação em 1969 feita por Howard que outro, mais “alto-nível”, sistema de prova, conhecido como dedução natural, pode ser diretamente interpretado em sua versão intuicionista como uma variante tipada do modelo compuitacional conhecido como lambda cálculo.

Em outras palavras, a correspondência de Curry-Howard é a observação de que duas famílias de formalismos que pareciam não relacionadas (os sistemas de prova e os modelos computacionais) eram, nos dois exemplos cosiderados por Curry e Howard, na verdade estruturalmente os mesmos tipos de objetos.

Se agora nos abstrairmos das peculiaridades desse ou daquele formalismo, a generalização imediata é a seguinte: “uma prova é um programa, a formula que ela prova é um tipo para o programa”. Informalmente, isso pode ser visto como uma analogia que diz que o tipo de retorno de uma função (isto é, o tipo dos valorer retornados por uma função) é análogo a um teorema lógico, sujeito a hipoteses correspondendo aos tipos dos valores usados na função como argumentos; e que o programa para computar a função é análogo a prova daquele teorema. Isso estabelece uma foma de programação lógica em uma base robusta: “provas podem ser representadas como programas, e especiamente temos lambda” ou, em outras palavras, “provas podem ser executadas”.

A correspondência foi o ponto inicial de um grande número de novas pesquisas após sua descoberta, levando a criação de uma nova classe de sistemas formais designados a agir tanto como sistemas de prova e como tipos de linguagens de programação funcional. Isso inclui a teoria de tipos intuicionista de Martin-Lof e o Cálculo de Construções de Conquad, dois tipos de Calculos nos quais provas são objetos comuns do discurso e nos quais um pode dizer propriedades de provas da mesma maneira que é feita em qualquer programa. Esse campo de pesquisa é normalmente chamado de teoria dos tipos moderna.

Esses lambda calculos tipados derivados do paradigma de Curry-Howard levarem ao desenvolvimento de programas como o Coq, no qual provas, vistas como programas, podem ser formalizadas, checadas e executadas.

Um direção diferente é usar um programa para extrair uma prova, dada a sua corretude – uma area de pesquisa que está intimamente relacionada a código portador-de-prova. Isso somente é fazível se a linguagem de programação usada para escrever o programa é ricamente tipada: o desenvolvimento desses tipos de sistemas tem sido parcialmente motivado pelo desejo de fazer a correspondência de Curry-Howard relevante sob um conceito prático.

A correspondência Curry-Howard também levando novas perguntas em relação ao conteúdo computacional de conceitos de provas que não foram cobertos pelos trabalhos originais de Curry e Howard. Em particular, a lógica clássica tem se mostrado correspondete à habilidade de manipulas a continuação de programas e a simetria do Calculo de Sequentes para expressar a dualidade entre duas estratégias de valoração conhecidas como chamada-por-nome e chamada-por-valor.

Especula-se que a correspondência de Curry-Howard pode levar a uma substancial unificação entre a lógica matemática e a base da ciência da computação.

Lógica de Hilbert e dedução natural são somente dois tipos de sistemas de prova dentre uma grande familia de formalismos. Sintaxes alternativas inclues o Cálculo de Sequentes, redes de prova, cálculo de estruturas, etc. Se admitirmos que a correspondência de Curry-Howard como um principio de que qualquer tipo de sistema de prova esconde um modelo computacional em seu âmago, uma teoria sobre as estruturas computacionas não tipadas subjacentes a esses tipos de provas deve ser possível de existir. Logo, uma questão natural é se alguma coisa matematicalmente interessante pode ser dita sobre esses Calculos Computacionais subjacentes.

Conversalmente, lógica combinatória e lambda calculo simplesmente tipado não são os únicos modelos computacionais. A lógica linear de Girard foi desenvolvida partindo da análise do uso de recursos de alguns modelos de lambda calculo; podemos imaginas uma versão tipada de uma Máquina de Turing que se comportaria como um sistema de prova? Linguagens assembly tipadas são um exemplo desses modelos de computação “baixo-nível” que contém tipos.

Por causa da possibilidade de escrita de programas que nunca param, modelos Turing-completos de computação (como linguagens com funções recursivas arbitrárias) devem ser interpretadas com cuidado, uma aplicação ingênua da correspondencia leva a uma lógica inconsistente. A melhor forma de lidar com computação arbitrária de um ponto de vista lógico é ainda uma questão de pesquisa extremamente debatida, mas uma abordagem popular é baseada no uso de monads para segregar que provavelmente para de cógigo que potencialmente não para (uma abordagem que também generaliza modelos computacionais muito ricos, e é ela própria relacionada a lógica de modelas por extesão natural do ismorphismo de Curry-Howard ). Uma abordagem mais radical, feita por programação totalmente funcional, é eliminar recursões sem restrição (e evita a completude de Turing, mas ainda assim matendo uma complexidade computacional alta), usando correcusão mais controlada onde comportamento “não-parável” é na verdade desejável.