Como funciona a correspondência “provas como programas” para a igualdade?
A relação de igualdade $=$ pode ser representado como um tipo, assim como qualquer outra proposição na correspondência de Curry-Howard.
Eu entendo o sentido em que os símbolos lógicos básicos $\land,\lor,\to, \forall, \exists,\neg$ correspondem a construções de tipo, e o sentido em que uma prova que tem um tipo é um programa (por exemplo, uma prova de $A\to B$ é um programa que faz uma prova de $A$ e produz uma prova de $B$)
Mas como é uma prova de $a=b$um programa? Qual é a ideia geral aqui? Eu não vi uma explicação clara ainda.
Respostas
Como Zhen Lin mencionou nos comentários, os detalhes dependerão de como você está interpretando $=$em sua teoria de tipo. Aqui vou descrever como$=$é tratado em HoTT para concretização, mas você verá que, uma vez que temos um tipo fixo que representa a igualdade, tudo funciona como você esperaria.
No HoTT, adicionamos a seguinte regra de inferência à nossa lógica:
$$\frac{\Gamma \vdash A \text{ type} \quad \Gamma \vdash a, b : A}{\Gamma \vdash a =_A b \text{ type}}$$
Ou seja, para cada tipo $A$, e para cada dois valores $a,b : A$, afirmamos a existência de um tipo $a =_A b$. Os valores que habitam este tipo são provas de que$a$ e $b$ são iguais.
Para falar sobre como os valores $p : a =_A b$são programas, falaremos sobre suas regras de introdução / eliminação. Vou jogar um pouco rápido e solto com minha notação aqui para tentar manter as regras legíveis. Se você quiser os detalhes sangrentos, consulte o apêndice no livro HoTT com link acima.
Existe apenas uma regra de introdução:
$$ \frac{\Gamma \vdash A \text{ type} \quad \Gamma \vdash a : A}{\Gamma \vdash \text{refl}_a : a =_A a}$$
Sempre há uma prova $\text{refl}_a$ (para reflexividade) afirmando que $a=a$.
A regra de eliminação é bastante sutil. Ele forma a base do que é chamado de "indução de caminho" no HoTT e é uma fonte comum de confusão no início. Não vou entrar em muitos detalhes sobre essas sutilezas aqui, no entanto.
$$ \frac{ \Gamma, p:a =_A b \vdash C(p) \text{ type} \quad \Gamma, a_0 : A \vdash c(a_0) : C(\text{refl}_{a_0}) }{ \Gamma \vdash \text{ind}_{=_A}(c) : C(p) } $$
Isso diz que, dado qualquer tipo de família $C$ dependendo $p : a =_A b$, se pudermos eliminar a única regra de introdução, poderemos eliminar o tipo inteiro. Isto é, se algum$c(a_0) : C(\text{refl}_{a_0})$, então podemos obter um valor $\text{ind}_{=_A}(c) : C(p)$ para qualquer $p : a =_A b$nós gostamos. Além disso,$\text{ind}_{=_A}$ satisfaz a regra de computação:
$$(\text{ind}_{=_A}(c))(\text{refl}_a) = c(a)$$
Se parece surpreendente para você que obtemos toda essa expressividade trabalhando apenas com $\text{refl}_a$, você está em boa companhia. Esta é apenas a ponta do iceberg de "sutileza" a que me referi anteriormente. Intuitivamente, desde$\text{refl}_a$é o único construtor para um tipo de igualdade, uma vez que provamos algo para ele, provamos algo para todo o tipo de igualdade. Isso é análogo a provar algo para cada valor em$\mathbf{1}$ provando isso para $\ast : \mathbf{1}$. A única diferença está em nossas cabeças: gostamos de imaginar$\ast$ como sendo o único elemento de $\mathbf{1}$, embora seja fácil para nós imaginar vários elementos possíveis de $a =_A b$, especialmente porque nosso único construtor é para $a =_A a$, que parece uma condição mais fraca. É claro que a teoria dos tipos não se preocupa com nossas dificuldades. Existem muitos modelos de teoria de tipos com igualdade onde$\text{refl}_a$honestamente, é o único valor de qualquer tipo de igualdade.
Quanto a realmente "computar" as coisas com tipos de igualdade, a praticidade óbvia do resto do cálculo lambda falha um pouco. Embora estejamos tecnicamente programando, não tenho certeza se há algum análogo de tipos de igualdade que, digamos, um engenheiro de software possa se importar. Isso está em total contraste com outras construções na teoria dos tipos, que correspondem a tipos de dados algébricos (e que, portanto, têm aplicações computacionais do mundo real óbvias que podemos apontar). Tenho certeza de que alguém pensou no que esses tipos podem calcular corretamente, mas não estou familiarizado com qualquer literatura sobre o assunto.
Espero que isso ajude ^ _ ^
A ideia geral por trás da prova como programa é a mesma para todas as proposições como tipos.
Você escreveu:
uma prova de A → B é um programa que pega uma prova de A e produz uma prova de B
Eu prefiro escrever:
uma prova de A → B é um programa que pega um termo do tipo A e produz um termo do tipo B
Da mesma forma, uma prova de $a=b$ é um programa que leva os termos $a$ e $b$ e produz um termo do tipo $a=b$. Dependendo de como a igualdade é definida em sua teoria de tipo, um termo de$a=b$ podem ser coisas diferentes, mas isso é outra história ...
Na ideia por trás da prova como programa, o programa está computando em termos, não em provas. De proposições como tipos, você obtém provas como termos, mas um termo com uma variável é um programa, portanto, você tem termos como programas e, portanto, provas como programas ...