ラムダ計算 #4 FLと型体系 - 気まぐれエンジニア日記

ラムダ計算セルフブログリレー4日目です. 今日も平常運転, くまちゃんです. 3日目はこちら.
kumachan-math.hatenablog.jp

今日からは, 型の話です. 型の話をするために, ラムダ計算を拡張したFL言語というものを考えましょう.
FL言語は, ラムダ計算にint型とbool型の基本型とその演算に加え, リスト型と空リストであるnil, if文, let文, リストのパターンマッチングであるcase文を加えたものです. 基本型に対する演算はカリー化された二項演算からなるものとします. これは,

$+: \mathrm{int} \to \mathrm{int} \to \mathrm{int}$
$>: \mathrm{int} \to \mathrm{int} \to \mathrm{bool}$
$\&: \mathrm{bool} \to \mathrm{bool} \to \mathrm{bool}$

というように捉えるということ, またそれ以外の演算は考えないということを言っています.

4.1 Natural Step Semantics

FL言語の実行ステップの公理と推論規則について詳しく見ていくことにします.

(app1) $\displaystyle \frac{L \to L'}{LM \to L'M}$
訳 : ラムダ式の連接の左側は右側に何ら影響することなく簡約することができます.
(app2) $\displaystyle \overline{(\lambda x.L)M \to L[x := M]}$
訳 : ラムダ抽象への右からの連接は関数適用であり, 代入操作に簡約できます.
(app3) $\displaystyle \frac{L \to L'}{\mathrm{op}~L \to \mathrm{op}~L'}$
訳 : 2項演算子がある時には, まずその後ろにある引数から簡約をします.
(app4) $\displaystyle \frac{L \to L'}{\mathrm{op}~c~L \to \mathrm{op}~c~L'}$
訳 : 2項演算子の引数は第1引数が簡約されきって初めて, 第2引数を簡約します.
(app5) $\displaystyle \overline{\mathrm{op}~c_1 ~ c_2 \to c} ~~~ただし, c = \mathrm{op}~c_1 ~ c_2$
訳 : 定数同士の演算はその演算結果に簡約できます.

FL言語では純粋ラムダ計算と異なり, 必ず左から右に簡約が進んでいくということがこの5つの規則からわかります.

(if1) $\displaystyle \frac{B \to B'}{\mathrm{if}~B~\mathrm{then}~T~\mathrm{else}~E \to \mathrm{if}~B'~\mathrm{then}~T~ \mathrm{else}~E}$
訳 : if文は条件式からまず簡約されます.
(if2) $\displaystyle \overline{\mathrm{if}~\mathrm{true}~\mathrm{then}~T~\mathrm{else}~E \to T}$
訳 : if文の条件式がtrueに簡約されたら, if文全体はthen節に簡約されます.
(if3) $\displaystyle \overline{\mathrm{if}~\mathrm{false}~\mathrm{then}~T~\mathrm{else}~E \to E}$
訳 : if文の条件式がfalseに簡約されたら, if文全体はelse節に簡約されます.

(let) $\displaystyle \overline{\mathrm{let} ~x = M ~ \mathrm{in} ~ L \to L[x := M]}$
訳 : let文はLの中(in)のxをMに置き換えるという意味です.

(case1) $\displaystyle \frac{L \to L'}{ \begin{align} &\mathrm{case} ~ L ~ \mathrm{of} ~ \mathrm{nil} => N~|~h::t => M \\ \to &\mathrm{case} ~ L' ~ \mathrm{of} ~ \mathrm{nil} => N~|~h::t => M \\ \end{align} }$
訳 : パターンマッチングはマッチング対象からまず簡約されます.
(case2) $\displaystyle \overline{\mathrm{case} ~ \mathrm{nil} ~ \mathrm{of} ~ \mathrm{nil} => N~|~h::t => M \to N}$
訳 : マッチング対象がnilに簡約されたら, case文全体はnilの時に置き換わるラムダ式に簡約されます
(case3) $\displaystyle \overline{\mathrm{case} ~ \mathrm{H::T} ~ \mathrm{of} ~ \mathrm{nil} => N~|~h::t => M \to M[h \mapsto H][t \mapsto T]}$
訳 : マッチング対象がH::Tに簡約されたら, case文全体はh::tの時に置き換わるラムダ式に簡約されます. ただし, 簡約時にhはHに, tはTに置き換えられます.

4.2 型体系

型を検査するための方に対する公理と推論規則を詳しく見ていきます. これは型環境, ラムダ式, 型からなります. 型環境とは, ラムダ式の中の自由変数に対する型を与えるものです. 型環境 $\Gamma$ , ラムダ式 $L$ , 型 $\tau$ に対して, 型に関する論理式(型判定式)を
$\displaystyle \Gamma \vdash L:\tau$
と書きます. これは型環境 $\Gamma$ の下で, ラムダ式 $L$ の型が $\tau$ である, という命題です.

以降で, 型判定式に関する公理と推論規則を見ていきましょう.

(var) $\displaystyle \overline{\Gamma, x: \tau \vdash x:\tau}$
訳 : ある変数の型はそのほかの変数の型環境によらず独立に決定します.

(con) $\displaystyle \overline{\Gamma, \vdash c^\tau :\tau}$
訳 : 定数は他の型環境によらず暗黙的に型を持っています.

(list) $\displaystyle \frac{\Gamma \vdash e:\tau~~~\Gamma \vdash l:\mathrm{list}(\tau)}{\Gamma \vdash e::l:\mathrm{list}(\tau)}$
訳 : $\tau$ 型の要素を $\tau$ 型のリストに連接したものもまた $\tau$ 型のリストです.

(nil) $\displaystyle \overline{\Gamma \vdash \mathrm{nil}:\tau}$
訳 : niはリストですが, 何型のリストであるかということは規定されません.

(if) $\displaystyle \frac{\Gamma \vdash B:\mathrm{bool}~~~\Gamma \vdash T:\tau~~\Gamma \vdash E:\tau} {\mathrm{if}~B~\mathrm{then}~T~\mathrm{else}~E:\tau}$
訳 : 条件式がbool型で, then節とelse節が同じ型ならif文全体もthen節, else節と同じ型を持ちます.

(abs) $\displaystyle \frac{\Gamma, x:\tau \vdash L:\tau'} {\Gamma \vdash \lambda x.L :(\tau \to \tau')}$
訳 : ラムダ抽象は, 引数の型からラムダ式の型への関数型を与えます.

(app) $\displaystyle \frac{\Gamma \vdash F:\tau \to \tau'~~~\Gamma \vdash L:\tau} {\Gamma \vdash FL:\tau'}$
訳 : 関数型に引数の型を食わせる関数適用は, 返り値の型を与えます.

(let) $\displaystyle \frac{\Gamma \vdash M:\tau'~~~\Gamma, x:\tau' \vdash L:\tau} {\Gamma \vdash \mathrm{let} ~x = M ~ \mathrm{in} ~ L:\tau}$
訳 : 自由変数が $\tau'$ 型であるような型環境においては, $\tau'$ 型のラムダ式をその自由変数にlet文で代入することができます. またlet文による代入は元のラムダ式の型を変えることはありません.

(case) $\displaystyle \frac{ \begin{align} \Gamma \vdash L:\mathrm{list}(\tau)~~~\Gamma &\vdash h:\tau~~~\Gamma \vdash N:\tau' \\ \Gamma, h:\tau, t:\mathrm{list}(\tau) &\vdash M:\tau' \end{align} } {\Gamma \vdash \mathrm{case} ~ L ~ \mathrm{of} ~ \mathrm{nil} => N~|~h::t => M:\tau'}$
訳 : nilの時に置き換わるラムダ式が $\tau'$ 型で, h::tの時に置き換わるラムダ式も $\tau'$ 型なら, case文全体も $\tau'$ 型です. ただし, h::tの時に置き換わるラムダ式はh, tをそれぞれ自由変数として持っている必要があります. さらに, マッチング対象が何らかリストで, hがそのリストの要素と同じ型で, tがそのリストと同じ型である必要があります.

今日は公理と推論規則をたくさん見たのでここまでです. 明日は, 最終回です. これらの公理と推論規則を元に, 例を用いて型検証と型推論を扱います.