[Solved]: type theory notation troubles

Problem Detail: 

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

Asked By : Hath995

Answered By : David Richerby

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

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/41834

3.2K people like this

 Download Related Notes/Documents