Por que os tipos recursivos são necessários como primitivos para provas em sistemas de tipos dependentes?

10

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 ).Π01NatΠ(N:).Π(S:NN).Π(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
fonte

Respostas:

7

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:τ. y
Πb:Bb=ttb=ff()
Bind:ΠP:BP(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) B{fτ}τττττfτtt,ff

fN(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,ff()B

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.()()Bind

chi
fonte
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:NN).Π(Z:N).N)SZ
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. NatS,Znn(T)(ST)(ZT)=ZTTT=Bn(B)(S)(Z)=S(Z)nλT:.if T=B then n
chi
@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:TTv(T)(x)=xTT=Nv(N)(x)=x+1
chi