テスト駆動開発と静的型付け言語

テスト駆動開発という開発手法があって、開発する前にまずテストを書きましょうというものだと理解しているのだけど、強い型付けをする言語とはあまり相性が良くないのではないかという話。

テスト駆動開発だと、最初にテストを書くから、テストされるコードの方は最初は未実装かスタブコードになるんじゃないかと思う。例えば、とりあえずあるメソッドを呼んでみて、未実装だと例外が返る、というような。だけど強く型付けられた言語の場合、未実装な関数を呼んだりすることはもちろんできない。assert falseみたいにスタブコードを書くことはできるけど、これコンパイルは通るのにいざ実行するとクラッシュするという静的型付けの意味をなくしてしまうようなコーディングだと思う。スタブコードを出荷コードにうっかり残してしまうと大変。(コンパイラフラグでassert falseを通さないようにできたかもしれないけど)。(できないみたい)

というわけで、テスト駆動開発を強い型付けを持つ言語(OCamlとかHaskellとか)に持ち込むのはあまり自然でない気がする。こういう言語では、私はまず型を書いてコンパイルが通るか見て、そのあとでテストを書いていく。まあテストし忘れてあーってなることも多いけど。

87クロッカーズ 2

 無茶苦茶な話になっているような。

MacBook Pro Retinaモデルを購入した

使っていたLet's Noteがだんだん遅くなってきて、何か作業するごとに数分かかかるようになった。新しいPCを検討していたわけだが、仕事で使っているVaioは今ひとつだし、Let's noteはどうもサイズがしっくりくるモデルがない。Lenovoはデザインが好きじゃない。というわけで、前から興味があったMacにしてみた。iPhone、iPadときて本丸を攻め落とされた感じ。

感想を箇条書きで。

• ディスプレイは美麗。入っているフォントが美しいのもあるかもしれない。ただ、ビットマップでアイコンを表示させているようなアプリ(Google日本語入力だとか)だと表示が汚く見える。
• 喧伝されているジェスチャー機能だが、功罪相半ば、という感じ。確かに面白いし、覚えると便利そうだ。だが、ちょっとした動きを意図しないジェスチャーとして解釈されてしまい、意外な動作をされてしまうことも多い。これを書いているとき、デスクトップを切り替えようとして、ブラウザのバック操作になってしまい、一旦投稿画面がまっさらになってしまって焦った。Undoボタンで戻るんだね、こういう時。ジェスチャーよりもわたし的にはMacはキーボードショートカットが覚えやすい(メニューにそのまま書いてある)ことの方が助かっている。いやWindowsでもキーボードショートカットを覚える良いやり方はあるのかもしれないけど。
• 普通にUnixのコマンドが使える。これは嬉しい。ただOCamlの環境をインストールするのはそれなりに面倒なのだろうか。Godiとか動くみたいだけど、バグがあるとかいうメールも流れてるし(分かってません)。Linuxほどすんなりは動かなさそう。手で入れるのが一番簡単そうだけど、あとでOCamlのバージョンを変える時、パッケージ管理システムがないとわけがわからなくなるので。
• Windowsと違っていて戸惑うことも多いのだが、(例えば、右クリックと左クリックの違いとか)、全体的に言うとMacのほうが洗練されていて使いやすい気がする。(個人の感想です)例えば、WindowsのバックアップとMacのTime Machineを比較すると、自動で履歴管理までしてくれるTime Machineの方が圧倒的に優れていると思う。
• Finderはまだ使いこなせていない。マイファイルにはEmacsで編集したファイルは更新されたファイルとしてリストされないのかな。そうだとするとEmacs使いとしてはあまり意味が無さそうな…

まあこんな感じです。開発環境の導入はまだなので、そうしたら文句とか出てくるかも。

そこをなんとか

jmukさんが紹介していたので読んでみた。弁護士就職難の時代に何とか就職した新米弁護士、楽子（もとキャバ嬢)が右往左往する話。1話で笑わせ、法律知識を散りばめつつ楽子のキャラも立て、最後は「いい話」的な結末に持っていこうとしているので、何だか1話ごとの密度が高い感じ。1回読んだだけでは分からない部分もあったり。

まあ面白いと思います。続きを買うかは未定。

人生をプレーンテキストで管理する

昔は頭の中で考えて済ませて、外にメモったりはしない質だった。実際、数学についてはいくらメモをとっても、見返すときにはもっと考えが進んでしまっていて役に立たないことが多い。でも日々の雑事を全部頭に入れておくのは無理だ。

というわけで、メモアプリということになるわけだが、世の中的にはEvernoteとOneNoteがよく使われているようだ。私もEvernote→OneNoteと来た人間。ただし時間管理は紙の手帳でしている。しかし、どちらもメモの形式が事実上プロプライエタリなので(Evernoteはデータ形式を公開しているけれども個人レベルでそれをハックするのはかなり大変そう)、プレーンテキストかそれに近い形式でメモを保存するツールを検討していた。

思いつくのは3つくらい

1.howm
2.org-mode
3.Gmailをメモツールとして使う。

まあEmacsユーザーなので。でも3.は結構まじめに考えた。Gmailを使えば検索もできるし、タグも貼れるし、モバイルでも参照できる。実際、Noteというタグがデフォルトで付いているということは、メモツールとして使うことも想定されているのかな？ただ、やはりUIはメール前提なので、使いづらいという声が検索をかけてみるとちらほら。必ずスレッド表記になるので、検索の時どのメモに検索語が含まれているか探すのが大変とか(これはメールの場合もそうなので、何か方法がある気がするが。)、メールとして例えば自分に送ってしまうと、それを編集するのが面倒とか。下書きにメモを貯めておく事を勧める人もいるが、自分としては下書きはメールの下書き用に取っておきたい。何より怖いのは、自分用のメールを間違って他人に送ってしまうこと。やはりメモツールとメールは分けたほうが良い気がする。

というわけで、あとはhowmかorg-modeだが、全文検索ベースでシンプルな作りというところが気に入ってhowmにしてみた。org-modeもiPhoneクライアントがあるみたいだし、なかなか良さそうだけど、アジェンダに表示するページを手で登録しなくてはいけないようなので、面倒だなと思ってやめた。

で、howmだが、まだ使い始めたばかりなのでなんとも言えない。色々足りない所があって、elispを書かなくてはいけない所が楽しいかも（?）。

また使い方が固まってきたら報告したい。

ゲーデルの不完全性定理からP≠NP問題にアプローチする

ゲーデルの不完全性定理からP≠NP問題にアプローチする試みがあるのだけれど、それを(私の偏った見方から)紹介してみたい。

論理学から P≠NP問題 にアプローチするやり方はいくつかあって、例えば記述複雑度を使ったやり方(以前、 Deolalikarが使っていた方法)であるとか、命題論理の証明の長さを用いた方法などがある。その中の一つが、限定算術を使ったアプローチだと思う。

さて、まず限定算術とは何かだが、論理学では自然数の公理系を算術と呼ぶことが多い。自然数の公理にはいろいろ重要なものがあるが、自然数を最も特徴付けるのは数学的帰納法の公理だと思う。この数学的帰納法をどのような言明に適応できるかで算術の体系の強さが決まる。限定算術では、数学的帰納法を適応できる言明を量化（「すべて」や「存在する」）が言及する範囲が有限
の範囲に限定されている。（ので限定という。）例えば、「$n$から$2n$の間に双子素数が存在する」という言明について数学的帰納法を使うのは良いが、「$n$以上の双子素数が存在する」に対して数学的帰納法を用いることはできない。

限定算術の何が興味をひくかというと、計算量クラスとの間に密接な関係があるからだ。特に、Bussが定義した限定算術の階層 $S^1_2 \subseteq S^2_2 \subseteq \cdots$は多項式時間階層と対応していて、Bussの階層の分離から多項式時間階層の分離へアプローチすることが試みられてきた。

では、$S^1_2 \subseteq S^2_2 \subseteq \cdots$とは何かというと、まず通常の算術に比べて幾つか基本となる関数記号を追加する。特に重要なのが$a\#b$という関数で、意味的には$2^{|a|\cdot |b|}$ ($|a|$は$a$の2進表現の長さ）を表している。この関数によって、多項式時間関数の増大度を抑えることができるようになる。この上で、Bussは数学的帰納法に使われる言明の中の量化の個数によって階層を定義する。例えば、$S^1_2$では1個の量化しか数学的帰納法の中で使ってはいけない。ちなみに2は$\#$関数が入っていることを表している。

さて、ではこのBussの階層と多項式時間階層がどうつながるかというと、｛$S^i_2$で停止性が証明できる関数｝=｛多項式時間階層のi番目の関数}という関係になる。例えば、$S^1_2$で停止性が証明できる関数は、多項式時間関数と一致し、$S^2_2$はNP関数に一致する。

さて、もしBussの階層がつぶれて、$S^1_2 = S^2_2$ (定理の集合として）となったとすると、上の関係からP=NPとなる。というわけで$S^1_2 = S^2_2$かどうかが問題になるわけだが、この手の話にありがちなように、これはまだ未解決問題だ。一般に、Bussの階層がつぶれれば（つまり$S^i_2 = S^{i+1}_2$)、多項式時間階層もつぶれる。一方で逆は今のところ示されていないが、公理としてP=NPを追加して、それでもつぶれないことを示せれば、P≠NPは示せる。（Takeuti 2000）

というわけで、Bussの階層がつぶれないか（上の方の理論が下の方の理論と違っているか）どうかがいろいろと研究されている。そして、ある理論Tと、その理論Tの拡張Uがあったとして、それが違うことを示す常套手段はゲーデルの不完全性定理だ。Tは自分の無矛盾性Con(T)を示さない。一方、UがCon(T)を示せば、TとUは違うことが分かる。

しかし、残念なことにこの方法は限定算術には直接には適応できない。というのも、限定算術はほとんど何の無矛盾性も示すことができないという結果があるからだ。（Wilkie,Paris 1987)

そこで、証明の概念を変えてみたり、更に弱い体系を考えてみたりといろいろ工夫されているが、今のところ成功はしていない。この件で私も1つ論文を書いてみたんだけど、その話はまた疲れてきたのでいずれ。

2013/06/28追加 続きを書いている。ゲーデルの不完全性定理からP≠NP問題にアプローチする - その２

Logical Methods in Computer Scienceに投稿してみた。

LMCS(Logical Methods in Computer Science)という雑誌に私の論文が掲載された。内容は、P=NP問題にゲーデルの不完全性定理からアプローチするという試みに関係したものだけど、内容のことはここでは置いておく。

で、書きたいことは投稿した雑誌のこと。この雑誌のことは多分、まともに計算機科学の研究をされている方はすでによくご存知だと思うが、私は少し前にAvigadが書いているのをどこかで読んで初めて知った。この雑誌、オープンアクセスの雑誌なのだけど、編集長がDana Scott、編集委員にBenjamin PierceとかGordon Plotkinとか、私の投稿した論文の分野だとKrajicekと有名な人が並んでいる。インパクトファクターも0.8くらいだからロジックの雑誌としては高いのかな？論文はCreative Commonライセンス（改変不可）で再配布可能。査読も早くて、私の場合、投稿したのが3月の始めだったので5ヶ月くらい。

技術的なことを言うと論文のストレージと配布はArXivに基づいている。オンラインジャーナルは継続性が不安だけど、ArXivなら安心できるような気がする。本体のhttp://www.lmcs-online.org/index.phpは、1度ディスクがいっぱいになって操作できなくなったりしたけど、なかなか使いやすかった。

ていうわけでなかなか良いんじゃないでしょうか。