Por que os tipos recursivos são necessários como primitivos para provas em sistemas de tipos dependentes?
Sou relativamente novo em teoria de tipos e programação dependente. Eu estudei o cálculo de construções (CoC) e outros sistemas de tipo puro. Estou particularmente interessado em usá-lo como uma representação intermediária de preservação de prova para um sistema de compilador.
Entendo que os tipos (co-) recursivos são representáveis , computacionalmente , usando como o único construtor de tipos. Eu li, no entanto, que eles não podem ser usados ​​para criar provas por indução (perdoe-me, não consigo encontrar onde agora!), Por exemplo, que não pude provar que em CoC simples (embora ser digitado como ).ΠΠ0≠10≠1NatNatΠ(N:∗).Π(S:N→N).Π(Z:N).NΠ(N:∗).Π(S:N→N).Π(Z:N).N
Suponho que é por isso que eles construíram o cálculo de construções indutivas (CIC). Isso está correto? Mas por que? Não encontrei nenhum material que explique por que essas provas não podem ser representadas sem o uso de tipos (co) indutivos como primitivos. Se isso não for verdade, por que adicioná-los como primitivos no CIC?
— paulotorrens
Não sou especialista, mas vou compartilhar o que entendi até agora com um exemplo.
Vamos considerar o tipo booleano no CoC, usando sua codificação padrão: Podemos esperar provar De fato, isso segue rapidamente de o princípio de eliminação / indução dependente que temos, por exemplo, em CiC
B=Πτ:∗τ→τ→τtt=λτ:∗,x:τ,y:τ. xff=λτ:∗,x:τ,y:τ. yB=Πτ:∗τ→τ→τtt=λτ:∗,x:τ,y:τ. xff=λτ:∗,x:τ,y:τ. y
Πb:Bb=tt∨b=ff(∗)Πb:Bb=tt∨b=ff(∗)
Bind:ΠP:B→∗P(tt)→P(ff)→Πb:BP(b)Bind:ΠP:B→∗P(tt)→P(ff)→Πb:BP(b)
No entanto, não podemos esperar (*) manter todos os modelos de CoC! Intuitivamente, um valor em deve ser aproximadamente uma família de funções atribuindo a cada tipo um valor na interpretação de . Mas isso não força a ser um entre os valores de . Poderíamos ter, por exemplo, (informalmente) BB{fτ}τ{fτ}ττττ→τ→ττ→τ→τfτfτtt,fftt,ff
fN(n)(m)=n+mfN(n)(m)=n+m
Para ter certeza de que os valores de são os únicos valores possíveis, precisamos nos restringir a modelos paramétricos . De fato (eu acho) a propriedade pode ser comprovada a partir do teorema livre associado ao polytype .tt,fftt,ff(∗)(∗)BB
No entanto, até onde eu entendo, o CoC não descarta modelos ad-hoc, nos quais a parametridade não se aplica. Em alguns deles, é simplesmente falso. Pela solidez, na presença de um contra-modelo, concluímos que não é habitado no CoC. Consequentemente, também não há termo no CoC.(∗)(∗)(∗)(∗)BindBind
Não tenho certeza se sigo. Por exemplo, dada uma expressão como , existem muitas maneiras de criar construtores para o Nat, mas, em última análise, todas elas não seriam construídas a partir do ou ? (λ(Nat:∗).(...))(Π(N:∗).Π(S:N→N).Π(Z:N).N)(λ(Nat:∗).(...))(Π(N:∗).Π(S:N→N).Π(Z:N).N)SSZZ
— paulotorrens 6/01/19
@paulotorrens Dentro da lógica, sim, acredito que essas são as únicas opções. Mas, em um modelo de CoC (um modelo ad-hoc), pode haver valores de que não podem ser definidas através de . Pense em um valor natural tal que para todos os tipos exceto em que . O valor se comporta como "zero" na maioria dos tipos e como "um" para booleanos. Não podemos escrever no CoC para definir esse valor , mas em um modelo ad-hoc esse valor pode estar presente. NatNatS,ZS,Znnn(T)(ST)(ZT)=ZTn(T)(ST)(ZT)=ZTTTT=BT=Bn(B)(S)(Z)=S(Z)n(B)(S)(Z)=S(Z)nnλT:∗.if T=B then …λT:∗.if T=B then …nn
@paulotorrens Talvez você possa entender a questão mais facilmente se você pensar sobre . Esse tipo é habitado apenas pela identidade (polimórfica) e, nos modelos paramétricos, esse é realmente o único valor possível para os termos desse tipo. Mas, em um modelo ad-hoc, podemos definir um valor para todos os tipos mas para que . ΠT:∗T→TΠT:∗T→Tv(T)(x)=xv(T)(x)=xTTT=NT=Nv(N)(x)=x+1v(N)(x)=x+1