Twitter: @kinaba
私が一番好きなSFと言えば『百万年の船』ですが、 昨日読んで『タウ・ゼロ』が二番目に好きなSFに なりました。最近本の感想が大袈裟です。このどうしようもなく取り返しのつかない方向に お話が突っ走っていくっぷりが楽しい。あと、私が感情移入する気になれる主人公ってそうそういない。 いやそれはともかく、 まだこの二冊しか読んだことないのですけど、どうも自分はポール・アンダースンを読み漁るべきっぽいな。
UTPC というのに参加してました。 みんな解いてるから解けるはず！と思って挑み続けた E が結局解けずじまいでした。 うわーん。K かせめて H に時間使うべきだった。しかし若者勢とロートル勢のバランスが絶妙だ。
→ 提出物一式。
ICFP Programming Contest のページが更新されてました。
Tim Sheard って Template Haskell のひとだ！ きっと激しくコンパイル時メタプログラミングする問題が出るに違いない！ と適当なことをページ開いて３秒で思ったのですが、調べてみると ICFPC 2002 の荷物運びコンテストの Organize もされてたみたいですね。スタイルシートがほぼ同じだ。 これは予習をするなら2002年の問題でやるべき！（適当）
結局 [PDF] "Parametric polymorphism through run-time sealing, or Theorems for low, low prices!" （形無しλ計算（Scheme）と型付きλ計算（ML）をハイブリッドに混ぜる言語を作るときに、 MLでのパラメタ多相型の値の対応物をScheme側でどうとると嬉しいことになるかという話。 型変数に対応する値を Sealing（動的なアクセス制限みたいなの）で隠して扱うとパラメトリシティが成り立つよー とかなんとか。） と "Foundations of the C++ Concurrency Memory Model" （C++のメモリモデル（マルチスレッド対応版）をどうにかするスレ。 tryLockを変な風に使うと大変なことになりますという例が考えたことなかったので面白かった。 あとJavaと違って"変なコードは全部undefinedだぜ" という規格にしちゃっていいので ある意味C++の方が規格化するの楽だ、という辺り興味深い。） と "Making Data Structures Confluently Persistent" （普通に破壊的代入を使って定義されたデータ構造を後付で persistent （更新操作後も操作前の バージョンに常にアクセスできるタイプのデータ構造） に変換する手法は Tarjan 辺りが既に確立している わけだけど（更新操作毎にリビジョン番号打っておいて、リビジョン指定からその時のバージョンを 効率的に取り出せるような工夫をして頑張る感じ）、それをさらに拡張して confluently persistent 化 （複数のバージョンのデータをマージする二項演算、三項演算等に対してもpersistentなデータ構造）するお話。 要はリビジョン番号の打ち方を上手いこと工夫すると上手く行く。） を読んでました。
帰りは くるるさん一押し の本で時間つぶし。とりあえず
……完全性定理、不完全性定理の評価はともかく、連続体仮説と選択公理の整合性の証明ですら彼の真価を示すものでは ないんです。連続体仮説の整合性を証明したのに 2א0 = א2 を主張し、Lと共存しうるような巨大基数しか知られていなかったときに 巨大基数公理が連続体仮説に関係すると看破した、その見通しのすごさ。
…という感覚はよくわかった気がする。素晴らしい。 あとはちゃんと全部定理を追って、今度こそ Forcing を理解するぞ大会に人生で５回目くらいの挑戦を…。 帰りに同時並行で脳内開催していた今度こそ5次方程式に解の公式がない理由を理解するぞコンテスト （人生７度目くらいの挑戦）が こちらで紹介されてた本 のおかげでだいぶ達成に近づいた気がするので、こっちも頑張る。
出力が少なすぎてよくない
安い航空券にしたせいで、明日の昼から20時間近く 飛行機/空港で時間つぶさないといけない上に、その対策として週末に買い込んだはずの文庫本を 何故か大部分読み終わっちゃってピンチなのです。 なにか面白い論文なんぞあったら明日の朝までに紹介してもらえると僕が凄く喜ぶらしいですよ！ とりあえず [PDF] "Parametric polymorphism through run-time sealing, or Theorems for low, low prices!" とか印刷してみた。タイトルで選ぶ。
まあ、電源の保つ限り D の翻訳でもして、あと数日前から再開してみた Project Euler の 185 を考えてたら終わる気もする。これホント全然解けないんですけど。 他残ってる２問は手を動かすだけだと思う。
『谷崎潤一郎犯罪小説集』読んだ。 なにこの傑作集。春琴抄とか痴人の愛とかじゃなくてこの辺の作品が代表作とされるべきだよ。 新潮でも同じ系統のが出てるみたいなんだけど4725円か…。
あとさっきAmazonまとめ買いする本を見繕ってて気づいたんですが、 はこぶね白書が最終回とな。 これは楽しみ。好きなマンガが終わって嬉しいと感じるのはなかなか自分でも不思議なことですが、 藤野もやむのこれまでの作品 ‐ ナイトメアも賢者もPBSも、どれも最終話がとても好きなので ついつい期待してしまう。いや途中も好きなんですが。複雑だ。
ヒット 16件 ってのが意外だったので言葉だけブチ上げておこう。「証明駆動開発」（テスト駆動開発的な意味で。
きむらさんの引用 を読んでての感想なんですが、「定理証明支援系 (Coq とか Agda とか) を使うことで、書いたプログラムの正しさを 厳密に証明できる」という見方は、間違ってはいないと思うけれど違和感があります。 「テストツール（JUnit とか Test::Unit とか）を使うことで、書いたプログラムをテストできる」 と同じくらいの違和感。だって、"テスト"って テストファースト で使わないと価値半減ってレベルじゃ済まないですよね。"証明" も同じ。
「先にテストを書いて、それを通すようにコードを書く」スタイルが設計やコードの書き方に 影響を与えるのと同じように、「先に証明の筋道と途中で使う補題を書いて、それを満たすようにコードを書く」 スタイルは、設計やコードの書き方に大きく影響します。 そういう観点でもう少し語られてもいいのではないかと思ったりしました。 （ついでにいうと、 そういう風に書かれたコードでないと、ぶっちゃけ、 いくら証明支援系を使おうが証明なんて事実上無理です。 100年後にどうかは知りませんが、すくなくとも今は難しすぎる。）
自分自身は "Development" と言えるようなレベルでそこまで考えたことないので、 まあ、Proof Driven Coding くらいですけど、最近わりと証明することを意識してコードを書いています。 その方が楽なことがわかってきた。
再帰するときは、無限ループしちゃわない証明のために、どの引数が「減る」か必ず考えながら書くとか。 id:uskzさんの "ループ使うならちょーかんたんな場合を除いてloop invariant使ってドキュメント化しておくべき" もそういう意味で同意だったりします。
先日の Bootstrapped Queue の実装ですけど、 あれ一番複雑なのはコンストラクタなんですが、あいつは、 まず Queue の各メソッドが正常動作することの証明を頭の中で考えて、 その証明を成り立たせるための仮定（事前条件）を考えて、 Queue のインスタンスでそれが常に成り立つ（不変条件）ようにするにはどうするか、 という思考の結果あのコードになりました。（コンストラクタにコードが集中する設計も こう考えた結果だったりする。）考えた不変条件はコード中に残してありますが、 そこからはほとんど自動的にサクサクあの実装が出てきます。不変条件を考えなかった場合 もっとスパゲッティなコードを試行錯誤するはめになったと思う。
まあ、そもそも考えた不変条件自体が不十分だったので、思いっきりバグってたんですけどね！
ただ、ここでもし証明支援系を使って書いていれば、 こういう「僕の考えた仮定・証明」の正誤判断を全自動で手助けしてくれて確実にバグが見つかったはずです。 そういう風に、まず先に "証明駆動開発" というスタイルがあって、それをサポートするものとして 証明支援系がある、というのが今の自分の認識。
例によって何がいいたいのか自分でもわからなくなってきたので、箇条書きで逃げましょう。
※追記： >> b:id:sshi 私の中では "Constructive Programming" == "Curry-Howard based Purely Proof-driven Programming" 的イメージ（「仕様を満たす出力が存在する」という命題の構成的な証明を書いて、そこから プログラムを抽出する手法） なんですけど、たぶん私が構成的プログラミングを狭く捉えすぎなので、 要するに同じことのような気もしてきました。 例えば「仕様を Hoare Triple で考えて、適当に中割りしながら間をつなぐプログラムを考える方式」 って構成的プログラミングになるのかな ←よくわかってない
寝る前に布団の中でゴロゴロしながら 『ソードアート・オンライン』 読んでたら朝の8時になってました。
おもしろい。まあ元々自分は"仮想世界"モノが好きすぎるんですけど、うん、面白い。 SAO1 は、「よくできたバーチャルリアリティなゲームに閉じこめられましたゲーム内で死ぬと プレイヤーも死にます」 のワンテーマ一点突破。巧くできてる、と思う。結末に至る流れが好き。 SAO2, 3 も基本的にその続きで、ストーリー的にはともかくテーマ的には外伝と言っていいくらいじゃ ないかと思うんだけど、でも、ここで着実に作り上げた世界が、蒔いた種が、SAO4 で炸裂するのだ。 "仮想世界"モノが行き着く先は、究極的には一つだと思う。 その"一つ"がこういう方向にあるというのはちょっと予想してなかった。 ク○○○○○だと思ってたらグ○○○○○だった的な（丸の数は適当）。 あと SAO4 の仮想世界のレンダリングを支えるとされるSF的アイデアが、 多分わりとよくあるんだと思うんですけど、自分の脳内引き出しに無かったので新鮮だったかも。 さらにそれとは別に作中に出てくる技術に、STLという名前のがあって名前だけで燃え萌えできてよかったりとか
が何個かあるんだけど、一記事 20KB は軽く行きそうなのばっかりでなんかめんどい。３行でまとめろ俺。
lethevertさんに言及いただいた 「Java(のGenerics)は(DのTemplateと比べて)便利だなあ」発言 ですが、 そういえば、この記事書いた後ひとに突っ込みもらって、用語の選択ミス等々で伝えたいことを 上手く伝えられてなかったっぽいと気づいたことを今思い出しました。 というわけで、今頃になってフォロー記事を書いてみます。
件の Finger Tree でも使われてましたが、純粋関数型データ構造を作るときに頻出のテクニックの一つとして、 "Non-uniform type" / "Non-uniform recursion" ていうのがあります （Nested datatype とか Polymorphic recursion とか別の名前で呼ばれることもあります）。 あ、まずその前に、Non- じゃない "Uniform type" / "Uniform recursion" っていうのは要するにごく普通の再帰的なデータ型/再帰関数 のことです。たとえばツリーとか。
class Tree<E> { E data; Tree<E> left, right; }Treeの定義にTreeが登場してる…つまり再帰的な定義なんですが、 この再帰の時に型パラメタの部分はいっしょ （Tree<E> の定義には Tree<E> を使っている） なことを指して、uniform と呼ばれています。
さて、Non-uniform recursion というのは…もうおわかりだと思いますが、 型パラメタを変えながら再帰すること。 例えば、「キュー Queue<E> を実装するのに、 Queue<List<E>> を使うとすごい高速！」 というファンキーな技があります。 （c.f. このPowerPoint の"Bootstrapped Queue"あたり。前９章の内容前提な上に口頭で補足するの前提な資料なので わかりにくいですが。スミマセン）
// Java
class Queue<E> { ... Queue<List<E>> impl; ... }
// D
class Queue(E) { ... Queue!(List!(E)) impl; ... }
// C++
template<typename E>
class Queue { ... Queue< List<E> >* impl; ... }
でですね、これは、Java の Generics なら普通に何も考えず↑こう書けば実装できます。 一方で C++ や D の Template だと、できません。テンプレートを型パラメタ毎に別々に実体化 しないといけないので、Queue<int> を使うには Queue<List<int>> が必要で、 Queue<List<int>> を使うには Queue<List<List<int>>> が必要で、 Queue<List<List<int>>> を使うには…（以下略。無限のテンプレート実体が 必要になっちゃうからです。Java ならイレイジャでの実装なので、パラメタが違ってても実体は１つです。
※本当かな？と思って実際にC++やDで書いてみる人向け注意。
単に↑のように再帰的にimplというメンバを定義するだけだと、implは使われないので実体化もされず、
無限ループもしません。何かimplを使うメンバ関数
（例えば、bool empty() { return !impl || impl->empty(); } とかなんとか）
を適当に実装して呼び出してみるとコンパイルが止まらなくなって楽しい気分になれます。
追記： ちゃんとしたサンプルとして Java版 Booststrapped Queue を
実装 sub/BtsQ.java
（遅延評価してないのであんまり意味ないけど）しました。
これを C++/D に移植してみるとコンパイルが止まらなくなって楽しい気分になれます。
追記の追記：バグってた！ので修正。
「型を変えて適当にキャストを挟み込む」とか「実際に実行時に使われる再帰の段数は大抵logオーダーなので、 32段くらいで強制的に再帰をストップするようなテンプレートを書く」とか無理矢理なんとかする手は あるんですが、まあ不便ですよね、という。
「C# とか C++ とか」って書いてあったので反応してみた２。
が、C# とか C++ とかを使っていると、静的型があるのが苦しくて苦しくて仕方がない。 … (略) … これは単純にポリモーフィズムのお話で、静的型付け というよりは、nominal subtyping が 脳のリソースを大きく引っ張っていく割に、作りたいことの本質ではないから。 動的型付OOPLとか OCaml のような、structural subtyping のほうが ぜんぜん Lightweight に感じます。
from LLとOO - みねこあ
最初に結論から書いておくと、「C++ ほど Structural Polymorphism 大好きな言語を他に私は知らない。」 ので、↑と感じるとしたら C++ 的でない使い方で C++ を使っているか、 あるいは脳のリソースを引っ張っているというのは実は別の部分なのではないでしょうか…等々。 あとこれも最初にお断りとして、私 Smalltalk まったく知らないに等しいため Smalltalk と比較して どうかは判断がつかないので、引用部で例にあがっている動的型付OOPLの例としてRubyとPython、 あとOCamlをなんとなく念頭に置いて以下を書きました。
とっさに頭に浮かんだのは、「既存のStringクラスと互換性のある別の文字列クラスを作りました。
でも、それに対して既存のRegexpクラスで正規表現検索することができません。」
なんての（id:ku-ma-me:20070730）
が許されるのはLLまでだよねー。
String と同じメソッド群を 持ち同じように振る舞うならそれは String である…っていうと Duck Typing になっちゃうか、 えーとえーと、「Regexp が要求するあれとこれとそのメソッドを持ってれば全て正規表現検索対象にできます」 っていうのが Structural Typing 的な考え方であって、"String" っていう"特定の"クラスだけを 検索対象にできます、っていうのは Nominal Typing 的な考え方だと思います。 そしてもちろん、C++のregex は前者です。 果ては Xpressive みたいな、正規表現を文字列以外の方法で記述できる実装だと、 「文字」の「列」ですらなくても「文字とおなじようにふるまうもの」の「列」に対して正規表現 使えちゃったりとか。intの配列から、100未満の値が繰り返されてる部分を取り出し！
※ 正規表現という例は恣意的にすぎる、という指摘はアリだと思います。 例えば仮に 100% Pure Ruby で実装された正規表現エンジンがあったとすれば、 それはおそらく、当然のようにString互換のRopeなども検索対象にできるでしょう。 標準のRegexpがそれをできないのは、その部分は速度のためetcでCで実装されているためであり、 速度のためetcでStringのデータ表現を仮定しなければならないからだ、例外だ、という。 でも、いかなる都合であれ、その言語の使い手誰もが使う標準ライブラリという部分ですら貫けないような 概念はその言語の看板にはならないと思ってて、で、一方で、C++はありとあらゆるレベルで Structural な方式を貫くことができる言語ですし、実際「イマドキの」C++のコードはそのように作られていると思う。
※ それと、そうだ、"文字列"として最低 std::string と std::wstring と char* と wchar_t* の４種くらいは デフォルトで存在するので対応しなくちゃいけない大変面倒くさい状況だからこそ C++ はそんなことに なってるのではないか？という指摘もある程度その通りだと思いますが、それは原因に対する考察であって、 原因はどうであれ、とにかく結果としてC++のライブラリはやたらGenericだという結果に違いはないと思うのです。
そもそも STL （C++標準の、データ構造＆アルゴリズムのライブラリ）が 徹底して「あれとこれとそのメソッドを持ってるオブジェクト全てが処理対象です」という形式で 機能を提供しているのが始まりだと思うんですが、正規表現に限らず、あらゆる（というと言い過ぎですが） C++ のライブラリはこんな方向でできています。例えば asio (ネットワークI/O) のドキュメントなんかが、ちゃんとハイパーリンクされてて一番わかりやすいかも。 引数 SyncReadStream や MutableBufferSequence をクリックしてみるとわかるように、 「○○の派生クラスのインスタンスを引数として受け取ります」みたいなAPIではなく、 「read_someメソッドを提供しているオブジェクトならなんでも引数として受け取ります」という定義に なっています。そういうふうにできている。
まとめ。「C++ コミュニティから出てくるライブラリは、 特に2008年の今ならほとんどすべて、ユーザーから受け取る型を Structural に定義しています。 その徹底度合いは私の乏しい知識の中で知っている言語（動的静的を問わず）の中でも トップレベルに感じられます。そういう意味で、Structural Polymorphism は "C++ Way" と言えるのではないかと思います。」
「生きてるオブジェクト」を示す式 を見て、それだと解が一つに定まらないので "live はこれを満たす最小の集合とする" か何か 注釈つけないとダメじゃね？ と重箱の隅を突っつきたくなったんですけど、考えてるうちに、 これはこれでアリかと思えてきたりした朝でした。
この式を満たす最小の集合は、適当に日本語で言うと「Root からポインタをたどってたどりつける オブジェクト全部の集まり」になって、これが「生きてるオブジェクト」の定義として直感的に 意図されるものだと思います。じゃあ、その式を満たす最大の集合は何だろう。 これはたぶん、「Root もしくは循環参照してるオブジェクト、 からポインタをたどってたどりつけるオブジェクト全部の集まり」になる。 なんかこれはこれで、ある意味で、 というか何の工夫もない参照カウントGCから見て生きているオブジェクトという意味で、 意味があるような気がしなくもない。自己参照だけは検出できるような参照カウントGCだと、 また別の中間の解に落ち着いたり。
なお類題として
Na = {n ∈ String | (n="") or (∃nn∈Na. n="na"+nn)}
Oyatsu = {o ∈ String | (∃nn∈Na. o="Ba"+nn)}
"Bananananananana..." (無限文字列) は Oyatsu に入りますか問題などがあります。
不可思議２ Final Dungeon クリアしたー！ たしか、リリースされた頃ほぼ同じ時期に Cresteaju もリリースされてそっちにハマりまくっているうちに自分の記憶からフェードアウトしてたなあ、 というのをちょっと前に思い出して始めてみたのでした。 マイナスアイテムが致命的すぎるな上に種類多いのがきっついですが、敵を1～3発で倒せる ＆ 自分も 4～5 発くらいで倒される 程度に調整されてるバランスは結構テンポがよくて面白かった。