気まぐれエンジニア日記

ひよっこエンジニアの雑記

ラムダ計算 #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は任意の型.


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

ラムダ計算 #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がそのリストと同じ型である必要があります.


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

ラムダ計算 #3 マクロ, 不動点結合子と再帰関数

ラムダ計算

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

あれ, 2日目をさっき書いた気がしなくもないんですけど, まあいいです. 昨日(確かに昨日, うん)は, ラムダ式の簡約について書きましたが, 今日はマクロと不動点結合子, 再帰関数を扱います.


マクロとは, ラムダ式であって自由変数を1つも持たないものをいいます.

3.1. ブーリアン

まず手始めに, \overline{\mathrm{if}}を定義しましょう. if文には条件, then節, else節の3つがあればいいです. そこで,

\overline{\mathrm{if}} := \lambda bte.bte

と定義しておきましょう.
これに従うと, 条件であるブーリアンについて次が満たされていれば良いことがわかります.

  • trueはthen節とelse節の2つを入力として, then節を返せば良い.
  • trueはthen節とelse節の2つを入力として, else節を返せば良い.

すなわち,

\overline{\mathrm{true}} := \lambda tf.t
\overline{\mathrm{false}} := \lambda tf.f

とすればいいことがわかります.


さらに \overline{\mathrm{not}}, \overline{\mathrm{and}}, \overline{\mathrm{or}}も一気に定義してしまいましょう.

\overline{\mathrm{not}} := \lambda b.b~\overline{\mathrm{false}}~\overline{\mathrm{true}}
\overline{\mathrm{and}} := \lambda b_1b_2.b_1 ~(b_2~\overline{\mathrm{true}}~\overline{\mathrm{false}}) ~\overline{\mathrm{false}}
\overline{\mathrm{or}} := \lambda b_1b_2.b_1 ~\overline{\mathrm{true}} ~(b_2~\overline{\mathrm{true}}~\overline{\mathrm{false}})

この \overline{\mathrm{and}}, \overline{\mathrm{or}}だと, b_1の評価結果に応じて, b_2が評価されたりされなかったりします. すなわち, CやJavaでいうところの2重記号のand(&&)とor(||)に対応することになります. もし必ず両方評価されるもの, すなわち単体のand(&)とor(|)を定義しようとすると, 次のようになるでしょうか.

\overline{\mathrm{and}} := \lambda b_1b_2. b_1 ~(b_2~\overline{\mathrm{true}}~\overline{\mathrm{false}}) ~(b_2~\overline{\mathrm{false}}~\overline{\mathrm{false}})
\overline{\mathrm{or}} := \lambda b_1b_2. b_1 ~(b_2~\overline{\mathrm{true}}~\overline{\mathrm{true}}) ~(b_2~\overline{\mathrm{true}}~\overline{\mathrm{false}})

3.2. 整数

ブーリアンと論流演算が定義できたので, 次に整数と算術演算を定義しておきましょう.

\overline{\mathrm{0}} := \lambda sz.z
\overline{\mathrm{1}} := \lambda sz.sz
\overline{\mathrm{2}} := \lambda sz.s(sz)
\overline{\mathrm{3}} := \lambda sz.s(s(sz))
...
sは1を足す関数, zはゼロだと思ってみてください.


このとき, \overline{\mathrm{add}}と \overline{\mathrm{mul}}は次のように定義されます.
\overline{\mathrm{add}} := \lambda mn.(\lambda sz.ms(nsz))
イメージ的には, 0に1をn回足したものに1をm回足せばmとnの和になるよねといった次第です.
\overline{\mathrm{mul}} := \lambda mn.(\lambda sz.m(ns)z))
\overline{\mathrm{mul}}はなんと括弧を付け替えただけです. イメージ的には0に「1をn足す操作をしたもの」をm回足す操作をしたものはmとnの積になるよねといった次第です.


最後に指数です. 指数 m^n = \overline{\mathrm{exp}}~\overline{\mathrm{m}}~\overline{\mathrm{n}}は次のように定義されます.
\overline{\mathrm{exp}} = \lambda mn.(\lambda sz.nmsz)
超単純！ビビるこれはビビる！えーまあみていきましょう.
\overline{\mathrm{m}}~\overline{\mathrm{n}} = \lambda sz. \underbrace{m(m(\cdots m(}_{n個}s)\cdots))z
となります. これを踏まえると,
\overline{\mathrm{exp}}~\overline{\mathrm{m}}~\overline{\mathrm{n}} \to m (\overline{\mathrm{exp}}~\overline{\mathrm{m}}~\overline{\mathrm{n - 1}}) z

先の \overline{\mathrm{mul}}の定義のときにみたように, \lambda sz.m(ns)zは nを m倍したものに対応したのですから, 上の式は
m^n = m \times m^{n-1}
に対応しそうだということが想像できます.

次に確認しておくべきは, この漸化式の出発点
\overline{\mathrm{exp}}~\overline{\mathrm{m}}~\overline{\mathrm{0}} = \overline{\mathrm{1}}
です.
\lambda sz.(\overline{\mathrm{exp}}~\overline{\mathrm{m}}~\overline{\mathrm{0}})sz \to \lambda sz.(\lambda sz.z)\overline{\mathrm{m}}sz \to \lambda sz. sz =: \overline{\mathrm{1}}

したがって, \overline{\mathrm{exp}} = \lambda mn.(\lambda sz.nmsz)は m^nを表しうることがわかりました.

3.3. 不動点結合子と再帰関数

次に不動点結合子ですが, 結論からいきましょう.

命題3.1 不動点結合子
\overline{\mathrm{Y}} := \lambda f.(\lambda x. f(xx))(\lambda x. f(xx))
は符号点結合子である. すなわち, \overline{\mathrm{Y}}Fは Fの不動点を与え, F(\overline{\mathrm{Y}}F) = \overline{\mathrm{Y}}Fを満たす.

証明 :
\overline{\mathrm{Y}}F \to (\lambda x. F(xx) )(\lambda x. F(xx))\to (F(xx) )[x\mapsto (\lambda x. F(xx) )] \to F( (\lambda x. F(xx) )(\lambda x. F(xx) ) ) \equiv F(\overline{\mathrm{Y}}F)


次に, 再帰関数を考えていきましょう. \overline{\mathrm{pre}}を整数を引数にとり1つ小さい整数を返すマクロとします. 定義は煩雑なので省略します. この時次のラムダ式を考えます.

\overline{\mathrm{F}} := \lambda g. \lambda n. \overline{\mathrm{if}}~(\overline{\mathrm{iszero}} ~n) ~\overline{\mathrm{1}} ~(\overline{\mathrm{mul}}~n~(g(\overline{\mathrm{pre}}~n)))

ここで, \overline{\mathrm{iszero}}は与えられた整数が \overline{\mathrm{0}}なら \overline{\mathrm{true}}, それより大きければ, \overline{\mathrm{false}}を与えるマクロであって次で定義されます

\overline{\mathrm{iszero}} := \lambda n. n~(\lambda x. \overline{\mathrm{false}})~\overline{\mathrm{true}}

整数の z, すなわちゼロのところに \overline{\mathrm{true}}を, s, すなわち1を足す関数のところに, 問答無用で \overline{\mathrm{false}}を返す関数 \lambda x.\overline{\mathrm{false}}を差し込んだものです.

さて, 上の \overline{\mathrm{F}}を不動点結合子を食わせたもの \overline{\mathrm{Fact}} := \overline{\mathrm{Y}}~ \overline{\mathrm{F}}は, 階乗関数になります. それは簡単に確認することができます.

\overline{\mathrm{Fact}}は[ \overline{\mathrm{F}}の不動点ですから,
\overline{\mathrm{Fact}} = \overline{\mathrm{F}}~\overline{\mathrm{Fact}}
ところが,
\overline{\mathrm{F}}~\overline{\mathrm{Fact}} \to \lambda n.\overline{\mathrm{if}}~(\overline{\mathrm{iszero}} ~n) ~\overline{\mathrm{1}} ~(\overline{\mathrm{mul}}~n~(\overline{\mathrm{Fact}}(\overline{\mathrm{pre}}~n)))
ですから, 結局
\lambda n.\overline{\mathrm{Fact}}~n = \lambda n.\overline{\mathrm{if}}~(\overline{\mathrm{iszero}} ~n) ~\overline{\mathrm{1}} ~(\overline{\mathrm{mul}}~n~(\overline{\mathrm{Fact}}(\overline{\mathrm{pre}}~n)))
を得ました. と, こんな感じで, 不動点結合子を使うと簡単に再帰関数を表現できることになります.

3.4. フラグ回収

ここから先は, 著者と同じ講義を受けている人向けの内輪ネタです. はじめの方の講義で, 木構造を集合として扱ったことを覚えているでしょうか. 木構造を
T_{n + 1} = I_A(T_n) := \{\bot\} + A \times T_n \times T_n
で再帰的に定義していって,
\displaystyle T := \bigcup_{n\in \mathbb{N}} T_n
と膨らませていったものは, I_Aの不動点になったのでした. これとラムダ計算の講義資料34ページをよーーーく見比べてみてください. 全く同じことを言っていることがわかるかと思います. さすが頭の良い教員だけあってこの辺りのフラグ建築が一級品ですよね.

演習問題もこれで解きやすくなるかもしれませんね. 発展課題って不動点関連でしたよね. 無限まで考えると不動点になるんですか? やってみましょうかね.


今日は以上です. 明日は, 型体型の話に入ります. それでは！

ラムダ計算 #2 簡約

ラムダ計算

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

はてなブログにはカテゴリーなるものがあって記事を分類できるらしいことがわかったので, カテゴリ名に「ラムダ計算」とつけてみました. センスのかけらもありませんね. まあそんなもんです.


どうでもいいんだけど, 記事のカテゴリ分類を自動でやってカテゴリを振ってくれたりしないかなって思ったりしました. それただのクラシフィケーションの問題ですね. というか絶対誰かやってるでしょ. ブログはみんな書いてるからデータと正解ラベルあるし, なんなら勝手にデータ増えていくから研究はしやすそうよね. 最初と最後の方にテーマやまとめとしてカテゴリ名に関連する単語が出て来やすいとかで特徴量取れるだろうし, ディープラーニングなんて重い処理しなくても解けそう.
まあ愚痴はこの辺にしておきましょうか.


昨日は, 変数やラムダ式とはなんぞやというもの定義したので, 今日から本題です. 簡約を扱います.

簡約とは, いわゆる計算を進めていく操作, 評価のことです. 5 + 3を8に置き換えるのは簡約と言えるし, 階乗関数 f(n)を n \times f(n-1)に置き換えるのも簡約です. まず1番最初は, 何らかのラムダ式の簡約 L \to L'ができたとすると, それが全体のラムダ式にどのように作用するのかということを推論規則として定めておきます.

定義2.1. 簡約の推論規則
Vを変数全体の集合, \Lambdaをラムダ式全体の集合とする. L, L', M, M' \in \Lambda, x \in Vとする.
\displaystyle \frac{L \to L'}{LM \to L'M} ~~~~~~~~ \frac{L \to L'}{ML \to ML'} ~~~~~~~~ \frac{L \to L'}{\lambda x.L \to \lambda x.L'}

1つ目と2つ目の規則から, ラムダ式が連接している時には, 右から評価しても左から評価しても良い, つまりどんな順番で評価しても良いということをいっています. これにより, ラムダ式の評価の仕方には任意性があることがわかります. これについては後述します. 3つ目の推論規則は, 束縛変数を持つラムダ式は, その中身だけを独立に評価するということを言っています.


次に, \lambda x.Lなるラムダ式のイメージを定式化します. このラムダ式はイメージ的には変数 xを引数にとってラムダ式 Lを返す関数といったような感じです. それを式で表したのが \beta簡約です.

定義2.2 \beta簡約と代入
Vを変数全体の集合, \Lambdaをラムダ式全体の集合とする. L, M \in \Lambda, x \in Vとする.
\displaystyle (\beta)~~ \overline{(\lambda x.L)M \to L [x \mapsto M]}

これを日本語にすると, 「束縛変数 xを持つラムダ式 Lに別のラムダ式 Mを作用させることは, Lの中の xを Mに置き換えることで評価できます」となります. これによって, 束縛変数への「代入」なる概念が定義できたことになります.


次に, 束縛変数の名前を変更しても良いということを \alpha変換として定めておきます.

定義2.3 \alpha変換と変数名変更
Vを変数全体の集合, \Lambdaをラムダ式全体の集合とする. L \in \Lambda, x \in V, y \notin FV(L)とする.
\displaystyle (\alpha)~~ \overline{\lambda x.L \to \lambda y.L[x \mapsto y]}

これは例えば, f(x) := xと g(y) := yは相互に変更できるべきだということを言っています. 今まで xと呼んでいた引数名を新しく yと名前を変えたとしても, 何ら問題はないということです. これは計算を進める簡約ではないので, 変換と呼ばれます. ただし, f(x) = ax + bのように自由変数を含む関数の場合, これは g(a) := a\cdot a + bとは異なることに注意しなければいけません.


さて, 今まで L[x \mapsto M]なんていう記号をさらっと使っていましたが, これは当然未定義記号です. ここで定義しておきます.

定義2.4. L[x \mapsto M]
Vを変数全体の集合, \Lambdaをラムダ式全体の集合とする.

  • \displaystyle \forall x, y \in V, \forall L \in \Lambda, x [y \mapsto L ] := \begin{cases} L& x \equiv y \\ x & x \not\equiv y \end{cases}
  • \displaystyle \forall x, y \in V, \forall L, M \in \Lambda, (\lambda x.L)[y \mapsto M ] := \begin{cases} L& x \equiv y \\ \lambda x.L[y \mapsto M] & x \not\equiv y \land x \notin FV(M) \\ (\lambda z.L[x \mapsto z])[y \mapsto M] & \mathrm{otherwise} ~~ただし, z \notin FV(L) \cup FV(M) \\ \end{cases}
  • \displaystyle \forall y \in V, \forall L, M, N \in \Lambda, (LM)[y \mapsto N] := (L[y \mapsto N])(M[y \mapsto N])

1番目, 3番目のルールは特に説明する必要はないでしょう. 2番目のルールは少し複雑です.

yが束縛変数なら, それをどんなラムダ式に変えても意味がありません. 例えば. f(x) = ax + bの xという名前を今勝手に pqrとかして f(p, q, r) = a\cdot pqr + bとしても関数の意味は変わりませんよね.

次に yが自由変数であって, 変更先のラムダ式 Mの自由変数の中に束縛変数 xが含まれていないなら, 中身のラムダ式の yだけをそのまま Lに置き換えても良いです. 例えば, f(x) = ax + bの aを cに変えた場合は, ax + bの部分を cx + bに変えればいいですが, aを xに変えてしまうと f(x) = x^2 + bになってしまって意味が変わってしまいますよね.

この意味が変わってしまう場合, すなわち, Lのなかの自由変数 yを Mに置き換えたいんだけれど, Mのなかに束縛変数 xが含まれてしまっていたら, どうしたらいいでしょうか. この場合は簡単です. 今まで xと呼んでいた束縛変数を, 今相手にしているラムダ式たちと全く関係のない新しい名前 zに呼び直してしまえばいいのです. zは全く関係のない名前でなければいけない, というのが
「ただし, z \notin FV(L) \cup FV(M)」
の部分に含まれています.


次に, \eta簡約と \eta展開について触れておきます. これは関数は入力となる引数のラムダ式と出力となるラムダ式が全て等しければ互いに変換できて良いだろうというルールです.

定義2.5 \eta簡約と \eta展開, 外延的等しさ
Vを変数全体の集合, \Lambdaをラムダ式全体の集合とする. L \in \Lambda, x \in V\backslash FV(L)とする.
\lambda x. Lx \leftrightarrow L
を \eta簡約, \eta展開という.

M \in \Lambdaを勝手に１つ取るとき,
(\lambda x. Lx)M \to (L[x \mapsto M])(x[x \mapsto M]) \to LM ( \because x \notin FV(L))
また,
(L)M \equiv LM
となるので,
(\lambda x. Lx)M \leftrightarrow (L)M
を得ます. 引数となる Mは, ラムダ式でさえあればなんでも良いのですから, このなんでもいい引数を取り去ってしまって, \lambda x. Lxと L自体を相互に変換できると考えても良いのではないか, というのが \eta簡約と \eta展開です.
言い直すと, どんな引数に対してもそれぞれ返り値が等しいのだから, 関数として相互に変換できて良いのではないかということです. この忌避数と返り値のペアが等しいという外延的等しさを認めるのが \eta簡約と \eta展開です.


さて, 簡約( \to)が定義できたので, 2つのラムダ式が等しい( =)という概念を定義できます.

定義2.6. ラムダ式の等しさ
ラムダ式の間の関係 =を (\rightarrow \cup \leftarrow)^*で定める. すなわち2つのラムダ式 Lと Mが等しいとは, Lに対して簡約とその逆操作である展開を施して Mにできることである.

例:2.7 等しいラムダ式
(\lambda xy. xycd)ab = (\lambda x.cd)(ab)
証明:
(\lambda xy. xycd)ab \rightarrow (\lambda y.aycd)b \rightarrow abcd \leftarrow (\lambda x.xcd)(ab)


ここまで簡約について, 色々とやってきましたが, 簡約を進めていくといずれこれ以上簡約できない形になることが予想できます. これを正規形といいます.

ところが, どれだけ頑張って簡約をしていったとしても, 正規系にならないラムダ式も存在します. すなわち簡約が無限に続くということです.
例を1つあげます. 簡単です.
(\lambda x.xx)(\lambda x.xx)
これを簡約すると
(\lambda x.xx)(\lambda x.xx) \to yy[y \mapsto \lambda x.xx] \to (\lambda x.xx)(\lambda x.xx)
元に戻ってしまいました. 無限ループです本当にありがとうございました.

また, 簡約の仕方は1つでないといいました. その例を1つあげてみましょう.
\lambda u.((\lambda v.uvrs)q)p

ご指摘を受けて修正しました.
修正前 : \lambda u.((\lambda v.uvrs)p)q

これは, 先に外側から見て,
\lambda u.((\lambda v.uvrs)q)p \to (\lambda v.pvrs)q \to pqrs

ご指摘を受けて修正しました.
修正前 : \lambda u.((\lambda v.uvrs)p)q \to (\lambda v.pvrs)q \to pqrs

ともできるし, 先に内側から見て,
\lambda u.((\lambda v.uvrs)q)p \to (\lambda u.uqrs)p \to pqrs

ご指摘を受けて修正しました.
修正前 : \lambda u.((\lambda v.uvrs)p)q \to (\lambda u.uqrs)p \to pqrs

ともできます. すなわち, ラムダ式の簡約には複数の「戦略」があると言えます. またこのとき, 簡約と正規形には次の3タイプに分けることができると言えます.

  • どのような戦略を取っても正規形に必ずなるもの. 例: \lambda u.((\lambda v.uvrs)p)q
  • どのような戦略を取っても必ずいつまでも正規形にならないもの. 例: (\lambda x.xx)(\lambda x.xx)
  • 戦略によって, 正規形になったり, いつまでもならなかったりするもの. 例 (\lambda z.y)((\lambda x.xx)(\lambda x.xx) )

3つ目の例としてあげたものは, \lambda z.yになんかの引数が食わされていると考えれば, すぐに yに簡約できますが, (\lambda x.xx)(\lambda x.xx)が何らかのラムダ式の引数になっていると捉えると, いつまでも簡約が終わりません. したがって, ラムダ計算においてはこの簡約戦略が非常に重要であるということがわかります.


今日はこの辺にして, 明日はラムダ計算のマクロ, 不動点結合子と再帰関数について扱います.

ラムダ計算 #1 公理系

ラムダ計算

いやはや, 試験というものはいつになっても嫌ですね. 試験勉強をほっぽり出して研究をしています. 今日も平常運転, くまちゃんです.
いい加減試験勉強をしなくてはいけないのだけど, 全くやる気が起きないので, こうしてブログにまとめることで自分の勉強を進めようと思います. ラムダ計算についてまとめます. 同じ科目の試験を受ける人の参考になれば一石二鳥といったところですしおすし.



ラムダ計算について勉強をするためには, まずラムダ式とは何かということを定義として定めておくべきでしょうから, 形式的に(といってもこれが重要なのだけれど)定義を述べておきましょう.

定義1.1. ラムダ式
変数全体の集合を1つ固定して Vとする. ラムダ式全体の集合 \Lambdaは, 次を満たすものとして定義する.

  • x \in V \Rightarrow x \in \Lambda
  • L, M \in \Lambda \Rightarrow (L~M) \in \Lambda
  • x \in V, L \in \Lambda \Rightarrow (\lambda x.L) \in \Lambda. このとき, xを Lの束縛変数という.


また, ラムダ式の略記法を次のように定めておきます.

定義1.2. ラムダ式の略記法

  • L_1, L_2, \cdots, L_n \in \Lambdaに対し, (L_1~L_2 \cdots L_n)とは, ((L_1~L_2) \cdots L_n)のことである.
  • x_1, x_2, \cdots, x_n \in V, L \in \Lambdaに対し, (\lambda x_1x_2\cdots x_n.L)とは, (\lambda x_1.(\lambda x_2.\cdots(\lambda x_n.L)))のことである.
  • x\in V, L_1, L_2, \cdots, L_n \in \Lambdaに対し, (\lambda x.L_1~L_2 \cdots L_n)とは, (\lambda x.( (L_1~L_2) \cdots L_n))のことである.
  • L, M \in \Lambdaに対し, L~Mとは, (L~M)のことである.
  • x \in V, L \in \Lambdaに対し, \lambda x.Lとは, (\lambda x.L)のことである.

次に, ラムダ式の自由変数を定義しておきます.

定義1.3. 自由変数
ラムダ式 Mの自由変数全体の集合 FV(M)を次で定義する.

  • x \in Vに対し, FV(x) := \{x\}
  • L, M \in \Lambdaに対し, FV( (L~M) ) := FV(L) \cup F(M)
  • x \in V, L \in \Lambdaに対し, FV( (\lambda x.L) ) := FV(L) \backslash \{x\}

この定義から分かるように, 自由変数でないものが束縛変数になります.



とりあえず今日は議論のための準備を進めたということで, この辺で.

明日は, 簡約について扱います.

EMアルゴリズムまとめ

最適化とパターン認識

なんか気分なので, また記事を書こうと思います. 筆者は大学生なので, 定期試験と言うものを受けなければいけません. 今回の定期試験の範囲にEMアルゴリズムっていうのがあるのでそれについてまとめてみたいと思います. パターン認識を専門にしようと考えている以上理解しなければいけないので, 自らの頭の整理もかねて文章に起こそうと思います.

1. 確率モデルと最尤推定

EMアルゴリズムの説明に入る前に, 確率モデルあるいは生成モデルと最尤推定について説明しなければいけません.

確率モデルとは, 確率的に様々な値をとる事象があった時に, それぞれの値がどのくらい発生しやすいかを数式でモデル化したものです. 正規分布や指数分布, 一様分布, 二項分布といったような確率分布の名前を聞いたことがある人も多いと思います. 確率モデルといった場合には確率密度関数のことを指すことが多いですが, 累積分布関数の格好で書いても, どんな形であっても確率を数式で表したものは広く確率モデルと呼ばれます.

さて, 確率モデルにはいくつかパラメタが存在する場合があります. 例えば, 単に正規分布といっても様々なものがあって, 一般にはその確率密度関数は平均 \mu, 分散 \sigma ^2をパラメタとしてもった次の式で書かれます :
\displaystyle N(x; \mu, \sigma ^2) := \frac{1}{\sqrt{2 \pi \sigma ^2}}e^ {-\frac{(x - \mu) ^2}{2\sigma ^2}}
パターン認識では, あるモデルに従って発生した値の列がデータとして与えられた時に, そのパラメータを推定したい, なんてことがまま起こります. 集めたデータは正規分布に従って発生しているはずだということはわかるのだけど, その平均と分散を推定したい, などです. その推定の1つの方法として最尤推定があります.

パラメタとして \thetaを持つ確率モデル M(\theta)から値 x_1, x_2, \cdots, x_nが観測されたとしましょう. このとき, モデル M(\theta)における, 観測データ x_1, x_2, \cdots, x_nに対する尤度 L(M(\theta))を次で定義します :
\displaystyle L(M(\theta)) := \prod_{i = 1}^n P(x_i|M(\theta))
ここに, P(x_i|M(\theta))は, モデル M(\theta)から値 x_iが生起する確率です.

最尤推定とは, 尤度が最大となるようにモデルのパラメタ \thetaを推定することを言います. すなわち最尤推定によって求められた最適なモデルのパラメタ \theta ^*は次の式でかけます :
\theta ^* = \mathrm{argmax} L(M(\theta))
今, 尤度を定義しましたが, この値はモデル M(\theta)から値 x_1, x_2, \cdots, x_nがこの順に出てくる確率に他ならないことに注意しましょう. すなわち, 最尤推定とは, モデル M(\theta)から値 x_1, x_2, \cdots, x_nがこの順に出てくるという, 今まさに観測した事象が最も起こりやすいようなモデルを最適としましょうといっているのです. とりあえずモデルを動かしてみたら値 x_1, x_2, \cdots, x_nがこの順に出てきた. じゃあこれが最も起こりやすいのが正解のモデルなんじゃないのというスーパー安直な方法なのです.

「なんでこのモデルが最適だと思ったの？」「だって今目の前で起こったことが1番起こりやすいんだもん」「それはそう」という会話なわけです, ええ.

2. 正規分布と最尤推定

確率モデルが正規分布のように単純なものであれば, 最尤推定は簡単に行うことができるということを今からお見せしましょう. N(x; \mu, \sigma ^2)から, 値 x_1, x_2, \cdots, x_nがこの順に出てきたとき, 平均 \mu, 分散 \sigma ^2を推定します. こういう時には, パラメータでのグラディエントを求めて, それが零ベクトルになるような場所を探せばいいわけです. さて, 対数関数は単調増加ですから, 尤度 L(M(\theta))を最大化することは, その対数をとった
\displaystyle \log{L(M(\theta))} = \sum_{i = 1}^n \log{P(x_i|M(\theta))}
を最大化することと同値です. このとき, 正規分布では,
\displaystyle \log{L(\theta)} = \sum_{i = 1}^n \log{\frac{1}{\sqrt{2 \pi \sigma ^2}}e^ {-\frac{(x_i - \mu) ^2}{2\sigma ^2}}} = \sum_{i = 1}^n \log{\frac{1}{\sqrt{2 \pi}} - \frac{1}{2}\log{\sigma ^2} -\frac{(x_i - \mu) ^2}{2\sigma ^2}}
なので, \muで微分して,
\displaystyle \frac{1}{\sigma ^2}\sum_{i = 1}^n (x_i - \mu) = 0
\displaystyle \mu = \frac{1}{n}\sum_{i = 1}^n x_i
\sigma ^2で微分して,
\displaystyle \sum_{i = 1}^n - \frac{1}{2 \sigma ^2} + \frac{(x_i - \mu) ^2}{2} \cdot \frac{1}{(\sigma ^2) ^2} = 0
\displaystyle \sigma ^2 =\frac{1}{n} \sum_{i = 1}^n (x_i - \mu) ^2
とよく見慣れた式が出てきました. つまり, 正規分布の平均 \mu, 分散 \sigma ^2の最尤推定の結果は, 観測したデータの平均と分散そのものであるということがわかります.

3. EMアルゴリズム

単純な確率モデルの最尤推定であれば, 先のように観測データから得られる尤度の関数をパラメタで微分して極値を求めることで, 解析的に行うことができました. しかしながら, 確率モデルの中に, 観測できないデータがある場合にはそう簡単にはいきません. 例として確率モデルの重ね合わせを考えます.
M_1(\theta_1), M_2(\theta_2), \cdots, M_k(\theta_k)を確率モデルとし, パラメタを推定したいモデルが
\displaystyle M := \sum_{i = 1}^k w_iM_i(\theta_i)
ただし,
\displaystyle \sum_{i = 1}^k w_i = 1\land\forall i\in \mathbb{N}\cap[1, n], w_i\geq 0
と与えられているとします. このとき, 値 x_1, x_2, \cdots, x_nを観測した場合の最尤推定をしようと思うのですが, モデルが重み付き和で表されているので, 先のように対数をとってもうまくいきそうにありません. そこでこんなことを考えます.
モデル Mは確率 w_iでモデル M_i(\theta_i)を選んで, そこから値を取り出していると見なすことができるんだから, 値 x_1, x_2, \cdots, x_nに加えて, どのモデルから出てきたかの情報が得られれば良いのではないか. もし, どのモデルが出てきたかがわかってしまえば, 各モデル M_i(\theta_i)から出てきた値だけに注目して, 先と同じように微分して極値を求められそうではないかと考えるわけです.

そこで, あるモデル
\displaystyle M := \sum_{i = 1}^k w_iM_i(\theta_i)
をとりあえず1つ固定して, 値 x_1, x_2, \cdots, x_nが M_1(\theta_1), M_2(\theta_2), \cdots, M_k(\theta_k)のどれから出てきたと考えるべきかの確率
P(M_j|x_i, M)
を求めてみよう, その上でもっといいモデル
\displaystyle M^* := \sum_{i = 1}^k w_i^* M_i(\theta_i^*)
に少しずつ更新しようと考えるわけです. 実は, この確率がもとまってしまえば, 新しいモデル M'の推定は簡単にできてしまうよ, というのがEMアルゴリズムのキモなのです. 詳しく見ていきましょう.

今, モデル Mを1つ固定します. 最尤推定で最大化したい値はもっといいモデル M^*における, 観測データ x_1, x_2, \cdots, x_nに対する尤度 L(M^*)で,
\displaystyle L(M^*) := \prod_{i = 1}^n P(x_i|M^*)
あるいはその対数
\displaystyle \log{L(M^*)} = \sum_{i = 1}^n \log{P(x_i|M^*)}
です.
今, 各 x_iについて,
\displaystyle \sum_{j = 1}^k P(M_j|x_i, M) = 1
ですから,
\displaystyle \log{L(M^*)} = \sum_{i = 1}^n \log{P(x_i|M^*)} = \sum_{i = 1}^n 1\cdot \log{P(x_i|M^*)} = \sum_{i = 1}^n \sum_{j = 1}^k P(M_j|x_i, M) \log{P(x_i|M^*)}
となります.
次がポイントです. こんな式変形をしようと思ったのはなぜだったか思い出してください. 値 x_1, x_2, \cdots, x_nに加えて, M_1(\theta_1), M_2(\theta_2), \cdots, M_k(\theta_k)のうちのどのモデルから出てきたかの情報が得られればいいのになぁと考えていたわけです. すなわち,
P(x_i, M_j |M^*)
たちだけの式にしてしまえば, \log{L(M^*)}を最大化するようなパラメータ \theta_1, \theta_2, \cdots, \theta_kたちは簡単に求められそうだという条件下で話をしていたわけです. この値が出てくるように, もう1回だけ変形をしてみましょう. 条件付き確率の定義によって,
\displaystyle P(x_i|M^*) = \frac{P(x_i, M_j |M^*)}{P(M_j |x_i, M^*)}
ですから,
\displaystyle \log{L(M^*)} = \sum_{i = 1}^n \sum_{j = 1}^k P(M_j|x_i, M) \log{ \frac{P(x_i, M_j |M^*)}{P(M_j |x_i, M^*)}} = \sum_{i = 1}^n \sum_{j = 1}^k P(M_j|x_i, M) \left(\log{P(x_i, M_j |M^*)} - \log{P(M_j |x_i, M^*)}\right)
ここで,
\displaystyle Q(M, M^*) := \sum_{i = 1}^n \sum_{j = 1}^k P(M_j|x_i, M)\log{P(x_i, M_j |M^*)}
\displaystyle H(M, M^*) := -\sum_{i = 1}^n \sum_{j = 1}^k P(M_j|x_i, M)\log{P(M_j |x_i, M^*)}
とおけば,
\log{L(M^*)} = Q(M, M^*) + H(M, M^*)
となります.
はあ, やったやったと安心してはいけません. 最初の目的をもう一度思い出しましょう. モデル Mを固定して, そこから得られる情報を使って, ちょっといいモデル M^*を導きたいのでした. つまり,
\log{L(M^*)} - \log{L(M)} > 0
となるように M^*を決めましょうということになるのです. しかもその差はなるべく大きい方が良さそうですよね.
\log{L(M^*)} - \log{L(M)} = Q(M, M^*) - Q(M, M) + H(M, M^*) - H(M, M)
ですが, H(M, M^*) - H(M, M)はダイバージェンスなので, M^*として, Mとは違うものを選べば自動的に H(M, M^*) - H(M, M) > 0となります. この説明は後述します. 一方, Q(M, M^*) - Q(M, M))は, Q(M, M^*)を最大化することができれば, 最大化できます. すなわち,
\displaystyle Q(M, M^*) := \sum_{i = 1}^n \sum_{j = 1}^k P(M_j|x_i, M)\log{P(x_i, M_j |M^*)}
を最大化するように M^*を選べば良いということがわかります. 嬉しいことに, P(M_j|x_i, M)はすでに求めることができていますし, P(x_i, M_j |M^*) の値の評価は簡単にできるという条件で話をしていましたから, この問題は無事に解けそうそうだということがわかります.

Mから M^*へちょっといいモデルに更新ができました. あとはこれを繰り返していけば, どんどんいいモデルになりそうですね. これがEMアルゴリズムです.

EMアルゴリズムの手順をまとめると次のようになります.

  1. 初期モデルを決める.
  2. モデル Mとモデル化したい確率的な現象の値の列 x_1, x_2, \cdots, x_nから, P(M_j|x_i, M)を計算する.
  3. P(M_j|x_i, M)をもとに, Q(M, M^*)を最大化するようなちょっといいモデル M^*を推定する.
  4. Mを M^*に置き換えて, 2に戻る.

3. ダイバージェンスは正

ちょっとちょっと, 終わった気になっていませんか？？まだ, 1つ残っていますよ.

H(M, M^*) - H(M, M)はダイバージェンスなので, M^*として, Mとは違うものを選べば自動的に H(M, M^*) - H(M, M) > 0となります.

ほんまか？？ 証明しましょう.

p_{ij} := P(M_j|x_i, M), q_{ij} :=P(M_j |x_i, M^*)とおいて, 次を証明すれば良さそうです.

命題 ダイバージェンスは正
p_{ij}, q_{ij}が
\displaystyle \sum_i \sum_j p_{ij} = 1\land\forall i, j, p_{ij}\geq 0
および
\displaystyle \sum_i \sum_j q_{ij} = 1\land\forall i, j, q_{ij}\geq 0
を満たすとする. このとき,
\displaystyle - \sum_i \sum_j p_{ij}\log q_{ij} + \sum_i \sum_j p_{ij}\log p_{ij} \geq 0
等号成立は p_{ij}, q_{ij}がそれぞれ等しいときである.

証明:
f(x) = -\log x + x - 1とおく.
\displaystyle f'(x) =-\frac{1}{x} + 1 = 0
を解くと, x = 1.
しかも 0 < x < 1\Rightarrow f'(x) < 0かつ x > 1\Rightarrow f'(x) > 0より,
f(x)は, x = 1で最小値0を取ることがわかる.
したがって x > 0\Rightarrow -\log x \geq 1 - xであり, 等号成立は x = 1とわかる. このとき,

\displaystyle - \sum_i \sum_j p_{ij}\log q_{ij} + \sum_i \sum_j p_{ij}\log p_{ij} = - \sum_i \sum_j p_{ij}\log\frac{q_{ij}}{p_{ij}}
\displaystyle \geq \sum_i \sum_j p_{ij}(1 - \frac{q_{ij}}{p_{ij}}) = \sum_i \sum_j (p_{ij} - q_{ij}) = \sum_i \sum_j p_{ij} - \sum_i \sum_j q_{ij} = 1 - 1 = 0
等号成立は, \displaystyle \frac{q_{ij}}{p_{ij}} = 1,
すなわち p_{ij} = q_{ij}のときである.


おしまい！！お疲れした〜！

いいレポートにするにはどのように書くべきかを自分なりにまとめてみた

お久しぶりです. 本当に1年ぶりとかでしょうか. 文章を書くのは苦手なもんで, 気が向くのがこれくらいのペースなのです.

さて, 久しぶりと言っておきながら, 今日書くことは数学のことではありません.
筆者は理系の大学生なので, 実験レポートを書く機会が多いのですけど, 大学というのは残念なもので, レポートを書く機会, すなわち課題の量は多いにも関わらず, どのようにかけばいいレポートになるかという指導がほとんどされないのです. そのため, 自分では頑張っていいレポートを書いたつもりであるのに, いいレポートの条件を知らないためにいつまで経ってもいい点数がつかないなんてことがずっと続いてしまう人も少なくないようです.

どのようにかけばいいレポートになるかということは, 本来は大学の実習・実習科目で教えられるべきことではあるのだけれど, 最初に言ったように大学はいつまでも誰も教えてくれないようです. なので, 筆者自身がレポートを書くときに普段気をつけていることを書こうと思います. 一学生の意見に過ぎないし, プロである教員から見ればまだまだ足りない部分も多いと思うけれども, まとめておいて損はなさそうなので.

全体の構成

実験・実習のレポートを想定しますと, 全体の構成は次のようになるのがベタだと思います.

1 . テーマは何か.
2 . 何をやったのか.
3 . どんな結果が得られたのか.
4 . 得られた結果からどんなことが考察されるか.
5 . 考察を踏まえて次に何をするべきか.

これらを1つずつ見ていくことにします.

テーマとやったこと

テーマは, 解いた問題や注目した事柄について述べ, どんなことをゴールに設定したのかを書くべきでしょう. 例えば, この文章であれば, テーマは「どのようにかけばいいレポートになるかを記述する」になります. 今からこんなことを話しますよ, ここに注目しますよ, これ以外は考えないよ, と高らかに宣言してしまうのです.

2つめの何をやったのかというのは必ずしもテーマとは一致しません. テーマである解きたい問題や注目したい事柄を考慮したときに, どのような方法や手法を用いたのかを記述するべきでしょう. 情報系であれば, 実行したコマンドを書いたり, 具体的なアルゴリズムや数式の説明ということになると思います. この文章であれば, 「上で述べた５つに分けて話をすることにします」と述べたことが対応するでしょうか.
同時に, 問題を解くにあたって独自に導入した概念や未定義語があったりした場合はここで説明しておくべきだろうし, 使用した方法や手法がなぜうまくいくと考えたかの説明もした方が良いでしょう. ここで, うまくいくと思ったことが, 実際にはうまくいかなくても構わないのです. それは結果で提示すればいいし, 原因を考察すればいいです. ひとまずは, こうやればきっとうまくいくはずだよね, ということを納得してもらうことを考えましょう.

結果の提示

「やったこと」で述べた手法に従って何らか実験を行えば, 当然何らか結果が得られるはずです. 結果の提示では, 実験中に見たままを書きます. 何かの値の測定実験であれば, 値がこんな風に上下したとか, 最大値・最小値はいくつだったとか, そんなことを書きます. その分野のことを全く知らない人が見たとしても誰でもわかること, をかけばいいのです. 結果の報告は知識が変にない方がうまくできると言ってもいいでしょう.

見たままを書きますと言ったけれど, むしろ書かなくてはいけません. 数値を測定したら, 表やグラフを作ることもあるかもしれないし, オシロスコープの波形測定のように画面の表示そのものを結果として提示することも多いですが, その図や表をペタッと貼り付けただけでは不十分です. その図のどんなところに注目したらどんな特徴が見て取れたかということを文章で書く必要があります.

見ればわかるだろって思うかもしれませんが, それはあなたが得られた表や図のどこに注目するべきか, どんな結果が期待されるかを知識として知っているからで, 何も知らない人からすれば, 何をどう見ていいかわからないものです. 「見てみて, ここすごいよ！」とか「ここみてよ！こんなことになってるよ！」っていうことを書いてなければいけません.

加えて, 全ての結果はなるべく数字を使って説明されるべきです. 大きくなった, 小さくなったではなくて, いくつ変化したとか何倍になったというように数値化をすることを考えましょう. 数値化するために新しい指標を独自で定義してもいいと思います. 複雑な指標を用いる際には, 自分で導入した指標がどのような意味を持ち, それが感覚的なものと矛盾しないことを説明する必要があります.

1つ例をあげましょう. 2つのグループA, Bに分かれている講義の書き起こし文の集まりが与えられて, それがどの科目のものなのかを推定することを考えます.(これが先に述べたことで言えばテーマです) そこで, 事前に決めた単語がグループA, Bの文章にそれぞれいくつずつ入っているかを調べる実験をしたとします.( これは先で述べたことで言えばやったことです.)

表1. 各グループのテキストの単語の出現回数の和

単語 グループA グループB
エントロピー 136 0
問題 80 76
データ 90 84
確率 130 2
キャッシュ 0 112
記憶 1 104

この時, 筆者は次のように結果を報告します :
各グループの単語の出現回数の合計を表1に示す. (図や表の参照先の提示)
グループAとグループBを比較すると, グループAだけに多く含まれる単語は, 「エントロピー」と「確率」であり, グループBだけに多く含まれる単語は「キャッシュ」「記憶」であった. (1番言いたいこと)
今あげた, 一方だけに多く含まれる単語についてみると, 多く含まれるグループでの出現回数が100を上回っているのに対して, 少ないグループでの出現回数は10を下回っており, 大きな差があった. 一方で, 「問題」や「データ」といった単語はグループAとグループBの出現回数の差が10以下と小さかった(数字を用いた説明).

ここで, グループA, Bの講義名が〇〇であるということは一切述べていないことに注意してください. 表を見て, そこから単純に読み取れることだけを書いています. なんども言いますが, 結果は数字をなるべく使って見たままを書くのです.

一方, 見たままとは言え, こんな結果の報告の仕方は最悪です :
各グループの単語の出現回数の合計を表1に示す. 今回調べた単語の中には出現回数に偏りがあるものが多くあった.

偏っているというのがどういう状況なのかわからないし, どの単語に, どの程度, どちらのグループ側に偏りがあるのかもわかりません. 高い数字が出たとか, 妥当な値であったとか, 正しい結果だった, というのも同様によくわかりません.

まとめると, 結果には
* 図や表, 数値から読み取れる見たままのことについて
* どこに注目すると
* (なるべく数字で表現をして)どの程度
* どんな現象が見られたのか

を書くといいと思います. 図や表をペタッとして参照先を書くだけではなくて, ちゃんと文章で書きましょう.
見りゃわかるだろ！いやわからんが....

考察の記述

考察は,

  • 結果として提示したような見たままではわからないことを
  • 事前に知っている知識と照らし合わせながら
  • 得たい結論に繋げたり
  • 得られた結果の妥当性を検証したり

するための自分の考えを述べていくことを言います. 事前に知っている知識を長々と書いて, 実験で妥当性が確認できたと書くだけでは不十分で, なぜ妥当であると言えるのかということまで書く必要があるでしょう. 理論の式に実験の数値を代入して比較したり, 理論をこういう風に捉えれば一致するということを 実験結果に基づいて 書く必要があるでしょう. ふとした疑問「なぜ」を全部潰すつもりで書くといいと思います.

考察の記述にはさらに注意点があります.

  1. 終わりの見えない他人の考えなんて誰も読みたくないので, どのような観点で考察を進めるのかをはじめに明記する. (テーマの提示と似ている)

2.1. 結果の報告で記述した見たままの事実に書かれていないこと, および一般論として知られている事実以外のことに基づく考察は書かない.
2.2. もしデータを見ているうちに新しく考察が出てきたなら, その根拠となる事項を結果の章にも書き加えなければならない.

3.1. 「と思われる」「と考えられる」などの曖昧な表現はしない. 「と言える」「と断定する」「と考える」と書く. 自信がないことは書かない.
3.2. もしどうしても推定の域を出ないことを書きたいならば, 推定であることを明記した上で, どのような実験をすればこの推定を脱することができると考えるかを記述する.

4.1. 文章中で主張が一貫していることを十分に確認する. 矛盾する主張が出てきそうになったら, 元の主張自体を書かない.
4.2. どうしても最終的な主張と違う事実が1つ2つあり, 特例のように扱いたいなら, 外れ値があることを明記した上で, なぜ外れ値が生じたと考えるかを記述する.

5.1. 実験者が実験から導く理論に飛躍があってはならない. 循環論法(示したいことを使って論を組み立てること)は論外.
5.2. 逆に, 誰でもすぐに検証が可能な数式の同値変形を細かく記述する必要はない.

例をあげようと思うと大変なのでやりませんが, こんなことに注意してみるのがいいと思います.

次にやること

考察の際に, 推定の域を出なかったことについて追実験を考えたり, 今回行った手法と別の手法を提案するのが良いと思います. 別の手法の提案をするときには, こうやればきっとうまくいくはずだよね, ということを納得してもらうための説明を書くと良いでしょう. こうして, 最初に述べた5ステップをぐるぐる回しながら実験を進めれば良いと筆者は考えます.

終わりに

あー疲れた. レポートって大変ですね.
そしてこれを教えてくれないW大学CS学科はマジでなんなんですかね.
まあ諦めましょう. 代わりに筆者が書いたから. それではまた！