2013年1月28日月曜日

Emacsと改行の問題

Emacsは国際条約で禁止すべきだ、という意見もあるが、私は最近Emacsを見なおした派。文章を書くのは全部Emacs上にしたい。とはいえ、ちょっと厄介なのが改行の扱い。Emacs上ではauto-fill-modeで文章をある文字数で改行したほうが扱いやすい。TeX(これも禁止の声が上がっている)だとこれで問題ないのだけど、HTMLやブログの場合、改行が無視されずそのまま表示される。これはウィンドウ幅に合わせて表示を変えたいとき(普通、HTMLやブログではそうだと思う)にとても困る。

そこで、というかlonglines-modeというものが用意されている。これは、auto-fillではsoft line breakのみを挿入し、改行がEmacs上だけで意味を持つようにするものらしい。soft line breakはコピー・ペーストの時には削除されるようなので、上の問題が解決される、ように思ったのだが。残念なことに、longlines-modeではsoft line breakは削除されるが、その位置に空白が残ってしまうようだ。英文では問題無いだろうが、日本語では問題になる。

そこで、簡単なスクリプトを書いてみた、というのが本題。

(defun unfill ()
  (interactive)
  (while (re-search-forward ".+$" nil t)
    (if (not (= (char-after (+ 1 (point))) ?\n))
        (delete-char 1))))

unfillを実行すると、空白行とパラグラフ最後の改行以外の改行が削除される。もっとエレガントに書けるかもしれないけど、とりあえず動いているので満足。

2013年1月20日日曜日

ゲーデルの不完全性定理からP≠NP問題にアプローチする - その2

ゲーデルの不完全性定理からP≠NP問題にアプローチするで、限定算術の無矛盾性証明を使って計算量の問題を考えるアプローチを紹介した。また、限定算術ではほとんどの体系の無矛盾性が言えないことも紹介した。今回は、無矛盾性概念を弱めることで限定算術の分離に用いようという色々な試みを紹介し、それから私のアプローチ(Yamagata 2012)を紹介したい。

前回紹介したParis Wiklie 1987の結果によると、限定算術はロビンソン算術Q(普通のペアノ算術から数学的帰納法を除いたもの)の無矛盾性を言わない。ただし、この結果はQが任意の述語論理を使えると仮定しているので、述語論理を弱めることが考えられる。例えば出てくる論理式の複雑度(量化子の数)を制限したり、カットなしの証明に制限したりすることが行われてきた。Pudlàk 1990は$S_2$($S^i_2$をすべて合わせたもの)が、$S^1_2$の証明で現れる論理式の量化子がすべて限定されている証明の無矛盾性を言わないことを示した。また、BussとIgnjatović 1995では、$S^i_2$は$S_2$から帰納法を除いた体系で、証明に現れる量化子の数がi個以下のものの無矛盾性($S^{-1}_2-B^i$)を言わないことを示した。

また、カット無しの体系の無矛盾性をいう試みについても否定的な結果が得られていて、Adamowiczらの研究では、エルブラン無矛盾性という弱い無矛盾性を定義して、これが限定算術で言えないことを示している。また、Buss 1986ではカットルールが公理に対してだけ適応されるよう証明を制限した$S^i_2$について、その無矛盾性が$S^i_2$で言えないことを示している。

もっとも、これらは必ずしも否定的な結果とは言えなくて、例えばもし$S^{-1}_2-B^i$の無矛盾性がもっと上の階層で言えれば、限定算術の分離ができる。もちろん、まだ言えていないけど。

さて、こうした否定的結果の原因はなんだろうか。まず、限定算術が数学的帰納法をのぞいた体系の無矛盾性を言えなかったりするのは、限定算術が実は帰納法を除いた体系で(帰納的カットを使って)解釈可能なことから当然だろう。では、それらの無矛盾性が、対応する限定算術より上の方の階層の限定算術で、なかなか言えそうにないのはなぜだろうか。限定算術ではなくて$I\Sigma^n$では、$I\Sigma^{n+1}$で$I\Sigma^n$の真理定義が可能なことからその分離ができるのだった。このやり方は限定算術では使えない。というのも、項を評価する関数が限定算術では定義できないからだ。

ここから、限定算術では項の指示対象の存在していると仮定できない、と考えるというのが私の考え。なので、これまでの限定算術は不完全で、これに加えて項の存在を示すために使われる公理と推論を体系に加える必要がある。Yamagata 2012では、これを$S^i_2E$として、ここから通常と同じ限定算術が導けることを示した。もっと重要なことは、BussとIgnjatović 1995と同様の体系$S^{-1}_2E-B^i$を定義して、この無矛盾性が$S^{i+2}_2$で言えることを示した。

これで、BussとIgnjatović 1995と同様に、$S^i_2$で$S^{-1}_2E-B^i$の無矛盾性が言えないことを示せれば、限定算術の階層の分離ができるのだが、この2年くらい色々考えているけどまだ言えていない。(Yamagata 2012はだいたい2年くらいまえの考えのスナップショット)まあどこまで言えるかわからないし、名目上の本業とも違うのだけど、やれるところまでやってみるつもり。ペトロス叔父みたいになるのが怖いけどね。

2013年1月14日月曜日

抽象によるソフトウェア設計 - Alloyで始める形式手法


今更ながらざっくりとだけど、Alloy本を読み終わった。最近読書時間がなくって。

感想だけど、読みながらあまり理詰めで考えず、手を動かしながら読むのが一番だと思う。理詰めに考えてしまうと論理の話になって難しくなる。私は通勤時間に読んでいたので、表面的な理解しかしていないと思う。

一番面白かったのが関係論理の部分で、関係論理については初めて知った。これって人間の自然な論理に近いんじゃないだろうか。モンタギュー意味論とかだと高階の概念が大量に出てくるけど、関係論理を使うと一階の世界である程度できるんじゃないだろうか。誰かもうやっているだろうけど。

2013年1月5日土曜日

荘子の「斉物論」とは何か



書物としての「荘子」は33篇が伝えられているのだけど、そのうち最初の2篇、 「逍遥遊」篇と「斉物論」篇が中核をなしていて、おそらく人物としての「荘子」の思想に最も近いだろうと考えられている、のだと思う。「逍遥遊」篇は序論めいた内容なので、「荘子」の思想を最もよく伝えるのは「斉物論」篇ということになる。

さて、この「斉物論」とはどういう意味なのだろうか。解説によると「物論を斉しくす」と読んで、いろいろな立場の統合を図る、と読む意見もあるのだそうだが、「物を斉しくする論」と読んで、万物が大道のもとで1である、という主張をしていると考えるのがまあ普通。

ただ、こう読んでしまうと、この主張をすくなくともナイーブに受け取れば間違っているとしか言いようがない訳で、莊子が一貫した哲学的主張を持っていると考えたければちょっと困る。いや、なんでそう考えたいのかというと、結局ナイーブに間違った主張以上の何かがあるような気がするからで、循環論法なのだけど。

と言うわけで、ここで荘子は単純な「斉物論」を唱えているわけではない、と主張したい。では何を主張しているかというと、それは非常に難しい問題だと思うが、とりあえず斉物論にもっとも関連しているであろう次の節を読むと、莊子が上記のようなナイーブな斉物論を批判していることがわかると思う。

古の人、その知至る所あり。悪くにか至る。持っていまだ始めより物あらずと為す者あり。至れり尽くせり、加うべからず。其の次は以て物ありと為す、而も未だ始めより封あらざるなり。其の次は以て封ありと為す、而も未だ始めより是非あらざるなり。是非の彰かなるや、道のかくる所以なり、道のかくるところの所以は、愛のなる所以なり。果たして成るとかくると有るか、果たして成るとかくると無きか。成るとかくると有るは、故ち昭氏の琴を鼓するなり。成るとかくると無きは、故ち昭氏の琴を鼓せざるなり。昭文の琴を鼓するや、師曠の策を枝つるや、恵子の梧に拠るや、三子の知は幾くすや、皆その盛んなるものなり。故にこれを末年に載せ、唯其のこれを好みては、以て彼に異なり、其のこれを好みては、以てこれを明らかにせんと欲す。彼、明らかにす所きに非ざるに、而もこれを明らかにせんと欲す。故に堅白の昧きを以って終う。而してその子また文の綸を以って終え、身を終うるまで成るなし。是くの若くにして成るというべきか、我もいえどもまた成るなり。是くの若くにしては成ると謂うべからざるか。物と与に成るなし。是の故に滑疑の耀きは、聖人の図る所なり。是れが為めに用いずしてこれを庸に寓す。此れを明を以うと謂う。
(岩波文庫「荘子 第1冊 内篇」4節64ページ)

この節は3つに分解できる。最初はまず「古の人」から「愛のなる所以なり」まで。これだけ読むと、確かに莊子はナイーブな斉物論を主張しているように思える。「古の人」の何も物がない、という立場が完成されていると言っているのだから。しかし、次のパート、「果たして成るとかくると有るか」から「物と与に成るなし。」までを読むと、莊子はそもそも「完成された」とか「欠けている」という区別がどこまで有効か、疑っている。一見完成されている「昭文の琴」、「師曠の策」、恵子の弁舌、そしておそらく「古人の知」も結果的には次第に頽落してしまった。これで完成されたといえるのであろうかと。そして、最後のパート、「是の故に滑疑の耀きは」から「此れを明を以うと謂う。」では、このように「完成」されたものを聖人は取り除こうとする(岩波文庫版の日本語訳から)、つまり斉物論のようなものも取り除いて、用いないのだ、と言っている。

では庸に寓すとはどういうことか。「平常(ありきたりの自然さ)にまかせていくのであって」と日本語訳にはあるが、自然という古代中国の思想の結果出てきた概念を無批判に使ってしまって、わかった気になっていいのだろうかと思う。

ひとつの可能性は「唯其のこれを好みては、以て彼に異なり、其のこれを好みては、以てこれを明らかにせんと欲す。」の1文にあるように、古の人の立場も実は正しいのかもしれないが、それを用いて他の意見に異を唱えたり、また言葉として表現したりすることができない、と言っているのかもしれない。似たような主張として、次のような文がある。(5節、67ページ後半)

既己に一たり、はた言あるを得んや。既己にこれを一と謂う。はた言なきを得んや。一と言とは二たり。二と一とは三たり。此れより以往は巧歴も得ること能わず。而るを況んや其の凡をや。故に無より有に適くすら以て三に至る、而るを況んや有より有に適くをや。適くなくして是れに因らんのみ。

万物が一である、という主張は、それを主張した途端に誤りに成るという厄介な文である、と指摘する。だから、このような主張は間違い、と現代人は思ってしまうが、莊子の解決は、「適くなくして是れに因らんのみ」。これは「庸に寓す」と同じような解決策だろう。「万物が一である」というような絶対的主張は成り立たず、いろいろな見方が世の中にあることを受け入れなさい、というのが莊子の主張であるような気がする。(最後の方適当)


2013年1月4日金曜日

人気エントリー一覧

皆様新年あけましておめでとうございます。抱負とかは、公言しないほうが実現確率が高まるらしいのであえて言わない。

さて、去年アクセスが多かったエントリをリストしようと思う。

  1. モナドとは何か - 私の見方
  2. モデル検査の「モデル」とは
  3. 87クロッカーズ
  4. MacBook Pro Retinaモデルを購入した
  5. ゲーデルの不完全性定理からP≠NP問題にアプローチする
今年もよろしくお願いします。

昔の映画を見た



今更ながら、アマデウスのディレクターズカットを見た。うーんどうだろう、正直劇場版のほうが良かった気がする。ディレクターズカットでは、物語がなんだか間延びしているし、サリエリがただの悪人、モーツァルトはただのダメ人間になっている気がする。

ちょっと面白いのが、昔聞き取れなかった英語のセリフが聞き取れるようになったことで、字幕とせりふがいろいろ違うことに気がついた。特に、最後の場面。最初見た時、結局サリエリはモーツァルトを殺したんだろうかどうなんだろうか、という疑問が湧いたけど、最後の場面のサリエリのセリフを聞くに、神がモーツァルトを殺し、レクイエムを未完成に終わらせた、というのがサリエリの認識であるみたい。凡人サリエリが作曲の過程に関わったレクイエムを神は完成させることを許さなかったと。

ま、私の解釈ですが。