5
$\begingroup$

In type application Rule :

$$\dfrac{ \Gamma \vdash t_1 : T_{11} \to T_{12} \qquad \Gamma \vdash t_2 : T_{11}} { \Gamma \vdash t_1 \ t_2 : T_{12} } \textsf{ (T-App)}$$

if we deriving the term from bottom up, how to get $T_{11}$ from ? How you'll know what is $T_{11}$? Its not clear to me.

$\endgroup$
  • 2
    $\begingroup$ It's because this community wants to be kind of encyclopedia of Q&A. By helping you with your particular problem people want future learners to benefit from their knowledge. There can be lots of questions on some topic or family of topics (like "Type application Rule"). So imagine what will happen if all possible questions will have the same title. That's why Raphael justifiably insists on giving more precise titles. So definitely nothing personal here. $\endgroup$ – Anton Trunov Apr 1 '16 at 18:29
  • 1
    $\begingroup$ Did you mean "deriving the term from bottom up" or "deriving the type from bottom up". If you have a term $t_1\,t_2$ and want to derive its type, using the rule, in a bottom up fashion, here's what you do: Find the type of $t_1$; find the type of $t_2$; use the application rule, if possible, to find the type of $t_1\,t_2$. $t_11$ is the type of $t_1$. $\endgroup$ – Theodore Norvell Apr 1 '16 at 21:11
9
$\begingroup$

You can look at this rule in two ways:

As a checking rule, it says that, to verify that $t_1 t_2$ has type $T_{12}$, we check that there exists some $T_{11}$ such that $t_1 : T_{11} \to T_{12}$, and we check that $t_2 : T_{11}$. If these checks hold, then the typing of the application must hold.

As an inference rule, it says that to infer the type of $t_1 t_2$, we infer the type of $t_1$ and verify that it has the form $T_{11} \to T_{12}$ for some types $T_{11}, T_{12}$, infer the type for $t_2$ and check that it is equal to $T_{11}$. If these checks hold, then we return $T_{12}$ as the type of the application.

So for knowing what $T_{11}$ is, it depends on what you're doing. If you're doing checking, then usually it is a type that has already been given to you. If you're doing inference, then you infer the type of the function, and inspect that type to verify that it's an arrow type, and can be broken into its parts. $T_{11}$ is one of these parts you break it into.

There's nothing saying you need to get $T_{11}$ only from the function's type. You could alternately infer it from the type of the argument, and then verify that it matched the function type.

$\endgroup$
5
$\begingroup$

The rules state what kinds of proofs are valid. No one ever promised it would always be easy to find a valid proof for any particular term of your choice. There may be multiple rules that could be used at any point; it's not the type rules' job to do anything about that.

Instead, that's the role of a type-checking algorithm. Depending on the type system, there may or may not be an efficient algorithm to find a valid proof (one that's deemed valid according to the rules), i.e., a valid sequence of rules to apply that proves the desired result.

$\endgroup$
  • $\begingroup$ Okay. thanks. While solving , i generally assume what T11 is should have. Is that okay ? $\endgroup$ – Pushpa Apr 1 '16 at 17:10
0
$\begingroup$

You can't derive bottom up. It doesn't matter what T11 is. It's just some type; the rule holds no matter what it is. More precisely: if this is supposed to be a rule in a sequent calculus then I believe it is incomplete. The bottom sequent should have type annotations for every term. So you already have t11. Which suggests that jmite's answer is not quite right, insofar as it says we need to find some t11. But we dont, we're already given it in the premises, and the rule carries it over to the conclusion. If all you have is a,b:T, and you do not already know the types of a and b, you cannot infer them.

$\endgroup$
0
$\begingroup$

T11 is can be find on derivation on the right branch of that rule for type checking. On the right hand branch, you will eventually have

    {x:T}|-x:T11 

something like this. You apply "T_VAR" rule and get "T11=T". since above statement says, variable "x is type of T in syntax" there T should be equal to T11.

try some type checking, denote T11, then you see eventually T11 equals some type which is already known.

$\endgroup$

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.