What does the leading turnstile operator mean?

Question

I know that different authors use different notation to represent programming language semantics. As a matter of fact Guy Steele addresses this problem in an interesting video.

I'd like to know if anyone knows whether the leading turnstile operator has a well recognized meaning. For example I don't understand the leading $\vdash$ operator at the beginning of the denominator of the following:

$$\frac{x:T_1 \vdash t_2:T_2}{\vdash \lambda x:T_1 . t_2 ~:~ T_1 \to T_2}$$

Can someone help me understand? Thanks.

Answer 1

On the left of the turnstile, you can find the local context, a finite list of assumptions on the types of the variables at hand.

$$ x_1:T_1, \ldots, x_n:T_n \vdash e:T $$

Above, $n$ can be zero, resulting in $\vdash e:T$. This means that no assumptions on variables are made. Usually, this means that $e$ is a closed term (without any free variables) having type $T$.

Often, the rule you mention is written in a more general form, where there can be more hypotheses than the one mentioned in the question.

$$ \dfrac{ \Gamma, x:T_1 \vdash t : T_2 }{ \Gamma\vdash (\lambda x:T_1. t) : T_1\to T_2 } $$

Here, $\Gamma$ represents any context, and $\Gamma, x:T_1$ represents its extension obtained by appending the additional hypothesis $x:T_1$ to the list $\Gamma$. It is common to require that $x$ did not appear in $\Gamma$, so that the extension does not "conflict" with a previous assumption.

Answer 2

As a complement to the other answers, note that there are three levels of "implication" in typing derivations. And the same remark holds with logical derivations since there is actually a correspondence between the two (called the Curry-Howard's correspondance).

The first implication is the arrow that appears in formulas, and it corresponds to logical implication in a formula (or a function type for the $\lambda$-calculus).

The second implication is materialized by the turnstile symbol, and means "assuming every formula on the left, the formula on the right holds". In particular, the rule you give tells how one should prove an implication: to prove $A \Rightarrow B$, then one must prove $B$ under the assumption that $A$ holds. In terms of the $\lambda$-calculus, to prove that $\lambda x.t$ has type $A \to B$, one must show that $t$ has type $B$, assuming that $x$ is a variable of type $A$ (see the correspondence?).

The third level of implication is materialized by the horizontal bar, and means "if every premise (elements at the top) holds, then the conclusion (the element at the bottom) holds". You can link that to the interpretation of the typing rule for $\lambda$-abstraction that you gave (see the explanation in the previous paragraph).

Answer 3

In type checking systems, the ($\vdash$) represents the ternary relation over type environments, expressions and types: $\vdash \texttt Env \times \texttt Exp \times \texttt Typ$.

In your example, the expression $t_2$ is typed at type $T_2$ wrt a type environment having a type assumption mapping $T_1$ to some type variable $x$

In this context, a type environment is a partial function that assigns types to variables, usually denoted with $\Gamma$ where $\Gamma \in \texttt Env : Var \rightharpoonup Typ$

Note that, the operator reserves its functionality regardless of where it appears, either in the premise or the conclusion of the rule.

Answer 4

In every situation that I've seen, $X\vdash Y$ means that there is a proof of $Y$ assuming that $X$ holds. If $X$ is empty, that means that $Y$ is a tautology: it has a proof without needing any assumptions.