# Assertion of Type Inference Rules/Type Checking

I have a problem in a book I am trying to accomplish.

I understand the overall type of the expression is boolean and how it derives. (y * x) will be rule 4 (counting from top right). (y * x) + x when evaluated will be rule 3 and the overall expression when evaluated will be rule 5.

What I want to figure out is what is the correct way to illustrate the my working? Can someone give or link an example of the correct way to answer a question like this?

Question 2

Proposed solution:

Well, you need to construct a typing derivation which has what you want to prove as a conclusion, and no open premise (i.e., leaves must be axioms, or rules with no premises). In the case of your example, the conclusion will be

$$int\;x,\,int\;y\;\vdash\;(x < (x \times y) + x) : bool$$

so the proof will start by

$${int\;x,\,int\;y\;\vdash\;x : int \quad\quad\quad int\;x,\,int\;y\;\vdash\;((x \times y) + x) : int} \over {int\;x,\,int\;y\;\vdash\;(x < ((x \times y) + x)) : bool}$$

and then you continue building up the tree until you reach leaves (i.e., rules with no premises). This will immediately be the case in the left branch since you only have a variable.

Here is the full proof (as an image):

• Thank you for this. Can you please illustrate a more advanced example with multiple branches/more entries in a tree? Commented May 24, 2018 at 14:42
• I wanted to give you the full typing derivation (the full tree), but there does not seem to be any easy way of writing it here... Anyway, it is really easy because you only need to look at the term you want to type. Only one rule apply for every term shape, for instance in the right branch you will want to apply the rule for the $+$ symbol. Commented May 24, 2018 at 14:47
• Thanks, appreciate the help. I think I roughly understand how to do it but still not 100% sure. Do you have any recommendations for external sources/YouTube videos that will give a full example? Commented May 24, 2018 at 14:56
• There are loads of ressources and textbooks, for example cis.upenn.edu/~bcpierce/tapl/index.html. Note that I uploaded an image of the complete proof. Commented May 24, 2018 at 15:07
• A note for future answers: you can draw derivations in LaTeX using \dfrac{premise1 ... premiseN}{conclusion}, suitably nested. (The result is not that good when some premise is a nested dfrac and some other one is not, but one can simply use dfrac on all premises to avoid that case)
– chi
Commented May 25, 2018 at 21:23