論理学にできること

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

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

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

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

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

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

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

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

形式手法の未来

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

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

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

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

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


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

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

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

ミーティングマン

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

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


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

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

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

https://github.com/yoriyuki/ulib

まだ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の各モジュールを紹介していく、かもしれない。

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

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

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

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

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

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