I am working through the Dependent Types chapter from Advanced Topics in Types and Programming Languages (ATTAPL) by Benjamin Pierce et al. I am confused with the calculus presented Fig 2-7 (Calculus of Constructions) that extends $\lambda LF$ to support Prop type. I have multiple questions.

  1. Can a Prop term be $\beta$-reduced at all? The rule (BETA-ALL) on the next page suggests that only the body of a Prop can be reduced. That is, in the term forall x:T.t, only t is reduced.

  2. There are no atomic propositions like True, False. So how can one build a term of type Prop (and Prf p). Any simple example suffices.

  3. I am not sure I understand the type equivalence rule QT-ALL in Fig 2-7.

  4. The encoding of nat (and zero later on) is confusing. For the sake of readability I am writing it down here.

    nat = all a:Prop.all z:Prf a.all s:Prf a ->Prf a. a

    What is the meaning? Specifically, what is a - any Prop? Why are proofs of z (zero) and s (succ) required?

I think these are lot of questions. I would appreciate answers to any of these questions.

EDIT: I was suggested to move this to cs.stackexchange.com. However, the question is about the meta-theory of Coq and I thought cstheory is an appropriate forum. But if multiple users suggest moving this, I can do that.

  • $\begingroup$ Please move to cs.stackexchange.com. This site is for research-level questions, which explanations of textbooks are not. $\endgroup$ – Andrej Bauer Dec 2 at 18:47
  • $\begingroup$ @AndrejBauer coq.inria.fr/community says to post questions in TCS stackexchange. Hence I took it to here since this is about the theory of Coq (The calculus discussed there is of Calculus of Constructions). If appropriate, I have no issues moving the question to cs.stackexchange.com but I want to make sure that I understand the etiquette before doing so. $\endgroup$ – Ram Dec 2 at 19:17
  • $\begingroup$ @AndrejBauer Also, I have edited the question to make this explicit. $\endgroup$ – Ram Dec 2 at 19:20
  • 1
    $\begingroup$ The Coq website should probably give better advice. Not every question about Coq is research-level. $\endgroup$ – Andrej Bauer Dec 2 at 21:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.