14
$\begingroup$

The Calculus of Constructions is a very simple core functional language with dependent types. Per curry-howard isomorphism, it could, potentially, be very useful for writing programs and proofs. It, though, has a few problems: induction isn't derivable, it isn't possible to prove 0 != 1, and pattern matching on algebraic data structures take linear time. In order to solve those issues, practical languages such as Coq are based on the Calculus of Inductive Constructions instead, which add a layer of primitive datatypes on top of CoC. That, unfortunately, makes the core language very complex.

An alternative solution to those problems is a new primitive, self, which is a construction that allows a type to reference its typed term. This construct, together with the Parigot encoding, and a slightly weakened but still useful notion of contradiction, is sufficient to solve the problems above. The proposed language, though, is still somewhat complex. In particular, it has different Pi types, complex kind machinery and requires a restricted form of recursion (for the Parigot encoding).

Is it possible to be simpler? I.e., can the calculus of constructions with only self types and nothing else from this paper still be able to derive induction and employ the parigot encoding?

$\endgroup$
5
  • $\begingroup$ I feel like I answered a similar question here: cs.stackexchange.com/questions/49638/…. How is your current question different? Also, you seem to be asking 2 different questions in the title and the body. $\endgroup$
    – cody
    May 1, 2017 at 14:18
  • $\begingroup$ @cody I am so sorry. I spent some time googling and looking up to make sure I wasn't asking a repeated question (as I was fairly sure I had discussed something similar here), but I missed your answer to that post specifically covered this. It has none of the keywords I googled for... $\endgroup$
    – MaiaVictor
    May 1, 2017 at 16:27
  • 1
    $\begingroup$ No problem, and I actually vote for the question to stay open, since it may attract some interesting answers. $\endgroup$
    – cody
    May 1, 2017 at 21:32
  • $\begingroup$ You may want to look at guarded recursion. For example itu.dk/people/mogel/papers/lics2017.pdf $\endgroup$
    – xavierm02
    Jul 27, 2017 at 15:05
  • $\begingroup$ I'm interested int this subject too. Have you got answers to your questions? Your quote "adding a new primitive, self" is incomplete. The paper states that you need to add mutually recursive definitions too, which break the analogy of types-as-proofs... Here is a newer work of same authors. The quote I'm talking about is in the penultimate paragraph of the first page. $\endgroup$ Jul 11, 2018 at 14:41

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.