2012年11月30日金曜日

お財布をプレーンテキストで管理する

mohとは?

家計簿を付け始めて何年か、いろんな方法を試してきた。主に電子的なやり方でやってきていて(紙ですることも検討はしてみた)、最近はGnuCashからExcelに戻って、簡単な表を作って、あまり細かい項目は書かずに大雑把な合計だけを書くようにしていた。

だけど、自宅PCがMacに変わった。わざわざMS Officeを買う必要もないかと思いLibreOfficeで家計簿をつけてみることにしたのだけど、これが失敗。以前Excelで使っていた表をインポートすると、なんだか表の表示が崩れてきてしまう。

では、ということでNumbersを試してみたけど、データのインポートがうまくいかない。なんだか同じ列なのに金額だったり日付だったり異なった種類のデータとして解釈されてしまう。GnuCashは操作がしにくい感じがするしなあ。

ということで、家計簿ソフトを自作することにした。howmとhowmoneyを参考に、howmのメモに書き散らした支出入の記録から会計簿を作成するようにした(howmに依存はしていない。多分org-modeとかでも使えるはず)。また、GnuCashを参考に、一応二重簿記になっている、と思う。

インストール

まずOCamlをインストールして欲しい。最初はRubyで書こうかと思ったけど、なんとなく再帰で処理するところがしっくりこなくて、OCamlで書いた。

次にhttps://github.com/yoriyuki/moh (2013/8/27追記:masterブランチはRubyで実装されるようになったので、OCaml版はhttps://github.com/yoriyuki/moh/tree/OCamlから。)からmoh.mlをダウンロードして適当なところに置く。財務データが置かれているディレクトリのトップに置くと便利かも。

これでインストールはおしまい。

使い方

データの準備

当然、mohを使うには家計簿を付けなくてはいけない。家計簿はフリーフォーマットのプレーンテキストファイルで、財務データ以外のデータを含んでいても構わない。また、ひとつのファイルにまとまっている必要はなく、複数のファイルに分散していて良い。

例えば、~/kakeiboに財務データを置くことにしたとすると、~/kakeibo/foo/bar/kakei1などといったファイルに書き込めば良い。

財務データは1行で書かれている必要がある。例えば、

[2012-11-30]\$ Wallet  -> Expense 昼食 セブンイレブン 焼肉弁当 700

と書くと、財布から700円を昼食として支払ったことを表す。「セブンイレブン コンビニ」はコメント。

Wallet,Expense,Incomeは特別な口座で、略記法が用意されている。上は

[2012-11-30]\$ 昼食 セブンイレブン 焼肉弁当 700

と書ける。

もし、40万円給与をもらったとすると、

[2012-11-30]\$\$ 給与 400000

と書ける。

レポートの作成

ここで、

ocaml moh.ml -d XXX Wallet 20120101 20121231

とすると、XXXのサブディレクトリを再帰的に探索して財務データを抽出し、集計してレポートとして表示する。上は、Walletの年次リポートを作成している。-dが省略されれば、カレントディレクトリをトップトップとして扱う。

今後

いろいろ足らないところはあると思う。Githubで公開しているのでどんどん改良してくだされば嬉しい。

2012年11月25日日曜日

荘子とコミュニケーションの問題



コミュニケーションにはいろいろな問題があって、例えば上司と部下の関係とか、実際的な問題もたくさんある。だけど、ここではとりあえずもっと原理的に、感情とか意図とか、一般に心の内部にあって他人から観察できないものをどうやって伝えることができるのか、という問題を、特に荘子に書かれた議論から考えてみたい。といっても、(書物としての)荘子がコミュニケーションについて触れている箇所は多くなくて、秋水篇の最後だけだと思う。読み下し文を引用する。(荘子 第2冊 金谷 治訳注 岩波文庫)

荘子、恵子とごう梁の上に遊ぶ。荘子いわく、ゆう魚出で游びて従容たり。これ魚の楽しみなりと。恵士曰く、子は魚に非ず。安んぞ魚の楽しみを知らんと。荘子曰く、子は我に非ず。安んぞ我の魚の楽しみを知らざることを知らんと。恵士曰く、我は子に非ざれば、もとより子を知らず。子も固より魚に非ざるなり。子の魚の楽しみを知らざること、全しと。荘子曰く、請う、その本に循わん。子の曰いて、女安んぞ魚の楽しみを知らんと云う者は、既己に吾れのこれを知ると知りて我に問えり。我はこれをごうの上りに知るなりと。
(変換できなかった文字はひらがなのままにした。)「これ」が何を指しているのかわかりにくいので、解釈に迷うのだけど、こういう議論をしているような気がする。

恵子の立場は、ときどき村上春樹の小説に出てくるようなコミュニケーション不可能論者みたいな感じがする。すべての人は違った考えを持っているから、コミュニケーションは不可能。コミュニケーションが不可能であることさえ、コミュニケートすることも不可能であると。

これに対する荘子の答えは簡単で、違っていると言える時点で何か共通の尺度でその考えを比較している、つまりコミュニケーションの可能性を仮定している。ただし、コミュニケーションの必要十分条件が共通性にあると仮定する限りで。ここでは、コミュニケーションを私秘的な物が知られる可能性があることを指して使っているので、この必要十分性は仮定して良いと思う。

というわけで、荘子は恵子的立場を否定するのだが、では荘子は魚と人間がコミュニケートできると主張したいのだろうか。多分そうではないと思う。ここでのポイントは、「共通性がコミュニケーションの可能性である」というテーゼが最初から論証なしに仮定されている点で、荘子はこれへの背理法を試みている気がするのだが、そこまで掘り下げた議論が書かれていないので、なんとも言えない。

2012年11月5日月曜日

電子書籍への失望

一時期私も電子書籍に期待して、本をKindleで買ったり自分で自炊したりしていたのだけど、最近は幻滅している。

電子書籍といっても、最初から電子データで提供されているものと、もともと紙だったのをスキャンしたものと、大きく2つに分けられると思う。で、どちらも今ひとつなのだ。

まず電子データで提供されているものへの不満
  • タイトルが少ない。フッサールのイデーン(の英訳)はあったけど、ヴィトゲンシュタインは論考のみ。
  • Kindleの表(Real World Haskell、あとARM System Developer's Guide)とか数式の組版がめちゃくちゃ
  • 誤植も多い。
じゃあ紙の本から自炊すればいいかというと、そうでもなくて、
  • 自炊は面倒。日曜の晴れた日に自炊していると、人生いかにも無駄にしている気がする。業者に頼むことも出来たけど違法っぽいし。
  • ページをめくるのが遅い。まあこれは私が未だにiPad1でPDFも上手に作れていないからだろうけど、そんなことにいちいちお金や時間を投資してられない。
  • 地味な問題点だけど、裁断してしまうと本としての形がなくなるので人に貸せない(その人がローテクだった場合)。
というわけで紙の本に回帰しようかなあと思っていたりする。

あと、一言付け加えると、AdobeのDigital Editionの電子ブックを2つ持っているけれど(どちらも数学書)、組版は文句のつけようがないものだった。

2012年10月19日金曜日

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

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

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

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

2012年10月9日火曜日

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使いとしてはあまり意味が無さそうな…
まあこんな感じです。開発環境の導入はまだなので、そうしたら文句とか出てくるかも。

2012年9月23日日曜日

そこをなんとか


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

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

2012年9月16日日曜日

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

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

というわけで、メモアプリということになるわけだが、世の中的には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を書かなくてはいけない所が楽しいかも(?)。

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


2012年8月19日日曜日

ゲーデルの不完全性定理から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問題にアプローチする - その2

2012年8月11日土曜日

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度ディスクがいっぱいになって操作できなくなったりしたけど、なかなか使いやすかった。

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

2012年7月27日金曜日

論理学にできること


学問に社会への成果の還元を求めても上手くいかないと思う。だけど、どのみち研究は何らかの基準で分野内で評価されるわけで、その基準があまりにひとりよがりだと分野ごと廃棄処分されてしまうんじゃないかと、最近のLipton先生の記事を読んでちょっと思った。では現代の論理学は何を社会に対して還元できるだろうか。

現代の論理学、まあフレーゲ以降の論理学ということになると思うけど、これってそもそも何を成し遂げたのだろうか?現代論理学は主に数学と、少しコンピュータで使われる推論を対象にしている。でもその割には、労力に見合った成果を数学やコンピュータサイエンスに還元することはできていないと思う。

一方で、伝統的な論理学、例えばスコラ哲学のものとかは、数学に限定せずあらゆる論証を対象にしていた。この仕事を専門的に引き継ぐ人たちは結局誰もいなくて、今はビジネスコンサルタントなんかの領域になってしまっている。お陰で、有名のビジネス書に、論理的推論は3段論法に尽きる、と書いてあったりする。

では、現代論理学で数学に特化していない一番の成果とはなんだろうか。私は一階述語論理の(健全性と)完全性定理だと思う。その重要性は2つの側面がある。一つは結果自体の重要性。もう一つはそこに至るまでの過程のもつ重要性。

結果自体で言うと、完全性定理はある意味で厚生経済学の基本定理に似ていると思う。厚生経済学の基本定理は、ある限定された条件のもとでは、市場経済と巧妙な課税を使えば理想的な経済が実現できるという、市場経済の可能性を示すものだった。同様に、完全性定理はある範囲での論証が与えられたルールで完全に記述できるという、形式論理の一つの到達点である。と同時に、経済学と同様、その限定された条件を超えると、例えば二階論理のように形式化できない部分が出てくるであるとか、あるいはたとえ一階の述語論理で原理的には記述可能であっても、それが現実的でない、といった形式論理の限界に触れるための入り口になるんじゃないだろうか。

もうひとつ、完全性定理を導く過程にも重要性があると思う。もちろん、証明自体は殆どの人にはトリッキー過ぎて理解出来ないと思うけど、「論理的帰結」の定義であるとか、そもそも健全性と完全性が論理を正当化するものであるとか言ったことは論理を考える上で重要だと思う。少なくとも「主語がある言語で考えるほうが論理的」みたいな言説がアホだということが分かるんじゃないか。

と、一階述語論理を持ち上げてみたけど、数学を除いて一階述語論理の公理系で実用的に書けるような知識体系てあまりないんだよね。だからインフォーマルな論理をもっと研究すべきだと思う。ただ、この辺はよく知らないのでなんとも言えない。トゥールミンとか読んでればなにか気のきいたこと言えたかもしれないけど。

それから一般的な推論と、誤謬推理の形を幾つかは、教養として広めてもいいんじゃないかと思う。帰謬法とか、そもそも推論は仮定がネストしてあらわれることとか。あまり実際の推論を形式によってするのは良くないと思うのであまりやり過ぎは良くないと思うけど。 誤謬推理に関しては、とにかく「ad hominem」に尽きるんじゃないだろうか。世の中の議論は99% ad hominemな気がする。





2012年7月20日金曜日

形式手法の未来

形式手法と漠然と呼ばれているソフトウェア開発手法があって、それなりに盛り上がったり盛り上がらなかったりしている訳だけど、その未来は明るいのだろうか。少し考えてみたい。

まず形式手法として最近主にネットで少し盛り上がっているのが定理証明支援系、例えばCoqやAgdaを使った開発だと思う。で、こういった手法に未来はあるだろうか。大方の見方に反して、私は無いと思う。まあこれは私が習得することが出来なかったという面もあるかもしれないけど、それだけじゃなくて、定理証明支援系自体の問題もあると思う。

定理証明支援系の問題は、まずとにかく使いこなすのが難しいこと。それからたとえ使えても証明を手作業でするので時間がかかること。短期間、少ないコストでソフトウェアを開発することが要求されている今のソフトウェア開発の現場に導入するのは無理だと思う。定理証明支援系を使って開発しても、仕様自体にバグがある可能性があるからバグはゼロにはならないし、正しさの証明ができるといっても、ほとんどのエンジニアは証明とはなにか理解できていないので、結局、現場には定理証明支援系の良さは理解されないだろう。

定理証明支援系の問題はもうひとつ有って、それは他の手法の問題点でもあるのだけど、仕様やプログラムを独自の記述言語で表現すること。これらの言語で完全に閉じた開発が出来ればいいのだろうけど、例えばCoqが生成したOCamlコードは遅すぎて実用に供するには手を加える必要があったりするように、他の言語への変換が発生するのが普通だと思う。そうすると、その変換をどう正当化するのかという問題が生ずる。OCamlとか実際に使われている言語でかかれたプログラムをそのままの形でそれについて推論できるくらいになってほしい。

さて、では定理証明支援系と並んで重要な形式手法であるモデル検査はどうかというと、これも微妙な気がする。少なくとも現在使われているSpinやSMVは上の定理証明支援系と同じく翻訳の問題がある。非形式的な言語から形式的な言語への翻訳を完全に正当化するのは不可能だし、不完全な正当化をするにしても、例えば自然言語で書かれた仕様書からPromelaのコードに落とすとことを考えると、その落とす過程を文書化する必要がある。たとえば仕様書を分析して流れ図を書いたりと、ペーパーワークを沢山する必要があって、何だかなあという気がしてしまう。


なので、これからの方向性としては、独自言語ではなく実際に現場で使われている仕様記述言語(UMLとか)を直接検証できるといいような気がする。まあfUMLを検証する話とか、あるみたいだし。

それ以外の形式手法についてだが、まずAlloyのことはよく知らないのでコメントできない。ただ、やはり独自の言語を持っているということで、上に挙げた翻訳の問題はあるんじゃないかと思う。

それから、メモリ操作を含むプログラムのseparation logicを使った検証という話がある。定理証明支援系n上にseparation logicを実装する話もあるけれど、私が面白いと思っているのがJavaやCのソースコードの自動検証を行うもの。オープンソースだとjStar,プロプライエタリだとinferがある。私は触ったことが無いので具体的にはコメントできないけど、形式手法の将来としては、これらのツールが目指しているようなソースコードの自動検証になるのかもしれない。



2012年7月14日土曜日

ミーティングマン



筒井康隆のショートショートにこんな話があったと思う。舞台は近未来。ほとんどの生産活動は機械がするので人間は何もしないで暮らしている。唯一残った人間の仕事がミーティングで、主人公はそのミーティングをこなすため40歳まで特別な教育を受けたのだが、就職した次の日に催眠術で促成の教育を受けた若手に仕事を取られてしまう。

その後ある種の落ちがつくのだが、それは今回のエントリとは関係ない。ただ、このミーティングマンと言う職業、現代でもあるような気がするし、彼らの社会に対する影響力がますます高まっているように思う。彼らは新幹線や飛行機であちこち飛び回って、数分のプレゼンを見ただけで組織上重要な決定を下す。


で、これ本当にいいんですかねえという話。数分で語れることには限りがあるし、Presentation Zenは今の時代はコンセプトの時代だとか言っていたけど、それはやっぱりごまかしで、長い時間かけて物事をきちんと理解しようという姿勢が失われつつあるんじゃないだろうか。

2012年7月10日火曜日

ulib - OCamlのための新しいUnicodeインフラストラクチャー

バカの一つ覚えというか、またUnicodeライブラリを作っている。


まだBatteriesのRopeと以前作っていたUnicodeライブラリCamomileの一部を集めた状態だけど、できれば今年中にIOの部分を加えてRopeをスクラッチから実装し直して最初のバージョンをリリースしたいと思っている。(と去年の今頃も言っていた気がするけど気にしない)

一応目指しているのは、Camomileの反省も踏まえてこんな感じ。

  • 純粋関数的。CamomileではOCamlのstdlibの文字列処理を真似たため、手続き的なインターフェースになっている。でも流石に21世紀に入って10年以上経ってそれはないだろうと思うので。文字列データ型はRopeかなあと思っている。
  • 軽量。CamomileはちょっとUTF-8文字列を処理するのに、GB18030の文字コード表をインストールしなくてはいけないとか富豪的すぎて、引く人が多い。今考えているのは、ライブラリを分割して、Coreな処理だけulibライブラリに、それ以外のいろいろな文字列処理や文字列照合、正規表現などは別のライブラリとして配布しようと思っている。
  • 設定不要。Camomileではデータをロードするのに必要なパスを初期設定しなくては行けなくていろいろな問題を起こした。ulibではulib本体は設定不要にするつもり。また、データはできるだけソースに組み込んで配布できないか考えている。(marshalしたデータを文字列でソースに入れておくとか)
  • ファンクターは使わない。Camomileではサポートする文字列を切り替えたり初期設定のパラメーターを与えたりする所でファンクターを使っていたけど、これがライブラリを必要以上にとっつきにくくしてしまったと思う。ulibでは文字列型は1つにしようと思うし、設定もできるだけ不要にしようと思うので、これでも問題ないはず。
次回からulibの各モジュールを紹介していく、かもしれない。

2012年7月2日月曜日

自己言及文としてのコギト命題

先週Twitterで書いた、自己言及文としてコギト命題の話。

 コギト命題とは、デカルトの「我思う、ゆえに我あり」の前半部分、「我思う」のこと、だと思う。このコギト命題から思う主体、我を取り除くと「これは何かを意味している」という自己言及文になりそうだ。なぜならコギト命題の思う対象は、思う行為自体だから。もし思う対象が具体的ならば、間違える可能性がある。例えばUFOだと思って木星のことを考えるとか。デカルトは悪霊に騙される、なんて可能性まで考えている。 

さて、「これは何かを意味している」について。この文は自明に真ではないだろうか。もしこの文が何かを意味しているならこの文は真だから、この文は何も意味していないとする。すると、前の文は偽になる。偽になるということは、少なくとも意味はあるので、やはりこの文は真となる。 

やっぱりあまり説得力がないか。

2012/07/06 段落分けをやり直し。

2012年6月23日土曜日

例外のない法則は存在するか

自己言及のパラドックスの一例として、「例外のない法則はない」があげられることがある。なぜならもしこの言明が普遍的に妥当するとすると、一種の法則になってしまうわけで、そうすると自分自身の例外、つまり例外のない法則があってしまうことになる。

もっとも、これがパラドックスになるには、「例外のない法則はない」が真である、という前提がいる。もし、これを認めなければこれはパラドックスではなく、例外のない法則があることの証明と見なせる。つまり背理法を使って、例外のない法則がないとすると、上の議論から例外のない法則があることになってしまって仮定と矛盾するから、仮定の否定、例外のない法則があるが成り立つ。


この手の議論は古代からいろいろあると思うし、ツッコミどころ満載だと思うのだけど、ここでは上の証明に含まれる具体例、という観点から考えてみたい。とは言うものの、上の証明は背理法を使っているので、そのままでは具体例を抽出できない。しかし証明を少し変えることで、具体例を与える証明を作ることができる。

まず、「何か(状況や立場によらず)例外のない法則が存在する」という文を考える。もし、これに例外があれば、「例外のない法則は存在しない」ことになる。しかしこれは上の議論からありえない。よって、この文自体が例外のない法則といえる。

つまり、上の証明に含まれる具体例は「何か(状況や立場によらず)例外のない法則が存在する」というこれまた自己言及的な文である。とすると、上の証明はあまり面白くないもののように私には思える。多分、本当に普遍的であることを示したいのは、数学とかある種の倫理規範とか言うものであるのだろうから。


(ちょっと論証に無理があったかな。)

2012年6月17日日曜日

モデル検査の「モデル」とは

モデル検査の「モデル」とは何かを少し考えてみたい。というか考えるも何もモデル検査の開発者の一人Clarkeの文章を発見したので、それを報告するだけなのだけど。

まず、最近の一般的な理解は、どうもソフトウェアやハードウェアを単純化した「モデル」、ということであるらしい。例えば、Wikipediaには

モデル検査(Model Checking)とは、形式システムアルゴリズム的に検証する手法である。ハードウェアソフトウェアの設計から導出されたモデルが形式仕様を満足するかどうか検証する。仕様時相論理の論理式の形式で記述することが多い。

とある。またPrinciple of Model Checking
 
には
Model-based verification techniques are based on models describing the possible system behavior in a mathematically precise and unambiguous manner... ...This provides the basis for a whole range of verification techniques ranging from an exhaustive exploration (model checking) to experiments with a restrictive set of scenarios in the model (simulation), or in reality (testing).

とあって、「モデル駆動テスト」などのモデルと同じ意味だとしているみたい。 まあ、モデル駆動開発のモデルはUMLだったりして数学的に厳密とは限らないから、この本の言っているモデルとはちょっと違うけど。

でもそれは私の認識とは違っていて、私の認識では、モデル検査の「モデル」は数理論理学の「モデル」から来ている。数理論理学では、論理式で表された言明や公理と、それを満たしたり満たさなかったりする構造の対を考えるのだけど、構造が言明を満たしている時、その構造はその言明の「モデル」という。

ただ、何を典拠にそういう認識を正当化したら良いか分からなかったところに、Clarkeの文章 The Birth of Model Checking を発見した。これによると、

The Model Checking problem is easy to state: Let M be a Kripke structure (i.e., state-transition graph). Let f be a formula of temporal logic (i.e., the speci cation). Find all states s of M such that M; s |= f. We used the term Model Checking because we wanted to determine if the temporal formula f was true in the Kripke structure M, i.e., whether the structure M was a model for the formula f.
ここで、モデル検査では時相論理式というもので仕様を書くわけだけど、それに対応する構造はKripke構造と言われる。システムの状態遷移は簡単にKripke構造と見なせるわけだけど、そうみなしたときあるシステムが与えられた時相論理式のモデルになっているかを判定するのがモデル検査、とClarkeは言っている。というわけで、私の認識は正しいことになると思う。Clarkeは引き続いてこうも言っている。
Some people believe erroneously that the use of the term "model" refers to the dictionary meaning of this word (e.g., a miniature representation of something or a pattern of something to be made) and indicates that we are dealing with an abstraction of the actual system under study.
というわけで、モデル検査の「モデル」を考えているシステムを単純化したもの、という見方はすくなくとも原義からは離れた見方だということになる。

ただ、モデル検査を売り込むとき、モデル駆動開発のモデルと(暗に)同一視させることが行われているような気がして、多分、元々の意味は忘れられて行くんでしょうね。

2012年6月10日日曜日

ソフトウェアテスト技法ドリル



仕事で役に立つかと読んだ。うーん、どうだろう。仕事に役に立つかどうかは別として、なんかかっこよくないというか、未来じゃない。結構最近書かれた本なんだけどね。

まず最初に、仕様書を3色ボールペンを使って色をつけながら読むことを薦めているんだけど、紙に印刷するのか、分厚くなるんだろうなという感じ。確かに紙のほうが集中して読める気がするし、4色ボールペンは私もよく使っているけど、でも未来じゃない気がする。p83の「オブジェクト指向開発の場合は、データが隠蔽されてクロスリファレンスを解析しにくい場合もあるかもしれません。ところが実際にやってみると多くのケースで隠蔽がきちんと実装されていないためクロスリファレンスが取れるようです」には笑ってしまった。ちゃんと実装されていないことに依存するテスト技法って。

ここで「未来」てどういうことかというと、多分「そういうことができるのか!」、「そういうやり方をするのか!」という驚きのことだと思う。その点、この本にはそういう驚きがない気がする。教科書的な本ではなくて、テスト技法の著者独自のまとめがしてあるのだけど、それがなんかふーんという感じがしてしまうのだ。

それはさておき、真面目な話。この本はテスト技法そのものよりも、テストの考え方に重点をおいたものだ。それがどの程度価値があるかは、テストについてあまり勉強したことが無いので何とも言えないけれど。テスト技法についてもいろいろ紹介されているが(著者考案のHAYST法とか)あまり深くないので、この本を読んだだけではあまり分からなかった。一度テストについて勉強した人が、それを体系的に理解し直す本と言った感じ。

で、実務に役に立ったかというと、とりあえず5W1Hの定義を確認するのに使った。それ以外はまだだけど、これから使うかもしれない。









2012年6月2日土曜日

コーヒーの芳香を記述してみよ!

という文章がヴィトゲンシュタインの哲学探究にあったと思う。そのあと、「新しい言葉を用意すればいいのか。」と続いたはず。

これを読んだ時は、なるほどなあ、記述なんてできないよなあと思ったんだけど、2,3年前近所にスペシャリティコーヒーの店ができて、まさにコーヒーの芳香を記述している業界があることを知った。

スペシャリティコーヒーとは、正確な定義はないそうだが、上記のようなコーヒーの利き味(カッピングという)ができる専門家(カッパー)が(通常、個別に農場から)直接買い付けたコーヒーのことを言うようだ。カッピングといって、テイスティングと言わないのは、主観を排除して客観的な評価を行うからだとのこと。

カッピングで芳香をどうやって記述するかというと、例えば「バニラのような」とか「はちみつのような」、「花の香り」といったようにたとえで記述する。コーヒーに花の香がするんだろうかと少し思ったけど、そう言われて飲んでみると確かに果実のような香りがしたりする。これはスペシャリティコーヒーとして売られているものが、香り高いものだということもあるのだろう。実際、普通のコーヒーとは全然違う味がする。まあ、私は「はちみつのような」とか細かくは分からないんだけど。

カッピングでは味を記述するだけではなくて、味の点数化も行う。私もちょっとやらせてもらったけど、点数化するところまでは無理だった。これも客観的なものを目指していて、実際熟練したカッパー同士では、スコアリングが大体一致するとのこと。

カッパーになるには、今のところとくに資格試験のようなものはなくて、他のカッパーから認められれば良いそうだ。カッパーとして認められるまでは、自分で豆を焙煎してカッピングして、他のカッパーの意見を聞いて…ということを繰り返すらしい。

さて、このことから分かる教訓だが、まずアナロジーというのは我々の言語を拡張する強力なメカニズムだということが分かると思う。それから、ある「言語ゲーム」が社会で認められるためには、その言語ゲームについて一致する集団があることが、少なくとも条件の一つ(必要条件とも十分条件とも思わないが)になるということが分かるのではないか。私は、哲学探究の、いわゆる私的言語について議論しているとされる部分はよく理解出来ていないし、特に私的言語の不可能性を主張するするつもりもないのだけど、「社会的に認められた言語」になるためにはそれを一貫して使うことができる言語使用者の集団がある、ということがわりと自明な条件だとは言えると思う。

2012年5月26日土曜日

ソラリスの海はチューリングマシンの夢を見るか

今年はチューリングの生誕100周年らしい。で、チューリングの一番の貢献というと、やはりチューリングマシンを定義したことだろう。皆さんも御存知の通り、現代の計算機科学では、チューリングが考えたチューリングマシンを使って、計算可能性を定義する。これをチャーチのテーゼというのだけど、これについて考えてみたい。

そもそもチャーチのテーゼはどういうステータスの言明なのだろうか。経験的に検証/反証可能な命題なのだろうか、それとも反証も検証も意味が無いような、計算概念の定義とみなすべきなんだろうか。

もし計算概念の定義と見れば、多分これは、位相空間で空間概念を定義するのと似ている。位相空間の場合、まず空間という概念について我々が持っている直観があって、これをできるだけ満たしていてかつ厳密な定義を与えた、ということなのだと思う。これをチューリングマシンに当てはめると、チューリングマシンが、有限的なルールで記述される記号操作、という直観を上手く定式化しているということだろう。いろいろな定義が提唱されたけど、結局皆チューリングマシンと同等になったというのも位相空間の場合と似ている。チューリングマシンは、記憶領域に1次元のテープを用いる所が少しアドホックな気がするけど、記憶領域をテープの代わりにRAMやスタックにしても計算可能な関数は変わらないし、量子計算とかにしても変わらない。

ただ、位相空間の場合、3次元であったり4次元であったりする現実の空間が何であるかについて議論しているわけではなくて、数学は数学で自分たちで定義した空間概念で一応やってみる。それで現実の空間が何であるかは物理の仕事、数学はそのための材料を提供しているに過ぎない、と思われる点がアナロジーとしては少し気持ち悪い。どうして気持ち悪いかというと、チャーチのテーゼの場合、それは計算機科学の出発点のようになっていて、それを検証するということはなされていない、というよりどうやって検証するのか、見当もつかない。

話をさらにややこしくするのが、計算可能な手続全体をどう定式化して良いかなかなかわかりにくいのと相反して、個別に計算手続きが与えられた時、それが実行可能な計算であることは直観的に分かるような気がすることだと思う。このことから、例えばAckerman関数は計算可能だと思えることからチャーチのテーゼを検証する、と言った具合にチャーチのテーゼに対する検証実験というのが考えられそうだ。ただ、私的にはこういうのを検証実験と呼ぶには抵抗があって、それってただ意見聞いてるだけな気がする。

では、チューリングマシン以外に何か計算概念の定式化はあり得るだろうか。

一つは弱める方に行くことで、例えば作業テープの長さが無限大というのは厳格有限主義の立場からするとちょっとまずい。で、これを入力の多項式時間とかに制限するとPSPACEになる。あるいは定数にしてしまうと有限状態機械になる。

逆に強める方に行くとどんなものがあるかというと、例えば極限計算可能性などがあると思う。これは、一回で答えに到達するのではなく、無限回繰り返し答えを出し、ある時点で正しい答えになっていればよい、というもの。ただし、どの時点で正しい答えになっているかは分からない。例えば、停止問題などは極限計算可能になる。また、ヒルベルトが基底定理を証明した時、このような意味での計算可能性を念頭に置いていた、と林晋先生に聞いたことがある。我々が学ぶヒルベルトの基底定理の証明はとても非構成的だけど、それは20世紀になってあまり構成可能性を気にしなくなってからの再構成であって、オリジナルはかなり構成的なのだそうだ。

さて、表題に出るソラリスの海について。ソラリスの海はどんな計算概念を持っているのだろうか。計算概念など持っていない、という気が私にはする。有限的な手続き、という発想がソラリスの海には似合わなさそう。



2012年5月19日土曜日

圧縮したまま検索

「情報処理」に載った岡野原さんの記事「圧縮したまま検索」を読んだ。簡潔データ構造の解説だけあって、文章も簡潔で難解。LOUDSの部分で振り落とされてしまった。でも面白かったので、いつか自分で実装できればと妄想している。とりあえずライブラリの名前だけ決めた。


簡単に内容の紹介すると、まず、前半ではRank/Seleect辞書を導入して、これを用いてLOUDS、ウェーブレット木、圧縮全文検索とデータ構造を導入していく。後半はこれらを実装したライブラリの紹介をしている。

で、LOUDSで分からなくなったわけだけど、何処が分からなくなったかというと$\mathbf{parent}$を求める計算のところ。$\mathbf{parent}(b) = \mathbf{select}_0(B, p)$とあるのだが…なんか違わないか。$\mathbf{parent}(b) = \mathbf{select}_1(B, \mathbf{rank_1}(B, \mathbf{select}_0(B, p)) + 1)$くらいじゃないだろうか。勘違いしているのかもしれないけど。LOUDSの解説は情報系修士にもわかるLOUDS - アスペ日記にもあるけど、こちらは定式化が微妙に違うみたいな気がする。


2012年5月12日土曜日

モナドとは何か-私の見方

(プログラミング言語の)モナドについてはいろんな人がいろいろなことを言っていて、チュートリアルも沢山ある。ただ、どうも自分が見聞きした範囲では、そういったものは両極端にわかれているように思う。一つは正確だが難解なもの。去年秋の函数型言語プログラミングの集いでのtanakhさんの講演は多分これで、あまりに難解で笑ってしまった。(悪いという意味じゃないくて、分かっている人には含蓄のある講演だったと思う。)一方で、分かりやすい説明もあって、モナドは「計算」を表すものだ、というアナロジーが使われたりする。これはプログラマにはとっつきやすい説明だけど、よく考えると何を言っているか分からない。「計算」ってなんだ?というわけで(周回遅れかもしれないけど)私なりの理解を書く意味もあるかなと思う。ちなみに分かっている人のために書いておくと、Kleisli圏を使った説明になる。


さて、何か圏$\mathcal C$を考えよう。適当なプログラミング言語の型と関数の成す圏を考えれば良い。すると、関数$f : A \rightarrow B$が$A$から$B$への射となる。ただ、実際プログラミングしていると、この関数の戻り値を拡張したくなることがままある。例えば、関数$f$を$B$の値を返すだけではなくて、エラーも返すように書き換えたくなることがある。つまり $f : A \rightarrow B + E$ ($E$はエラーの型で+は直和)を$A$ から$B$ への射と見たい。もっと一般的に、何か型構築子$M$ について、$f: A \rightarrow M B$を$A$から$B$への射と見たい。

というわけで、オブジェクトが型$A, B,\ldots$でオブジェクト$A, B$間の射が元の圏$\mathcal C$の$A, MB$間の射であるような圏$\mathcal C^M$を新たに考える。これが圏になるためには、恒等射$\eta_A : A \rightarrow MA$と射の合成$\circ^M$があって、任意の$f : A \rightarrow MB, g : B \rightarrow MC, h : C \rightarrow MD$について、次が成り立たなければならない。

  1. $\eta_A \circ^M f = f \circ^M \eta_B = f$
  2. $(f \circ^M g) \circ^M h = f \circ^M (g \circ^M h)$
さて、$M$がモナドである時、上記のような$\eta$と$\circ^M$を導こう。$\eta$は通常のモナドのreturnそのものである。$f \circ^M g$は>>=から$f \circ (\lambda x. x >>= g)$ (ここで$\circ$は元の圏の合成)と定義できる。モナド則の左恒等則は
return a >>= f  f a
だった。よって左辺を変形して

$$ \eta_A a >>= f = fa $$

よって更に左辺を変形して

$$ (\lambda x. x >>= f) (\eta_A a) = fa$$

よって

$$ \eta_A \circ  (\lambda x. x >>= f) = f$$

よって

$$ \eta_A \circ^M f = f$$.   よって上の1の最初の等式が導かれた。次に右恒等則を考える。


m >>= return ≡ m

これを使って次のような式変形を行う。

$$\begin{align*} f \circ^M \eta_B &= f \circ (\lambda x. x >>= \eta_B) \\ &= f \circ (\lambda x. x >>= \text{return}) \\ &= f \circ (\lambda x. x) \\ &= f \end{align*}$$

よって$\eta$の恒等則が言えた。次に$\circ^M$の結合則だが

$$\begin{align*} f \circ^M (g \circ^M h) (a) &= f \circ (\lambda x. x >>= (g \circ^M h)) (a) \\ &= f(a) >>= (g \circ^M h) \\ &= f(a) >>= (g \circ (\lambda x. x >>= h)) \\ &= f(a) >>= \lambda y. g(y) >>= h \\ &= (f(a) >>= g) >>= h \\ &= (f \circ^M g) \circ^M h (a)  \end{align*}$$

となって結合則が導かれた。よって$\mathcal C^M$が圏をなすことが分かった。(実はいろいろごまかしているけど)

まとめると

  1. モナドというのは型AからMBへの関数を型AからBへの「関数」と思う仕掛けである
  2. 正確にいうと、型をオブジェクト、型AからMBへの関数をオブジェクトAからBへの射とする圏$\mathcal C^M$がモナドMから構成できる
  3. モナド則から、$\mathcal C^M$の恒等則、結合則が導ける
となる。

2012年5月5日土曜日

87クロッカーズ



byflowでのsoutaroさんの紹介を見て、買ってみた。面白いけど、「のだめ」のゴミの部屋でショパンを弾くというイメージが強烈だったのに比べると、普通な感じ。面白くなるかどうかは、今後の展開次第な気がする。パラテクとか87とか何処から来てるんでしょうね。

ところで、私はあまりハードには興味が持てなくて、それは何故かというとハードウェアをいろいろ知っても、パーツメーカーの掌で踊っているような感じがするからなんだけど、まあソフトもOSや言語の掌で踊っているといえば言える。(私の場合、ソフトと言ってもプラットフォーム依存の部分はやはりあまり興味がなくて、アルゴリズムとか言語設計そのものとかに興味が有るわけだけど。)その辺、漫画を読んでハードを触る面白さが何かしら分かればいいかもしれない。でも自分のPCに液体窒素は使わないと思うけどね。

2012年4月29日日曜日

「科学的思考」のレッスン-学校では教えてくれないサイエンス (1)




科学哲学の立場から、科学的に考えるとはどういうことか(科学リテラシー)、そして科学リテラシーを身につけることで市民は何が出来るか、論じた本。分かりやすくて明快。科学哲学の予備知識は不要で、哲学について何も知らなくても納得できるように書かれている。ただし、例えば$p^2/a^3$は一定などと書かれてもたじろがないくらいの科学的な素養は必要。

内容は2部構成で、第1部では科学的であるとはどういうことかが論じられる。まず、科学/非科学を2分法で議論できないとした上で、理論がより良い(科学的である)であるための条件を論じる。普通はここで、より事実に近いのが良い理論、と考えがちだけど、それは上手くいかないとする。そして、これまでの科学の歴史を振り返りながらいわば帰納法で、科学的であるための3条件

  1. より多くの新奇な予言をしてそれを当てることができる
  2. その場しのぎの仮定や正体不明の要素をなるべく含まない
  3. より多くの既知の事柄を、できるだけたくさん同じ仕方で説明してくれる
を抽出して、それぞれ説明していく。

第2部では、科学的であるとはどういうことか、が分かった上で市民が科学に対して何ができるか、が論じられる。科学的な問題については、科学的に解決されなければいけないのはもちろんだが、「トランスサイエンス」な問いについては、科学だけで解決することはできず市民の参加に寄って解決されなければならないとして、「コンセンサス会議」という手法を紹介している。

というわけなのだが、やはり幾つかもにょる所がある。ここでは、「科学的であるとはどういうことか」、という論点に絞って議論したい。

この本では上で書いたように、科学的であること、を事実からの距離で定式化するできないとしている。この結論を導く議論は、1ページくらいの簡単なものだけど、我々は今の科学を通してしか事実というものを見ることができないので、事実との一致、という基準では単に今の科学との距離を測ることになる、それは違うだろう、とまとめられると思う。そこで、著者は事実というような抽象的なものではなく、「予言を当てることができる」といったいわば操作的な基準や、「その場しのぎの仮定や正体不明の要素をなるべく含まない」といった理論に内在する基準によって科学の良し悪しを定義付けようとする。

しかし、本当にそうだろうか。

普通、科学者はやはり「事実」を明らかにしようとしていると思う。確かに、ある科学理論があってそれが事実かどうかを完全に確かめることはできないのだけど、科学理論が事実を「志向」していることは確かだろう。(すいません、志向とか意味がよく分かっていない哲学用語使ってしまいました。)上の3条件に異議を唱えるわけではないけれど、上の3条件は科学であるための究極の基準ではなく、科学が事実を志向していることから導き出される2次的な基準ではないだろうか。

上の3条件が科学であるための究極の基準だとすると、何がまずいか。まず、上に書いたように科学に関する自然な直観が生かせない、ということがある。さらにそもそも、3条件の導出の仕方がまずい。この本では、上の3条件を具体例を見ながら導出していくわけだけど、結局それは「勝ち組」の科学理論に基づいた帰納法にならないだろうか?「勝ち組」は現代の科学の視点から決まっているので、結局、科学であることの基準を現代科学の立場から見てしまうという、「事実との一致」という基準の問題点と同じ問題を抱えることになってしまわないだろうか。

むしろ、実際のところはこうなっているのではないかと思う。まず「事実との一致」という基準がある。もちろん、これは操作的な基準には成り得ないから、直接はそれを使って理論の良さを判定したりすることはできない。しかし、これに加えて科学の「形而上学的枠組み」というものがあって、これで実際の研究場面で「どちらがより良い理論か」という判断が行われているのだど思う。

ここで「形而上学的」と言っても、悪いという意味ではない。また、哲学でいう形而上学(経験を超えた、存在するもの一般に妥当する学)とも少し違う。確かに経験は超えているのだけど、ここでいう経験は今考えている理論の適用範囲内のもので、例えば、天文学について考えているのだとすると、光学はこの形而上学的枠組に入る。光学によって望遠鏡が遠くのものを拡大してみせるのがわかるから、太陽黒点の存在が正当化される、といったような。

さて、では上に上げた3基準はどのように導出されるかというと、まず、理論が事実に一致する度合いが高いほど基準1,3が満たされることは明らかだろう。基準2はオーバーフィッティングを避ける仕組みで、「自然は単純である」という形而上学的基準から来ているのだと思う。だから逆に対象領域が単純でないような分野、例えば歴史学などは法則を立てる科学としてはなかなか成り立ちにくいのかもしれない。

まあ、似たようなこと考えている人はきっと居て、もう議論済みのことかもしれないけど。あともう1点もにょる所があって、それについてはいずれ書くかもしれないし書かないかもしれない。


欝っぽい日記再び

どうも朝寝坊する傾向が最近あって、これを直すべく朝に日記でも書こうと思う。名前も最初に日記を書き始めたもの(欝っぽい日記)に戻し、インターフェースがシンプルなBloggerに移転する。以前のブログはそのままhttp://d.hatena.ne.jp/yoriyuki/から読むことができる。

なお、「欝っぽい」と漢字で書かれていることから分かるように、「欝」は医学的な「うつ」とは関係ない(医学上の「うつ」は漢字ではなくひらがなで書くことになっている)のであしからず。