ラムダ計算 #5 型検査・型推論演習 - 気まぐれエンジニア日記

ラムダ計算セルフブログリレー5日目, 最終回です. 今日も平常運転, くまちゃんです. 4日目はこちら.
あれ？4日目をさっき書いたような気もするんですけど...まあいいでしょ笑笑
kumachan-math.hatenablog.jp

今日は例を使ってバリバリ証明図を書いていくぞー！おー٩( 'ω' )و

5.1 型検査

問題1. $\vdash \lambda x.x::\mathrm{nil}:\mathrm{int} \to \mathrm{list}(\mathrm{int})$ を示す証明図を書け.

$\displaystyle \frac{ \displaystyle \frac{ \overline{x:\mathrm{int} \vdash x:\mathrm{int}}~~~\overline{x:\mathrm{int} \vdash \mathrm{nil}:\mathrm{list}(\mathrm{int})} }{ x:\mathrm{int} \vdash x::\mathrm{nil}:\mathrm{list}(\mathrm{int}) } }{ \vdash \lambda x.x::\mathrm{nil}:\mathrm{int} \to \mathrm{list}(\mathrm{int}) }$

ラムダ抽象は, 引数を型環境の方に追い出して, その型環境のもとで返り値のラムダ式の型を規定する(abs)ということに注意しておきましょう.
また, 上に積まれる推論規則は下にあるものの計算環境を引き継ぐことにも注意しましょう.

問題2. $\vdash (\mathrm{let}~f = \lambda x.x::\mathrm{nil}~\mathrm{in}~f~0):\mathrm{list}(\mathrm{int})$ を示す証明図を書け.

$\displaystyle \frac{ \displaystyle \frac{ 問題1 }{ \vdash \lambda x.x::\mathrm{nil}:\mathrm{int} \to \mathrm{list}(\mathrm{int}) } ~~~ \displaystyle \frac{ \overline{f:\mathrm{int} \to \mathrm{list}(\mathrm{int}) \vdash f:\mathrm{int} \to \mathrm{list}(\mathrm{int})} ~~~ \overline{f:\mathrm{int} \to \mathrm{list}(\mathrm{int}) \vdash 0:\mathrm{int}} }{ f:\mathrm{int} \to \mathrm{list}(\mathrm{int}) \vdash f~0:\mathrm{int} } }{ \vdash (\mathrm{let}~f = \lambda x.x::\mathrm{nil}~\mathrm{in}~f~0):\mathrm{list}(\mathrm{int}) }$

問題3. $\vdash \lambda x. \lambda y. \lambda z. x(yz):(\tau_2 \to \tau_3) \to (\tau_1 \to \tau_2) \to \tau_1 \to \tau_3$ を示せ

$\displaystyle \frac{ \displaystyle \frac{ \displaystyle \frac{ \displaystyle \frac{ \displaystyle \frac{}{x: \tau_2 \to \tau_3, y: \tau_1 \to \tau_2, z:\tau_1, \vdash x: \tau_2 \to \tau_3} ~~~ \displaystyle \frac{ \displaystyle \frac{}{x: \tau_2 \to \tau_3, y: \tau_1 \to \tau_2, z:\tau_1, \vdash y:\tau_1\to \tau_2} ~~~ \displaystyle \frac{}{x: \tau_2 \to \tau_3, y: \tau_1 \to \tau_2, z:\tau_1, \vdash z:\tau_1} }{ x: \tau_2 \to \tau_3, y: \tau_1 \to \tau_2, z:\tau_1, \vdash yz: \tau_2 } }{ x: \tau_2 \to \tau_3, y: \tau_1 \to \tau_2, z:\tau_1, \vdash x(yz): \tau_3 } }{ x: \tau_2 \to \tau_3, y: \tau_1 \to \tau_2 \vdash \lambda z. x(yz): \tau_1 \to \tau_3 } }{ x: \tau_2 \to \tau_3 \vdash \lambda y. \lambda z. x(yz): (\tau_1 \to \tau_2) \to \tau_1 \to \tau_3 } }{ \vdash \lambda x. \lambda y. \lambda z. x(yz):(\tau_2 \to \tau_3) \to (\tau_1 \to \tau_2) \to \tau_1 \to \tau_3 }$

うーんもう何もわからん. 多分あってると思うんですよ. 知らんけど. (abs)と(app)と(var)をたくさん使いました. それしか覚えてません.

5.2型推論

答えの型がわからず推論をしなければいけない場合には, 答えの型を変数でおいていって, 連立方程式のようなものを解くことで型を導きます.

問題4: $\lambda x.x::x$ はいかなる型も持たないことを示せ.

$\lambda x.x::x$ が $\tau$ 型を持つと仮定して証明図を書くと矛盾することを示す.
$\displaystyle \frac{ \displaystyle \frac{ \displaystyle \frac{}{ x: \tau_1 \vdash x: \tau_3 } ~~~ \displaystyle \frac{}{ x: \tau_1 \vdash x: \mathrm{list}(\tau_3) } }{ x: \tau_1 \vdash x::x:\tau_2 } }{ \vdash \lambda x.x::x:\tau }$

これが正しい証明図であるためには,
$\displaystyle \begin{cases} \tau = \tau_1 \to \tau_2 \\ \tau_1 = \tau_3 \\ \tau_1 = \mathrm{list}(\tau_3) \\ \tau_2 = \mathrm{list}(\tau_3) \end{cases}$
でなければなければならないが, これらからは, $\tau_3 = \mathrm{list}(\tau_3)$ が導かれるため矛盾する.

問題5. $\lambda x.\lambda y.x$ の主型を推論せよ.
型変数をおいて証明図を書くと次のようになる.
$\displaystyle \frac{ \displaystyle \frac{ \displaystyle \frac{}{x: \tau_x, y: \tau_y \vdash x:\tau_2} }{ x: \tau_x \vdash \lambda y.x: \tau_1 } }{ \vdash \lambda x.\lambda y.x: \tau }$
これが正しい証明図であるためには,
$\displaystyle \begin{cases} \tau_2 = \tau_x \\ \tau_1 = \tau_y \to \tau_2 \\ \tau = \tau_x \to \tau_1 \\ \end{cases}$
でなければならない.
$\displaystyle \begin{cases} \tau_2 = \tau_x \\ \tau_1 = \tau_y \to \tau_2 \\ \tau = \tau_x \to \tau_1 \\ \end{cases} \Leftrightarrow \begin{cases} \tau_2 = \tau_x \\ \tau_1 = \tau_y \to \tau_x \\ \tau = \tau_x \to \tau_1 \\ \end{cases} \Leftrightarrow \begin{cases} \tau_2 = \tau_x \\ \tau_1 = \tau_y \to \tau_x \\ \tau = \tau_x \to (\tau_y \to \tau_x) \\ \end{cases}$
よって, 答えは, $\tau = \tau_x \to (\tau_y \to \tau_x) = \tau_x \to \tau_y \to \tau_x$ である. ただし, $\tau_x$ , $\tau_y$ は任意の型.

問題6. $\lambda f.\lambda x.f(fx)$ の主型を推論せよ.
型変数をおいて証明図を書くと次のようになる.
$\displaystyle \frac{ \displaystyle \frac{ \displaystyle \frac{ \displaystyle \frac{}{ f: \tau_f, x: \tau_x \vdash f:\tau_3 \to \tau_2 }~~~ \displaystyle \frac{ \displaystyle \frac{}{ f: \tau_f, x: \tau_x \vdash f:\tau_4 \to \tau_3 }~~~ \displaystyle \frac{}{ f: \tau_f, x: \tau_x \vdash x:\tau_4 } }{ f: \tau_f, x: \tau_x \vdash fx:\tau_3 } }{ f: \tau_f, x: \tau_x \vdash f(fx): \tau_2 } }{ f: \tau_f \vdash \lambda x.f(fx): \tau_1 } }{ \vdash \lambda f.\lambda x.f(fx): \tau }$
これが正しい証明図であるためには,
$\displaystyle \begin{cases} \tau = \tau_f \to \tau_1 \\ \tau_1 = \tau_x \to \tau_2 \\ \tau_f = \tau_3 \to \tau_2 \\ \tau_f = \tau_4 \to \tau_3 \\ \tau_x = \tau_4 \\ \end{cases}$
でなければならない.
$\displaystyle \begin{cases} \tau_f = \tau_3 \to \tau_2 \\ \tau_f = \tau_4 \to \tau_3 \\ \end{cases}$ より, $\tau_3 = \tau_4, \tau_2 = \tau_3$ であるから整理すると.
$\displaystyle \begin{cases} \tau = \tau_f \to \tau_1 \\ \tau_1 = \tau_x \to \tau_2 \\ \tau_f = \tau_3 \to \tau_2 \\ \tau_f = \tau_4 \to \tau_3 \\ \tau_x = \tau_4 \\ \end{cases} \Leftrightarrow \begin{cases} \tau = \tau_f \to \tau_1 \\ \tau_1 = \tau_x \to \tau_x \\ \tau_f = \tau_x \to \tau_x \\ \tau_2 = \tau_x \\ \tau_3 = \tau_x \\ \tau_4 = \tau_x \\ \end{cases} \Leftrightarrow \begin{cases} \tau = (\tau_x \to \tau_x) \to (\tau_x \to \tau_x) \\ \tau_1 = \tau_x \to \tau_x \\ \tau_f = \tau_x \to \tau_x \\ \tau_2 = \tau_x \\ \tau_3 = \tau_x \\ \tau_4 = \tau_x \\ \end{cases}$
$\tau = (\tau_x \to \tau_x) \to (\tau_x \to \tau_x) = (\tau_x \to \tau_x) \to \tau_x \to \tau_x$ である. ただし, $\tau_x$ は任意の型.

以上です. ラムダ計算セルフブログリレーもこれでおしまい(のはず)です. お疲れ様でしたー！