<p><em>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.</em></p>

<ol>
<li><p>The rule <code>BETA-ALL</code>, which says we can beta-reduce terms underneath the <code>all</code> binder (but not the type of the argument), is not part of the typing or equivalence rules of <span class="math-container">$\mathsf{CC}$</span>. Pierce is extending his definition of <span class="math-container">$\beta$</span>-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.</p></li>
<li><p>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."</p>

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

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

<p>To add a proof of <span class="math-container">$\mathsf{True}$</span>, use rule <code>K-App</code> to deduce that <span class="math-container">$\mathsf{Prf} \:\mathsf{True}$</span> has kind <span class="math-container">$\ast$</span>, i.e. is a type, and apply <em>term variable binding</em> again to add some proof <span class="math-container">$\mathsf{Unit} :: \mathsf{Prf} \,\mathsf{True}$</span> to the context.</p></li>
<li><p>When introducing <span class="math-container">$\mathsf{Prop}$</span>, we also introduce this new binder called <code>forall</code>, which seems reasonable. Now we have to give this a semantics---how do we prove some <code>forall x, P</code>? The rule merely states that a proof of <code>forall x, P</code> is the same thing as offering "a proof of <span class="math-container">$P$</span> for every <span class="math-container">$x$</span>" 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 <span class="math-container">$\mathsf{Prf}$</span>, <span class="math-container">$\mathsf{Prop}$</span> acts like <span class="math-container">$\ast$</span>."</p>

<p>Perhaps you're wondering why this is interesting. We know that a proposition <span class="math-container">$p:\mathsf{Prop}$</span> can be coerced to a type <span class="math-container">$\mathsf{Prf} p : \ast$</span>, and the equivalence says the binder <code>forall</code> acts like a dependent product, so what is gained?. But notice that by using <code>T-ALL</code> and <code>QT-ALL</code>, <em><span class="math-container">$\mathsf{Prop}$</span> can effectively play the role of <span class="math-container">$T$</span> when forming the dependent product</em>, so we can quantify over <span class="math-container">$\mathsf{Prop}$</span> and still have a <span class="math-container">$\mathsf{Prop}$</span>. 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 <span class="math-container">$\mathsf{Prop} \equiv \ast$</span>, we would have <span class="math-container">$\ast : \ast$</span>, which is known to be inconsistent by a theorem of Girard.</p></li>
<li><p>To exhibit a natural number per Pierce's definition, you must be able to satisfy this criterion: If I give you any type <span class="math-container">$a$</span>, term <span class="math-container">$z : a$</span>, and successor function <span class="math-container">$s : a \to a$</span>, you must be able to offer me some term of type <span class="math-container">$a$</span>. Since you don't know the type <span class="math-container">$a$</span> in advance, the only thing you can do is apply <span class="math-container">$s$</span> to <span class="math-container">$z$</span> some number of times, and <em>that</em> is effectively the same thing as having a natural number. Pierce is showing that <span class="math-container">$\mathsf{CC}$</span> is expressive enough to type <a href="https://en.wikipedia.org/wiki/Church_encoding" rel="nofollow noreferrer">Church's encoding of the natural numbers </a>, which is good because that encoding becomes impossible when you move from untyped lambda calculus to STLC. <a href="https://www3.nd.edu/~dchiang/teaching/pl/2019/stlc.html" rel="nofollow noreferrer">See these course notes.</a> See also the <a href="https://en.wikipedia.org/wiki/System_F#System_F_structures" rel="nofollow noreferrer">Wikipedia page on System F</a> for more information---System F is less expressive than <span class="math-container">$\mathsf{CC}$</span> but still good enough to play this game.</p></li>
</ol>

CC BY-SA 4.0
2020-02-10T16:11:06.013Z
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 @)
Ram
CC BY-SA 4.0
2020-02-10T16:22:14.080Z
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.
Ram
CC BY-SA 4.0
2020-02-10T16:40:51.903Z
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 _
Ram
CC BY-SA 4.0
2020-02-04T17:32:01.063Z
2020-02-04T17:32:01.063Z
dunnl
<p>I am working through the <strong>Dependent Types</strong> chapter from <em>Advanced Topics in Types and Programming Languages</em> (ATTAPL) by Benjamin Pierce et al. I am confused with the calculus presented Fig 2-7 (Calculus of Constructions) that extends <span class="math-container">$\lambda LF$</span> to support <code>Prop</code> type. I have multiple questions.</p>

<ol>
<li><p>Can a <code>Prop</code> term be <span class="math-container">$\beta$</span>-reduced at all? The rule <code>(BETA-ALL)</code> on the next page suggests that only the body of a <code>Prop</code> can be reduced. That is, in the term <code>forall x:T.t</code>, only <code>t</code> is reduced.</p></li>
<li><p>There are no atomic propositions like True, False. So how can one build a term of type <code>Prop</code> (and <code>Prf p</code>). Any simple example suffices.</p></li>
<li><p>I am not sure I understand the type equivalence rule <code>QT-ALL</code> in Fig 2-7.</p></li>
<li><p>The encoding of <code>nat</code> (and <code>zero</code> later on) is confusing. For the sake of readability I am writing it down here.</p>

<p><code>nat = all a:Prop.all z:Prf a.all s:Prf a -&gt;Prf a. a</code></p>

<p>What is the meaning? Specifically, what is <code>a</code> - any Prop? Why are proofs of <code>z</code> (zero) and <code>s</code> (succ) required?</p></li>
</ol>

<p>I think these are lot of questions. I would appreciate answers to any of these questions.</p>

<p>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.</p>

CC BY-SA 4.0
2019-12-02T18:47:58.397Z
Please move to cs.stackexchange.com. This site is for research-level questions, which explanations of textbooks are not.
Andrej Bauer
CC BY-SA 4.0
2019-12-02T19:17:13.127Z
@AndrejBauer https://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.
Ram
CC BY-SA 4.0
2019-12-02T19:20:11.697Z
@AndrejBauer Also, I have edited the question to make this explicit.
Ram
CC BY-SA 4.0
2019-12-02T21:01:45.577Z
The Coq website should probably give better advice. Not every question about Coq is research-level.
Andrej Bauer
<pl.programming-languages><type-theory><dependent-type><coq><calculus-of-constructions>
Lack of atomic propositions in the Calculus of Constructions from ATTAPL textbook
Ram
# Lack of atomic propositions in the Calculus of Constructions from ATTAPL textbook

(Asked by: username_0 on 2019-12-02)

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.

**Tags:** pl.programming-languages, type-theory, dependent-type, coq, calculus-of-constructions

> **Comments:**
> **username_1**: Please move to cs.stackexchange.com. This site is for research-level questions, which explanations of textbooks are not.  
> **username_0**: @AndrejBauer https://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.  
> **username_0**: @AndrejBauer Also, I have edited the question to make this explicit.  
> **username_1**: The Coq website should probably give better advice. Not every question about Coq is research-level.  

---

## 1 answers

### Answer by username_2 on 2020-02-04. Score: 1 | Accepted answer

*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](https://en.wikipedia.org/wiki/Church_encoding) , which is good because that encoding becomes impossible when you move from untyped lambda calculus to STLC. [See these course notes.](https://www3.nd.edu/~dchiang/teaching/pl/2019/stlc.html) See also the [Wikipedia page on System F](https://en.wikipedia.org/wiki/System_F#System_F_structures) for more information---System F is less expressive than $\mathsf{CC}$ but still good enough to play this game.

> **Comments:**
> **username_0**: 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 @)  
> **username_0**: 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.  
> **username_0**: 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 _  

---

