ここでは <式> の代わりに e という記号(メタ変数),<識別子> の代わりに x という記号(メタ変数)を用いている. また,型(メタ変数 τ)として,整数を表す int, 真偽値を表す boolを考える. さて,型推論のアルゴリズムを考える前に,そもそも「式 e が型 τ を持つ」という関係がどのような時に成立するかを正確に記述したい. 例えば「式 1+1 は型 int を持つ」だろうが, 「式 if 1 then 2+3 else 4 は型 int を持つ」は 成立しないと思われる.この,「式 e が型 τ を持つ」 という判断を型判断(type judgment)と呼び,e : τ と略記する. しかし,一般に式には変数が現れるため,例えば単に x が int を持つか,といわれても判断することができない.このため,変数に対しては,そ れが持つ型を何か仮定しないと型判断は下せ