3 ms·
> However, Calculus of Constructions doesn't have inductive constructions, without which it's very hard to formalize interesting mathematics in it. Inductive t
by jbapple 12y ago
> However, Calculus of Constructions doesn't have inductive constructions, without which it's very hard to formalize interesting mathematics in it.
Inductive types is something I've wondered about for a couple of weeks.
I know it's possible to simulate inductive types in some formalisms, then add them as a conservative extension. I think this is how HOL-Light works - inductive types aren't in the logical kernel, but they can be added without any new axioms.
To what extent is this possible in the Calculus of Constructions without inductive types?
Wiedijk has pointed out that it's impossible to prove "0 =/= 1" in plain CoC. Is this related?
One of the original CiC papers can be read here:
Frank Pfenning, Christine Paulin-Mohring, "Inductively Defined Types in the Calculus of Constructions", http://repository.cmu.edu/cgi/viewcontent.cgi?article=2907&context=compsci http://repository.cmu.edu/cgi/viewcontent.cgi?article=2907&c...
It makes some claims about what can't be proven in plain CoC that I don't know the justifications for.
- solomatov 12y agoActually, AFAIU, you can define simple inductive types via church literals. However, you can't define induction principle for them. However, without induction principles, you can't prove anything useful.
- mafribe 12y agoYou can define induction, but you can't prove it, you need to introduce it as an assumption. That's inconvenient.
- solomatov 12y agoYou can define induction operator, but it won't have required type.
- llcv 12y agoCan you explain further?
- solomatov 12y agoFor example, let's see how to define induction principle for Nat. We should define two terms with the following types: NatRec : (R : Set) -> R -> (R -> R) -> Nat -> R NatInd : (C : Nat -> Set) -> (C zero) -> ((n : Nat) -> C n -> C (suc n)) -> (n : Nat) -> (C n) For the first we can represent zero and suc as functions of the first type (it will be church literals). However, we can't do the same for the second. We can create a term which has that type but it won't typecheck.