日々の流転

λ. 借りた本

• 小説すばる　2001年2月号
• 「スポーツ障害を防ぐ - 健康のためのスポーツ安全学」　中原英臣
• 「通貨政策の経済学 - Massachusetts Avenue Model」　ポール・クルーグマン(Paul R. Krugman)[著]　林康史+河野龍太郎[訳]
• 「5日間のパリ」　ダニエル・スティール(Daniel Steel)[著]　天馬龍行[訳]
• Century Books 人と思想 「フィヒテ」　福吉勝男[著]

λ. Ruby Relaxer

う〜ん。感想っすか。PrologでDCGを使って書いたパーサのバグとるのに苦労したし、しばらくはXMLは勘弁って感じ。というかRelaxerって何?って状態なんで、そんな事訊かれても…

λ. Script-Fu

Script-Fuのinterp_slib.cにaproposという関数を見付けたので、コンソールで(apropos)とかしてみたら固まったし。

λ. 最終発表

あらら……

発表向きのネタではないとは分かっていたのだけど、CPLの方は実装が間に合わなかったのだもの。しょうがないよね。……と思ったが、やっぱ成果物を作れなかったなりに、圏論ついて発表しておけば良かったなぁ。

まあ、これで明日から、真・夏休みって感じ。

λ. Ruby-GNOME2

えっと、GCとリファレンスカウンタの扱いで、またヤバイ点に気が付きました。とりあえず、見なかった事にしよう。

λ. さあ

寝よう

λ. 某所で夏祭り

落ち込んでたけど、自分が今悩んでることが、どうでもよい小事に思えてきた。もうやりたいようにやろう。立ちふさがるものは全部なぎ倒して踏み潰せばいいし。

λ. "擬データを用いた対話的関数プログラミングに関する研究", 石井裕一郎

を読んだ。単一代入や変数による通信は論理型言語みたいで面白いなぁ。私は関数論理型言語については全然知らないのだけど、ひょっとしたら関数論理型言語と相性のよいフレームワークなのではないだろうか。あと、関数型言語の視点でみると、参照透明性こそ保たれているものの、定義があまりにも操作的なので、もう少しなんとかならないかなぁとも思った。

• http://web.archive.org/web/*/http://www.tennodai.com/~yuich/

[2005-07-28 追記] Haskellでcomonadベースの似たような枠組みを書いてみて気づいたのだけど、「4.2.5 競争的書き込み」のmergeRは有限のリストに対しては正しく動作しないはず。なぜならば、writeはnilに出会ったときに擬データをnilに確定しないため、mergeRの結果のリストの終端はいつまでたっても確定しない。

λ. 飲み会＠串屋

.

λ. Persistent Data Structures

MIT の Advanced Algorithms, Fall 2005 の第二回の資料 Persistent Data Structures を読んだ。

変更を行うとそれ以前のデータにアクセス出来なくなる ephemeral なデータ構造に対して、変更を行う以前のデータに自由にアクセス出来るデータ構造が persistent なデータ構造。過去のデータを自由に読むことは出来るけど、変更は最新のデータにしか出来ないのは partialy persistent なデータ構造。

ポインタを使ったデータ構造をpersistentにするための一般的な手法として fat nodes と path copying があるが、どちらも追加的コストが比較的大きい。それに対して、Sleator と Tarjan の modification box を使う手法は両者の優れた点を組み合わせた手法で、O(1) の追加的コストでいけるそうだ。

λ. 靖国神社：元軍人らの遺族、合祀取り消し求め初提訴へ

またしょーもない訴訟を……というのが正直な印象。この手の話は自衛官合祀訴訟の最高裁判決で一応の結論は出ていると思う*1のだが……。遺族の方には申し訳ないが、具体的利益のためにではなく、みずからの政治的主張のために裁判所を利用しているように見えて仕方が無い。

λ. 万能数値表現法 URR

Matzにっき(2006-07-26)より。面白い表現法だな。ただ、-∞ を表現しつつ +∞ や無限小は表現できないというのは少し気持ちが悪い。何故そうなっているかというと、以下のように区間分割を進めていき、その区間の最小値という形で表現されるため。

• [-∞,∞)
  • [0, ∞)
    • [0,1)
      • [0.5, 1)
        • [0.25, 0.5)
        • [0.5, 1)
      • [0, 0.5)
        • [0, 0.25)
        • [0.25, 0.5)
    • [1, ∞)
      • [1, 2)
        • [1, 1.5)
        • [1.5, 2)
      • [2, ∞)
        • [2, 4)
        • [4, ∞)
  • [-∞, 0)
    • [-1, 0)
      • [-0.5, 0)
        • [-0.25, 0)
        • [-0.5, -0.25)
      • [-1, -0.5)
        • [-0.75, -0.5)
        • [-1, -0.75)
    • [-∞, -1)
      • [-2, -1)
        • [-1.5, -1)
        • [-2, -1.5)
      • [-∞, -2)
        • [-4, -2)
        • [-∞, -4)

λ. 『GOTH—リストカット事件』 乙一

を読んだ。 先に漫画の方を読んでいたからか、話の持っていきかたや描写が冗長に思えて仕方が無い。内容は普通に面白かったが。

λ. Modal Algebras

昔、途中で挫折した First Steps in Modal Logic を再び読んでいるのだが、命題 3.4 の自然言語で書かれた証明に頭がこんがらがってきた。以前に読んだ時にはあっさり理解できたはずなのだが……。

これはどういう命題かというと、遷移関係が

1. 反射的(reflexive)
2. 推移的(transitive)
3. pathetic: a R b ⇒ a=b
4. 稠密(dense): a R b ⇒ ∃x. a R x R b

であることと、□X = {a | ∀x. a R x ⇒ x∈X} で定義される演算子 □ が

1. Deflationary: □X⊆X
2. Nearly inflationary: □X⊆□□X
3. Inflationary: X⊆□X
4. Nearly deflationary: □□X⊆□X

であることが、それぞれ同値だという命題。

それで、「頭がこんがらがるのは自然言語で証明が書かれているからだ」と思い、Agdaで書いてみた(ModalAlgebras.agda)　一応、頭はスッキリしたが、かえってややこしくなっている気もしないでもない。

追記

ちなみに、反射律を「a=b ⇒ aRb」と書くと、patheticであることと双対の関係にあることが分かる。 同様に、推移律を「(∃x. a R x R b) ⇒ a R b」と書くと、稠密性と双対の関係にあることが分かる。 考えてみれば当たり前だけど、最近まで気付いていなかった。

λ. Categories with attributes (cwa)

依存型とcatamorphism の話を書くために、まずは依存型を持つ体系の圏論的なモデルとして Categories with attributes を導入する。

Categories with attributes

Category with attributes (cwa) は依存型を持つ計算体系の圏論的なモデルとしてよく使われる圏で、以下の構成要素と条件からなる。

• 圏 C
• 終対象 1∈|C|
• 前層 Fam : C^op → Set
  • 射に対する作用については S[f] := Fam(f)(S) という記法を用いる。
• 任意の Γ∈|C| と S∈Fam(Γ) に対して、Γ・S ∈ |C| という対象と射 π_S : Γ・S → Γ が存在する
  • 記法を濫用して π_S のことを、単に S と書くことがある。
• 任意の射 f : Δ → Γ と S∈Fam(Δ) に対して、射 f・S : Δ・S[f] → Γ・S が存在して、
  
  がpullbackになっていて、さらに id_Γ・S = id_Γ・S と (f∘g)・S = (f・S)∘(g・S[f]) が成り立つ

依存型を持つ体系のcwaでの大雑把な解釈

まず、π_S の section からなる集合を Tm(Γ, S) := {M: Γ→Γ・S | π_S∘M = id_Γ} と書くことにする。 そうすると、依存型を持つ体系はcwaに大雑把にはこんな感じで対応する。

• 文脈 Γ は Γ∈|C| に対応し
• 文脈 Γ での型 S 、すなわち Γ ├ S set であるような S は、S∈Fam(Γ) に対応
• 文脈 Γ での項 M 、すなわち Γ ├ M : S であるような M は、M∈Tm(Γ, S) に対応

これは一見すると奇妙な解釈に見えるけど、スライス C/Γ を考えると、普通の解釈を一般化したものになっている。 C/Γでの終対象は C の id_Γ: Γ→Γ なので、C での π_S : Γ・S → Γ を C/Γ では単にSと書くことにすると、M∈Tm(Γ, S) は C/Γ ではちゃんと点 1→S とみなすことが出来る。

代入

それから、M∈Tm(Γ, S) と f : Δ→Γ に対して、M[f] ∈ Tm(Δ, S[f]) を、pullback の性質から以下の図のように定義する。

S[f] や M[f] と書いたが、これらはもちろん代入(substitution)を表している。 例えば、Γ ├ N : T と Γ, x : T ├ M : S から Γ ├ M[x:=N] : S[x:=N] を得ることが、N ∈ Tm(Γ, T) と M ∈ Tm(Γ・T, S) から M[N] ∈ Tm(Γ, S[N]) を得ることに対応している。

このように、構文的な代入を意味論的な代入にうまく対応させられるのが、cwaの嬉しいところ。

ただ、ちょっと面倒なのは weakening をする際にも、型や項の側では要らない変数を捨てるような代入を明示的に適用しなくてはいけないところ。 例えば、Γ ├ S set と Γ ├ M : S から weakening で Γ, x : T ├ S set と Γ, x : T ├ M : S を得るのは、S∈Fam(Γ) と M∈Tm(Γ, S) から、π_T : Γ・T → Γ を使って S[π_T]∈Fam(Γ・T) と M[π_T]∈Tm(Γ・T, S[π_T]) を得ることに対応する。

これくらいの例なら問題ないのだけど、ちょっと複雑なものを書こうとすると、すぐ訳がわかんなくなってしまうよ……*1

λ. 『洗脳原論』 苫米地 英人

読了。