日々の流転

λ. AVL木

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

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

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

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

• e₁: (T×S)×Y^T×S→Y
• e₂: S×(Y^T)^S→Y^T
• e₃: T×Y^T→Y

e₁ は T×X→Y の形なので、e₃について
e₁ = e₃(1_T×[e₁]) ……(1)

ここで、[e₁]: S×Y^T×S→Y^T は、S×X→Y^T の形なので、e₂について、
[e₁] = e₂(1_S×[[e₁]]) ……(2)
1_T×[e₁] = (1_T×e₂) (1_T×S×[[e₁]]) ……(2')

ところで、e₃(1_T×e₂): T×S×(Y^T)^S→Y は (T×S)×X→Yの形をしているので、e₁について、
e₃(1_T×e₂) = e₁(1_T×S×[e₃(1_T×e₂)]) ……(3)

e₁(1_T×S×[e₃(1_T×e₂)] [[e₁]])
= e₁(1_T×S×[e₃(1_T×e₂)]) (1_T×S×[[e₁]])
= e₃(1_T×e₂) (1_T×S×[[e₁]]) (∵(3))
= e₃(1_T×[e₁]) (∵(2'))
= e₁ (∵(1))

∴ e₁(1_T×S×[e₃(1_T×e₂)] [[e₁]]) = e₁ …(4)

e₃(1_T×e₂) (1_T×S×[[e₁]] [e₃(1_T×e₂)])
= e₃(1_T×e₂) (1_T×S×[[e₁]]) (1_T×S×[e₃(1_T×e₂)])
= e₃(1_T×[e₁]) (1_T×S×[e₃(1_T×e₂)]) (∵(2'))
= e₁(1_T×S×[e₃(1_T×e₂)]) (∵(1))
= e₃(1_T×e₂) (∵(3))

∴ e₃(1_T×e₂) (1_T×S×[[e₁]] [e₃(1_T×e₂)]) = e₃(1_T×e₂) …(5)

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

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