6
$\begingroup$

I'm working through "Types and Programming Languages" by Benjamin Pierce and I don't quite understand the notation. Particularly on Page 106, (chapter 9 Simply Typed Lambda-Calculus) there is a lemma (9.3.7):

$$ \text{If } \Gamma \vdash t:T \text{ and } x \notin dom(\Gamma) \text{, then } \Gamma, x:S \vdash t:T. $$

I understand the idea roughly but I can't quite read this statement out in english. How do I translate the turnstile symbol (\vdash in tex) in this context? In the book I've seen $$ \vdash t:T $$ translated as t is a closed, well-typed term but I don't quite see how to apply that in this context. Looking around apparently the turnstile symbol is also used to mean provable.

Gamma is the typing context and provides binding of variables and their types. t:T means the term t is has the type T. The function dom(gamma) is the set of variables bound by Gamma.

So my best guess for translating this is as follows:

If the term t having type T is a closed, well-typed term under the typing context gamma and x is not in the set of bound variables of gamma, then the term t having type T is still a closed, well-typed term in the typing context gamma after binding the term x having type S.

Is this roughly right? It makes sense but I still feel a bit shaky on the translation. Anyone have any other suggestions, corrections, or comments? Thanks

$\endgroup$
6
$\begingroup$

$X \vdash Y$ means "The information in $X$ lets you prove that $Y$ is true." This is true in logic in general, as well as in type theory specifically. I often read this as "$X$ says that $Y$ is true."

So,

If $\Gamma\vdash t\colon T$ and $x\notin\mathrm{dom}(\Gamma)$, then $\Gamma,x\colon S\vdash t\colon T$

translates as

If we can prove that that $t$ has type $T$ using $\Gamma$, and $\Gamma$ doesn't directly assign a type to $x$, then adding to $\Gamma$ the assumption that $x$ has type $S$ doesn't change the type of $t$,

which is just my way of writing what you wrote.

$\endgroup$
  • $\begingroup$ Thanks, that is quite a bit clearer than my interpretation. $\endgroup$ – Hath995 Apr 25 '15 at 21:15

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.