読者です 読者をやめる 読者になる 読者になる

いきるちから

気が向いたときに適当なことを書きます

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

はじめに

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

そもそもRaspberry Piって?

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

自動ノート取り装置とは

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

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

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

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

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

続きを読む

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

数学 本の紹介

はじめに

輪講で『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,k) = P(n,k) \frac{\prod_{i=1}^{U} (a_in + b_ik + c_i)!}{\prod_{i=1}^V (u_in + v_i + w_i)!}x^k
と書けること。ただし  P多項式で、  a_i, b_i, c_i, u_i, v_i, w_i は全て整数で他のパラメタを含まず、
 U,Vは非負整数である。

気持ちとしては  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_kk \mathbb{Z} 全体を動くとし、 \binom{n}{n+1}等は全て0となるとします。

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

等式自動導出の概略

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

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

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

漸化式の導出

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

Celineアルゴリズム
適当な正規性条件の下、漸化式
 \sum_{i=0}^I \sum_{j=0}^J a_{i,j}(n) F(n-j,k-i) = 0
を導出するアルゴリズムが存在する。
ただし、 a_{i,j}(n)多項式

アルゴリズムがなぜ働くのか大雑把に解説します。未知なのは  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のアルゴリズム
適当な正規性条件の下、漸化式
 \sum_{j=0}^J a_{j}(n) F(n+j,k) = G(n, k+1) - G(n,k)
を導出するアルゴリズムが存在する。
ただし、 a_{j}(n)多項式で、 R(n,k) = G(n,k)/F(n,k)は有理関数。

例えば
 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がでてきたら、もう一つおまけの等式も得ることができるのです。

このようにWZ pairは一つの等式から新しい等式を得るのに有用です。他にも (F(n,k), G(n,k))がWZ pair なら  (G(-k-1, -n), F(-k, -n - 1)) もWZ pairとなることが示せます。これで新たに2つの等式を得ることができました。

他にもWZ pairを用いて新しい等式を得る方法がいくつもあります。WZ pairはZeilberger + Hyperと比べると一般性のない方法ではありますが、等式の発見ができるという点が有用で面白いです。

あとがき

ここで述べたアルゴリズムは適当な数式処理ソフトを用いて実際に使うことができます。例えばフリーソフトのSageを用いるなら、つぎのリンクが参考になると思います。
github.com

参考文献

Petkovšek, Marko, Herbert S. Wilf, and Doron Zeilberger. "A= B, AK Peters Ltd." Wellesley, MA 30 (1996).

*1:解は有理関数かも知れませんが、適当に定数倍すれば多項式にできます。

*2:有限個の k を除いて0

*3:n によらない有限個のhyper geometric termの和で書ける

『紅殻のパンドラ』(六道 神士、士郎 正宗(原案))

オタク

尊い

『科学哲学』(サミール オカーシャ)

本の紹介 科学

まえがき

今は数理工学を学んでるけど院では科学寄りの分野に戻るつもりなので、さすがに一回くらい科学哲学を体系的に学ぶべきだろうと思って読み始めた。真面目に講義取ったり本読んだりをしたことはなかったけど、どこかしらで聞いた話がちらほらあったしとくに詰まることなく読めた。中高大の教育環境がよかったんだなあと思う。圧倒的感謝。あとはちょうど高校のとき原発事故があって、この手の話に向き合わざるを得なかったのもあるかもなあ。

科学哲学 (〈1冊でわかる〉シリーズ)

科学哲学 (〈1冊でわかる〉シリーズ)

読んだのは上の本。

内容のまとめと思ったこと

1 科学とは何か

科学革命以降の科学史をふりかえりつつ、「なぜ科学哲学を学ぶのか?」や「科学とは何か?」といった問いに挑んでいく章。当然だが完全な解答が与えられるわけではない。

科学とは何か?

科学と擬似科学をどう区別するのか?という例を用いて、科学哲学がどう「科学の研究技法」を分析するかを説明している。この問いに関して一番有名なのはホパーの反証可能性だろう。実際この本でもまず先にホパーについて触れられている。

反証可能とは、理論は何らかの予測をなし、場合によっては観察結果と矛盾してその理論は棄却されうることである。ホパーは反証可能性が科学の根本的な特徴だと主張した。しかしこれはナイーブ過ぎると指摘されている。例えば、地動説は天王星の軌道予測に失敗し続けた。そこで天文学者は未知の惑星が存在していると考えたし、実際それは正しかった。しかしこの行いはホパーの意味で正しいのだろうか?天王星の軌道予測に失敗した時点で地動説は棄却されるべきではなかったのだろうか?未知の惑星の存在を仮定してよいのなら地動説は反証不能な理論になってしまうのではないだろうか?

ホパーの基準は単純すぎる。このことは、どこまでが科学か境界線がひくことがそもそも可能なのかという問いを投げかけている。

続きを読む

『位相と論理』を読んだ

数学 本の紹介

『位相と論理』という本を読んだ。タイトル的に位相空間を使ったヤバい意味論をガンガンやる本かなあと思って読み始めたけど、実際には束論と位相の本だった。要するにStoneの表現定理+α。他の本でカバーされてる内容も多かったけど、束を前面に出した簡潔な議論とか、位相空間とフレームの随伴とか見所は多かった。

位相と論理 (日評数学選書)

位相と論理 (日評数学選書)

読んでから気がついたけどこの本高い。びっくりした。

どんな本なの?

この本では論理はブール代数のことを意味している。ブール代数位相空間、あるいはもっと一般に束と位相空間にはどういう関係性が有るのかを探っている。主要な結果は以下の2つである。

特段今すぐ使える知識が身につくという感じではなかったが、束、論理、位相、圏あたりの幅広い話に触れられて楽しいのでオススメ度は高い。まあ気が向いたときとか、ちょっと束やりたい気分の時とかに気軽に読むといいと思う。薄いし。圏を知ってないと最後の随伴のところのモチベがわかりにくいかもなあとは思った。ここが面白いところなんだけど。逆に圏を知ってる人が読むと、一般論の具体例が得られるし、真面目に証明読まなくてもいいので楽しいと思う。僕は楽しかった。

各章の感想

1 順序と束

名前の通り束論の基本をやる。Heyting代数が出てきたあたりから随伴が出てくる。束における随伴の存在定理が、各点Kan拡張で証明できて楽しかった。他にも随伴と極限の保存とか圏論で束論をやれて楽しい。この辺はSGL*1とかもそうだけど。

2 命題論理とブール代数

ここもそのままタイトル通り。命題論理がブール代数の例になっていることを見る。完全性定理を束論で示すのは簡潔で面白かった。最後に付値の空間に位相を入れて、後のStone双対性に話をつなげている。

3 構造とモデル

超べきでコンパクト性定理を示す。確かに束論の応用と言えなくもないよなあ。

4 ブール代数の表現定理

圏の言葉は使わないが、ブール代数との圏とStone空間の圏が圏同値になるのを見る。Stoneの表現定理自体は新井基礎論でやったけど、束の言葉で読んだのは初めてだし、圏同値くらいいい性質がなりたつのは知らなかった。良さ。

5 フレーム

4章の結果を一般化する。フレームと呼ばれる、無限分配律を満たす束の圏と位相空間の圏の間には随伴関手がある。フレーム自体は使ったことなくてモチベがわかなかったけど領域理論とかででてくるっぽいですね。そのうちやることになりそう。

分配束イデアルの集合を束とすると、これはフレームになる。このフレームが普遍性とか位相空間に送り込んだときの同相性とかいい感じなので前章の拡張と思える。

6 カテゴリー

圏論の基礎をやりつつ、4、5章の内容を圏論の言葉で整理する。随伴なのが分かって楽しい。

*1:Sheaves in Geometry and Logic

"Internal set theory: a new approach to nonstandard analysis"を読んだ

数学 論文紹介

あさぜみ*1で発表しておいて今更感あるけど、Internal Set Theoryを勉強した。"Real Analysis through Modern Infinitesimals"*2とかも読んだけど原論文が一番面白かった。

Internal Set Theoryとは

超準解析を公理化したもの。ZFCに1つの述語(st(x))と3つの公理(transfer, idealization, standarlization)を追加してISTにすると、今まで超フィルターとかでがんばって超準モデルを構成してたのがうまく扱えるようになる。しかもZFCの保存的拡大*3になってて、stを含む論理式は含まない「等価」な論理式に変形できる。

超べきモデルを作ったりしなくていいところと、「既存の数学」との対応関係が明確なとこが個人的に面白かった。後は久しぶりに公理論的集合論使えて楽しかった。

各章の内容

1. Internal set theory

3つの公理を導入して、いくつかこれから使う定理を準備しつつ使い方を覚えるって感じの章。追加された述語st(x)は「xはstandardである」と読む。普通の超準解析で定数記号として入れてたやるがstandardになるというイメージで大体あってる。stを含まない論理式はinternalと言う。

追加される公理を見てみよう。
 \forall^{\mathrm{st}} \exists^{\mathrm{st}} はそれぞれ  \forall x (st(x)) \Rightarrow \exists (st(x))\landの略記とする。また \forall^{\mathrm{fin}} \forall x (xは有限) \Rightarrowの略とする。 \exists^{\mathrm{fin}}は上と同様にする。

*1:毎週誰かが数理工学の話題について発表するセミナー

*2:超フィルターとかを飛ばせるので、さっさと超準解析したいビギナーが読むにはいい本だと思う。

*3:stを含まない論理式がISTで証明できるならZFCでも証明可能

続きを読む

クワインと対角化定理 ~計算理論入門~

数学 情報科学

はじめに

クワインとは

この前プログラミングの教科書を読んでいたら面白い問題があった。大雑把には次のような感じ。*1

自分自身のソースコードを出力するプログラムを書け。

調べてみたところクワインというらしい。細かい話をすると入力を受け取るのもダメだそうなので上の問題文よりは厳しい。詳しい話はWikipediaにある。
クワイン (プログラミング) - Wikipedia
結構難しいし、SchemeとかHaskellはまだしもCのやつとか何やってるのか初見じゃ意味不明。頭がこんがらがるのが味わえるのでぜひ考えてみて欲しい。

クワインと計算理論

ところで、計算理論をかじったことある人は「これ対角化して不動点つくればいいんじゃね?」と気がつくと思う。実際その方針でこの問題は解けるし、Cとかのわけ分からん例もこのことを理解してるとすんなり分かる。もろに理屈っぽい計算理論が割と身近に思えるクワインに応用できるのが面白い。

というわけでこの記事では計算理論を紹介しつつ、それを軸にクワインをどう作ったらいいか考えていく。計算理論は本当は厳密に理論展開されてるけれど、この記事ではフィーリングでやっていく。チューリングとか黎明期の人たちにとっては計算機は理論的な存在で、扱うのは大変だったんだろうと思うし、真面目にこの分野を研究とか勉強するならフィーリングで済ませるべきではないとは思う。だけど僕らは幸い生まれながらに計算機に親しんできた世代なので直感が使えるし、ちょっと計算理論をかじってみる分には十分だと思う。計算理論の楽しさとかクワインの作り方がわかってもらえれば幸いである。

*1:手元に本がないのでわからない

続きを読む