# 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? – Frank Duckworth West May 24 '18 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. – Rodolphe Lepigre May 24 '18 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? – Frank Duckworth West May 24 '18 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. – Rodolphe Lepigre May 24 '18 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 May 25 '18 at 21:23