1
$\begingroup$

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.

$\endgroup$
  • $\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 '19 at 18:47
  • 1
    $\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 '19 at 19:17
  • $\begingroup$ @AndrejBauer Also, I have edited the question to make this explicit. $\endgroup$ – Ram Dec 2 '19 at 19:20
  • 3
    $\begingroup$ The Coq website should probably give better advice. Not every question about Coq is research-level. $\endgroup$ – Andrej Bauer Dec 2 '19 at 21:01
1
$\begingroup$

I have no thoughts on whether this is on-topic for TCS and if need be I can repost my answer elsewhere. But I think the question is a good opportunity to demonstrate how to think about the CoC pending some consensus to move it.

  1. The rule BETA-ALL, which says we can beta-reduce terms underneath the all binder (but not the type of the argument), is not part of the typing or equivalence rules of $\mathsf{CC}$. Pierce is extending his definition of $\beta$-reduction first seen in Section 2.3 (section "Strong Normalization"), which itself is defined "As an auxiliary device for the soundness and completeness of algorithmic typechecking." Specifically the fact that this reduction is strongly normalizing can be used to show that typechecking halts.

  2. Pierce mentions on page 51 that "We may use type and term variables declared in a fixed initial context to simulate the built-in types and operators of a programming language."

    Also see Figure 2-1 (First-order dependent types), in which one of the context formation rules (labelled "term variable binding") is that if $\Gamma$ is a well-formed context and $T$ is a well-formed type, we can pick a variable name $x$ and and then $\Gamma, x :: T$ is a well-formed context. (It seems to be implicit that $x$ should be a fresh name, i.e. does not conflict with the rest of $\Gamma$, and that $T$ is well-formed in context $\Gamma$.).

    Now combine this with rule of Figure 2-7 which states that $T ::= \ldots \mathsf{Prop}\ldots$, meaning $\mathsf{Prop}$ is a type. Therefore we can add $\mathsf{True} :: \mathsf{Prop}$ to the context. Likewise with $\mathsf{False}$.

    To add a proof of $\mathsf{True}$, use rule K-App to deduce that $\mathsf{Prf} \:\mathsf{True}$ has kind $\ast$, i.e. is a type, and apply term variable binding again to add some proof $\mathsf{Unit} :: \mathsf{Prf} \,\mathsf{True}$ to the context.

  3. When introducing $\mathsf{Prop}$, we also introduce this new binder called forall, which seems reasonable. Now we have to give this a semantics---how do we prove some forall x, P? The rule merely states that a proof of forall x, P is the same thing as offering "a proof of $P$ for every $x$" where the latter is defined as a dependent product (something our system already had). In a sense, the rules just say "by using the operator $\mathsf{Prf}$, $\mathsf{Prop}$ acts like $\ast$."

    Perhaps you're wondering why this is interesting. We know that a proposition $p:\mathsf{Prop}$ can be coerced to a type $\mathsf{Prf} p : \ast$, and the equivalence says the binder forall acts like a dependent product, so what is gained?. But notice that by using T-ALL and QT-ALL, $\mathsf{Prop}$ can effectively play the role of $T$ when forming the dependent product, so we can quantify over $\mathsf{Prop}$ and still have a $\mathsf{Prop}$. This is the "impredicativity" Pierce refers to, and it makes the system drastically more expressive. If we tried to get rid of the coercion just take $\mathsf{Prop} \equiv \ast$, we would have $\ast : \ast$, which is known to be inconsistent by a theorem of Girard.

  4. To exhibit a natural number per Pierce's definition, you must be able to satisfy this criterion: If I give you any type $a$, term $z : a$, and successor function $s : a \to a$, you must be able to offer me some term of type $a$. Since you don't know the type $a$ in advance, the only thing you can do is apply $s$ to $z$ some number of times, and that is effectively the same thing as having a natural number. Pierce is showing that $\mathsf{CC}$ is expressive enough to type Church's encoding of the natural numbers , which is good because that encoding becomes impossible when you move from untyped lambda calculus to STLC. See these course notes. See also the Wikipedia page on System F for more information---System F is less expressive than $\mathsf{CC}$ but still good enough to play this game.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ in your response (2), Ξ“,π‘₯::𝑇, you probably meant Ξ“,π‘₯:𝑇 (since :: is reserved for type variable binding)? (Dunnl, I can't seem to tag your user name using @) $\endgroup$ – Ram Feb 10 at 16:11
  • $\begingroup$ Also, in point (3) of your response, "We know that a proposition 𝑝:π–―π—‹π—ˆπ—‰ can be coerced to a type 𝖯𝗋𝖿𝑝:βˆ—," , again, you probably meant "𝖯𝗋𝖿𝑝::βˆ—" (since 𝖯𝗋𝖿𝑝 is a type)? Just making sure I got the relations right. $\endgroup$ – Ram Feb 10 at 16:22
  • $\begingroup$ I am confused with the inconsistency thing in (3). I am familiar with Girard's paradox, but I don't see the point you are making here. What do you mean "Prop $\equiv$ * ? Isn't Prop::* already? Could you please expand your answer on the following statement by giving an example. π–―π—‹π—ˆπ—‰ can effectively play the role of 𝑇 when forming the dependent product, so we can quantify over π–―π—‹π—ˆπ—‰ and still have a π–―π—‹π—ˆπ—‰ $\endgroup$ – Ram Feb 10 at 16:40

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.