0
$\begingroup$

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.

$\endgroup$
3
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – PePe Sep 8 at 10:39
  • $\begingroup$ 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. $\endgroup$ – varkor Sep 8 at 10:51
  • $\begingroup$ 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. $\endgroup$ – PePe Sep 8 at 11:05

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.