単純階型理論の推論をしてみる
まずは簡単な例から
$ K\equiv \lambda xy.x: A\to B\to Aを推論する
一番下に書く
https://gyazo.com/3e946c47ab7b44459a3df9da1925cbee
ラムダ抽象の略記をやめたり、関数型に括弧をつけるとわかりやすい
→は右結合
https://gyazo.com/9df603da182c65c60ac19b4c2546657d
→を導入
https://gyazo.com/6d6016abd67d1214c5617620da70a56d
さらに→を導入
https://gyazo.com/22a369bd57a8be152b6afc005b6af6bf
おわり