日々の流転

λ. FINAL FANTASY

FINAL FANTASYの映画を友人達と見て来た。カーナビに翻弄されつつも(笑)なんとか映画館にたどり着くことが出来た。案外すいてた。内容は、いかにもFINAL FANTASYって感じの陳腐なSFで、FINAL FANTASY以外の名前でこれ作ったら、誰にも受け入れられないよな〜って感じ。

λ. Mew 2.0.53

Mewを1.95b121から2.0.53に乗り換えた。スレッド関係のキーバインディングが結構変わってて少し戸惑った。そういえば、最近、掲示板のログとかをメールに変換して読んでいるんだけど、Wanderlustは「必要なバックエンド関数を書くだけで新たなリソースに統一された操作性でアクセスできる」らしくていいなぁ。

λ. Vain Linux

むふふ…

λ. アナグラム

そういえば、「ゲームの国」は、無意味にアナグラムを連発してて、笑えたな〜　続編希望。

λ. スプリガン

CATVで映画版をやってたので見た。原作を知らないと辛いし、いまいちな出来かも。まあ、音楽は気に入ったけどね。つーか、左手折れてたんじゃないのか? > ラストシーン

λ. 米国同時多発テロ事件

「言わせてもらっただけ。」なんて卑屈な言い方はしないで、もっと自分の意見に自身を持ちなよ。ああいう風に書いたけど、この現実が残酷だなってのは僕だってそう思うし、そういう皮膚感覚みたいなのってやっぱ大事だ。で、結論としては…　君は繊細なんだね、好意に値するよ。(爆)

λ. メモ

• 世界貿易センタービル(NY)はなぜ一気に崩壊したのか? (km日記)
• オサマ・ビン・ラディン情報 (世界のテロ組織と対テロ組織 Terrorist & Counter-Terrorism)
• 国際戦略コラム
  • 石油がなくなる時
  • テロに突いて
  • 米国の侵攻とイスラム民衆の反感

λ. ごろごろしてます。SFC-Antennaの移行で何か手伝う事もあるかなと思ってたけど、何も無く少し拍子抜け。

λ. 宇宙のエンドゲーム

の書評を日経で読んで、銀茄子さんの「有限の中の無限 〜〜主観的定常宇宙論〜〜」を少し連想。

【追記】 ……と思ったら、銀茄子さん自身が2002/12/13の雑文でこのことについて書いていた。

λ. モンゴル文字

小熊さんのツッコミで思い出したけど、これ読もう読もうと思っていながら、すっかり忘れていた。こんど学校に行ったときにコピーしてこよっと。

• A.バリデン, 矢島敬二, "コンピュータによるモンゴル語文字処理の現状", bit, 共立出版, Vol. 28, No. 12, Dec. 1996.

λ. Gauche-gtk

これも自動生成か。

ところで、クロージャを介して循環参照が発生する問題にはどうやって対処してるんだろう?

λ. evalの性能

λ. ページ番号を指定してPDFにリンク

ページ番号を指定してPDFにリンクを張るには「sample.pdf#page=4」等のように書けば良いそうだ。

λ. 読書

『彼氏彼女の事情』14

津田 雅美 [著]

λ. polymorphism

• google://polymorphism 多相 : 約55件
• google://polymorphism 多態 : 約124件

λ. 『百億の昼と千億の夜』, 光瀬 龍

読了。萩尾望都による漫画版はずいぶん前に読んでいて、原作もそのうち読もうとずっと思っていたんだが、ずいぶん経ってしまった。

λ. Eastern Dawn　東方の夜明け

申し込み開始ですよ。とりあえず申し込んでみた。

λ. ヴァン・ヘルシング(VAN HELSING)

を観てきた。スタイリッシュな映像と音楽がいい感じで、結構盛り上がれた。ストーリーはご都合主義的な点が目に付くが、あまり気にならなかった。

λ. Propositional equality の証明の equality

Propositional equality の型である Id a b の要素はせいぜい一つしかないので、要素が二つ与えられたらそれらは等しいに決まっている。それを証明したい。が、以下のコードは内側のcaseの部分で「Error in the definition of eqId because: cannot case: exps [x, x] must be distinct variables.」というエラーになってしまう。(e1へのcaseでa,b,xがunifyされているためこのようなエラーメッセージになってる。2005-05-16 の case on non-var でも書いたが、この制約は必要以上に厳しい気がする)

eqId (|A::Set) (|a,|b :: A) (e1,e2 :: Id a b)
  :: Id e1 e2
  = case e1 of
    (ref x)->
      case e2 of
      (ref y)->
        ref@_ (ref@_ x)

Agdaでこの命題を証明する方法はあるだろうか?　SET.alfa では Id a b の Collapsed も定義されてないし、やっぱり無理なのか?　Per Martin-Löfの Intuitionistic Type Theory でもこれは証明できるので、「Martin-Löf. の型理論に基づく対話型定理証明支援系」と呼ばれているAgdaでこれが証明できないとしたら、納得いかん。

(2005-09-17 追記) Intuitionistic Type Theory は propositional equality type の strong elimination を含む extensional な型理論だから、「Agdaでも証明できるべき」という理由にはならない気がしてきた。というか、私はその辺りの話が全然分かってない。Intuitionistic Type Theory 以降の Martin-Löf 流の型理論を学ぶには何を読めば良いのだろう?　Bengt Nordström, Kent Petersson, Jan M. Smith の Programming in Martin-Löf's Type Theory - An Introduction ?

(2006-02-05 追記) Thierry Coquand の Pattern matching with dependent types の p.9 には次のように書いてあった。

By contrast, it is not clear how to represent the following computation rule in term of the usual elimination rules⁴. We have seen that the unique contextual mapping

{y := x, p := refl(N,x), q := refl(N,x)}: (x : N) → Δ,

is a covering of Δ = x,y : N; p,q : Id(N, x, y). It follows that it is correct to add a new constant f : (x,y : N; p,q : Id(N,x,y))Id(Id(N,x,y),p,q) together with the computation rule

f(x, x, refl(N,x), refl(N,x)) = refl(Id(N,x,x), refl(N,x)) (x : N).

---

⁴ This problem has been independently suggested by Thomas Streicher.

(2006-04-18 追記) Michael Hedberg の A coherence theorem for Martin-Löf's type theory には次のように書かれていた。というわけで、elimIdではいくら頑張っても証明できないことになります。証明するにはAgdaに対して何らかの拡張が必要になるでしょう。

Although one might expect the identity sets to be collapse, it is impossible to prove in general that they are, as long as type theory is restricted to the standard elimination rules. This negative result is proved by Hofmann and Streicher [11], using a groupoid interpretation of type theory.

---

[11] M. Hofmann and T. Streicher. A groupoid model refutes uniqueness of identity proofs. In Proceedings of the 9th Symposium on Logic in Computer Science (LICS), Paris, 1994.

(2006-05-14追記) この「A groupoid model refutes uniqueness of identity proofs」を読んだ。20060514#p01を参照。

λ. [ruby-ext:02317] Procをブロックとして渡すには

RubyKaigiの後に聞いてみようと思っていたのに、すっかり忘れていた質問。拡張ライブラリで少しメタなことをやろうとすると、結構必要になると思うんだけどな。

λ. M2ミーティング

非生産的すぎ。

λ. RD+スタイルでプラグイン引数がエスケープされる

以前、tDiaryのRDスタイルに同様の問題を発見したときに、hikiにも同様の問題がないか疑うべきだった。不覚。

【2008-06-08 追記】 Hiki Issue Tracking System - Ticket-96 に登録。

【2008-07-06 追記】 [Hiki-dev:01199] で CVS HEAD に取り込んで貰えた。

λ. 100円ショップで買った携帯のストラップ

2006-01-29にダイソーで買ったストラップが壊れたので、新しいのを今度はキャンドゥーで買ってみた。 だけど、前のと比べて無駄にかさばって邪魔な感じ。

λ. 100円ショップで購入した「ハンディークリップピン」

普通にガチャダマ(中)を買うと50個500円だけど、これは30個100円でだいぶお得。

λ. 100円ショップで購入した「A4クリヤーホルダー　カラー5枚入り」

3色フォルダを試してみようと思って買ってみた。 本には数百円と書かれていたが、フォルダだけなら100円。

λ. 観測の扱いと閉じた系・開いた系

昨日の圏論勉強会でもちょっと話した話で、数学的・物理的な根拠は全く無いただの思いつきなんだけど、観測の扱いが複雑なのは、ひょっとして観測者が系の外部として扱われているから、つまり開いた系を考えているからではないのかと思った。 観測者自身も系の一部として含めた閉じた系を考えれば、全部ユニタリ変換だけになったりしないのか?

そう思ったきっかけは、Decoding the Universe の p.208 で以下のように、デコヒーレンスが環境とのエンタグルメントとして説明されていたこと*1。

The process of an object's gradual and increasing entanglement with its environment — the flow of information about an object into its surroundings — is known as decoherence.

あと、これはちょっと違う話だけど、宇宙全体を閉じた系として考えるとして、The principle of deferred measurement が一般に成り立つのなら、すべての観察は宇宙の終わり*2まで先延ばししてしまって、宇宙の終わりまでは全部ユニタリ変換だけで考えたりしてはいけないのだろうか。 もちろん、それは我々の視点での現象を説明しなさそうだけど。

λ. 推移閉包が一階述語論理で表現できないことの証明

推移閉包が一階述語論理で表現できないことについて何度か書いたけど、最近になって“First-Order Logic as a Lightweight Software Specification Language - The ETPTP Toolkit”(Michel Rijnders)で、どうやって証明するかを知った。

二項関係 T が二項関係 R の推移閉包であることを論理式 φ によって表現できると仮定して、矛盾を導く。まず、

• σ₀ = ￢R(a,b)
• σ_n+1 = ∀x₁,…,x_n+1. ￢(R(a,x₁)∧R(x₁,x₂)∧…∧R(x_n, x_n+1)∧R(x_n+1,b))
• Σ = {σ_n | n∈N }
• Γ = {φ, T(a,b)}∪Σ

と定義する。 すると、 Γ の任意の有限集合 Γ' は( σ_n∈Γ' であるような任意の n よりも2以上長いパスによって)充足可能なので、コンパクト性定理により Γ も充足可能なことが言える。 しかし、実際には Σ 全体は a から b へ到達不能であることを主張しているので、 Γ は充足出来ない。 これは矛盾なので、背理法よりこのような論理式 φ は存在しない。

コンパクト性定理って、あまり応用を知らなかったけど、こういう使いでがあるのね。便利だ。

関連

• 推移閉包は一階述語論理では表現できないのね - ヒビルテ(2007-12-10)
• 推移閉包が一階述語論理では表現できないことをAlloyで確認する - ヒビルテ(2009-07-14)