Mixing
what 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. https://www.youtube.com/watch?v=7HKbjYqqPPQ
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 follow:
$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
asked 3 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. https://www.youtube.com/watch?v=7HKbjYqqPPQ
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 follow:
$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
asked 3 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. https://www.youtube.com/watch?v=7HKbjYqqPPQ
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 follow:
$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
asked 3 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. https://www.youtube.com/watch?v=7HKbjYqqPPQ
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 follow:
$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
asked 3 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 3 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 2 hours ago
asked 3 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 3 hours ago
Jim Newton
234
asked 3 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
4
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 2 hours ago
chi
9,9981525
add a comment |Â
up vote
0
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.6k1594179
add a comment |Â
2 Answers
2
active
oldest
votes
2 Answers
2
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
4
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 2 hours ago
chi
9,9981525
add a comment |Â
up vote
4
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 2 hours ago
chi
9,9981525
add a comment |Â
up vote
4
down vote
accepted
up vote
4
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 2 hours ago
chi
9,9981525
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 2 hours ago
chi
9,9981525
edited 2 hours ago
answered 2 hours ago
chi
9,9981525
answered 2 hours ago
chi
9,9981525
answered 2 hours ago
chi
9,9981525
9,9981525
add a comment |Â
add a comment |Â
up vote
0
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.6k1594179
add a comment |Â
up vote
0
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.6k1594179
add a comment |Â
up vote
0
down vote
up vote
0
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.6k1594179
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.6k1594179
answered 1 hour ago
David Richerby
61.6k1594179
answered 1 hour ago
David Richerby
61.6k1594179
answered 1 hour ago
David Richerby
61.6k1594179
61.6k1594179
add a comment |Â
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%2fwhat-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
