4 ms·

The Calculus of Constructions is dependently typed, and it has a reasonably sized kernel, compared to HOL and ZFC: Freek Wiedijk, "Is ZF a hack?", http://www.c

• solomatov 12y ago
  >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.
  • CHY872 12y ago
    > 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_s 12y 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.html https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.h... http://agda.chalmers.narkive.com/E2UeRTOx/re-coq-club-propositional-extensionality-the-return-of-the-revenge http://agda.chalmers.narkive.com/E2UeRTOx/re-coq-club-propos...
  • 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 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.
      • mafribe 12y ago
        You can define induction, but you can't prove it, you need to introduce it as an assumption. That's inconvenient.
        • solomatov 12y ago
          You can define induction operator, but it won't have required type.
          • llcv 12y ago
            Can you explain further?