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

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

<p>$\sigma&gt;\rho\quad$ if $\quad\dfrac{\Gamma\vdash P:\sigma}{\Gamma\vdash P:\rho}$</p>

<p>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&gt;\forall\alpha.\sigma$, then $\alpha\notin FV(\Gamma)$, which is exactly what he needs in the proof (and from where the imprecision comes).</p>

CC BY-SA 3.0
2012-02-27T09:45:05.097Z
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)](http://www.lmcs-online.org/ojs/viewarticle.php?id=984).
Alejandro DC
CC BY-SA 3.0
2011-11-11T11:30:03.387Z
2011-11-11T11:36:19.213Z
2011-11-11T11:36:19.213Z
Alejandro DC
<p>I found a problem in Barendregt's proof of subject reduction (Thm 4.2.5 of <a href="http://www.cs.rhul.ac.uk/~zhaohui/Barendregt92.pdf" title="Lambda calculi with types">Lambda calculi with types</a>).</p>

<p>The last step of the proof (page 60), says:</p>

<p>"and hence by Lemma 4.1.19(1), $\quad\Gamma,x:\rho\vdash P:\sigma&#39;$."</p>

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

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

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

<p>Can somebody, please, tell me what I am missing here?</p>

CC BY-SA 3.0
2011-11-09T14:31:05.107Z
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.
Dave Clarke
CC BY-SA 3.0
2011-11-09T15:03:10.553Z
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...
Alejandro DC
<lo.logic><type-theory><lambda-calculus><proof-theory>
Barendregt's proof of subject reduction for $\lambda2$
Alejandro DC
# Barendregt's proof of subject reduction for $\lambda2$

(Asked by: username_0 on 2011-11-09)

I found a problem in Barendregt's proof of subject reduction (Thm 4.2.5 of [Lambda calculi with types](http://www.cs.rhul.ac.uk/~zhaohui/Barendregt92.pdf "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?

**Tags:** lo.logic, type-theory, lambda-calculus, proof-theory

> **Comments:**
> **username_1**: 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.  
> **username_0**: 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...  

---

## 1 answers

### Answer by username_0 on 2011-11-11. Score: 8 | Accepted answer

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

> **Comments:**
> **username_0**: 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)](http://www.lmcs-online.org/ojs/viewarticle.php?id=984).  

---

