# Isomorfismo de Curry-Howard

O isomorfismo de Curry–Howard é uma relação direta entre programas de computador e provas matemáticas. Também conhecido como correspondência de Curry–Howard, correspondência provas-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 é:
* 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.
* 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.
* 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 computacional 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 considerados 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 valores retornados por uma função) é análogo a um teorema lógico, sujeito a hipóteses 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 forma de programação lógica em uma base robusta: “provas podem ser representadas como programas, e especialmente 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-Löf e o Cálculo de Construções de Coquand, dois tipos de cálculos 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 cálculos tipados derivados do paradigma de Curry-Howard levarem ao desenvolvimento de programas como o Coq, no qual provas, vistas como programas, podem ser formalizadas, verificadas e executadas.
Um direção diferente é usar um programa para extrair uma prova, dada a sua corretude – uma área de pesquisa que está intimamente relacionada a código portador-de-prova. Isso somente é factí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 levanta 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 correspondente à habilidade de manipular a continuação de programas e a simetria do cálculo 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.
Sistemas de Hilbert e dedução natural são somente dois tipos de sistemas de prova dentre uma grande família de formalismos. Sintaxes alternativas incluem o cálculo de sequentes, redes de prova, cálculo de estruturas, etc. Se admitirmos a correspondência de Curry-Howard como um princípio de que qualquer tipo de sistema de prova esconde um modelo computacional em seu âmago, uma teoria sobre as estruturas computacionais não tipadas subjacentes a esses tipos de provas deve ser possível de existir. Logo, uma questão natural é se alguma coisa matematicamente interessante pode ser dita sobre esses Cálculos Computacionais subjacentes.
Reciprocamente, 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 imaginar 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, pois uma aplicação ingênua da correspondência 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ódigo que potencialmente não para (uma abordagem que também generaliza modelos computacionais muito ricos, e é ela própria relacionada a lógica de modelar por extensão natural do ismorfismo 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 mantendo uma complexidade computacional alta), usando co-recursão mais controlada onde comportamento “não-parável” é na verdade desejável.

## Formulação geral

Em sua formulação mais geral, a correspondência de Curry-Howard é uma correspondência entre Cálculo da Prova formal e sistemas de tipos para modelos computacionais. Em particular, ela é dividida em duas correspondências. Um no nível de formulas e tipos que é independente de qual sistema de provas ou modelo computacional é considerada,e outra no nível de provas e programas que, por sua vez, é específica para o sistema de provas e modelo computacional considerado.
No nível de formulas e tipos, a correspondência diz que implicação se comporta como um “tipo função”, conjunção como um tipo “produto” (isso pode ser chamado de tupla, struct, lista ou algum outro termo dependente da linguagem), disjunção como um “tipo soma” (esse tipo pode ser chamado de união, union), a fórmula falsa como o tipo vazio e a fórmula verdade como um tipo conjunto-unitário (cujo único membro é o objeto null). Quantificadores correspondem ao espaço de funções dependentes ou produtos (o que for mais apropriado).
Isso pode ser resumido na seguinte tabela:
| Lado lógico | Lado programacional |
| quantificador universal | espaço de função generalizada (tipo Π) |
| qualificador existencial | produto cartesiano generalizado (tipo Σ) |
| implicação | tipo função |
| conjunção | tipo produto |
| disjunção | tipo soma |
| fórmula verdadeira | tipo unitário |
| fórmula falsa | tipo vazio |
No nível de sistemas de prova e modelos computacionais, a correspondência mostra principalmente a identidade da estrutura, primeiramente, entre algumas formulações de sistemas particulares conhecidos como sistemas de deduções de Hilbert e lógica combinatória, e, em segundo lugar, entre algumas formulações de sistemas conhecidos como dedução natural e lambda cálculo.
| Lado lógico | Lado programacional |
| Sistema de Hilbert | Sistema de tipos para lógica combinatória |
| dedução natural | Sistema de tipos para Lambda Cálculo |
Entre o sistema de dedução natural e o lambda calculo, existem as seguintes correspondências:
| Lado lógico | Lado programacional |
| hipótese | variável livre |
| remoção da implicação | aplicação |
| introdução da implicação | abstração |

## Correspondência entre os Sistemas de dedução de Hilbert e a lógica combinatória

Foi o início de um simples trecho do livro de Curry e Fey, 1958, sobre lógica combinatória: os tipos mais simples para os combinadores básicos K e S da lógica combinatória surpreendentemente corresponderam com o respectivo esquemas axiomáticos α → (β → α) e (α → (β → γ)) → ((α → β) → (α → γ)) usado nos sistemas de Hilbert. Por essa razão, esses esquemas são normalmente chamados axiomas K e S. <-- TODO: Exemplos de programas vistos como provas em uma lógica de Hilbert são dados abaixo. -->
Se nos restringirmos ao fragmento intuicionístico implicacional, uma maneira simples de formalizar lógica usando um sistema de Hilbert é a seguinte: Seja Γ um conjunto finito de fórmulas, consideradas hipóteses. Dizemos que δ é derivável a partir de Γ, e escrevemos Γ ⊢ δ, nos seguintes casos:
* δ é uma hipótese, isto é, ela é uma fórmula de Γ,
* δ é uma instância de um esquema axiomático; isto é, sobre o sistema axiomático mais simples:
** δ tem a forma α → (β → α), ou
** δtem a forma (α → (β → γ)) → ((α → β) → (α → γ)),
* δ é gerada por dedução, isto é, para algum α, tanto α → δ como α já são deriváveis a partir de Γ (essa é a regra de modus ponens)
Isso pode ser formalizado usando regras de inferência, que é o que fazemos na coluna a esquerda da tabela a seguir.
Podemos formular lógica combinatória tipada usando uma sintaxe similar: seja Γ um conjunto finito de variáveis, junto com seus tipos. Um termo T (também junto de seu tipo) vai depender nesses variáveis [Γ ⊢ T:δ] quando:
* T é uma das variáveis de Γ,
* T é um combinador básico; i.e., sob a base combinatória mais comum:
** T é K:α → (β → α) [onde α e β são os tipos de seus argumentos], ou
** T é S:(α → (β → γ)) → ((α → β) → (α → γ)),
* T é a composição de dois sub-termos que dependem das variáveis em Γ.
As regras de geração definidas aqui são dadas na coluna da direita abaixo. O trecho de Curry diz simplesmente que as duas colunas seguem uma correspondência de um-para-um. A restrição da correspondência para a lógica intuicionista significa que alguma tautologia da lógica clássica, como a Lei de Peirce ((α → β) → α) → α, são excluídas da correspondência.
| Lógica intuicionista implicacional de Hilbert | Lógica combinatória simplesmente tipada |
| ${\frac {\alpha \in \Gamma }{\Gamma \vdash \alpha }}{\text{Assum}}$ | ${\frac {x:\alpha \in \Gamma }{\Gamma \vdash x:\alpha }}$ |
| ${\frac{\Gamma \vdash \alpha \rightarrow (\beta \rightarrow \alpha )}}{\text{Ax}}_{K}$ | ${\frac{\Gamma \vdash K:\alpha \rightarrow (\beta \rightarrow \alpha )}}$ |
| ${\frac{\Gamma \vdash (\alpha \!\rightarrow \!(\beta \!\rightarrow \!\gamma ))\!\rightarrow \!((\alpha \!\rightarrow \!\beta )\!\rightarrow \!(\alpha \!\rightarrow \!\gamma ))}}{\text{Ax}}_{S}$ | ${\frac{\Gamma \vdash S:(\alpha \!\rightarrow \!(\beta \!\rightarrow \!\gamma ))\!\rightarrow \!((\alpha \!\rightarrow \!\beta )\!\rightarrow \!(\alpha \!\rightarrow \!\gamma ))}}$ |
| ${\frac {\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha }{\Gamma \vdash \beta }}{\text{Modus Ponens}}$ | ${\frac {\Gamma \vdash E_{1}:\alpha \rightarrow \beta \qquad \Gamma \vdash E_{2}:\alpha }{\Gamma \vdash E_{1}\;E_{2}:\beta }}$ |
Vista de um nível mais abstrato, a correspondência pode ser reescrita como mostrada na tabela a seguir. Especialmente, o Teorema da Dedução específico para a lógica de Hilbert corresponde ao processo de Eliminação da abstração da lógica combinatória.
| Lado Lógico | Lado Programacional |
| suposição | variável |
| axiomas | combinadores |
| modus ponens | aplicações |
| Teorema da Dedução | Eliminação da abstração |
Graças à correspondência, resultados da lógica combinatória podem ser transferidos para a lógica de Hilbert e vice-versa. Por exemplo, a noção de redução de termos na lógica combinatória pode ser transferida para a lógica de Hiolbert e ela provê uma maneira de canonicamente transformar uma prova em outra prova de uma mesma sentença. Também pode-se transferir a noção de termos normais para a noção de provas normais, expressando que as hipóteses dos axiomas nunca precisam estar todas desacopladas (já que a simplificação pode acontecer).
Reciprocamente, a improbabilidade da lógica instuicionista da Lei de Peirce pode ser transferida de volta para a lógica combinatória: existe nenhum termo tipado da lógica combinatória que tipável com o tipo ((α → β) → α) → α.
Resultados da completude de alguns conjuntos de combinadores ou axiomas também podem ser transferidos. Por exemplo, o fato de que o combinador X constitui uma base de único ponto da lógica combinatória (extensiva) implica que o única esquema axiomático
    (((α → (β → γ)) → ((α → β) → (α → γ))) → ((δ → (ε → δ)) → ζ)) → ζ,
que é o tipo principal de X, é um substituto adequado para a combinação dos esquemas aquimáticos
    α → (β → α) and
    (α → (β → γ)) → ((α → β) → (α → γ)).

## Correspondência entre dedução natural e lambda cálculo

Depois de Curry enfatizar a correspondência sintática entre a dedução de Hilbert e a [lógica combinatória], Howard tornou explícita em 1969 uma analogia sintática entre os programas do lambda cálculo simplesmente tipado e as provas da dedução natural. Abaixo, o lado esquerdo formaliza a implicação intuicionista da dedução natural como um calculo de sequentes (o uso de sequentes é um padrão em discussões sobre o isomorfismo de Curry-Howerd pois eles permitem que as regras de dedução sejam escritas mais claramente) com enfraquecimento implícito e o lado direito mostra as regras de tipagem do lambda cálculo. No lado esquerdo, Γ, Γ$_1$ e Γ$_2$ denotam sequências ordenadas de fórmulas enquanto no lado direito eles denotam sequências de fórmulas nomeadas (i. e., tipadas) como todos os nomes diferentes.
| Implicação intuicionista da dedução natural | Regras de tipagem de lambda cálculo |
| ${\frac{\Gamma _{1},\alpha ,\Gamma _{2}\vdash \alpha }}{\text{Ax}}$ | ${\frac{\Gamma _{1},x:\alpha ,\Gamma _{2}\vdash x:\alpha }}$ |
| ${\frac {\Gamma ,\alpha \vdash \beta }{\Gamma \vdash \alpha \rightarrow \beta }}\rightarrow I$ | ${\frac {\Gamma ,x:\alpha \vdash t:\beta }{\Gamma \vdash \lambda x.t:\alpha \rightarrow \beta }}$ |
| ${\frac {\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha }{\Gamma \vdash \beta }}\rightarrow E$ | ${\frac {\Gamma \vdash t:\alpha \rightarrow \beta \qquad \Gamma \vdash u:\alpha }{\Gamma \vdash t\;u:\beta }}$ |
Parafraseando a correspondência, provar Γ ⊢ α significa ter um programa que, dados valores com os tipos listados em Γ, construir um objeto do tipo α. Um axioma corresponde à introdução de uma nova variável com um novo, ainda não associado, tipo, a regra → I corresponde à função abstração e a regra → E corresponde a função aplicação. Observe que a correspondência não é exata se o contexto Γ é tomado como sendo um conjunto de fórmulas pois, por exemplo, os termos-λ λx.λy.x e λx.λy.y do tipo α → α → α não seriam distinguíveis na correspondência. <--TODO: Exemplos são dados abaixo. -->
Howard mostrou que a correspondência estende-se para outros conectivos da lógica e outras construções do lambda cálculo simplesmente tipado. Visto de um nível abstrato, a correspondência pode então ser resumida como mostrado na tabela a seguir. Especialmente, ela também mostra que a noção de formas normais em lambda cálculo corresponde à noção de dedução normal de Prawitz da dedução natural. Disso deduzimos, entre outras coisas, que os algoritmos para o problema de habitação de tipos pode ser transformado em algoritmos para decidir a probabilidade intuicionista.
| Lado Lógico | Lado Programacional |
| axioma | variável |
| regra de introdução | construtor |
| regra de eliminação | destrutor |
| dedução normal | forma normal |
| normalização de deduções | normalização fraca |
| provabilidade | problema de habitação de tipos |
| tautologia intuicionista | tipo habitado |
A correspondência de Howard naturalmente estende-se para outras extensões da dedução natural e lambda cálculo simplesmente tipado. Aqui está uma lista pequena:
* Girard-Reynolds System F como uma linguagem comum para tanto a lógica proposicional de segunda ordem para o lambda cálculo polimórfico,
* Lógica de alta ordem e o Sistema F$_ω$ de Girard,
* tipos indudivos como tipo algébrico de dados
* necessidade $\Box$ em lógica de modelos e computação por estágios
* possibilidade $\Diamond$ em lógica de modelos e tipos monadicos para efeitos
* O cálculo λ$_I$ correspondente a lógica relevante.
* A modalidade da veracidade local (∇) na topologia Grothendieck ou a equivalente modalidade "lax" (∘) de Benton, Bierman, e de Paiva (1998) correspondem a lógica-CL descrevebti "tipos de computação".