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 ). $\Pi$ $0\neq 1$ $\texttt{Nat}$ $\Pi(\mathbb{N}:*).\Pi(S:\mathbb{N}\rightarrow\mathbb{N}).\Pi(Z:\mathbb{N}).\mathbb{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?

type-theory dependent-types coq paulotorrens
fonte

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

\begin{array}{l} B = Π_{τ : *} τ \to τ \to τ \\ t t = λ τ : *, x : τ, y : τ . x \\ f f = λ τ : *, x : τ, y : τ . y \end{array}

$\begin{array}{l} \mathbb{B} = \Pi_{\tau:*} \tau \to \tau \to \tau \\ \mathsf{tt} = \lambda \tau:*,x:\tau,y:\tau.\ x \\ \mathsf{ff} = \lambda \tau:*,x:\tau,y:\tau.\ y \end{array}$

Π_{b : B} b = t t \lor b = f f (*)

$\Pi_{b : \mathbb{B}} b={\sf tt} \lor b = {\sf ff} \qquad(*)$

B_{i n d} : Π_{P : B \to *} P (t t) \to P (f f) \to Π_{b : B} P (b)

$\mathbb{B}_{ind} : \Pi_{P:\mathbb{B}\to*} P({\sf tt}) \rightarrow P({\sf ff}) \rightarrow \Pi_{b:\mathbb{B}} P(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) $\mathbb{B}$ $\{f_\tau\}_{\tau}$ $\tau$ $\tau\to\tau\to\tau$ $f_\tau$ $\sf tt,ff$

f_{N} (n) (m) = n + m

$f_{\mathbb{N}}(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 . $\sf tt,ff$ $(*)$ $\mathbb{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. $(*)$ $(*)$ $\mathbb{B}_{ind}$

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 ?

(λ (N a t : *) . (. . .)) (Π (N : *) . Π (S : N \to N) . Π (Z : N) . N)

$(\lambda(Nat:*).(...)) (\Pi(\mathbb{N}:*).\Pi(S:\mathbb{N}\rightarrow\mathbb{N}).\Pi(Z:\mathbb{N}).\mathbb{N})$

S

$S$

Z

$Z$

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.

N a t

$Nat$

S, Z

$S,Z$

n

$n$

n (T) (S_{T}) (Z_{T}) = Z_{T}

$n(T)(S_T)(Z_T) = Z_T$

T

$T$

T = B

$T=\mathbb{B}$

n (B) (S) (Z) = S (Z)

$n(\mathbb{B})(S)(Z) = S(Z)$

n

$n$

λ T : * . i f T = B t h e n \dots

$\lambda T:*. {\sf if}\ T=\mathbb{B}\ {\sf then}\ \ldots$

n

$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 : *} T \to T

$\Pi_{T:*} T\to T$

v (T) (x) = x

$v(T)(x) = x$

T

$T$

T = N

$T=\mathbb{N}$

v (N) (x) = x + 1

$v(\mathbb{N})(x) = x+1$

chi

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

Respostas: