Mixing
wWhat does the leading turnstile operator mean?
Clash Royale CLAN TAG#URR8PPP
up vote
1
down vote
favorite
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:
$$fracx:T_1 vdash t_2:T_2vdash lambda x:T_1 . t_2 ~:~ T_1 to T_2$$
Can someone help me understand?
Thanks.
type-theory denotational-semantics
edited 30 mins ago
David Richerby
61.7k1594179
asked 4 hours ago
Jim Newton
234
New contributor
Jim Newton is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
add a comment |Â
up vote
1
down vote
favorite
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:
$$fracx:T_1 vdash t_2:T_2vdash lambda x:T_1 . t_2 ~:~ T_1 to T_2$$
Can someone help me understand?
Thanks.
type-theory denotational-semantics
edited 30 mins ago
David Richerby
61.7k1594179
asked 4 hours ago
Jim Newton
234
New contributor
Jim Newton is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
add a comment |Â
up vote
1
down vote
favorite
up vote
1
down vote
favorite
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:
$$fracx:T_1 vdash t_2:T_2vdash lambda x:T_1 . t_2 ~:~ T_1 to T_2$$
Can someone help me understand?
Thanks.
type-theory denotational-semantics
edited 30 mins ago
David Richerby
61.7k1594179
asked 4 hours ago
Jim Newton
234
New contributor
Jim Newton is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
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:
$$fracx:T_1 vdash t_2:T_2vdash lambda x:T_1 . t_2 ~:~ T_1 to T_2$$
Can someone help me understand?
Thanks.
type-theory denotational-semantics
type-theory denotational-semantics
edited 30 mins ago
David Richerby
61.7k1594179
asked 4 hours ago
Jim Newton
234
New contributor
Jim Newton is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
edited 30 mins ago
David Richerby
61.7k1594179
asked 4 hours ago
Jim Newton
234
New contributor
Jim Newton is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
edited 30 mins ago
David Richerby
61.7k1594179
edited 30 mins ago
David Richerby
61.7k1594179
edited 30 mins ago
David Richerby
61.7k1594179
61.7k1594179
asked 4 hours ago
Jim Newton
234
New contributor
Jim Newton is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
asked 4 hours ago
Jim Newton
234
asked 4 hours ago
Jim Newton
234
234
New contributor
Jim Newton is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
New contributor
Jim Newton is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
Jim Newton is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
add a comment |Â
add a comment |Â
2 Answers
2
active
oldest
votes
up vote
5
down vote
accepted
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 also 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 also can be more hypotheses than the one mentioned in the question.
$$
dfrac
Gamma, x:T_1 vdash t : T_2
Gammavdash (lambda x:T_1. t) : T_1to 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.
answered 3 hours ago
chi
10k1525
add a comment |Â
up vote
1
down vote
In every situation that I've seen, $Xvdash 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.
answered 1 hour ago
David Richerby
61.7k1594179
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 $fracXvdash Y$ would mean if the $X$ is true then $Y$ is unconditionally true.
– Jim Newton
30 mins ago
1
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...
– David Richerby
28 mins ago
add a comment |Â
2 Answers
2
active
oldest
votes
2 Answers
2
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
5
down vote
accepted
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 also 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 also can be more hypotheses than the one mentioned in the question.
$$
dfrac
Gamma, x:T_1 vdash t : T_2
Gammavdash (lambda x:T_1. t) : T_1to 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.
answered 3 hours ago
chi
10k1525
add a comment |Â
up vote
5
down vote
accepted
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 also 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 also can be more hypotheses than the one mentioned in the question.
$$
dfrac
Gamma, x:T_1 vdash t : T_2
Gammavdash (lambda x:T_1. t) : T_1to 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.
answered 3 hours ago
chi
10k1525
add a comment |Â
up vote
5
down vote
accepted
up vote
5
down vote
accepted
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 also 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 also can be more hypotheses than the one mentioned in the question.
$$
dfrac
Gamma, x:T_1 vdash t : T_2
Gammavdash (lambda x:T_1. t) : T_1to 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.
answered 3 hours ago
chi
10k1525
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 also 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 also can be more hypotheses than the one mentioned in the question.
$$
dfrac
Gamma, x:T_1 vdash t : T_2
Gammavdash (lambda x:T_1. t) : T_1to 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.
answered 3 hours ago
chi
10k1525
edited 3 hours ago
answered 3 hours ago
chi
10k1525
answered 3 hours ago
chi
10k1525
answered 3 hours ago
chi
10k1525
10k1525
add a comment |Â
add a comment |Â
up vote
1
down vote
In every situation that I've seen, $Xvdash 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.
answered 1 hour ago
David Richerby
61.7k1594179
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 $fracXvdash Y$ would mean if the $X$ is true then $Y$ is unconditionally true.
– Jim Newton
30 mins ago
1
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...
– David Richerby
28 mins ago
add a comment |Â
up vote
1
down vote
In every situation that I've seen, $Xvdash 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.
answered 1 hour ago
David Richerby
61.7k1594179
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 $fracXvdash Y$ would mean if the $X$ is true then $Y$ is unconditionally true.
– Jim Newton
30 mins ago
1
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...
– David Richerby
28 mins ago
add a comment |Â
up vote
1
down vote
up vote
1
down vote
In every situation that I've seen, $Xvdash 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.
answered 1 hour ago
David Richerby
61.7k1594179
In every situation that I've seen, $Xvdash 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.
answered 1 hour ago
David Richerby
61.7k1594179
answered 1 hour ago
David Richerby
61.7k1594179
answered 1 hour ago
David Richerby
61.7k1594179
answered 1 hour ago
David Richerby
61.7k1594179
61.7k1594179
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 $fracXvdash Y$ would mean if the $X$ is true then $Y$ is unconditionally true.
– Jim Newton
30 mins ago
1
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...
– David Richerby
28 mins ago
add a comment |Â
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 $fracXvdash Y$ would mean if the $X$ is true then $Y$ is unconditionally true.
– Jim Newton
30 mins ago
1
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...
– David Richerby
28 mins ago
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 $fracXvdash Y$ would mean if the $X$ is true then $Y$ is unconditionally true.
– Jim Newton
30 mins ago
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 $fracXvdash Y$ would mean if the $X$ is true then $Y$ is unconditionally true.
– Jim Newton
30 mins ago
1
1
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...
– David Richerby
28 mins ago
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...
– David Richerby
28 mins ago
add a comment |Â
Jim Newton is a new contributor. Be nice, and check out our Code of Conduct.
Jim Newton is a new contributor. Be nice, and check out our Code of Conduct.
Jim Newton is a new contributor. Be nice, and check out our Code of Conduct.
Jim Newton is a new contributor. Be nice, and check out our Code of Conduct.
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fcs.stackexchange.com%2fquestions%2f97442%2fwwhat-does-the-leading-turnstile-operator-mean%23new-answer', 'question_page');
);
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
