日々の流転

λ. 花粉症?

このところ目が何か変な感じ。これって、ひょっとして、ひょっとすると、花粉症ってやつ?

λ. Parametricty and Mulry's Strong Dinaturality - A. Eppendahl

20061013#p03 を参照。

λ. Free Theorems in the Presence of seq - P. Johann and J. Voigtländer

スライド

The Impact of seq on Free Theorems-Based Program Transformations, Janis Voigtländer

seqが存在すると、関係を連続かつ正格なものに制限してもパラメトリシティは成り立たない。

foldr c n (build g) = g c n の反例

• g = seq, c = ⊥, n = 0
• g = λc n → seq n (c ⊥ ⊥), c = (:), n = ⊥

そこで、関係にさらに制約を加えることが考えられるが、 この論文では等式的な論理関係(equational logical relation)ではなく、不等号的な論理関係(inequational logical relation)にしている。 foldr/build に関する新しい定理は次にようになる。

• foldr c n (build g) ≧ g c n
• if c ⊥ ⊥ ≠ ⊥ and n ≠ ⊥, then: foldr c n (build g) = g c n

関係に対する幾つかの概念:

正格性(strictness)

(⊥,⊥)∈R

連続性(continuity)

∀i.(x_i,y_i)∈R ⇒ (∨x_i,∨y_i)∈R

全域性(totality)

∀(x,y)∈R. x≠⊥ ⇒ y≠⊥

left-closedness

≦;R = R

λ. (co)free でない代数的データ型

• 難しい点
  • word problem (語の問題)
  • (co)induction に証明が必要

λ. 蔵王で遭難の韓国人一行、捜索費用の支払い拒む

（・Д・）ポカーン・・・　　（⊇⊆）ゴシゴシ　　（・Д・）ポカーン・・・

「文化、国民性の違い」ってのはいいとしても、何でそこで「竹島」が出てくるんだか。