10
$\begingroup$

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

enter image description here (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?

|cite|improve this question
$\endgroup$
11
$\begingroup$

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

|cite|improve this answer
$\endgroup$
  • $\begingroup$ "Modern treatments" here means "computer sciency treatments that are mostly interested in computation". $\endgroup$ – Andrej Bauer Dec 3 '16 at 15:42
  • $\begingroup$ Fair enough. I almost brought up "Swedish" vs "French" schools of type theory, but I'm not sure that distinction actually exists. $\endgroup$ – cody Dec 3 '16 at 16:35
  • $\begingroup$ There is no such distinction, as witnessed by the fact that Thierry Coquand lives in Sweden. They're all computational. $\endgroup$ – Andrej Bauer Dec 3 '16 at 16:38
  • $\begingroup$ @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.) $\endgroup$ – Neel Krishnaswami Dec 7 '16 at 11:39
  • $\begingroup$ @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. $\endgroup$ – cody Dec 7 '16 at 16:02

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.