Derive Your Dreams

Twitter: @kinaba

17:17 08/01/30

ところで

C++ か JavaScript か PHP が批判されてるのを見ると思わず何か言いたくなってしまうのだけど、 考えてみるに、他の言語だと割とどうでもいい。そういう意味では、今の自分が好きなプログラミング言語は この3つということになるのかなあ……などと徒然なるままに思いました。 単純に、つきあいが長い方から3つというだけかもしれない。

いやしかし、PHPに対する批判の多くはその通りであるとは思うのですが。 Attacking PHP で触れられてる「リストであり辞書でもある」 array ってあれは普通に便利じゃないです? 結構他の言語でも欲しくなるのですが。

17:08 08/01/29

PHP で Yコンビネータ

PHP じゃ Y コンビネータつくれない と聞いて。

<?php
// PHPでは関数呼び出しは 関数名(...) か 変数(...) のどっちかの形式しかできなくて、
// (関数を返す式)(...) みたいなことができないので、関数を一時変数に置くか call_user_func するか
// しかないんですが、変数($tなど)に置く方が読みやすそうなのでそっちで書きました。
// 後は amachang さんのJavaScript版の直訳。

function Y( $f )
{
   $t = create_function('$g','
      return create_function(\'$m\',\'
         $f =  "'.addslashes($f).'" ;
         $g = "\'.addslashes($g).\'";
         $t = $f($g($g));
         return $t($m);
      \');
   ');
   return $t($t);
}

$fib = Y(
   create_function('$f','
      return create_function(\'$n\',\'
         $f = "\'.addslashes($f).\'";
         return ($n <= 2) ? 1 : ($f($n-1) + $f($n-2));
      \');
   ')
);

echo $fib(10); // →55

…すみません90%くらい、ネタにマジレスならぬマジにネタレスでした。 こんなん二度と書きたくないよ。JavaScript の方が絶対面白いです ←結論。 というわけで以下関係ないようなあるような雑談です。

PHP にはクロージャがないっていうのはその通りで、

function adder($x) { return create_function('$y', 'return $x + $y'); }
$f = adder(1);
echo $f(2);

ってしても 3 にならないんですよね。ただ、create_function が文字列を受け取るという性質を使うと、

function adder($x) { return create_function('$y', "return $x + \$y"); }
$f = adder(1);
echo $f(2);

これなら 3 になる。言い換えると、疑似クロージャをクラスで作ったり特殊なプリプロセッサを使ったりしなくても、 クロージャに閉じこめたいものが文字列化&&文字列からの復元可能なオブジェクトなら、create_function 一つで そのオブジェクトを捉えることができます。

で、create_function は何か謎の無名関数オブジェクトを返す関数ではなく、 「謎の無名関数オブジェクトを作って、それに他とかぶらない名前をつけて、その名前を文字列で返す」関数なのです。 つまり create_function の返値は文字列化&&文字列からの復元が可能! ただし "\0lambda_1" みたいな名前なので一度 addslashes してやらないと大変なことになるのでした。

まとめ

lambda やクロージャを使って何ができるかやってみるのも楽しいけれど、 時には、逆に、lambdaやクロージャは何と何を使ってできてるのか、とか、何と何があれば lambdaやクロージャがどのくらいのレベルまで実現できるのか、を考えてみるのも楽しいこともあるかも。 役には立つかどうかは人によるような気がする。

そういう風に「○○は何と何があればできるのか?」を突き詰めてった一つの究極が …… 「ループって再帰で書けるよね」 「名前付き関数っていらないよね。無名関数だけでいい。」 「再帰もYコンビネータがあればいいしね。」 「自然数ってChurch Encodingすればこれも無名関数で書けるよね。」 「booleanとif文も全部関数だけで実現できちゃった。」 …… λ計算

で、もう一つの究極が …… 「要はどんなオブジェクトも文字列化できる言語なら、create_functionみたいなの さえあればクロージャ要らんよね。」「全部文字列でいい。」「クラスオブジェクトとかもJSONとかみたいなので なんか文字列になるよきっと。」「関数も全部"関数本体のソース"っていう文字列で表すことにしちゃえ。」 「つまり文字列操作さえできれば他全部要らない」「文字列操作っつーか、一文字ずつ読んで隣の文字の処理に 移って…みたいな一文字ずつの処理さえあれば実はおk」 …… チューリングマシン

だったりもする。

12:01 08/01/28

CodeCraft

結局夜中の12時まで研究室に残って参加してたり。 結果 は3問しか解けなかった大惨敗。むー。 しっかしランク見るとほとんどの人が Score<Penaltiy でなんだか凄いな。

解けたの

Q1 は降順ソートして 1 と 2 と 3 にちょっと気をつけるだけ…なんだけど 1 だけは複数来る場合があるという条件を見落としててペナルティ食らいまくり。 絶対こんな条件最初なかったって! 1 と shall の間にスペース無い辺り怪しいって! ←言い訳

Q4 は普通にDPなんだけど mod 1000000007 をどのタイミングで取ればいいのか混乱して適当なのをsubmitしたらペナルティ食らいまくり。 まあ真面目に安全側に倒して書いたら通った。

Q10癒し系問題。

解けなかったの

Q2Q7 は問題の意味がよくわかってない。

Q5 は一筆書きのやり方が何通りあるか数えろ問題。 Q8 もグラフ。Q8辺りは最後まで粘ってちゃんとやれば解けた気もする。が、気力がなかったあとで考える。

Q6 は Nimだ!Nimになるやつだ! というか K=1 ならNimそのものだ! と思ったはいいものの還元方法がわからんかったです。こういうのに慣れてる人には簡単なんだろうなあと思いつつ。 うーむ実力不足。反省。

Q3 も 凄く綺麗な問題だし解けてる人多いしきっと定石があるんじゃないかと思う。 とりあえず駄目元でkd-treeで長方形内の木を全列挙してみるコード書いて送ってみたけど当然ながらTLE。 ちょっと知識不足がひどい。

Q9 は K≦10^9 という条件を見ずに O(K) 時間のDPを書いて送ったら当然ながらTLE。メモリ消費だけ定数に抑えようねという問題かと思ったんだよう。 問題文はちゃんと読みましょう。これ O(√K) とか O(log K) とかで解けたりするの?うおお全然わからん。

とりあえず

Q3 と Q6 と Q9 が面白いと思うのでみんな挑戦するといいよ!

12:47 08/01/26

The 1st Futamura Projection

Python 高速化ライブラリ Psyco や、 その発展版であるところの Python による Python 実装 PyPy について最近詳しく調べてまして、こいつら、実は自分が今まで思っていたよりずっと超格好いい代物 なのではないか、と気づき始めました。そのお話。

Specialization

プログラムの最適化の一種(というと語弊があるかもしれませんが)、 "Specialization"("Partial Evaluation" ともいう)というのがあって、例えば

function keisan(x, y) { return (x-1)*(y-2) + (x-3)*(y-4) }

という関数があるんだけど、実はプログラム中で keisan(3, ...) みたいに第一引数が定数 3 で呼ばれている ことが非常に多い!などというときに、xを3に固定した特殊化バージョンを作って keisan(3, ...) をそっちに 置き換えちゃう

function keisan_x3(y) { return 2*(y-2) }

というのが Specialization の一番簡単なケースです。

ところで、Specialization を使うと インタプリタを使ってコンパイルができる (住井さんの記事) という面白い考え方があります。 Specialize(keisan,3)==keisan_x3 であると同時に Specialize(eval,source)==compiled_source である、という。 (さらに話を進めて、Specialize処理自体も関数と考えると、 Specialize関数をevalに特殊化すると Specialize(Specialize,eval) == compile コンパイラになったり、もう一段話を進めると Specializer だけから Specialize(Specialize, Specialize) == generate_compiler_from_eval コンパイラコンパイラが出てくるという楽しい世界がありますがそれはまた別のお話…)

PyPy

この Specialize(eval, source) == compiled_source という等式、 実に魅力的なんですが自分の中ではいまいち現実味がありませんでした。 握力×体重×スピード=破壊力 みたいなもんかと。というのは、論文やアカデミックな世界で閉じてる実装くらいでしかこの式を 見たことがなかったので。

ところがどうも、調べてみると PyPy はまさにこれをやっている。 RPython という制限付き Python で書かれた Python インタプリタを、実行時に 渡されたソースに Specialize することでコンパイルして実行している。 Python に限らず Prolog でも JavaScript でも RPython でインタプリタを書けば、 あとは同じ Specializer を使ってコンパイルすることができている。 Psyco も、完全にピタリその式に収まる形ではないですが、あれも中身を見ると JIT コンパイラである以前に Specializer として作られている。

これは凄い。 Psyco は日常的に使っていて、実際高い効果があると言うことも体感して知っていました。 まさか、"現実味がないと思っていた" 概念が既に目の前で繰り広げられていたとは。 毎日隣の席に座ってた人が実は花山薫だった級の驚きですよこれは。すげーすげー。

参考資料

[スライド,PDF] PyPy: Making the Dream of Partial Evaluation Come True in Practice

シェル

シェルを作る課題、システムコールだけで、 という話題を見てていつも思い出されるのが、シェルの対話ループを for 文でも while 文でも関数の再帰呼び出しですらなく、execve(自分) で実現してた 某友人のコードなのであった。あれを見てはじめて末尾再帰≒ループ、の意味が理解できたよ。

14:27 08/01/22

ふたたび

シドニーにいます。 勝手に Haskell Hackathon のオセアニア会場作っていいですかっ…て、あ、WebCam ない。

postfix to infix

postfix to infix ネタバレ期間になったのでネタバレ。

とりあえず頭にあったのが、 「ボトムアップに性質が定まる木が前置記法で渡された場合、後ろから読んでみるといいかも」 という tanakhさんの卓見 です。 同じ考えで、トップダウンに性質が定まる(ある部分式を括弧でくくる必要があるかないかは"親の"演算子に よって決まる)木が後置記法で渡された場合も、後ろから読んだ方が綺麗に行くだろう、と。 後ろから読むと問題が prefix to infix に早変わりするので、あとは素直に再帰下降で。

括弧の要不要判定は最初の頃は "//*--+ /+ /- *+" [p+c] とかそんなんで地道にやってたんですけど、途中で +-*/ を 0123 に変換すればOKなことに気づいて今の最終形に。 ただ、一番素直な "+-*/".index$& より短くなるビット演算がなかなか出てこなかった。 19 & 86%$&[0] の前は確か 53 .% $&[0]^46 とか。

22:37 08/01/17

AirCraft

1/20 の便が取れたらしい。

CodeCraft

CodeCraft '08 っていうコンテストの宣伝メールが来てました。 多分 Uva に登録したアドレスに来たのかな。 暇があったらやってみようかと思ったんですけど、1/27 って多分まだ家にネットがないような気がする。無念。電話するのめんどいなどと言って 12月中に手続きしてこなかったツケがここに。

18:44 08/01/15

ビザ

キタ━━━━━━(゚∀゚)━━━━━━ !!!!!

けど今度はこの季節全然飛行機の席がない。

最短経路の本

id:ranha さんのとこで シュプリンガーの最短経路の本を筑波大学内書店で買いました という記述を見かけて、 「グラフ理論の本とかじゃなくて最短経路にテーマ絞って一冊書いちゃった人がいるのか!なんだその 面白そうなマニアックそうな本は!!!」と思って調べてみたら

 → 最短経路の本 / レナのふしぎな数学の旅

まんまそういうタイトルの本なのですね。これはやられた。早速今日読んでみました。

実際は、Dijkstra と Bellman-Ford と Warshall-Floyd から始めて延々と最短路問題を 扱いまくる本…というわけではなく、とてもわかりやすく書かれたグラフ理論の入門書でした。 数学ガールのグラフ版みたいな。グラフガール?

で、感想ですが… 今日からは、「グラフの勉強したいんだけどいい資料ない?」と聞かれたら迷うことなく この本をすすめることができます。むしろグラフの勉強したくない人でも面白いからちょっと読めと 無理矢理すすめたくなってきましたよ。

概要に書かれているとおりに、ややこしい数式を出したりせずに物語の中で色々なアルゴリズムが 解説されていくわけですが、そこで"なんとなくのイメージ"を伝えるだけの解説に逃げずに、きっちり 細かいところまでそれぞれのアルゴリズムの意味を説明しきっているのが特に凄いと思いました。 例えば Dijkstra 法がどういうアイデア/直感に基づいていて、それに基づいてアルゴリズムを 考えると具体的にどんな手順になって、それがどうして正しく最短経路を求められるのか、というのが ちゃんと登場人物の対話となっているという。ここまで書いてある本は逆に教科書なんかでも少ないのでは ないでしょうか。すごいすごい。 というかむしろ、数学ガール的なスタイルの方が、お堅い書き方よりも、 理論やなにかの「気分」「感覚」まで含めて伝えるのには適しているのかもしれませんね。

量的にも、自分が大学3年のときにうけたグラフ理論の授業とちょうど同じくらいの範囲を扱っている感じで、 つまりこれ一冊読めばひととおり基礎は押さえられると思います。おすすめおすすめ。

16:51 08/01/12

memo: POPL 3

POPL 2008 の 面白かった発表めも最終日。たぶん論文名でググればPDFが見つかるものが多いと思います。

"Clowns to the Left of Me, Jokers to the Right"。昔から勝手に大ファンの Conor McBright 氏の発表なのです。Zipper はコンテナの中を行ったり来たりしながら 1個1個順番に操作を加えるデータ構造だけど、コンテナの要素の型は変えない。この論文では、 コンテナの要素を別の型に置き換えていく操作に一般化したZipperみたいなものを与えています。 …ってわかりにくいな。map をステップバイステップでできるようにしたのが Zipper だとすれば、 今度のは fold をステップバイステップでできるようにしたもの、というか。 そしてあるコンテナのZipperは、そのコンテナの型を微分!すれば 自動的に得られるのに対し、今度のは型に対するDissectionという操作で自動的に得られる。

"Extensible Encoding of Type Hierarchies"。 多重継承対応かつインクリメンタルな、クラスの継承関係を効率的に判定する方法 "ESE"。 既存手法も色々おもしろい(→前まとめた記事)けどこれも面白い。 方法としては、クラスの集合をできるだけ少ない個数の "Straight Slice" の集合に適当に分割する、 というもの。Straight Slice とはクラスのリストで「リスト内で ..., classA, ..., classB, ..., classC, ... の順にクラスが並んでたらclassAの派生クラスかつclassCの派生クラスなクラスは全てclassBの派生クラスでもある」 ようなもの。こうすると、任意のクラス c について、「cの先祖」は必ず各Straight Slice内で連続して並ぶ ようになる。なるので、その範囲を覚えておけば先祖判定が少ない手間でできるようになる。 新しいクラスを追加するときには、可能な限り親と同じスライスの親の隣に置くようにする、という感じで PQ Encodingとかより局所的な手間で追加もできる。 (※追記:比較対象の DSTの論文 (リンク先PDF) 読んでみたら、もうこっから Straight Slice に基づく手法なのか。なるほど。 このスライスの格納の仕方が違うと言うことかな)

"The Design and the Implementation of Typed Scheme"。PLT Scheme に #lang typed-scheme を実装。 元々PLT Schemeにcontractのシステムがあるので、untyped scheme からは typed scheme で書かれた モジュールの型は contract として見えるようにしてあるというのが、へーと思った。 "型" は例えば (define-type-alias Complex (∪ Number (cons Number Number))) こんなんで、Number か NumberとNumberのペア、だけが入ることを期待することを表現したりできる。 データを表現するS式の構造を型とする感じだろうか。 あと厄介なのが同じ変数に、場所によって違う型をつけなきゃいけないパターン (lambda (x : (∪ Number Boolean)) (if (number? x) (+ x 1) (not x))) で、これをやる既存の型システムはなかなかないと。number? のような述語の判定がどうなるかtrue/falseまで 型判定に含めておいてif式で分岐するところで別の環境を使えるようにするシステムになってるみたい?

他に、知識不足で全然わからなかったのだけど "Foundations for Structured Programming with GADT"。 GADT も何かのファンクタの始代数になってることのconstructiveな証明、という理解でいいのかな。 酒井さん辺りが詳しそうだ。 この発表のあと昼食やコーヒー休憩のときに周りで Kan extension について語ってる人が急増してた感じが。 あと他には、招待講演の "Caml Trading" で「他の言語機能はまだともかく、Algebraic Data Type がない言語はそれだけで死ねる」って趣旨のことをおっしゃってて、256% 同意 なのであった。いわゆる"関数型言語"の機能のうち最強のものだけが主流の言語の 機能にならずに残ってる、というのはほんと不思議。closure入れるより先にやることが あるだろう…って全然講演関係ないぞ俺。

とまあ、そんな感じでした。 正確で網羅的なまとめは 住井さんのメモ をどうぞ!

16:47 08/01/11

memo: POPL 2

POPL 2008 の 面白かった発表めも二日目。たぶん論文名でググればPDFが見つかるものが多いと思います。

"Subcubic Algorithm for Recursive State Machines"。 「辺にラベルのついた有向グラフG と 文脈自由言語L が与えられたときに、 Gの全点間到達可能性を判定せよ。 ただし、通る辺のラベルの列がLに入るようなパスで到達できる時のみ到達可能であるとする」 ていう問題を解くアルゴリズムは従来法ではGの頂点数nに関してO(n3)だったんだけど O(n3/log n)にしたよ、というもの。これは著者曰く2+2=4 くらい簡単な成果で、 よく知られているらしい word trick という技を使っただけ、と。メインの成果はさらにLにある制約を課すと O(n3/(log n)2) にできるという結果らしい。 ICPCやTopCoder界隈の人はO(n3)アルゴリズムから考えてみると面白いんじゃないかと。 私この word trick ていうの知らなかったので、その簡単な方の話に感心してしまいました。 word trick :: 「n以下の自然数の集合をbitvectorで表すと、普通にやるとunionやintersecitionの計算時間は O(n) になる。ただしここで、bitvector を (log n)/2 ビット毎のブロックに区切って、(log n)/2 ビットの ビット演算が定数時間でできることを仮定すると、計算時間は O(n / log n) でよい。 そりゃ実際log n/2 <= 64ならビット演算一命令で済むかもしれないけど一般的には無理だろそれ /log n って 言わないだろ、と思ったらどうするか。 ビット演算の結果を全部テーブルに前計算して覚えておけばいい。p=(log n)/2 ビット同士 の2項演算は全部合わせても 2p*2p = O(n) 通りしかない。 n2 回 O(n) の集合演算をするので O(n3) かかっていたアルゴリズムも、 この手を使えばあら不思議 O(n log n) + n2*O(n/log n) = O(n3/log n) に」 (※追記:やっぱこの議論は怪しいな。ダメ。これだけだと最終的な出力がnビットである以上 n/log n にならない。 論文の方ではさらに計算結果から集合の実態を取り出すのにビット列のMSBの計算が必要でそれもpビットまで 定数時間で引けるようにしておくと、結果計算量がO(n/log n+出力サイズ)になるので以下略、みたいに議論を 進めてたのでそこまでやるとうまく行くんだろう。log n/2のチャンクに分ければチャンク毎の演算表はサイズnでOK、 って考え方をしたことがなかったのですげーと思ったのだけどこれは下手に使うと間違えそうだ。)

"Automatic Inference of Stationary Fields: a Generalization of Java's Final Fields"。 stationary field という概念を提唱。定義は「オブジェクトの初期化処理中は読んだり書いたりされるけど、 初期化が済んだらもう変化しない、読み取り専用で使われるフィールド」。「初期化処理中」の捉え方が面白いところで この論文では、「オブジェクトが生成されてから、他のオブジェクトから参照されるようになるまで」を 初期化処理とみなしている。final のような、ほぼ「コンストラクタの中」っぽい定義と違う。 「引数なしのコンストラクタを呼ぶFactoryMethodで一旦フィールド未初期化のままオブジェクトを作って、 setterでひととおりフィールドに値を設定してから使い始める」みたいなパターンも、そのフィールドが 後の実行で書き換えられないなら実際上はfinalみたいなもんであって、こういうのをstationary fieldの定義なら 捉えることができる、という。findbugsとかazureusとかjeditとか色々なプロジェクトのソースをかき集めて 実験してみたところ、final な使われ方をされてるフィールドが全体の10%強だったのに対して、 stationary な使われ方をされてるフィールドは実に全体の50%にもなったという調査結果。

"Demand-Driven Alias Analysis for C"。Cのプログラムの2つの別のポインタ変数が同じ領域を指す (aliasing) 可能性があるか静的に解析するアルゴリズム。最近のこの分野では、ポインタの指しうる アドレスの集合(points-to set)を計算する解析が主流で、それを使えばintersectionが空かどうかで alias解析もできるよーという流れだったんだけど、この論文は直接aliasingだけを解析することで 高効率なアルゴリズムを実現、ということみたい。SPEC2000 Benchmarkのソースを時間0.5msメモリ65KBで 96%の精度でalias解析できたという実験結果が書いてある。かなり物凄いような気がするけれども この分野については門外漢もいいとこなのでよくわからない。 よくわからないのになんでここで触れているかというと、points-to/alias解析は↑↑のテーマだった グラフ上の文脈自由言語による到達可能性を使って計算するのがスタンダードなのですね。 朝知った知識が昼早速でてきて楽しいなあという。

22:13 08/01/10

memo: POPL 1

POPL 2008 の 面白かった発表めも一日目。たぶん論文名でググればPDFが見つかるものが多いと思います。 あと自分は Separation Logic という単語を聞くと眠くなる体質はどうにかした方がいいです。

"Much Ado about Two"。 「型に依存しない形で書かれているソートアルゴリズムの正しさを証明するには、 そのアルゴリズムが bool のリストを全て正しくソートできることさえ証明すればよい」 という有名な原理があります。この論文では、 「結合則を満たす演算子に対してscanl1を計算するアルゴリズム(※:結合則を満たすという前提があるとscanlは並列化可能になるので、 色々な並列化戦略がありうるのです)の正しさを証明するには、0 か 1 か 2 しか入ってないリストのscanlを 正しく計算できることさえ証明すればよい」ことを証明。 (正確には、特定の順で0,1,2が並んだリストと特定の2種類の演算に関するscanl1での証明だけすればOK、というもの) ソートの場合は bool = 0, 1 だったけど、こっちの場合はちょっと 2 が増えてます。 "具体例が一般的な正しさを保証する" という原理の根本は Parametricity から導き、要は結合的演算の適用される計算木の構造が scanl1 として正しいかを検証すればいいんだけど その木構造のチェックは3ステートのツリーオートマトンで可能という観察から、0, 1, 2 の三値で行ける という結論に辿り着く。おもしろい!

"A Logical Account of PSPACE"。λ計算+bool型+if式、という言語に対する STAB という型システム。 この型システムでちゃんと型がつくプログラムは PSPACE で計算できるし、逆に、PSPACE で解ける問題は すべてこの言語の型チェックを通す形で解ける、というもの。型システムは線形型(Linear Type)を使ったもので、 ちゃんと理解できてないですけど、!の導入則からして、これで型がつくプログラムというのはほぼ「入力データだけは 何回でも使っていいけれど、途中のテンポラリなデータは全て1個1回しか使わない(何回も必要なデータは 何回も計算し直すべし)」ようなプログラムになっているような気がする。ただ、if文の条件式で使ったデータをbodyで もう一度使う、というパターンだけは許されているような。

"Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures"。 純粋関数型データ構造の計算量評価をするためのライブラリ。遅延評価のサンクが作られるところに 手で "tick" ていう注釈(…実態はただの恒等関数)を入れていくと、それぞれのサンクに "あとnステップ評価すると実際の値が手に入るサンク" みたいな型が Dependent Type としてつくように作られてる。 償却計算量の評価のためにコストを負わせる箇所に挟み込む "pay" という注釈も合わせたりして、 型を使って、意図した計算量になってるかをチェックできる感じ。 ちょっと実際使ってないとどんな感じかいまいちわからんですけど楽しげです。

23:11 08/01/09

memo: Coq

例えば「以下に引用する、85年に発表されたこれこれの補題は重要であり この論文でも何度か使うので覚えておいてね」みたいなことを書いてからその補題を 書き写したりしていて。例えばPreliminariesと言ってお決まりの用語定義を並べていて。 …このコピペしてる感はよくないなあ、と常に感じるのが、最近本気で定理証明支援系を 使えるようになりたい私の理由であったりします。 仮にもコンピュータ科学の研究者が コード == 定理・証明 をコピペってどうなのよ、みたいな。 automathとかそういうレベルの話しでなくて、自分で前書いた証明を自分で個人的に いじって考えるときくらいは#includeじゃなくてimportしたい。

というわけで行ってきた Coqのチュートリアル なんですけど、全俺の予想通り発表の準備してたり体調最悪でそもそも 午前中欠席してたりでしっかり聴けていないというのが実情です。はい。 住井さんのまとめ にリンクしておく。

これのあと中野さんに、 一度Tree Transducerの議論をCoqでやろうとしてRanked Treeの表現の時点ですでに大変だった、 というお話を聞きました。チュートリアルで使った変数束縛の表現方式も、翌々日のPOPLで発表されるくらい non-trivialなテクニックなんですよね。そういう、なんというか、「証明を表現するデータ構造」みたいなものを 今まさにみんなで整備しているような段階なのかなーと思いました。なんという適当な感想。

19:25 08/01/03

あけました

おめでとうございます。

さっきまで "生物と無生物のあいだ" を読んでました。で、中身はまあそこそこ普通に面白かったんですけど、むしろ本文よりも エピローグにびっくり。著者の方が住んでた宿舎って自分が高校の頃まで住んでたところだ。 通ってた小学校 も一緒。知らんかった。エピローグに書かれている場所もどこもかしこも懐かしい。

How is it designed?

なにかしらプログラミング言語の標準ライブラリ/APIが、どういう方針どういう根拠で設計されているか、 逐一記したような文書ってどこかにありませんかね。

具体例で行きましょう。ストリーム入出力ライブラリのAPI設計。 自分の考えでは、言語側の文字コードが固定されているなら Java API などなどのように、「バイナリIO(InputStream/OutputStream)とテキストIO(Reader/Writer)を 完全に別のレイヤとして分ける」 べきである、のですが、これについてどの程度 過去に考察がなされているのかが知りたい。例えば、このようにレイヤを分けるとテキストとバイナリが 混在したストリームを読み出すのが難しくなる(と思われる。実際Javaの InputStreamReaderは読み込み操作を満たすのに丁度必要な量よりも多くバイナリストリームを 消費しちゃってよいことになっている)けれども、こういう混在読み込みをあっさりあきらめてよいものか。 良いとしたらそれは何故か、みたいなことが延々と綴ってあるドキュメントがあったら読んでみたい。

Boost の Formal Review や Python の PEP はたぶんかなり求めている物に近いのですけど、 できればもっと基本的な部分のライブラリ設計について知りたい。

presented by k.inaba (kiki .a.t. kmonos.net) under CC0