単純階型理論の型付け規則を使って推論をしていく手順

まずは簡単な例から

K\equiv \lambda xy.x: A\to B\to Aを推論する

一番下に書く

ラムダ抽象の略記をやめたり、関数型に括弧をつけるとわかりやすい

→ は右結合

→ を導入

さらに → を導入

おわり