Radium Software

Home - Archive - About - RSS

移行

2008-04-20

http://d.hatena.ne.jp/KZR/ に移行しました。

正しさのコストとリスク

2007-07-18

それで,けっきょくどうすればいいんだろう?

まあ,これまでの「絶対的な正しさは存在しない」だとか,「数学的なアプローチは難しい」だとか,そういうのは深くつきつめたときの話であって,あまり深刻に考えこむ必要はないと思うんだ。ある程度の正しさだったら,それを確かめるための決まりきった手順は存在するし,数学的なアプローチだって,分野によってはそれが有効にはたらくこともある。

なんにしろ大切なのは「すべての工学的な活動は経済性にもとづいている」ということだと思う。

なにかを実現するための工学があったとして,そこから得られる利益が,それに要されるコストを下回っていたとしたら,それは工学として成立しない。これは分かるよね?

「正しさ」を確かめるにはコストがいる。だから工学としては,限りなくコストをかけて「絶対的な正しさ」を確かめるってわけにはいかない。どこかで見切りをつけないと,それは工学として成立しなくなってしまう。

他方で,「正しさ」が確かめられていなければ,そのぶん運用時のリスクが生まれる。どの程度のリスクが許容されるかっていうのは,その工学が扱う問題の種類によってことなってくる。たとえば,原子力発電所とドリンク自販機では,許容されるリスクの程度がぜんぜん違うよね。

そこで重要になってくるのが,その問題においてどの程度のリスクが許されて,どの程度の「正しさ」が確かめられているべきかっていうことを,その当事者たち,ないしは責任者が判断してコミットする――ええと,「表明を行う」ということなんだ。

そういう合意が無いと,「正しさを確かめる」っていう工程は,ただやみくもに問題の領域をさまよう作業になってしまう。結果として,風が吹くだけで壊れる原子力発電所を作ってしまったり,ミサイルが当たっても壊れない自販機を作ってしまったりしてね……。「そんなばかな!」って思うかもしれないけれど,ソフトウェアの分野によっては,その分野が若くて洗練されていないがゆえに,そういう悲劇が生じてしまうこともあるんだ。

……ああそうだ,それともうひとこと! ここから,独りで「正しさ」を確かめることの難しさも推し量ってほしい。「正しさ」が当事者たちの合意のうえにのみ成り立つものだとしたら,それを独りでどうにかしろっていう方が無理な話じゃないかな?

プログラムと一般性

2007-07-13

それじゃあ数学を真似すればいいのかな?

けっきょくはプログラムも,どこかに「絶対的な正しさ」が存在するわけじゃなくて,人と人との間のやりとりの中から「恐らくの正しさ」を見つけ出していくしかない……ううむ,それじゃあ,数学がそれをやっているのを真似すれば,プログラムも「正しさ」を確かなものにしていくことができるのかな。

「数学の真似をする」というのは,よさそうなアイデアのように感じられるかもしれない。でも,これを実際にやっていくのはちょっと難しそうだ。なぜなら,「プログラムの検証は数学の検証ほど刺激的なものではない」からね。

数学の定理っていうのは,ものすごく抽象性・一般性の高い概念で,そこからさまざまな分野への応用が生み出されるものなんだ。だから,数学の定理の「正しさ」を確かなものにするという作業は,人々にとってすごく大切なことで,研究者にとってはすごく刺激的なことでもある。

ところがプログラムっていうのは,いわば理論の応用であって,問題の種類としては枝葉に位置するものだったりする。もちろん,それに価値が無いってわけじゃない。でも,個々のプログラムの「正しさ」を確かめることは,数学の定理の「正しさ」を確かめることと比べると,限られた人の興味しか呼ぶことができないし,研究者にとっては刺激の薄いことでもある。

ちょっと具体的な例を見てみよう。ここにフランスは INRIA の Yves Bertot という人が執筆した論文があって, GMP 多精度演算ライブラリの平方根関数の形式的な証明を行っている。もとは 30 行ほどの小さな関数なんだけれど,それの証明に 25 ページほどの紙面が割かれている。なんでも,その実装の形式的な証明の記述は1万3千行にも達するんだそうで,とても人手には確かめようがないので Coq という証明補助ツールを使っていたりする。

これはまさに「数学的な手続きでプログラムを検証してみた」という例になるわけだけれど,この証明をそのまま鵜呑みにすることはできない。ざっと考えただけでも,いくつかの疑問がわいてくる。

おそらく,ちゃんとした数学の知識があって,さらにプログラムの知識があって,あとは多少の根気があれば,この論文を読むことによって,その正しさに確信が持てるかどうかを判断することができるんだろう。でも……はたして,そこまでする人がこの世に何人いるんだろう?

この例はまだましな方で,多精度の平方根関数っていう一般性の高い問題に取り組んでいるから,もしかしたら興味を持つ人が現れてくれるかもしれない。でも,もっと一般性の低い,ごく普通のプログラムについて,検証に興味を持つ人なんて現れるものかな? そもそも, 30 行の関数を検証するのに 25 ページも使っているのに,実用規模のプログラムを検証しようと思ったら,はたして何ページの紙面が必要になるんだろう?

検証と確信

2007-07-12

それじゃあプログラムの場合はどうだろう?

プログラムの場合も同じで,たとえどんな理屈を持ち出したとしても,そこからいきなり「絶対的な正しさ」を断言したりすることはできないと思うんだ。プログラムが持つべき「正しさ」というのは,そこに関わる人たちの総意のうえに成り立つ「恐らくの正しさ」であって,「絶対的な正しさ」ではない。そこを履き違えてしまうと,ありもしないものを頼りにしてしまったり,得られようのないものを求めてしまったりすることになるんじゃないかな。

たとえば,あるプログラマーに,ある仕様の実装を依頼したとして,その実装が納品されてきたとしよう。そして,そのプログラマーが,こんなことを言ってきたとする――

「いやあ,このプログラムは正しいですから,信じてもらって結構ですよ」

まあ,これは論外だよね。確かめてみないことには,正しいかどうかなんて分かりようがない。

するとそのプログラマーは,こう切り返してくる。

「そこはちゃんと,いくつものテストプログラムを用意して検証しましたから大丈夫ですよ」

ううむ,でも,テストプログラムなんかは,しょっちゅう間違えて書いちゃうものだってことを,みんな知っているはず。間違ったテストプログラムを書いて,間違った検証をしているだけなのかもしれない。つまり,テストプログラムを検証してみないことには,正しい検証が行えているかどうかなんて分かりようがないんだ。

そこでさらに,そのプログラマーは,こう切り返してくる。

「いやあ,そう思って,最新の検証技術であるところの MacroSoft Visual ProofSafe を使って仕様との適合性チェックを行っているんですよ。最新のソリューションが正しさを保証してくれるんですよ」

いやしかし,どんなにその検証ツールが厳格なものだったとしても,そのツールに入力した「仕様の記述」と「本来の仕様」とのあいだに差異があったとしたら,やはり検証は役立たずになってしまうんじゃないかな。だから,まずその「仕様の記述」を検証しなきゃいけないし……それに,そもそも,そのツールはほんとうに信頼できるものなの?

結局のところ,検証のための手法や道具はさまざまに存在するものだけれど,「検証から確信を得る過程」というのは,それぞれの人の心の中で起こるできごとであって,それに対する手法や道具なんてものがあるわけじゃない。もちろん,その確信だけを抜き出して人へ伝えるってこともできない。確信を得たいと思うなら,その過程を自分の中で再現することによって,自分の中から確信を生み出さなきゃならないんだ。

理想なのは,そこに関わるひとたちすべてが,そういった確信を得られる状態にすること。それを無しに,ただ「絶対的な正しさ」を求めてプログラムの中を探し回ってみたところで,最終的に納得のいく結論に辿りつくことはできないと思うんだよね。

正しさを与えるもの

2007-07-11

「正しさ」はどうやって確かめることができるんだろう?

たとえば数学なんかは,どうやってその正しさを確かめているんだろう? 数学は,とても広大で複雑な体系を,論理的な演繹によって築き上げている。論理的な演繹によって動くという理屈ならプログラムも同じこと。それじゃあ,プログラムの「正しさ」も,数学の「正しさ」と同じような理屈で確かめることができるかもしれない――そう思わない?

それじゃあたとえば……ここにリーマン予想の証明を記した論文があると思ってみてほしい。すると,そのことを知ったあるひとが,こんなことを言うかもしれない。

「ああ,これでリーマン予想は証明されて,定理になったんだ」

いやいや,そういうわけにはいかないよね。リーマン予想を証明したとされる論文は前にもいくつか発表されていて,そのたびに誤りのあることが指摘されてきた。今回のだって間違っている可能性はある。まずはそう考えておくのが無難なんじゃないかな。

それじゃあ,どうしたらリーマン予想は証明された定理になることができるんだろう?

それにはまず,その論文が数学者のコミュニティ(学会)に向けて発表されなきゃならない。すると,その論文は多くの専門家の目による精査を受けることになる。そして,そのすべてを通過することができたなら,そのときにはじめて「証明は十分に正しい」ものとして認められることになる。そこまでしなければ,その証明が正しいかどうかなんて,誰にも断言することはできないんだ。

まあ,そんなこんなで,このリーマン予想の証明が正しいと認められたとしよう。

「ううむ,なんだ,この証明は最初から正しかったんじゃないか。学会で認められることなんて待たずに,最初から信じておけばよかったよ」

いやいやいや,そういうわけにはいかないよ! 「最初から正しかった」なんてことは,誰も言っちゃいないんだ。コミュニティの精査を受けることによって,「数学の体系へ組み入れるのに十分な程度の正しさを持つ」っていう判断が下されただけで,それは絶対的な正しさを意味しているわけじゃない。

「これまでも,そしてこれからも,絶対的に正しくあり続ける」なんて理屈は,なかなか存在するものじゃない。「よっぽどのことがないかぎり,これは正しいということにしておいてよさそうです」という合意を作っては,それを延々と積み上げていっているに過ぎない。数学の体系というのは,そうやって築き上げられてきたものなんだ。

さあ,ここでちょっと考えてみてほしい。けっきょく,この証明の「正しさ」とは,どこからやって来たものなんだろう?

どうもその「正しさ」とは,その証明の中に最初から備わっていたものではないようだ。その「正しさ」とは,論文の執筆者とコミュニティとの間の意見の交換という,社会的な過程の中から生まれてきたものと言えるんじゃないかな?

プログラムと正しさ

2007-07-10

プログラムにとっての「正しさ」って,なんだろう?

僕らは日常的に,このプログラムのこの部分は間違っているだとか,この部分は正しいだとか,この部分にはバグがあるだとか,バグが無いだとか,そういうことを話し合ったりする。でも,ここでいう「間違い」や「正しさ」,それから「バグ」っていうのは,いったいなんのことを指しているんだろう。

ちょっと視点を変えてみよう。たとえば……「完璧に正しいプログラム」,つまり「バグのまったく無いプログラム」を組むことって,はたして可能かな?

僕らは,どんなプログラムにも,多かれ少なかれ,バグが存在するってことを知っている。それは仕方のないことで,どんなに頑張ったとしても,必ずプログラムにバグは混じってしまう。

それに,間違いをおかしてしまうのはプログラミングの話ばかりではなくて,プログラムのもととなる仕様が不完全なものだったり,矛盾を含んだものだったりすることだってある。もとの仕様がダメなものだったら,そこから生まれるプログラムだってダメなものになるのは,仕方がないことなんじゃないかな。

でも……もし,ここに超人的な知性を持つひとがいて,そのひとが超人的な知性と注意力をもって完璧な仕様を作り上げて,そこから完璧なプログラムを導き出したならば……そのプログラムは「完璧に正しい」「バグのまったく無いプログラム」になるかもしれない。

そう思わない?

ああ,なぜかそうは思えないんだな。「バグのまったく無いプログラム」なんてのは,理想とかいうものでもなくて,いわゆるナンセンスのたぐいのような気がする。それを考えること自体に意味が感じられない,っていうこと。

なぜそう思うんだろう――ちょっとそのことについて考えてみよう。

参考文献

Richard A. De Millo, Richard J. Lipton, Alan J. Perlis. Social Processes and Proofs of Theorems and Programs. Communications of the ACM, 22(5). 1988.

Robert Pollack. How to Believe a Machine-Checked Proof. In Twenty Five Years of Constructive Type Theory. Oxford University Press. 1998.

Yves Bertot, Nicolas Magaud, Paul Zimmermann. A proof of GMP square root using the Coq assistant. Rapport de recherche, INRIA. 2002.

Tupper's Self-Referential Formula

2007-06-15

Jeff Tupper. Reliable Two-Dimensional Graphing Methods for Mathematical Formulae with Two Free Variables. In Proceedings of SIGGRAPH 2001, 77-86.

トロント大学の Jeff Tupper は,陰関数のグラフを安定して生成するためのアルゴリズム群を考案した。これらのアルゴリズムは Pedagoguery Software の GrafEq というソフトウェアに応用されている。同製品のギャラリーページでは,これらのアルゴリズムによって生成された様々な陰関数グラフの例を見ることができる。

070615_0.png
Image from Tupper's paper

上図はそれぞれ以下の式から生成されている。

(a)  x cos y cos xy ± y cos x cos xy ± xy cos x cos y = 0

(b)  sin((x ± sin y)(sin x ± y)) = cos sin((sin x ± cos y)(sin y ± cos x))

これらの見た目に凝った例のほか,他のグラフソフトでは誤りが生じがちないくつかの数式についても,こちらのページで触れられている。

他には,こんなトリッキーな例もある。

070615_1.jpg
Image from Tupper's paper

この「グラフ」は以下の式から生成されている。

070615_2.jpg

ただし,このグラフは値の範囲が特殊で, (x, y) = (0, 960 939 379 918 958 884 971 672 962 127 852 754 715 004 339 660 129 306 651 505 519 271 702 802 395 266 424 689 642 842 174 350 718 121 267 153 782 770 623 355 993 237 280 874 144 307 891 325 963 941 337 723 487 857 735 749 823 926 629 715 517 173 716 995 165 232 890 538 221 612 403 238 855 866 184 013 235 585 136 048 828 693 337 902 491 454 229 288 667 081 096 184 496 091 705 183 454 067 827 731 551 705 405 381 627 380 967 602 565 625 016 981 482 083 418 783 163 849 115 590 225 610 003 652 351 370 343 874 461 848 378 737 238 198 224 849 863 465 033 159 410 054 974 700 593 138 339 226 497 249 461 751 545 728 366 702 369 745 461 014 655 997 933 798 537 483 143 786 841 806 593 422 227 898 388 722 980 000 748 404 719) の辺りから生成が行われている。

この式は y の値の取り方しだいで自在なビットマップを描くことができるように工夫されたものだから,このような「自己記述するグラフ」も不思議なことではないのだけれど……でもやっぱ面白い。こんなシンプルな数式でも,平面上にグラフを延々と展開していくと,そのどこかに自己記述を行っている部分があるというのだから……。

いちおう,この数式には "Tupper's Self-Referential Formula" という名前が付けられており, Wolfram MathWorldWikipedia にも対応する項目が用意されている。

デスクトップの景色

2007-06-14

070614_0.jpg
Image from Lewis's website

J.P. Lewis, Ruth Rosenholtz, Nickson Fong, Ulrich Neumann. VisualIDs: Automatic Distinctive Icons for Desktop Interfaces. ACM Transactions on Graphics (TOG), Volume 23(3), August 2004.

例えば,自分の部屋の本棚からある本を取り出したいとする。もしその本の書名を正確に覚えていなかったとしても,本棚を一瞥すれば,たいていその目当ての本を見つけることができるだろう。こんなとき,人は書名から本を見つけ出すわけではない。それぞれの本の配置だとか,本自体の大きさや色だとか,背表紙の模様だとか,そういったいくつかの要素を組み合わせたものを,本を見つけるための「手掛かり」として利用している。

ここでは,そういった「物の配置」や「物の外見」などの視覚的要素を組み合わせることによって得られる統合的な視覚情報のことを「景色」 (scenery) と呼ぶことにする。人間は文字情報よりも「景色」の方が記憶しやすく,判別も素早く行うことができる。多くの生物において「景色」の認知が基本的な機能として備わっていることを考えれば,当然のことなのかもしれない。

では次に,自分のPCからあるファイルを取り出してくるという作業を行うとする。曖昧な記憶を頼りに,ディレクトリのあっちをたぐってみたり,こっちをたぐってみたり……。あるいは,ファイル名を記憶していれば「検索」を使うという手もある。でもそれも,目当てのファイルが気のきいたファイル名を与えられていなければ一苦労することになってしまう。

中にはこんな人がいるかもしれない――自分はデスクトップをフル活用しているから大丈夫。たいていの重要なものはデスクトップに置いてあって,デスクトップのこの辺りはこういったものが,あの辺りにはああいったものが,というような具合に配置されているんだ……。なるほど,つまりそれは,デスクトップを介すことによって「景色」における「配置」の要素を利用しているということになるのかな。

現在のデスクトップユーザーインターフェースの主流においては,ナビゲーションのための手掛かりを文字情報に大きく依存している。だから,何か特定のファイルを探し出そうとすると,本棚の中から書名だけを頼りに本を探し出してくるときのような不自由さが生じてしまう。ならば,もしこれに「景色」の概念を与えることができたならば,ナビゲーションはもっと容易で覚えやすいものになるのではないか。

前述のように,「景色」における「配置」の要素は現状のインターフェースにおいてもある程度サポートされている。それに対して「外見」の要素は圧倒的にサポートが弱い。ファイルの外見であるアイコンは,多くの場合ファイルの形式に対して割り当てられているものであって,同形式のファイル群から個々のファイルを判別することができない。アイコンを個々のファイルの判別に用いようと思うならば,個々のファイルに対して割り当てられるアイコンがもっと多様なものになっていなくてはならない。

南カリフォルニア大学の J.P. Lewis らによって開発された VisualID と呼ばれる技術は,このような見地に立ったものであるとされる。 VisualID を用いると,個々のファイルの名前から様々な模様を自動生成することができる。この自動生成のアルゴリズムでは,似たファイル名は似た模様になるという工夫がなされており,同類のファイルを視覚的に群と捉えることを可能にしつつ,かつ個々のファイルを判別することまでが可能になっている。

Lewis らは 25 人の被験者を集め,多数のファイルの中から特定のファイルを選び出すまでの時間を同一アイコンの場合と VisualID アイコンの場合とで比較するという実験を行っている。その結果として,同一アイコンの場合は平均で 30.5 秒かかっていた作業が VisualID では 23.2 秒にまで短縮されたと記している。

さて, VisualID はとても面白い技術だけど,やはりちょっと気になるのは,自動生成される有機的なデザインが現在主流のルック&フィールとは合いそうにないということ。上の画像ではかなり頑張ってめかしこんでいるものの,それでもまだ違和感を覚える。これらのアイコンをずらっと平面上に並べると,まるで微生物の標本カタログのようになってしまう。有機的なデザインで攻めるよりも,例えば Identicon に使われたキルト模様パターンのように,幾何的・抽象的なデザインから攻めることはできないものかな。