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 en CoC simple (même si peut être typé comme Π ( N : ∗ ) . Π ( S : N → N ) . Π ( Z : N ) . 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?
la source