トップ «前の日記(2002-04-13) 最新 次の日記(2002-04-15)» 月表示 編集

日々の流転


2002-04-14 [長年日記]

λ. AVL木

暇潰しにAVL木のコードを書いて、バグってたのでムッキー。

[2005-04-19 追記] 不変量を型によって強制することによって、ここで犯したようなミスはほとんど回避できる。詳しくは、AVL木でGADTを試してみる を見よ。

λ. YT×S ≅ (YT)S の証明についてのメモ

map object と evaluation map を以下のようにおく。

  • e1: (T×S)×YT×S→Y
  • e2: S×(YT)S→YT
  • e3: T×YT→Y

e1 は T×X→Y の形なので、e3について
e1 = e3(1T×[e1]) ……(1)

ここで、[e1]: S×YT×S→YT は、S×X→YT の形なので、e2について、
[e1] = e2(1S×[[e1]]) ……(2)
1T×[e1] = (1T×e2) (1T×S×[[e1]]) ……(2')

ところで、e3(1T×e2): T×S×(YT)S→Y は (T×S)×X→Yの形をしているので、e1について、
e3(1T×e2) = e1(1T×S×[e3(1T×e2)]) ……(3)


e1(1T×S×[e3(1T×e2)] [[e1]])
= e1(1T×S×[e3(1T×e2)]) (1T×S×[[e1]])
= e3(1T×e2) (1T×S×[[e1]]) (∵(3))
= e3(1T×[e1]) (∵(2'))
= e1 (∵(1))

∴ e1(1T×S×[e3(1T×e2)] [[e1]]) = e1 …(4)


e3(1T×e2) (1T×S×[[e1]] [e3(1T×e2)])
= e3(1T×e2) (1T×S×[[e1]]) (1T×S×[e3(1T×e2)])
= e3(1T×[e1]) (1T×S×[e3(1T×e2)]) (∵(2'))
= e1(1T×S×[e3(1T×e2)]) (∵(1))
= e3(1T×e2) (∵(3))

∴ e3(1T×e2) (1T×S×[[e1]] [e3(1T×e2)]) = e3(1T×e2) …(5)


[2005-04-19 追記] YT×S ≅ (YT)S は結局初等的な証明は出来るんだっけ? 米田の補題を使えば簡単に言えるけど。

【2008-06-08 追記】 単に米田の補題の証明を展開すればいいだけ。

Tags: 圏論