2019-01-31

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

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

2019-01-30

ラムダ計算 #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ページをよーーーく見比べてみてください. 全く同じことを言っていることがわかるかと思います. さすが頭の良い教員だけあってこの辺りのフラグ建築が一級品ですよね.

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

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

2019-01-29

ラムダ計算 #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)$ が何らかのラムダ式の引数になっていると捉えると, いつまでも簡約が終わりません. したがって, ラムダ計算においてはこの簡約戦略が非常に重要であるということがわかります.

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

2019-01-27

ラムダ計算 #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\}$

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

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

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

2019-01-20

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アルゴリズムの手順をまとめると次のようになります.

初期モデルを決める.
モデル $M$ とモデル化したい確率的な現象の値の列 $x_1, x_2, \cdots, x_n$ から, $P(M_j|x_i, M)$ を計算する.
$P(M_j|x_i, M)$ をもとに, $Q(M, M^*)$ を最大化するようなちょっといいモデル $M^*$ を推定する.
$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}$ のときである.

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

2019-01-10

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

お久しぶりです. 本当に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に示す. 今回調べた単語の中には出現回数に偏りがあるものが多くあった.

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

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

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

考察の記述

考察は,

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

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

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

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

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

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

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

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

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

次にやること

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

終わりに

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

2018-05-24

NFAエミュレータ

大学のプログラミングコンテストでボツになった自作問題です. 重要な問題だと思うのでみなさんといてみてください！

Description

非決定性有限オートマトン(NFA)とは、処理の実行による状態の遷移を記述するための概念で、形式言語を扱う際にも多く用いられる重要なものです。NFAは次の五つから構成されます： $Q$ ：状態全体の集合、 $\Sigma$ ：入力記号全体の集合、 $\delta$ ：状態遷移関数、 $q_0$ ：初期状態、 $F$ ：受理状態全体の集合( $Q$ の部分集合)

状態遷移関数 $\delta$ は現在の状態と入力記号を受け取ると次に移動する状態の候補を返す関数です。ある入力記号n文字の列 $w$ をNFAが受け取ると次のように動作します：・開始時の状態は初期状態です。入力記号列の1文字目と現在の状態(初期状態)を読み込んで、状態遷移関数の持つ、次に移動する状態の候補のうちのどれか1つの状態に移動します。次に移動する状態の候補が1つもないとき、エラーとして動作を強制終了します。
・次に、入力記号列の2文字目と現在の状態を読みこんで、状態遷移関数の持つ、次に移動する状態の候補のうちのどれか1つの状態に移動します。次に移動する状態の候補が1つもないとき、エラーとして動作を強制終了します。
・・・
・入力記号の列のn文字目と現在の状態を読みこんで、状態遷移関数の持つ、次に移動する状態の候補のうちのどれか1つの状態に移動します。次に移動する状態の候補が1つもないとき、エラーとして動作を強制終了します。エラーにならずにここまできた場合、n回目の移動先を最終状態とします。

動作の結果として最終状態が $F$ の要素となるような状態遷移の選び方が1つでもあるとき、NFAは入力記号列を受理する(Accept)といい、そうでないとき拒絶する(Reject)といいます。状態遷移の選び方をどのようにしてもエラーとなるときは、拒絶されます。

NFAの構成と入力記号列が与えられるので、入力記号列がNFAに受理されるか、拒絶されるかを判定してください。

Constraints

Input

1つの入力ファイルは複数のテストケースからなる。

入力ファイルの最初の1行目にはテストケースの個数 $T$ が記される( $1 \leq T \leq 100$ )。

2行目以降には、 $T$ 個のテストケースが記述されており、各テストケースは次の形式で表される。

$|Q|~ |\Sigma|~q_0$
$F$
$\delta_{00} ~ ~ ~ ~\delta_{01} ~ ~ \cdots ~ ~\delta_{0, |Q|-1}$
$\delta_{10} ~ ~ ~ ~ \delta_{11} ~ ~ \cdots ~ ~ \delta_{1, |Q|-1}$
$\vdots ~ ~ ~ ~ ~ ~\vdots ~ ~ ~ ~ \ddots ~ ~ ~ ~ \vdots$
$\delta_{|\Sigma|-1, 0} ~\delta_{|\Sigma|-1, 1} ~ ~ \cdots ~ ~ \delta_{|\Sigma| -1, |Q|-1}$
$w$

・ $Q$ は $0$ 以上 $|Q|$ 未満の整数全体、 $\Sigma$ は $0$ 以上 $|\Sigma|$ 未満の整数全体で表す。
・ $q_0$ は初期状態で $Q$ の要素、すなわち $0$ 以上 $|Q|$ 未満の整数。
・ $F$ は $Q$ の部分集合, すなわち $Q$ の要素が多くとも1度ずつのみ出現する数字列であって、各桁の数字は受理状態1つを表す。
・ $\delta_{a, q}$ は、入力記号 $a$ を状態 $q$ で読み込んだ時に次に移動する状態の候補で、 $Q$ の要素が多くとも1度ずつのみ出現する数字列または-1である。各桁の数字は次に移動する状態の候補1つを表すが、-1のときには次に移動する状態の候補が1つもないことを意味する。
・ $w$ は入力記号列で、 $\Sigma$ の要素1文字以上70文字以下からなる数字列である。

Output

各テストケースに対して、入力記号列がNFAに受理される場合は'Accept'、拒絶される場合は'Reject'と1行ずつ出力せよ。

Sample Input

3
2 2 0
1
01 1
-1 1
0111
10 1 0
9
012345678 -1 -1 -1 -1 -1 -1 -1 -1 -1
000000000
10 1 0
789
0123456789 123456789 23456789 3456789 456789 56789 6789 789 89 9
000000000

Sample Output

Accept
Reject
Accept

・1つ目のテストケースでは、0->0と状態を移動してしまうと次でエラーになりますが、0->1->1->1->1と状態を移動すれば受理状態を終了状態にできるので、受理されます。

・2つ目のテストケースでは、8文字目まで状態0に留まって9文字目で状態0から8までのいずれかに移動する以外はエラーとなります。状態0から8まではどれも受理状態ではないので、拒絶されます。

・3つ目のテストケースでは、うまく状態遷移していけばどの状態も最終状態となりうるので、受理状態7、8、を最終状態とする状態遷移の方法も存在します。よって、受理されます。

気まぐれエンジニア日記

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

ラムダ計算 #4 FLと型体系

4.1 Natural Step Semantics

4.2 型体系

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

3.1. ブーリアン

3.2. 整数

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

3.4. フラグ回収

ラムダ計算 #2 簡約

ラムダ計算 #1 公理系

EMアルゴリズムまとめ

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

2. 正規分布と最尤推定

3. EMアルゴリズム

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

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

全体の構成

テーマとやったこと

結果の提示

考察の記述

次にやること

終わりに

NFAエミュレータ

Description

Constraints

Input

Output

Sample Input

Sample Output