日々の流転

λ. 霧につつまれた森の中でピアノを弾いていると、誰かに「センスの悪さを曲への慣れで誤魔化している非常に筋の悪い演奏だ」というような指摘を受ける……という夢を見ました。的当を得た指摘だな、あまりにも。

λ. 小田急線が向ヶ丘遊園あたりでトラブルがあったらしく、大幅に遅れてました。ちょっと珍しい。

λ. Boxモデルの実装

で、電車が発射される発車するのを待っている間にBoxモデルの実装について考えてたんだけど、何とか考えがまとまった気がする。一番悩んでたのは、BoxをEXITした時に次にどのBoxに移動するかだったんだけど、S-Prologのデータ構造ならば、rightのtermからBoxを作ってそこに移動すれば良い。rightのtermが空の場合は、prevを辿りながら空でないrightを探す。rightもprevも無くなったらsuccess。次は組み込み述語の扱いについて考える予定。この辺りはSWI-Prologの方も参考にしよっと。

λ. 「もし人間が10進法で物を数えなければ、例えば6進法とかだったら、18歳くらいで成人だったのかな」

16進法で数えてたら0x10歳くらいで成人なのかなと思った。でも、0x20歳だったらやだな〜 < ダメ人間

λ. 逃避活動

データベース概論の課題からの逃避に、切符問題(from Island Life)を解いてみた。5問解くのに約30分で丁度良い気分転換になった。

λ. システムプログラミング

今日はネットワーク入門。どうせならgethostbyname等の古いAPIよりもgetaddrinfoやgetnameinfo等の新しいAPIを教えれば良いのにと、ちょっとだけ思った。

λ. google://非リカード的政策 (2件)

.

λ. るびま 0004号

きたー

λ. First Steps in Modal Logic の Theorem 10.3

10.3 THEOREM.

Let S be a canonical formal system with canonical valued structure (𝔖,σ). For each formula φ the conditions

1. 𝔖 ⊩^u φ
2. (𝔖,σ) ⊩^v φ
3. ⊢_S φ
4. ⊨_S^v φ
5. ⊨_S^u φ

are equivalent. In particular, each canonical system is Kripke-complete.

この定理の証明に Finally the implication (v)⇒(i) is an immediate consequence of canonicity. とあるが、このどこにcanonicityが利いてくるのかが良くわからなくてちょっと詰まった。

関係⊨_S^uの定義から ⊨_S^u φ ⇔ (∀A. (∀ψ∈∅. A ⊩^u ψ) → A ⊩^u φ) ⇔ (∀A. A ⊩^u φ) ⇒ 𝔖 ⊩^u φ という風に言えてしまわない?　と最初思ったのだが、これは関係⊨_S^uの定義を勘違いしていたためだった。 正しい定義は Φ ⊨_S^u φ ⇔ Φ∪S ⊨^u φ なので、証明は ⊨_S^u φ ⇔ S ⊨^u φ ⇔ (∀A. (∀ψ∈S. A ⊩^u ψ) → A ⊩^u φ) ⇒ 𝔖 ⊩^u φ となる。formal system S がcanonicalだということの定義は 𝔖 が S のモデルであること、つまり ∀ψ∈S. 𝔖 ⊩^u ψ なので、最後のステップが言える。

これなら納得。それにしても下らないことで時間を費やしたものだ。

λ. 異文化理解には相手の文化や信念の尊重が重要だが……

(『A Question of Belief』の感想をIRCから転載)

ペーターとメリーは、南太平洋に浮かぶ島国のシャーマニズムの影響が色濃く 残る村にボランティアとして赴任し、村人の生活向上を目標に意気揚々と活動 する。ある日メリーは衛生のために村の子供たちの体を洗い服を着替えさせる が、それは村の伝統に反し、シャーマンの怒りを買ってしまう。その数日後か らメリーは足の痛みを感じだし……

というちょっと神秘的な雰囲気のあるサスペンスであると同時に、援助や開発、 異文化理解の難しさについても教えてくれる小説である。少々不思議な読後感 の残る小説だと思う。

メリーに起こった異常はシャーマンの呪いだったのか、それとも医者の言うよ うに彼女自身の呪われたという思い込みのせいだったのか、というのがタイト ルの A Question of Belief の由来であり、物語の核心である。そう。人は信 念によって生きていて、時として思い込みによって人が死んでしまうことすら あるのだ。作中では医師が次のように語っている。

Sometimes people die, because they believe they are going to die. There is no other reason.

全く驚くべきことである。そして人が信念によって生きている以上、精霊や呪 いが本当に存在するかどうかはともかく、我々の「科学的」世界観が正しくて、 彼らの世界観が間違っていると決め付けていては、異文化理解は出来ないし、 開発や援助も出来ない。そういう意味では作中の

And the villagers' beliefs in spirits and in the powers of the shaman were important to them. I realised that it wasn't necessary for me or anyone else to change their spiritual beliefs to make their lives better.

というのは正しい。だが、現実はそう単純ではないのだ。例えば我々は人権を 普遍的価値と考えているが、我々の援助対象となる地域では女子割礼などそれ に反する文化があることもある。女子割礼の場合には現実に防止への取り組み が行われているし、単に文化や信念に干渉しなければ良いという問題ではない。

この小説を読むことで、あなたもちょっと不思議な読後感を感じるとともに、 きっと色々と考えさせられるのではなかろうか。

Quotation

`There is, Peter, there is!' she said. She grabbed my arm. `This thunder and lightning means the spirits of this island are angry with me. I know it!'

Excellent Translation

「そこにいるわ、ペーター、そこにいるの!」
メリーはそう言って僕の腕を掴んだ。
「この雷は島の精霊が私に怒ってるんだわ。私にはわかるの!」

Explanation

足の痛みが直らないメリーを医師に診てもらうため、村から遠く離れた都市へと二人が行こうとする途中の情景。メリーの恐怖が伝わってくる。

λ. 第2回 Kahuaセミナー

に参加中。 Kahuaはよく作りこまれてるな。 楽しい。 設定だるいけど。

パーミッションではまっている人多数。グループがどうだとかいじるのは面倒くさいので、あの場合suExecを有効にしてしまうのが手軽だったと思う*1。

GaucheやGuileではsyntaxを値として使えるらしい。ちょっと気持ち悪いかも。

λ. “Mechanizing common knowledge logic using COQ” by Pierre Lescanne

Coqの上で共通認識論理を形式化して色々する話。こういうのはとっくにやりつくされている話だと思っていたが、案外そうでもないらしい。

ヒルベルト流の共通認識論理を深い符号化法(deep embedding)でCoqに埋め込む。作る体系は普通のものではなくてCoqのパワーを生かしたもので、高階述語論理になってるし、論理結合子も→と∀を使ったチャーチエンコーディングで表現するようになっている。

共通認識論理の紹介としても分かりやすい。 ただ、最大不動点に関する話は、A→BのときAがBよりも大きいとしていて変な気がする。 共通認識様相を特徴付ける推論規則として、⊢ φ→ψ∧E_G(φ) から ⊢ φ→C_G(ψ) を導く推論規則があって、これは一種の余帰納法(coinduction)なのだから、A→BのときAよりもBが大きいとすべきだと思うが。

The muddy children という問題について、これを使って実際に証明をしている。ただ、専用のTacticsはまだ用意していない。

また、三賢者と帽子のパズルを例に、共通認識様相が実際には必要ない場合についての説明があった。「⊢ 仮定→結果」の形で示す場合には仮定に共通認識の様相が必要になるが、「事実 ⊢ 結果」の形で示す場合には事実には共通認識様相は不要*1。先日、SPASSで知識の論理を使って論理パズルを解く?で書いた話がまさにこれに当てはまっていて、うわっと思った。

あと、「Epistemic logic is usually mechanized by model checking」と書かれていて、Needham-Schroeder Public-Key Protocol の話が参照されていた。この話はモデル検査では有名な話だけど、知識論理と関係があるとは知らなかった。

それから、この論文とは直接の関係はないけど、ytbさんが知識様相論理をAgda2上に実装しているそうなので、どんな感じになるのか少し気になるのだった。

λ. 帰りに泳いできた

今日は帰りに久しぶりに泳いできた。 先週と先々週は調子が悪かったのと病み上がりで泳ぎに行かなかったので、3週間ぶり。 使ってなかった筋肉を久しぶりに使ってる感があった。 1kmを25分くらいで。

λ. 『数理論理学』 (古川康一, 向井国昭)

半年くらい前に出た古川先生と向井先生の本をざっと読んだ。 「問題を論理を使って表現して、推論によって問題解決する」という古きよき視点から、命題論理、一階述語論理、論理プログラミング、発想論理プログラム、帰納論理プログラムについて入門者向けに解説した本で、この視点からは良く纏まっている。 厚くないので読みやすいのではないかと思う。 また、個人的には一般論理プログラムの安定モデルによる意味論などをちゃんと説明しているのは、ちょっと好印象。

ただ、論理と計算のしくみ(萩谷 昌己/西崎 真也)などと違って、計算機科学・情報科学での論理の応用を幅広く押さえた本にはなっていないので、そこには注意が必要だと思う。 これには厚さの都合もあるだろうけど、「コンピュータサイエンス教科書シリーズ」というシリーズの中の一冊という位置づけだから、というのもあるのかなぁ、等と思った。