I've heard some claims that the calculus of constructions without inductive types isn't powerful enough to express proofs by induction. Is that correct? If so, why isn't the Church-encoding sufficient for that?
$\begingroup$
$\endgroup$
1
-
$\begingroup$ See also this thread: cstheory.stackexchange.com/questions/30923/… $\endgroup$– Martin BergerCommented Jan 23, 2017 at 10:28
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
3
How would you prove inside the pure CoC that the induction principle holds of the Church numerals? See Thomas Streicher's, Independence of the induction principle and the axiom of choice in the pure calculus of constructions.
-
1
-
$\begingroup$ @cody Geuvers' result is for second-order dependent types. Is it obvious that it generalises to higher-order dependent types? $\endgroup$ Commented Jan 17, 2017 at 12:58
-
1$\begingroup$ It's not obvious, no. I do think the model construction outlined in the paper generalizes though, as it's based on a model originally developed for the full calculus. $\endgroup$– codyCommented Jan 17, 2017 at 15:28
$\begingroup$
$\endgroup$
There is a result recently published within Annals of Pure and Applied Logic in which church encoded data are realizers of their own induction principle. In this system, the induction principle for natural numbers, trees, lists... are derivable. The core calculus doesn't have any datatype constructors packaged in. It starts at an extrinsic (curry style) System F adding 3 typing constructs: implicit product, heterogeneous equality, and dependent intersection.
Geuvers result does not apply to this calculus and is mentioned in the paper.
paper: "From Realizability to Induction via Dependent Intersection", by Aaron Stump
