日々の流転

λ. 認識論的様相?

様相論理学 - Wikipedia に以下のような記述がある。

クリプキはこの S5 に非常に単純な意味論が当てはまることを示した。しかし実際には、議論の目的によって適切な公理系は異なる。例えば、真理論的様相に関しては S5 が最も適当だが、認識論的様相では S4 という公理系が適切であると考えられている。

これ、「認識論的様相」というのが知識様相と信念様相のどちらを指しているのかがわからないんだけど、どちらにしても変。 知識を表しているのなら、知識論理(Epistemic Logic)では S4 だけでなく S5 も適切な公理系として用いられるし、一方で信念を意味しているとしたら、T を含む S4 は適切ではなく KD4 や KD45 といった公理系が適切。 直したいんだけど、どう直したものか……

λ. HIMA :: IRC Meeting

nwnさんの Cabal + Hackage の話と、kazuさんの Haskell のプログラミング環境をよくする Emacs Lisp の話。

nwnさんの話を聞いて、2年くらい書こうと思って書いていなかった、HackageDBのアカウントくれくれメールを書いた。そしたら、30分もかからず返事が返ってきてビックリ。

• nono weird science : HIMA の内容まとめ

λ. 純米大吟醸 電球

写真は飲み終わった後だけど、本当に電球にしか見えないな。

λ. 115 直江の実験（ゲルトあり）

久し振りに内輪で人狼をやるというので、こっそり混じって参加。 人狼を最後にやったのは、 内輪だと2006年4月の「112 春を待ち望む村」、一般だと同じく2006年4月に参加した「人狼審問 : (1296)学者の村」なので随分久し振りだったが、やっぱり人狼は楽しいなぁ。

この内輪村は、まだ各人がセオリーとかじゃなくて一から考えているので、なかなか思いもよらないことがあって面白い。 今の人狼BBSとかは、各人がセオリーに従って整然と行動するのが前提になっている気がしていて、純粋な頭脳ゲームとして面白いのだけど、初期の人狼BBSのような工夫や意外さの面白さは失われているように思うんだよな。

結果は、人狼側に不運が重なったことで人間側勝利。 結果として勝てたから良かったけど、読み返すと結構ヒヤヒヤするところもあった。

• 人狼をやろう！ - ザ・フィクション 戯れ言日記(InterJ)(2009-10-06)

λ. tDiaryの生成するRSSが RDF Validator でエラーになる

RDF/XMLではXMLの属性名に名前空間修飾が必要なのだけど、makerss.rbの生成するRSS中のxhtml要素の属性が名前空間修飾されていないため、RDF Validator でエラーになってしまうようだ。

• cozretro / tdiary / チケット #178
• パッチ makerss-xhtml.patch

Fastladder が拾ってくれてないらしいのは、ひょっとしてこれが原因だったりするのかな……

【追記】……と書いたけど、自分で手を入れた別の部分でもエラーになっていたみたいで、多分こっちが原因。 しかも、rdfs:seeAlso を勝手に書き加えながら、xmlns:rdfs=... を書き加え忘れているという初歩的なミス。恥ずかしい…… orz

λ. 同期飲み会

箸袋で星を作る方法を教えてもらった。

λ. “CFG⊆PEG?” Proofathon (CPon)

参加しようと思っていたけど、体調不良により参加できず。

• <URL:http://lingr.com/room/cpon>

λ. 湘南グリーンライン5600型

湘南モノレールの車両が新しいやつだったので驚いた。

λ. 計算機言語で定理証明 (Proof Party.JP)

計算機言語で定理証明とかいう、なんだか良く分からないし怖そうなイベントに参加してきた。

Agdaについては池上さんやranhaさんが紹介してくれるだろうから、対話型定理証明器をdisって、自動定理証明器の素晴らしさを語ろうと思っていたのだが準備が間に合わず、会場でずっとごにょごにょ作業していた。あんまり他の人の話を聞いてなくて済みません m(_ _)m

しかし、対話型定理証明器をdisろうと思っていたのだけど、私がそんなことをする以前にAgdaはフルボッコだった。 一方、Coqはやっぱり凄いなぁ、と思った。

お題

以下、作ったものとか色々。

さんすう

• 自然数(エンコーディングは問わず)の加算での可換法則、結合法則、分配法則を証明。
• (1 + 2 + ... + n) = n*(n+1) / 2 の証明

自動定理証明器である The E Equational Theorem Prover (eprover)に証明させてみた(nat.tptp)。 帰納法が必要なのだけど、普通の自動定理証明器は公理型(axiom schema)を書けないので、帰納法のインスタンスを個別に書く必要があって面倒くさい。 また、割り算の定義が面倒くさかったので、(1 + 2 + ... + n) = n*(n+1) / 2 の代わりに両辺をニ倍した (1 + 2 + ... + n)*2 = n*(n+1) を扱っている。

おまけに、Jahobでも証明をしてみた(Nat.java)。 実行結果(jahob-nat.txt)。 (1 + 2 + ... + n) = n(n+1) / 2 の証明に関しては、ホーア論理 - ヒビルテ(2003-05-16)も参照。

すうがく

• Bolzano–Weierstrassの定理(収束するとかいうヤツの方)
• 中間値の定理(The Intermediate Value Theorem)
• むしろ実数の構成周辺を埋める?

時間がなくて手を出せず。

kikxさんがCoqで華麗に証明していて痺れた。

アルゴリズムの性質

• concat(l1,concat(l2,l3)) = concat(concat(l1,l2),l3)を証明する。
• reverse (reverse list) = list : リストのリバース　のリバースが元のリストと等しい事を証明する。
• あるソート関数がちゃんとソートする事を証明?(ソート関数が何かはご自由)

concatとreverseに関する証明は「さんすう」と同様にeproverに証明させた(list.tptp)。 この問題は「さんすう」よりも遥かに簡単。

ソートに関しては、バブルソートの部分正当性をJahobで証明した(BubbleSort.java, Node.java)。 実行結果(jahob-bubblesort.txt)。 本当は最初はクイックソートの方の証明を試みていた(Quicksort.java)のだけど、現在公開されているJahobは関数呼び出しを正しく扱えないようなので断念。 あと、論文 An Integrated Proof Language for Imperative Programs に書いてあったカッコいい機能を使いたい場面があったのだけど、現在公開されているバージョンには実装されてなくて、しょぼーんという感じだった。

それから、こないだクイックソート関数をAgdaで定義したので、これがちゃんとソートを行う関数になっていることを証明するというのも、時間があったらやってみたかった。 まあ、これは出来るのは分かりきっていて、面倒くさいだけの話だけど。

数理論理学

• 1階命題論理でresolutionが成り立つ事を示す
• 直観主義論理での二重否定除去と排中律の同値性

resolutionに関しては、自動定理証明器の基づいているものなので、まあ導出できて当然。 resolution.tptp

二重否定除去と排中律の同値性については、普通の自動定理証明器は直観主義論理ではなく古典論理に基づいているので、パス。 ところで、そういえば直観主義論理のための自動定理証明器というのは、あまり聞かないな。何でだろう……

自動定理証明以外なら「二重否定除去⇒排中律」は以前2006-04-29にHaskellで書いた。 逆の「排中律⇒二重否定除去」も一応Haskellで書いておく(こっちはかなり自明だけど)。 命題論理の範囲ならAgdaよりもHaskellの方がお手軽。

{-# LANGUAGE RankNTypes, TypeOperators #-}

type Absurd = forall a. a
type Not a = a -> Absurd
type a `Or` b = Either a b

em2callcc :: (forall x. x `Or` Not x) -> (forall x. (Not (Not x) -> x))
em2callcc em nnx =
    case em of
      Left x -> x
      Right nx -> nnx nx

パズル

• 何か簡単なモノ
• 最もスタンダードなハノイの塔で、最短の手数が(2^n)-1に成る事を示す。

時間がなくて手を出せず。

簡単では無い系

• Church-Rosserの定理(型無しλ計算の合流性証明)
• 古典一階命題論理の完全性証明(ヒルベルト流 Lukasiewiczの公理系)

時間がなくて手を出せず。ただ、これは自動定理証明器では難しそうだ。

Church-Rosssrの定理は以前Agda1で書いて、去年の Haskell Hackathon in 2008 September のときにAgda2向けに書き直した(ただし未公開)のだけど、束縛を nested types で表した関係で素直な再帰にならなくて、停止性検査を通っていない状態なので、この機会になんとかするというのもやってはみたかったんだけど……

その他

• お昼:
• Domino On Acid - Natural Deduction Visualized As A Game Of Dominoes
• カタン
• 焼肉

関連リンク

• #proofparty
• Proof Party の問題をCoqで挑戦 - にわとり小屋でのプログラミング日記 (2009-10-23)
• Haskell Not 98 - Yet Another Ranha (2009-10-23)
• 定理証明の会で実演した中間値の定理の証明 - 菊やんの雑記帳 (2009-10-26)
• 計算機言語で定理証明#1 - Yet Another Ranha (2009-10-27)

λ. イノベーションの起こる場所

伊藤洋一の Round Up World Now! (2009.10.23放送分) 「ITスペシャル〜クラウド・コンピューティングの展望」で、「これまではB2Bでイノベーションが起きて、それがB2Cにそのうち降りてくるという感じだったのが、今はB2Cや個人間でイノベーションが起こり、それがB2Bにも取り入れられるという流れになってきている」というようなことを言っていて、なるほどと思った。

λ. 『ストリートファイター2 キャミィヒストリー』

読了。 これは中学の頃、読みたいと思いながら読み損ねていたもの。 なんか最近、こういう心残り回収イベントが多いな。

• ストリートファイター2 キャミィヒストリー〈1〉 (Wani heroes)(皆川 ゆか/うるし原 智志)
• ストリートファイター2 キャミィヒストリー〈2〉―雨の日に拾った子猫〈2〉 (WANI Heroes)(皆川 ゆか/うるし原 智志)

λ. ファイル名から U+200E LEFT-TO-RIGHT MARK を取り除く

Google Docs から Google Docs: Download と DownThemAll でダウンロードしたファイルのファイル名の先頭に、何故か U+200E LEFT-TO-RIGHT MARK が追加されてしまっていたので、簡単なスクリプトで取り除いた。

require 'win32ole'
WIN32OLE.codepage = WIN32OLE::CP_UTF8

# U+200E LEFT-TO-RIGHT MARK
re = /#{[0x200e].pack('U')}/u

fs = WIN32OLE.new("Scripting.FileSystemObject")
dir = fs.getFolder(".")
files = dir.Files
files.extend(Enumerable)
files = files.to_a

files.each{|f|
  fname = f.Name
  if fname = fname.gsub!(re, '')
    puts fname
    f.name = fname
  end
}

λ. 数学基礎論講演会 「ゲーデルの不完全性定理」

講師

田中 一之 （東北大学大学院理学研究科数学専攻教授）

題目

ゲーデルの不完全性定理

内容

ゲーデルの定理はどこまで自己言及的か？ 本質的決定不能性と証明の加速性，新しい独立証明など，ゲーデル以降の発展のポイントを概観すると共に，この定理の誤用例など負の部分にも触れる．

6月にあった田中一之先生の講演「数学基礎論の考え方・学び方」の盛況を受けて第二弾が企画されていたので、参加してきた。 ゲーデルの不完全性定理なんて、いまさらなテーマのように思えたけど、後半のΣ無矛盾性やゴールドバッハ予想に関する話は「おおっ、そうなのか」と思った。

ゴールドバッハ予想はΠ₁文なので、無矛盾な体系でゴールドバッハ予想が証明できればそれは(標準モデルで)真。一方で、ゴールドバッハ予想の否定の証明から(標準モデルで)偽であることを導くには、Σ健全性が必要。 さらに、双子素数予想はΠ₂文なので、証明されたときにそれが真であることを主張するには、公理系にさらに強い要請が必要となる。

本質的決定不能性や加速定理についても、考えたことがなかった話なので、非常に新鮮だった。ヘンキン文とLöbの定理については、この日記でも以前に ヘンキン文 - ヒビルテ(2007-09-16) で少し取り上げたけど、Löbの定理の系として第二不完全性定理を導出できるというのも、気づいておらず「おおー」と思った。

主な参考文献として以下の3つが挙げられていた。

Feferman他編 Kurt Gödel Collected Works, Vol.1, Oxford University Press, 1986

<URL:http://books.google.co.jp/books?id=5ya4A0w62skC>

田中一之編 『ゲーデルと20世紀の論理学』 全4巻 東大出版会, 2006-7.

Torkel Franzén 著 (邦訳書来年出版) Gödel's Theorem: An Incomplete Guide to Its Use and Abuse, A K Peters, 2005.

<URL:http://books.google.co.jp/books?id=71pK8Zz9Dd8C>

なお、次回は2010年5月ごろに「不完全性定理　その後」というテーマで予定しているとのこと。「ランダムネスと不完全性定理」「クリプキの別証明」「パリス・ハーリントンの独立命題」ということで、また面白そうだ。

終了後に、かがみさんの紹介で igarisさんにお会いしたのだけど、僕はすぐに Real World Haskell 読書会の方に移動してしまったので、あまりお話できずに残念だった。 あと、下の写真は帰りにキャンパス内で見かけたもの。

関連

• 数学基礎論講演会〜ゲーデルの不完全性定理 (かがみさん)
• 数学基礎論講演会 - IgaBlogue - イガブロギュ

λ. Real World Haskell読書会 2009-10

前回の読書会が8月で、9月はお休みだったので2ヶ月ぶり。 前回、7章「入出力」の7.2「ファイルおよびハンドルを使う」まで読んでいたので、今日は多分7.3「規模の大きい例：関数的入出力と一時ファイル」から7章の残りと、8章「効率的なファイル処理、正規表現、ファイル名マッチング」。

• Chapter 7. Input and output (原著オンライン版)
• Chapter 8. Efficient file processing, regular expressions, and file name matching (原著オンライン版)

といっても、上記の講演会が終わってから移動したので、付いたときには既に8章の半ばまで進んでいて、最後の方しか参加できなかったのだけど(苦笑。

それから、Real World Haskell がついに出版ということで、オライリーの動物カレンダーつきで献本して頂いてしまった。 読書会には参加していたもののあまりフィードバック出来ていなかったので、ちょっと申し訳なくもあるのだけど、ありがとうございました。

以下いろいろ

末尾再帰的でない (++) :: [a] -> [a] -> [a] の定義が「なぜ問題ないのか?」「なぜ固定空間で評価できるのか?」について、個人的には違和感をまったく感じなくなってしまっていたのだけど、他の参加者にとってはそうでもなかったみたいだった。 それと、「このような形の関数に何か名前がなかったっけ?」という話があったが分からず。個人的に思い浮かぶのは「余帰納法(coinduction)」、「余再帰(corecursion)」、「anamorphism」とかだけど、これらは多分違うよなぁ……

System.FilePath が (</>) :: FilePath -> FilePath -> FilePath という演算子を提供していて、パスの連結を "foo" </> "bar" のように書けることに感心した。 これは記号の使い方がうまい。

それから、The Typeclassopedia 日本語訳 の話で盛り上がるなどしたが、私は未読なのでちょっと疎外感を感じるなどする(笑。それに関係してかどうかは分からないけど、Real World Haskell の16章「Parsecを使う」でなぜApplicativeを使うのかという話があった。 Real World Haskell って既存の便利な関数はできる限り使う主義みたい(たとえば、前回もArrowをちゃんと紹介せずにsecondだけ使ってみたりしてたし)なので、単に便利な関数として使っているだけではないかという気がする。

ただ、モナドはパーサーの記述には提供されている演算が強力すぎるので、パーサコンビネータの実装側としては、より制限された演算しか持たないApplicativeを抽象化として用いるのは、あり得る選択肢と思う。 John Hughes が Generalising Monads to Arrows でArrowを導入した際にも、モナドベースのパーサライブラリでは Swierstra and Duponcheel のテクニックが利用できないがArrowベースなら利用できるという例が挙げられていたので。

それから、Traversableについては The Essense of the Iterator Pattern がまとまった資料だと思う。