Pourquoi les types récursifs sont-ils nécessaires en tant que primitives pour les preuves dans les systèmes de types dépendants?

Je suis relativement nouveau dans la théorie des types et la programmation dépendante. J'ai étudié le calcul des constructions (CoC) et d'autres systèmes de type pur. Je suis particulièrement intéressé à l'utiliser comme une représentation intermédiaire préservant les preuves pour un système de compilation.

Je comprends que les types (co) récursifs sont représentables , par calcul , en utilisant comme seul constructeur de type. J'ai lu, cependant, qu'ils ne peuvent pas être utilisés pour construire des preuves par induction (pardonnez-moi, je ne trouve pas où maintenant!), Par exemple, je ne pouvais pas prouver que $\Pi$ $0\neq 1$ en CoC simple (même si peut être typé comme ). $\texttt{Nat}$ $\Pi(\mathbb{N}:*).\Pi(S:\mathbb{N}\rightarrow\mathbb{N}).\Pi(Z:\mathbb{N}).\mathbb{N}$

Je suppose que c'est pourquoi ils ont construit le calcul des constructions inductives (CIC). Est-ce correct? Mais pourquoi? Je n'ai trouvé aucun document expliquant pourquoi de telles preuves ne peuvent pas être représentées sans utiliser des types (co) inductifs comme primitives. Si ce n'est pas vrai, alors pourquoi les ajouter en tant que primitives dans CIC?

type-theory dependent-types coq paulotorrens
la source

Réponses:

Je ne suis pas un expert, mais je partagerai ce que j'ai compris jusqu'à présent avec un exemple.

Considérons le type booléen dans CoC, en utilisant son encodage standard: On pourrait s'attendre à pouvoir prouver

\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}$

En effet, cela découle rapidement du principe d'élimination / induction dépendant que nous avons par exemple dans CiC

Π_{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)$

$\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$

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

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

chi
la source

(λ (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

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$

Π_{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$