12
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Related $\endgroup$ – leftaroundabout Sep 17 '18 at 21:23
  • $\begingroup$ Wow, this question has over "1k" views, which is more than the sum of views of all other 29 new questions! As I have checked, neither "type-theory" tag nor "denotational-semantics" tag is among the first 50 popular tags. I am curious about the cause behind this phenomenon. I do not have a clue. @D.W.? Do I have a meta question? $\endgroup$ – Apass.Jack Sep 18 '18 at 6:31
  • $\begingroup$ If I am not mistaken, you have to move the turnstile operator ($\vdash$), in the conclusion of the rule, between $\lambda x:T_1$ and $t_2$. I would also add the type-checking tag $\endgroup$ – mchar Sep 18 '18 at 7:22
  • 3
    $\begingroup$ @Apass.Jack It ended up in Hot Network Questions so is getting more attention because of that. $\endgroup$ – JAB Sep 18 '18 at 7:23
20
$\begingroup$

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.

$\endgroup$
7
$\begingroup$

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

$\endgroup$
3
$\begingroup$

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

$\endgroup$
-1
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ but if what you say is true, this is strange because that's also what the horizontal bar means, right? That if the top is true, then the bottom is true. Thus in effect, the $\frac{X}{\vdash Y}$ would mean if the $X$ is true then $Y$ is unconditionally true. $\endgroup$ – Jim Newton Sep 17 '18 at 13:57
  • 1
    $\begingroup$ The horizontal bar means that the thing on the bottom is an immediate deduction from the thing on the top. Though I agree that it looks very strange in your example that an unconditional truth is derived from a conditional one... $\endgroup$ – David Richerby Sep 17 '18 at 13:59
  • $\begingroup$ Type theory is not logic. It is of course related in many ways and (to some extent intentionally) uses similar notation, but there is certainly no a priori connection to the provability relation, and often no a posteriori connection either (at least not to a remotely reasonable logic). As written the answer is, at best, misleading because it suggests that "$x:T_1$" is a formula which it virtually never is in type theory, e.g. a language containing formulas like $(x:T_1)\lor(y:T_2)$ is generally not described and is often impossible in a standard meta-logic, e.g. for the linear lambda calculus. $\endgroup$ – Derek Elkins Sep 18 '18 at 1:13
  • $\begingroup$ @DerekElkins It's a proof system and proof systems are logics. $x\colon T$ is precisely a proposition, and $\Gamma\vdash x\colon T$ is nothing but the statement that the proposition holds when $\Gamma$ holds. The fact that disjunctions of propositions aren't formulas is simply a restriction of the logic's syntax. $\endgroup$ – David Richerby Sep 18 '18 at 7:47
  • $\begingroup$ It's not just disjunction. None of $\neg (x:A)$, $(x:A)\land(y:B)$, or $(x:A)\to(y:B)$ are formulas either. Or are you saying it's a logic that only has atomic propositions? I mentioned linear logic as an example. In ordered linear logic, it can very easily be the case that $x:A,y:B\vdash t:C$ holds while $y:B,x:A\vdash t:C$ does not. What connectives do the comma and $\vdash$ correspond to that take the "truth values" of $x:A$, $y:B$, and $t:C$ and produce the above behavior? There's an option if the meta-logic is also an ordered linear logic, but then we aren't explaining anything. $\endgroup$ – Derek Elkins Sep 18 '18 at 8:40

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.