日々の流転

λ. 僕がK君を見ていてイライラするのは、彼の中に自分と同じ弱さを見てしまっているからなのだと最近気が付いた。これからは暖かく見守ってあげよう。

λ. 拡張子

ファイルの拡張子でアプリケーションに関連づけるというのは、窓OSに限らずにわりと色々な場面で使われている。でも、ディレクトリに拡張子をつけるという話は聞いたことがない。ファイルに拡張子を付けるのならば、ディレクトリにも付けるのが自然に思えるが、いったい何故だろうか?

λ. 生け垣オートマトン: XML スキーマの形式的モデル

.

λ. 資本主義経済の幻想

• 「コモンセンスとしての経済学」という副題は気に入った
• 訳はイマイチかも。p.137に「ネットで見て 〜」という部分があるけど、 一般向きの本なのだから、普通は「ネット」って「正味」って訳すんでないの?
• 「解題」は毒にも薬にもならないので余計

λ. ねじの回転 〜 FEBRUARY MOMENT

恩田陸 の「ねじの回転」が、1月号の小説すばるで完結した。

予想を裏切る終り方。いや、そうでもないか?　ともかく連載ご苦労様でしたって感じ。

λ. Classificationと情報射の圏

19日に「チャネル理論のClassificationは情報射を射とする圏をなすようだ」と書いた。証明は簡単なんだけど、このままだとClassificationや情報射の定義を忘れてしまいそうなので、Classificationと情報射の定義を含めてメモしておこう。

定義

オブジェクト(= Classification)

オブジェクト A は、

• タイプの集合 typ(A)
• トークンの集合 tok(A)
• トークンとタイプの間の関係 ⊨_A

の組。

射(= 情報射)

射 f: A→B は、α∈typ(A), b∈tok(B) について f_tok(b) ⊨_A α iff b ⊨_B f_typ(α) であるような

• f_typ: typ(A)→typ(B)
• f_tok: tok(B)→tok(A)

の組。

射の結合

射 f: A→B, g: B→C の結合 gf: A→C を、

• (gf)_typ = g_typf_typ
• (gf)_tok = f_tokg_tok

と定義する。

恒等射

恒等射 1_A: A→A を

• (1_A)_typ = 1_typ(A)
• (1_A)_tok = 1_tok(A)

と定義する。

証明

射の結合が射になることの証明

射 f: A→B, g: B→C の結合 gf: A→C が射の条件を満たしている事を示す。

• fが射であることより、
  f_tok(b) ⊨_A α iff b ⊨_B f_typ(α)
  ⇒ f_tok(g_tok(c)) ⊨_A α iff g_tok(c) ⊨_B f_typ(α) …(1)
• gが射であることより、
  g_tok(c) ⊨_B β iff c ⊨_C g_typ(β)
  ⇒ g_tok(c) ⊨_B f_typ(α) iff c ⊨_C g_typ(f_typ(α)) …(2)

(1),(2)より、
(gf)_tok(c) ⊨_A α iff c ⊨_C (gf)_typ(α)
∴ gfは射

射の結合律

f: A→B, g: B→C, h: C→D について、

• (h(gf))_typ = h_typ(g_typf_typ) = (h_typg_typ)f_typ = ((hg)f)_typ
• (h(gf))_tok = (gf)_tokh_tok = f_tokg_tokh_tok = f_tok(hg)_tok = ((hg)f)_tok

∴ h(gf) = (hg)f

1_Aが射であることの証明

1_A: A→A は、 α∈typ(A), a∈tok(A) について、定義より明らかに、

• (1_A)_tok(a) = 1_tok(A)(a) = a
• (1_A)_typ(α) = 1_typ(A)(α) = α

よって、 (1_A)_tok(a) ⊨_A α iff a ⊨_A (1_A)_typ(α) であり、1_Aは射である。

恒等射

• f: B→Aについて、
  • (1_A・f)_typ = 1_typ(A)・f_typ = f_typ
  • (1_A・f)_tok = f_tok・1_tok(A) = f_tok
  ∴ 1_A・f = f
• g: A→C について、
  • (g・1_A)_typ = g_typ・1_typ(A) = g_typ
  • (g・1_A)_tok = 1_tok(A)・g_tok = g_tok
  ∴ g・1_A = g

∴ 1_Aは恒等射