undefined | Better HN

0 pointssolomatov11y ago0 comments

>The Calculus of Constructions is dependently typed, and it has a reasonably sized kernel, compared to HOL and ZFC:

However, Calculus of Constructions doesn't have inductive constructions, without which it's very hard to formalize interesting mathematics in it.

>Finally, do you know if this was a bug in the kernel, or if some other component (the compiler or caml virtual machine) can be blamed? It apparently was a problem with `vm_compute`, which I don't think I've ever used.

Actually, I am aware of another, much more serious problem with CoIC formalism which was found when Coq was tried to be used to formalize homotopy type theory. It was a bug in CoIC, not a software bug.

0 comments

5 comments · 2 top-level

jbapple11y ago· 2 in thread

> 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&c...

It makes some claims about what can't be proven in plain CoC that I don't know the justifications for.

solomatovOP11y ago

Actually, 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.

mafribe11y ago

You can define induction, but you can't prove it, you need to introduce it as an assumption. That's inconvenient.

1 more reply

CHY87211y ago· 1 in thread

> Actually, I am aware of another, much more serious problem with CoIC formalism which was found when Coq was tried to be used to formalize homotopy type theory. It was a bug in CoIC, not a software bug.

Do you have any references? Intrigued :)

vilhelm_s11y ago

The notion of guardedness (for structural recursion) was a bit too permissive. This lead to inconsistency if you assume e.g. (False->False = True) (which is implied by propositional extensionality, and by the univalence axiom). The same issue affected Agda also. It was discussed a lot on the Coq and Agda mailing lists, e.g. https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.h... http://agda.chalmers.narkive.com/E2UeRTOx/re-coq-club-propos...

j / k navigate · click thread line to collapse