12
$\begingroup$

I found a problem in Barendregt's proof of subject reduction (Thm 4.2.5 of Lambda calculi with types).

The last step of the proof (page 60), says:

"and hence by Lemma 4.1.19(1), $\quad\Gamma,x:\rho\vdash P:\sigma'$."

However, according to Lemma 4.1.19(1) it should be $\Gamma[\vec{\alpha}:=\vec{\tau}],x:\rho\vdash P:\sigma'$, since the substitution is made to the whole context, not only to $x:\rho'$.

I guess the standard solution may be to somehow prove that $\vec{\alpha}\notin FV(\Gamma)$, but I am not sure how.

I had a proof simplifying it by relaxing the generation lemma of abstractions, but I recently found that there was a mistake and my proof is wrong, so I am not sure how to solve this problem any more.

Can somebody, please, tell me what I am missing here?

Improve this question
$\endgroup$
2
  • $\begingroup$ Barendregt assumes the so-called variable convention, that bound variable names and free variable names are standardized apart, namely, we implicitly assume that they are different (using $\alpha$-conversion. Maybe this helps. $\endgroup$
    – Dave Clarke
    Nov 9, 2011 at 14:31
  • $\begingroup$ Thanks for your answer. But yet, it does not solve the problem. He arrives to $\Gamma,x:\rho\vdash P:\sigma'$ by using Lemma 4.1.19(1) in the following way: we has $\Gamma,x:\rho'\vdash P:\sigma''$ and we knows that $\rho'[\vec{\alpha}:=\vec{\tau}]=\rho$ and $\sigma''[\vec{\alpha}:=\vec{\tau}]=\sigma'$, so using that lemma, he can do the same substitution in the context and the inferred type at the same time... but he only substitutes on the x:\rho', no all the context! And that is my problem... $\endgroup$
    – Alejandro DC
    Nov 9, 2011 at 15:03

1 Answer 1

Reset to default
8
$\begingroup$

I still think there is an imprecision in how he uses the lemma. However there is a solution (I must thank to Barbara Petit who came with the solution).

In fact, the solution comes from the definition of $\geq$ (def. 4.2.1), which is morally this:

$\sigma>\rho\quad$ if $\quad\dfrac{\Gamma\vdash P:\sigma}{\Gamma\vdash P:\rho}$

However, instead of defining it in that way, he defines the relation in terms of the types only. The advantage on defining it in terms of sequents, is that we can deduce that if $\sigma>\forall\alpha.\sigma$, then $\alpha\notin FV(\Gamma)$, which is exactly what he needs in the proof (and from where the imprecision comes).

Improve this answer
$\endgroup$
1
  • $\begingroup$ I have used this technique in an extension of System F for the linear-algebraic lambda-calculus. The paper with all the details of the proof has appeared today in LMCS 8(1:11). $\endgroup$
    – Alejandro DC
    Feb 27, 2012 at 9:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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