　何を語ってもネタバレだし，販売サイトのあらすじですらネタバレ気味なので（少なくとも僕はそう思う），どう面白かったのか説明するのは難しい．ネタバレで面白さが損なわれる作品ではないと思うし，気にしすぎかもしれないが．ただ面白かったのは確かなので，騙されたと思って前情報なしでプレイして欲しい．体験版があるし，買うにしても650円で手を出しやすいので．

　この記事の前半ではネタバレなしの感想を，後半ではネタバレありで感想とか考察を書いていく．前半は購入しようか悩んでいる人の参考になればと思っている．僕の力量でこのゲームの独特の雰囲気を伝え切れてるかはわからないし，体験版をプレイするほうが早いかも知れないが．後半はクリア済みの人とオタクコミュニケーションをするのが目的．お前の考察はおかしいとかマサカリ投げてくれるのは大歓迎です．

2016-06-26

Raspberry Pi3で自動ノート取り装置を作った

はじめに

数理情報工学実験第二という演習で、Raspberry Piをつかって何かを作ることになりました。そこでAMATERASUという自動ノート取り装置を作ったので紹介します。

そもそもRaspberry Piって?

Raspberry Pi3 Model B ボード＆ケースセット (Element14版, Clear)-Physical Computing Lab

出版社/メーカー: TechShare
メディア: エレクトロニクス
この商品を含むブログ (3件) を見る

これです。安くて小型で色んなセンサーをつけて遊べるコンピュータです。今回はカメラモジュールを使いました。

自動ノート取り装置とは

自動ノート取りの目標は、講義を撮影した動画*1を処理することで、ノートの代わりとして使える画像を出力することです。具体的には次のgifのような画像を次々出力していくのを目標にしています。黒くなっている部分が何かについては後ほど説明しますが、そこには情報がないということを表しています。
f:id:dolicas:20160625184703g:plain

動画を入力して処理することもできますが、オンラインで処理することを想定しています。

出力される画像は次のような条件を満たすようにします。

情報の漏れがないです。教員が黒板に書いたことは、全てどこかのタイミングで出力される画像に写っています。
無駄な情報を省きます。つまり、同じ板書が複数回出力されないようにします。
教員が写りこまないようにします。

*1:正確には連続撮影された画像

2016-05-30

超幾何級数の等式自動導出

数学本の紹介

はじめに

輪講で『A=B』という超幾何級数の等式自動証明についての本を読みました。タイトルが簡素なとこが好き。
The Book "A=B"
pdfが著者のページからダウンロードできる。こういうのいいよね。

超幾何級数の等式自動導出とは

超幾何級数とは、 $\sum_k t_k$ という形で $t_k / t_{k-1}$ が $k$ についての有理関数となっているものです。まあ大雑把には、 $\binom{n}{k}$ とか $k!$ とか含む項の和だと思っててください。

超幾何級数の等式の例では、次のようなものがあります。
$\sum_k \binom{n}{k}^2 = \binom{2n}{n}$
これは組み合わせ論的にも証明できるけど、そういうのに甘んじず、数式処理ソフトで機械的に証明してやろうというのがこの本の趣旨です。さらには、右辺のような閉形式が分かっていないなら、それを求めることも行います。数式処理ソフトの中身がどうなってるのか気になる人とか、自動証明とか定理証明支援が好きな人には面白いと思います。

さて、自動証明をすることにはどのようなご利益があるのでしょうか。大体以下の3つにまとめられます。

人間が証明をサボれる。ミスがない
現実的に人の手じゃ無理な等式を証明できる
新しい等式の発見ができる

この本では、特に超幾何級数に絞って自動証明を扱っています。僕は統計畑の人間じゃないし、正直超幾何級数のありがたみは良く分かってないのですが、多分次のようなことがうれしいのだと思います。

超幾何級数は指数関数など良く見る関数を含む大きいクラスである
組み合わせ論、統計で等式証明をしたい機会がある

超幾何級数とは

超幾何級数について定義します。この本ではproper hypergeometric termがよく扱われています。

proper hypergeometric term
F(n,k)がproper hypergeomtric termであるとは


と書けること。ただし  は多項式で、  は全て整数で他のパラメタを含まず、
は非負整数である。

気持ちとしては $F(n+1,k)/F(n,k)$ と $F(n,k+1)/F(n,k)$ の両方が $n,k$ の有理関数になっていることを言っています。以下紹介していくアルゴリズムには、proper hypergeometric termに限定したときだけ、正当性が証明されてるものがいくつかあります。

$f(n) = \sum_k F(n,k)$ 　というように書ける、hypergeometric termの和が超幾何級数です。例えば、テイラー展開を考えれば指数関数はhypergeometric termの和で書けます。

以下特に断らない限り $\sum_k$ の $k$ は $\mathbb{Z}$ 全体を動くとし、 $\binom{n}{n+1}$ 等は全て0となるとします。

等式自動導出のアルゴリズム

等式自動導出の概略

等式自動導出は次のような手順で進みます。

$F(n,k)$ が満たす漸化式を求める。
適切な条件の下、両辺を $\sum_k$ をすることで $f(n) = \sum_k F(n,k)$ についての漸化式に変形する。
その漸化式を解く。

それぞれの手順を順に見て行きます。

漸化式の導出

$F(n,k)$ が満たす漸化式を導出するのは、Celineのアルゴリズム、もしくはその改良版であるZeilbergerのアルゴリズムを用いることで機械的に行えます。まずはCelineのアルゴリズムについて紹介します。

Celineのアルゴリズム
適当な正規性条件の下、漸化式

を導出するアルゴリズムが存在する。
ただし、 は多項式。

アルゴリズムがなぜ働くのか大雑把に解説します。未知なのは $a_{i,j}(n)$ なのでこれを発見するのが目的になります。まずは、 $I,J$ を固定して考えます。この時、両辺を $F(n,k)$ で割ると、 $F(n+m, k+l)/F(n,k)$ は有理関数になるので、適当に分母を払い整理することで $n,k$ についての多項式になります。変数 $k$ の $\mathbb{Q}(n)$ 係数多項式として整理して、全ての係数が $0$ になる $a_{i,j}(n)$ が発見できればよいことになります。これは $a_{i,j}(n)$ についての $\mathbb{Q}(n)$ -線型方程式になっています。*1 $I,J$ が変化するとき、未知変数 $a_{i,j}(n)$ は $IJ$ というオーダーで増えていきます。一方方程式の個数、つまり漸化式を整理したときの $k$ の次数は $I,J$ の線形オーダーで増えます。よって $I,J$ を小さいものから始めて行き、解が見つかるまで増やしていけば、いつかは未知変数のほうが多くなりこの線型方程式は解けます。

このCelineのアルゴリズムを発展させると次のZeilbergerのアルゴリズムが得られます。

Zeilbergerのアルゴリズム
適当な正規性条件の下、漸化式

を導出するアルゴリズムが存在する。
ただし、 は多項式で、は有理関数。

例えば
$F(n,k) = \frac{\binom{n}{k}^2}{\binom{2n}{n}}$
はZeilbergerのアルゴリズムを用いると
$F(n+1,k) - F(n,k) = G(n,k+1) - G(n,k)$
$G(n,k) = \frac{-3+2k-3n}{2(2n+1)(n-k+1)^2}F(n,k)$
という漸化式を満たすことが分かります。

$F(n,k)$ から $f(n)$ へ

次はZeilbergerのアルゴリズムで得られた $F(n,k)$ についての漸化式を $f(n)$ についての漸化式に変換します。 $G(n,k)$ は $k$ についてコンパクトなサポートを持つ*2という条件の下で両辺 $\sum_k$ を取ると
$\sum_{j=0}^J a_{j}(n)f(n+j) = 0$
となります。 $(G(n, k+1) -G(n,k)) + (G(n, k+2), G(n, k+1)) = G(n, k+2) - G(n,k)$ と途中の項が全て打ち消されるのがポイントです。

先ほどの $F(n,k) = \frac{\binom{n}{k}^2}{\binom{2n}{n}}$ についても、 $F$ がコンパクトサポートを持つことから、 $G$ もコンパクトサポートを持つと分かります。すると $f(n) = \sum_k F(n,k) = \mathrm{const.}$ が成り立つことが分かります。初期条件 $f(0) = 1$ は容易に示すことができます。これより $f(n) = 1$ 、つまり $\sum_k \binom{n}{k}^2 = \binom{2n}{n}$ が導かれます。

漸化式の求解

輪講では扱いませんでしたが、8章のHyperアルゴリズムを用いると以下のことができます。

漸化式が閉形式*3の解を持つかを判定する。
解があるならばそれを出力する。

これで無事超幾何級数の閉形式が未知であったとしても、閉形式の解があるかを判定し、あるなら求めることができ話が完結します。

WZ Phenomena

$\sum_k \binom{n}{k}^2 = \binom{2n}{n}$ の証明中にでてきた特殊な形の漸化式
$F(n+1, k) - F(n, k) = G(n, k+1) - G(n,k)$
について考えてみましょう。このような $(F,G)$ の組をWZ pairと呼びます。先ほどの話の一般化で、このような漸化式が得られれば、適当な条件の下 $\sum_k$ を取ることで $\sum_k F(n,k)$ についての等式を得ることができます。さらにこの漸化式は $F,G$ と $n,k$ それぞれの入れ替えについて対称性があります。よって、 $\sum_n$ を取ることで $\sum_n G(n,k)$ についての等式を得ることができます。等式証明の途中でWZ pairがでてきたら、もう一つおまけの等式も得ることができるのです。