<p>You should <span class="math-container">$\alpha$</span>-rename to avoid conflict with the variable names. That is, you should prove weakening of the form: <span class="math-container">$\Gamma \vdash (\upsilon y) P$</span> implies <span class="math-container">$\Gamma, x : T \vdash (\upsilon y) P$</span>.</p>
<p><span class="math-container">$\alpha$</span>-equivalence and capture-avoiding substitution is an important concept to understand in type theory: I would recommend studying this concept for the untyped or simply-typed <span class="math-container">$\lambda$</span>-calculus to begin with, before trying to prove things about a more complicated calculus.</p>

CC BY-SA 4.0
2020-09-08T10:39:02.910Z
Thank you for the answer! (That was fast!)

I'm aware of alpha-conversion and I'm defining it earlier in the text I'm writing. Also, I'm following Barendregt's variable convention, i.e. no name can be both free and bound and no name can be binding with two different scopes. The problem was, that definition for type environment didn't explicitly specify the names in the environment as free occurrences. After reading your answer, it seems quite clear (and I feel a bit stupid). Following Barendregt's variable convention, that "problematic" type judgement is not well formed.
PePe
CC BY-SA 4.0
2020-09-08T10:51:49.173Z
Authors will often leave out (deliberately or accidentally) these subtle conditions with variable naming, because it's generally assumed in type theory that variable bindings must not conflict, etc. So if the author hasn't specified it, but it seems necessary to make everything work, it's best just to assume the condition is implicit.
varkor
CC BY-SA 4.0
2020-09-08T11:05:31.643Z
It seems so :) That is good advice! I was trying to read the definitions and rules just as they are and I got very confused with this case. Usually I can find at least one work (article, lecture notes etc.), that gives the definite answer, but this time I couldn't. Then I started to think I'm missing something. I'm glad I asked here, this helps a lot.
PePe
CC BY-SA 4.0
2020-09-08T09:29:58.010Z
2020-09-08T09:29:58.010Z
varkor
<p>I'm writing a thesis about session types and am currently writing a section concerning type soundness for the system. I started to proof weakening lemma, which states, that
<span class="math-container">$$
\text{If } \Gamma \vdash P, \text{ then } \Gamma, x:T \vdash P.
$$</span>
That is, names not free in a process can be added to the typing environment. However, I can't understand how to find a derivation for
<span class="math-container">$$
\Gamma, x:T \vdash (\upsilon x)P
$$</span>
The rule T-RES for restriction is
<span class="math-container">$$
\frac
{
  \Gamma, x:T \vdash P
}
{
  \Gamma \vdash (\upsilon x)P
}
$$</span>
I tried to find a proof for the lemma (for session types, pi-calculus or other calculi), but all the proofs seemed to be something like &quot;a straightforward induction on the derivation of <span class="math-container">$\Gamma \vdash P$</span>&quot;.</p>
<p>I'm trying to understand, what I'm misunderstanding or missing. The rule T-PAR explicitly states, that <span class="math-container">$x$</span> is not in the environment in <span class="math-container">$\Gamma \vdash (\upsilon x)P$</span>. However, the lemma states, that <span class="math-container">$\Gamma, x:T \vdash (\upsilon x)P$</span> is valid.</p>

<type-systems><pi-calculus><soundness>
Pi-calculus (or session types) - proof for weakening lemma
PePe
# Pi-calculus (or session types) - proof for weakening lemma

(Asked by: username_0 on 2020-09-08)

I'm writing a thesis about session types and am currently writing a section concerning type soundness for the system. I started to proof weakening lemma, which states, that
$$
\text{If } \Gamma \vdash P, \text{ then } \Gamma, x:T \vdash P.
$$
That is, names not free in a process can be added to the typing environment. However, I can't understand how to find a derivation for
$$
\Gamma, x:T \vdash (\upsilon x)P
$$
The rule T-RES for restriction is
$$
\frac
{
\Gamma, x:T \vdash P
}
{
\Gamma \vdash (\upsilon x)P
}
$$
I tried to find a proof for the lemma (for session types, pi-calculus or other calculi), but all the proofs seemed to be something like "a straightforward induction on the derivation of $\Gamma \vdash P$".

I'm trying to understand, what I'm misunderstanding or missing. The rule T-PAR explicitly states, that $x$ is not in the environment in $\Gamma \vdash (\upsilon x)P$. However, the lemma states, that $\Gamma, x:T \vdash (\upsilon x)P$ is valid.

**Tags:** type-systems, pi-calculus, soundness

---

## 1 answers

### Answer by username_1 on 2020-09-08. Score: 4 | Accepted answer

You should $\alpha$-rename to avoid conflict with the variable names. That is, you should prove weakening of the form: $\Gamma \vdash (\upsilon y) P$ implies $\Gamma, x : T \vdash (\upsilon y) P$.

$\alpha$-equivalence and capture-avoiding substitution is an important concept to understand in type theory: I would recommend studying this concept for the untyped or simply-typed $\lambda$-calculus to begin with, before trying to prove things about a more complicated calculus.

> **Comments:**
> **username_0**: Thank you for the answer! (That was fast!)  I'm aware of alpha-conversion and I'm defining it earlier in the text I'm writing. Also, I'm following Barendregt's variable convention, i.e. no name can be both free and bound and no name can be binding with two different scopes. The problem was, that definition for type environment didn't explicitly specify the names in the environment as free occurrences. After reading your answer, it seems quite clear (and I feel a bit stupid). Following Barendregt's variable convention, that "problematic" type judgement is not well formed.  
> **username_1**: Authors will often leave out (deliberately or accidentally) these subtle conditions with variable naming, because it's generally assumed in type theory that variable bindings must not conflict, etc. So if the author hasn't specified it, but it seems necessary to make everything work, it's best just to assume the condition is implicit.  
> **username_0**: It seems so :) That is good advice! I was trying to read the definitions and rules just as they are and I got very confused with this case. Usually I can find at least one work (article, lecture notes etc.), that gives the definite answer, but this time I couldn't. Then I started to think I'm missing something. I'm glad I asked here, this helps a lot.  

---

