¿Por qué se necesitan tipos recursivos como primitivas para pruebas en sistemas de tipos dependientes?

Soy relativamente nuevo en teoría de tipos y programación dependiente. He estado estudiando el cálculo de construcciones (CoC) y otros sistemas de tipo puro. Estoy particularmente interesado en usarlo como una representación intermedia de preservación de pruebas para un sistema compilador.

Entiendo que los tipos (co) recursivos son representables , computacionalmente , usando como el único constructor de tipos. Sin embargo, he leído que no se pueden usar para crear pruebas por inducción (¡perdóname, no puedo encontrar dónde ahora!), Por ejemplo, que no podría probar que en CoC simple (aunque se puede escribir como ).0 ≠ 1 Nat Π ( N : ∗ ) . Π ( S : N → N ) . Π ( Z : N ) . $\Pi$$0\neq 1$$\texttt{Nat}$$\Pi(\mathbb{N}:*).\Pi(S:\mathbb{N}\rightarrow\mathbb{N}).\Pi(Z:\mathbb{N}).\mathbb{N}$

Supongo que es por eso que construyeron el cálculo de las construcciones inductivas (CIC). ¿Es esto correcto? ¿Pero por qué? No pude encontrar ningún material que explicara por qué tales pruebas no se pueden representar sin usar tipos (co) inductivos como primitivos. Si esto no es cierto, ¿por qué agregarlos como primitivos en CIC?

No soy un experto, pero compartiré lo que entendí hasta ahora con un ejemplo.

Consideremos el tipo booleano en CoC, usando su codificación estándar: Podríamos esperar poder probar Π b : B b =

$$\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}$$ De hecho, esto se deduce rápidamente del principio de eliminación / inducción dependiente que tenemos, por ejemplo, en CiC B i n d : Π P : B → ∗ P ( t t ) → P ( f f ) → Π b : B P ( b $$\Pi_{b : \mathbb{B}} b={\sf tt} \lor b = {\sf ff} \qquad(*)$$ $$\mathbb{B}_{ind} : \Pi_{P:\mathbb{B}\to*} P({\sf tt}) \rightarrow P({\sf ff}) \rightarrow \Pi_{b:\mathbb{B}} P(b)$$

Sin embargo, no podemos esperar que (*) se mantenga en todos los modelos de CoC. Intuitivamente, un valor en debería ser aproximadamente una familia de funciones { f τ } τ que asigna a cada tipo τ un valor en la interpretación de τ → τ → τ . Pero esto no obliga a f τ a ser uno entre los valores de t t , f f . Podríamos tener, por ejemplo, (informalmente) f N ( n ) ( m ) = n + $\mathbb{B}$$\{f_\tau\}_{\tau}$$\tau$$\tau\to\tau\to\tau$$f_\tau$$\sf tt,ff$

$$f_{\mathbb{N}}(n)(m) = n+m$$

$\sf tt,ff$$(*)$$\mathbb{B}$

$(*)$$(*)$$\mathbb{B}_{ind}$