研究グループの内輪の研究会がありまして，ET プログラムの自動デバッギングの話が面白かったです．

(人間が頭で考えて，直接ルール (プログラム) を手書きした場合用．また，原理的に，形式的仕様記述から自動生成されたプログラムは，仕様に対しては 100 % バグが無いわけですが，それとは別のレイヤーとして，生成されたプログラムが「人間の直感的意図 (ここはインフォーマル)」と異なる挙動を示した時には，仕様のデバッグが必要になってくるので，さらに高度な研究が必要になってくる)

その研究自体の詳細は (私の研究ではないので) 書けないのですが．既存研究との比較として挙げられていた，サーベイペーパーが，これまた興味深かったです．

Josep Silva, "A Comparative Study of Algorithmic Debugging Strategies", 2007

論理プログラムや関数プログラムのアルゴリズミックデバッギングという研究領域は，1982 年 shapiro 以来，比較的長い歴史があるようです．

(発祥となった Logic Programming の分野は，そもそも理論的バックグラウンドが怪しいので，それほど成果は出なかったのですが (例えば，あまりにも有名ですが，cut が入ったプログラムは，もうどうしようも無い．また，仕様とプログラムの区別も曖昧で，扱える空間が狭い))

通常 「デバッグ」 と言った場合には，人間が直感的に怪しそうな場所に printf を入れて出力を見たり，デバッガでステップ実行したりしてバグを探すわけで，2分探索で怪しいコードを絞り込んでいくようなことも，経験的に行われてきたわけですが．

アルゴリズミックデバッギングというのは，そこらへんのバグの絞込みと発見を，もう少し系統的にできないか ? というモチベーションで始まったものだと思います (まだちゃんと論文読んで無い) プログラムを実行し，実行木 (証明木) の全ての部分木において，その正しさに対して人間がオラクルをアルゴリズミックデバッガに与えてやり，バグを絞り込んでいきます．この時，いかに人間の判断 (質問回数) を減らし，怪しさ (依存関係) を検出し，効率的にバグを追い詰めていくか，というところで，いろいろな戦略 (Algorithmic Debugging Strategies) が存在するよ，という論文です．

プログラムコード片の正しさが検証しやすい宣言的プログラムの場合に特に有効ですが，命令型プログラムでのアルゴリズミックデバッギングの研究もけっこうあるようです (命令型プログラムの場合は，正しさの根拠となる理論が無いので，より直感的な作業になってしまいますが)．

面白くて，かつ比較的すぐ有用になりそうな研究なのに，あんまりネット上で触れられることが無い気がしたので，メモしておきます．こういう研究がもっと広まって，プログラミングが根性主義の肉体労働ではなく，真に知的な創造的行為に進化して欲しいなぁとしみじみ思います．

---

あるときは計算量学者，またある時はさすらいの変態 sed-er として名高い

/* Background Knowledge

    sed でチューリングマシン
    偉大なる変態 sed ハッカーたち (Great sed-er)
    wo さんの偉業 (BASIC compiler in sed)
    shinichiro_h さんの sed VM 論 (sed considered VM)
    shinh - sed
    sed のことしか考えられなくなってしまった shinh さん (brainf**k assembler in sed)
    素晴らしきマゾプログラミングの世界 (What a wonderful Maso-Programming World)
*/

シンXさんに，mixi で面白いコメントをいただきました (転載許可快諾済み）

コメント

2007年03月08日 17:35 あろは

全然関係無いですが，最近ブログ界隈の方で微妙に計算の複雑性の理論が話題になっていたのですが

http://www.kmonos.net/wlog/70.html#_2111070226

検索してたら「倉庫番はPSPACE完全」 という記述が sin-x で見つかったという収穫がありました

2007年03月08日 19:50 シンＸ

最近引っ越してから面倒くさくてアンテナ稼動をさせていないため、Web 日記界隈の流行がわからなくなりつつありますが、計算量の話が話題になってたんですね。

倉庫版の PSPACE 完全性は、確か5年ぐらい前にはわかってますね(←調べない奴)。一般化ぷよぷよとかテトリスも NP 困難、いや完全だったかな?

「『飛び出す絵本』を開く問題」も、読者が開くときに角度を付けながら開ける作業が NP 困難になるような本を作ることができて、もしかしたら PSPACE 困難まで言える(あるいは言ってる)かもしれません。本は紙面が限られているので、Turing 完全ではないですが、1ページ開くのに数億年かかっちゃうかもしれない、幼児泣かせの本は作れます。

2007年03月08日 23:04 あろは

おお，面白そうな話題．このコメントの一部 (計算量の部分) をブログのネタにしてもかまいませんかね ?

飛び出す絵本を開く問題，ちょっと検索してみたのですが，なかなかヒットしませんでした．英語での検索キーワードや論文リソースなどを教えていただければ幸いです

2007年03月09日 11:37 シンＸ

どうぞどうぞ、ネタにしてください。

飛び出す絵本の計算量についての論文は、JAIST の上原さん(エルデシュ数2保持者)の業績ページの“The complexity of a Pop-up book”です:

　http://www.jaist.ac.jp/~uehara/pub/tech.html

ついでに、この文献でも取り上げている「折り紙」の研究「も」している天才 Erik Demaine のページへの URL も紹介しましょう:

　http://theory.csail.mit.edu/~edemaine/

彼がどれほど凄いのかについては、Wikipedia を見れば明らかです:

　http://en.wikipedia.org/wiki/Erik_Demaine

12 歳で大学に入り，20 歳で MIT の教授という… っ ！ 一口にコンピュータサイエンスと言っても，やはり純粋数学に近付けば近付くほど，圧倒的な力量差が開いていくのですなぁ．凡人は生き残れない世界ですよ．
プログラミングなんてのは限りなくバッドノウハウに近い工学だから，経験や知識量がモノをいう世界だけど．

pop-up book の論文など，わずか 4 ページです．ここらへんの簡潔さが，いかにも数学の論文っぽくてカッコいい．

そんなこんなで，エルデシュ数の世界 で何が行われているのか，ってのはなかなか表に出てこない感じがするのですが，いろいろおもしろそうな世界の一端を垣間見た気がしたので，この感動を皆さんにも ！ という GIGAZINE 的紹介記事でした （僕には論文の中身や研究者の業績を解説できる力量はありませぬ）．

---

Gofer というのは Haskell の前身で，

• 純粋関数型言語


• 多相型システム


• 型クラス


• 型推論


• overloading


• 遅延評価

など，一通りのものが揃っている，比較的コンパクトな言語処理系のようです．

この Mark P. Jones の論文

The implementation of the Gofer functional programming system (1994)

では，Gofer システムの実装を丁寧に解説しているようです (まだアブストしか読んでない)．

12 年前とかなり古いのですが，純粋遅延関数型言語のコンパイラの貴重な資料だと思います．

C で書かれてるってのは，いろいろ微妙なところですが．

これは，当時の事情 (まだ MS-DOS の時代) を考えるとしかたがないでしょう．また，Turbo-C でコンパイルが通るように工夫してあるなど，いろいろと気を配って DOS と一般的な IBM PC で実行できるようにしてあるようです．

もしかして，配ってあるバイナリ i386 以上の DOS 環境ならば，今でも動くのかな ? (微妙) DJGPP (GNU C for DOS) とかいう謎のコンパイラでコンパイルしてあるみたいなんだけど，DOS エミュレータか何かで．

ちなみに，ソースコードは現在でも入手可能のようです．なかなか時代を感じますが．

Mark P. Jones : Gofer archive

gofer230a.tar.gz (zip もある) というのに，サンプルコードまでフルセットで入ってます．

ちなみに，今大学なので，ためしに cygwin で試してみたら，まず cc が無いよ ! と怒られ (基本)

src/Makefile を開いてみたら，非常に素朴なものだったので，テキトーに CC=gcc とか書き換えて，再び挑戦．

$ make
gcc -c -O gofer.c
In file included from gofer.c:22:
machdep.c:12:23: sys/ioctl.h: No such file or directory
machdep.c:292:19: sgtty.h: No such file or directory
In file included from gofer.c:22:
machdep.c: In function `normalTerminal':
machdep.c:318: error: `TIOCSETP' undeclared (first use in this function)
machdep.c:318: error: (Each undeclared identifier is reported only once
machdep.c:318: error: for each function it appears in.)
machdep.c: In function `noechoTerminal':
machdep.c:322: error: storage size of 'settings' isn't known
machdep.c:325: error: `TIOCGETP' undeclared (first use in this function)
machdep.c:329: error: `CBREAK' undeclared (first use in this function)
machdep.c:329: error: `ECHO' undeclared (first use in this function)
machdep.c:330: error: `TIOCSETP' undeclared (first use in this function)
gofer.c: In function `main':
gofer.c:73: warning: return type of 'main' is not `int'
gofer.c: At top level:
machdep.c:314: error: storage size of `originalSettings' isn't known
make: *** [gofer.o] Error 1

あらら．

ioctl.h はまだしも，sgtty.h という謎のヘッダが必要で無理っぽかったです．

sgtty って… 時代を感じる．ソース K&R C だし．

あと，他にも GNU readline が必要っぽい．

こういう古き良き時代のソースを見てると，autotools って意味あるんだろうか ? とか，いろいろ諸行無常な気分に．

まぁ，短期的には有用なのは間違い無いんだけど，10 年とか経ったら，普通，当時の環境なんてどこにも残ってないだろうし，そういうのは，いくら autotools でがんばったとしても，どうしようもないよね．

いや，ま，別に autotools が悪いわけじゃなくて，何をしたってどうしようも無いんだけど．Makefile がこれくらい素朴だと，ちょっとがんばればポートできるかも．という気にもなるよね．

思いっきり autotoolize されてて巨大なコードとかだと，どうしようもないよなぁと．

とか思っていたら，青木さんは Linux でコンパイルに成功していたらしい．

青木日記/T (2002-08-31) ■ Gofer

Linux でコンパイルも通ったー。やっぱり Linux だと古いプログラムはことごとく端末まわりで失敗するな。

しっかし，4 年半も前の記述だしなぁ．あと青木さんのことなので， Linux と言えども一味違う環境なのかもしれない．めちゃくちゃ古い Slackware とか Redhat の 4.x とか (偏見)

とりあえず Makefile を見る限り，コンパイルが成功すると，gofer gofc runtime.o という 3 つのバイナリが出力されるらしい．

たぶん，gofer がインタプリタで，gofc がコンパイラ．C コードを吐いて，それを C コンパイラでコンパイルして runtime.o とリンクという形になるのではないか (本当に素朴な作りだなぁ)

---

たまたま，全然違うことで検索してたら見つけた修士論文．

逐次型戦略に基づくTRSコンパイラの構築, 関 康夫, 1997年2月14日, 北陸先端科学技術大学院大学 外山研 修士論文

研究の方向性は，もちろん全然違うんですが．
コンパイラ関係の修士論文は，だいたいこういう風に書けば良いのかな ? という点で個人的に参考になりそうな気がしたのでメモ．

講義も (単位がちゃんと取れていれば) 全て終わり，僕もそろそろ修士論文を意識しつつ，真面目に研究を進めて行かなければならない時期にきたような気がするので (口だけ)．

項書き換え系 (Term Rewriting System ; TRS) ってのは，関数型言語と呼ばれるようなλ計算に基づくプログラミング言語の実行モデルのこと (だと思う)．

んで具体的には，その名の通り，

l → r

みたいな書き換えルール (Rewriting Rule) の集合こと．

んで，ルールにそって，マッチした左の項の中の簡約できる部分 (リデックス) をひたすらできるとこまで書き換えていく．んで，止まった時の項が，正規型とか呼ばれて，これがいわゆる関数の値ってやつに相当する (と思う)．

その他にも，TRS には，論理型言語の本質的な実行メカニズム (Selective Linear resolution for Definite clauses，いわゆる SLD-resolution) のモデル化 (SLD は，上から下へ「選択」，左から右へ 「線形」に「導出」を行う，つまり，確定節 (項 :- 項1，項2, .... の形の論理式) を項書き換えしてると見ることもできる) にも応用できたり，という面白い性質がある．

つまり，TRS は，関数型言語と論理型言語の (もともとの各パラダイムの理論的背景にはともかく，現実の計算機の上での実装手段として見ると) 共通の実行メカニズムであって，両者を関数論理型言語として一つにまとめることができる．

Functional Logic Languages: Basic Concepts and Operational Semantics

(via narrowingとresiduation)

全然関係無いけど，m-a-o さんもカレー好きと発覚．そういえば mmatsuoka さんもカレー好きということで，名前が m で始まる人はカレー好きなのではないかという仮説が (あるある大辞典もびっくり)

しっかし，m で始まる人って，他に誰かいたかな…

あ，msakai (SAKAI masahiro) さんとか (強引)
あと，sumim (SUMI masato) さんとか ｗ (ムリヤリだなぁ)

そもそも，カレーが嫌いな日本人って，あんまりいないような．まぁどうでもよろ．

何の話だっけ…

とにかく，TRS のコンパイラは大事だよ〜と．TRS の実装に関してはほとんど知識が無かったので，いろいろ面白かった．ナイーブにリデックス探して，ルールディスパッチして… なんてやってられるわけないので，FB インデックスオートマトンとやらを埋め込んだ C コードに落とすらしい．なるほど ！

FB というクラスの TRS ならば，効率的にコンパイルできて，なおかつ停止性や合流性が保証されてワンダフルらしいんだけど，あんまり最適化まではがんばって無いから，さすがに既存のコンパイラには負ける (gofer には勝つ ?) らしい (Future Work)．

項は木構造になっていて，ひたすらポインタを張り代えて行くことで簡約を行っていく．いわゆるグラフ書き換えってやつ．

もともとは高水準な関数型言語の，中水準の中間言語を意図して作られたらしい CLEAN なんかは，これを直接的に言語の意味論の組み込んでいたような ? Curry とか Haskell とかが，実際はどういう実装になっているのかは全然知らないけど．

書き換えの際のリデックスの選び方によって，いろいろな簡約戦略が生まれるわけで，ML とか ※ は，たぶん最内簡約とかで，これを最左最外簡約とかにすると，いわゆる遅延評価というやつになる (はず)．

※ まぁ，最内簡約だと，普通の手続き型言語の実行メカニズムとほとんど同じだから，馬鹿正直に項書き換え系で実装したりはしないだろうけど．

んで，グラフ書き換えだから，一度簡約したやつは二度と最計算されないことが保証される．これがいわゆる必要呼びとか，怠惰評価とか呼ばれるやつだったような．

あんまり本質じゃないけど，何でもカンデモ本当に項で内部表現しているのが面白かった．テストプログラムの fib とか fact とか典型的なやつで，整数を s(s(s(.....s(0) ....))) とかいう形にエンコードして項書き換えしているらしい．リストを使う reverse とか quick sort とかは Cons(hoge, Cons(foo, (...))) という形にエンコードされているらしい．ふむ．

これの前身となった TRS コンパイラは，けっこう自由に C コードをユーザ定義できたらしいんだけど．このコンパイラ自身はどうなのだろう．オートマトンとかを使うと，いろいろ面倒なことになりそうな気もする．

---

mkosaki さんがいた > カレー

どうでもいいけど，初めてこの fc2 のアドレスを見たとき，mk (make) os aki という意味不明な区切りかたを脳内でしばらくしていたのは秘密だ （UNIX コマンドに毒されすぎだ ！）

あと，mao という文字を見ると，中華一番を連想してしまう．

---

C 言語にフォーマルセマンティクス (操作的意味論) を与えたとかいう論文

An abstract dynamic semantics for C (1997)

を，いきなり読むのは厳しそうだったので，そもそも dynamic semantics ってなんじゃい ！ とテキトーに検索してみたら．

C 言語のための現実的なポインタ解析

という日本語の論文が見つかったので (直接的にはあんまり関係ないけど) ちょっと読んでみた．あんまりちゃんとは読んでないけど…

ポインタが，どこのメモリ領域を指すか，みたいな解析には抽象実行というテクニックを使うのが普通らしい．

Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints という論文が参考文献に挙げられているんだけど，印刷してみたらメチャクチャ読み辛い (全体的に薄い) あとけっこう難しそう．この他にも，なんかいろいろ参考文献が挙げられていて，お得感が漂う論文ですのう．

ポインタ解析は根本的に決定不能だから，精度の概念が重要になる，とか．いろいろ面白いけど，lattice (束) とかみたいな代数的構造についてはほとんど知識が無いので，lattice 使って解析します ！ とか言われても全然ピンとこないんですが… (駄目過ぎる)

要するに，lattice ってのは，任意の二要素が上限と下限を持つような順序集合らしい．

んで，メモリ領域ってのは，合法にアクセスして良い範囲ってのが明確に決まっているので，ポインタ変数や値の加減算とかは lattice を使ってモデル化するとピたっとはまるということなのでしょう．

全体的に，C 言語にフォーマルな意味論を与えるのは大変なんだなーという感じ．それなりに上手く行ってる感じなのがすごい．

しっかし，C 言語に意味論を与えて自動検証できるようになったとしても，現実の C プログラマが書くコードってのは Undefined だらけで，どうしようも無く破綻してそうな気がする．

一応，厳密には，規格上駄目でも，ほとんどのコンパイラでは期待通り動くようなイディオムは合法として解析しているらしい．明らかにナンセンスなポインタの使い方だけでも検出できれば，けっこう役には立つとは思うけど．

あと，関数ポインタを使われてるとお手上げっぽいですな．C プログラムの解析はいろいろ大変だな，と．

---