<p>You are correct, there is an error in that paper, and the rule should indeed read:
$$\frac{\Gamma\vdash M:\Delta}{\Gamma\vdash M\cong M} $$</p>

<p>the use of jugements of this style for equality (sometimes called "typed equality") originates already in Martin-Löf, I think (see <a href="http://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf" rel="nofollow noreferrer">here</a> for example). It's often replaced with an untyped operational definition in modern treatments, where there is no jugement of the form $\Gamma\vdash N\cong M$, and conversion is defined on raw terms.</p>

<p>Somewhat counter-intuitively, proving that the system with typed conversion is equivalent to the one without types is very difficult, and was settled in 2010 by <a href="https://www.lix.polytechnique.fr/~vsiles/papers/PTSATR.pdf" rel="nofollow noreferrer">Siles and Herbelin</a>.</p>

CC BY-SA 3.0
2016-12-03T15:42:55.757Z
"Modern treatments" here means "computer sciency treatments that are mostly interested in computation".
Andrej Bauer
CC BY-SA 3.0
2016-12-03T16:35:19.203Z
Fair enough. I almost brought up "Swedish" vs "French" schools of type theory, but I'm not sure that distinction actually exists.
cody
CC BY-SA 3.0
2016-12-03T16:38:55.907Z
There is no such distinction, as witnessed by the fact that Thierry Coquand lives in Sweden. They're all computational.
Andrej Bauer
CC BY-SA 3.0
2016-12-07T11:39:52.820Z
@cody: I thought pretty much all modern, computer-sciency treatments uses typed judgments, because it's the most convenient way to get the eta for pi/sigma. (Certainly Coq and Agda support that.)
Neel Krishnaswami
CC BY-SA 3.0
2016-12-07T16:02:38.527Z
@NeelKrishnaswami Typed conversion is necessary for eta to make sense in most situations, but I was under the impression that it could make meta-theory considerably more tricky. Maybe I'm entirely wrong and it actually makes everything simple. There's also the question of optimizing the conversion check in order to do the least amount of work, including extra type-checking obligations. Surely this would be a great follow up question.
cody
CC BY-SA 3.0
2016-12-03T02:52:58.900Z
2016-12-03T02:52:58.900Z
cody
<p>In the classic <a href="http://www.sciencedirect.com/science/article/pii/0890540188900053" rel="nofollow noreferrer">the calculus of constructions</a> paper there is a rule that states</p>

<p><a href="https://i.sstatic.net/4ljmZ.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/4ljmZ.png" alt="enter image description here"></a>
(page 7 of the pdf, page 101 of the original document)</p>

<p>This rule would mean that any context is reducible to a member of that context.  This seems like it shouldn't be correct, as it would entail</p>

<pre><code>1 ≅ Nat
3 ≅ Nat
1 ≅ 3
</code></pre>

<p>if Nat is a context.</p>

<p>I think the best interpretation is that the lower delta was meant to be an M.  Especially considering the rules given on the next page.</p>

<p>So is this simply a typo, or some subtle logical rule that I don't understand?</p>

<lo.logic><calculus-of-constructions><sequent-calculus>
Typo in the calculus of constructions paper?
user833970
# Typo in the calculus of constructions paper?

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

In the classic the calculus of constructions paper there is a rule that states

(page 7 of the pdf, page 101 of the original document)
This rule would mean that any context is reducible to a member of that context.  This seems like it shouldn't be correct, as it would entail
1 ≅ Nat
3 ≅ Nat
1 ≅ 3

if Nat is a context.
I think the best interpretation is that the lower delta was meant to be an M.  Especially considering the rules given on the next page.
So is this simply a typo, or some subtle logical rule that I don't understand?

**Tags:** lo.logic, calculus-of-constructions, sequent-calculus


---

## 1 answers

### Answer by username_1 on 2016-12-03. Score: 11 | Accepted answer

You are correct, there is an error in that paper, and the rule should indeed read:
$$\frac{\Gamma\vdash M:\Delta}{\Gamma\vdash M\cong M} $$

the use of jugements of this style for equality (sometimes called "typed equality") originates already in Martin-Löf, I think (see [here](http://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf) for example). It's often replaced with an untyped operational definition in modern treatments, where there is no jugement of the form $\Gamma\vdash N\cong M$, and conversion is defined on raw terms.

Somewhat counter-intuitively, proving that the system with typed conversion is equivalent to the one without types is very difficult, and was settled in 2010 by [Siles and Herbelin](https://www.lix.polytechnique.fr/~vsiles/papers/PTSATR.pdf).

> **Comments:**
> **username_2**: "Modern treatments" here means "computer sciency treatments that are mostly interested in computation".  
> **username_1**: Fair enough. I almost brought up "Swedish" vs "French" schools of type theory, but I'm not sure that distinction actually exists.  
> **username_2**: There is no such distinction, as witnessed by the fact that Thierry Coquand lives in Sweden. They're all computational.  
> **username_3**: @username_1: I thought pretty much all modern, computer-sciency treatments uses typed judgments, because it's the most convenient way to get the eta for pi/sigma. (Certainly Coq and Agda support that.)  
> **username_1**: @NeelKrishnaswami Typed conversion is necessary for eta to make sense in most situations, but I was under the impression that it could make meta-theory considerably more tricky. Maybe I'm entirely wrong and it actually makes everything simple. There's also the question of optimizing the conversion check in order to do the least amount of work, including extra type-checking obligations. Surely this would be a great follow up question.  

---

