日々の流転

λ. やばいやばいやばいやばいやばい……

λ. 日本のインフレターゲッティング政策FAQ

.

λ. CPL

きゅぴーん!。curryがλ抽象に見えてキター

• K = curry(pi1)
• S = curry(curry(eval.pair(eval.pair(pi1.pi1, pi2), eval.pair(pi2.pi1, pi2))))
• I' = curry(I.pi2)
• K' = curry(K.pi2)
• S' = curry(S.pi2)

と定義する。当然「eval.pair(eval.pair(S', K'), K') = I'」は成り立って欲しいのだけど、実際に「simp full eval.pair(eval.pair(S', K'), K')」としてみると 「curry(eval.pair(eval.pair(pi1.pi1, pi2), eval.pair(pi2.pi1, pi2)). pair(pair(curry(curry(pi1).pi2. pair(pi1, pi2).pair(pi1, pi2).pair(pi1, pi2).pair(pi1, pi2).pair(pi1, pi2)), curry(curry(pi1).pi2.pair(pi1, pi2).pair(pi1, pi2).pair(pi1, pi2))).pi1, pi2))」 になってしまった。

FULL-C-FACTでE_P,jがRそのものでない場合にはfactorizerの引数がelement(terminal objectをdomainとする射)でないので、通常の簡約を行えないのが原因。ad-hocな対処は簡単だけど、どうするのが良いのかな?

とりあえず、自己満足のために「eval.pair(eval.pair(S', K'), K')」の続きを手計算してみよう。

• = curry(eval.pair(eval.pair(pi1.pi1, pi2), eval.pair(pi2.pi1, pi2)). pair(pair(curry(curry(pi1).pi2), curry(curry(pi1).pi2)).pi1, pi2))
• = curry(eval.pair(eval.pair(pi1.pair(curry(curry(pi1).pi2), curry(curry(pi1).pi2)).pi1, pi2), eval.pair(pi2.pair(curry(curry(pi1).pi2), curry(curry(pi1).pi2)).pi1, pi2)))
• = curry(eval.pair(eval.pair(curry(curry(pi1).pi2).pi1, pi2), eval.pair(curry(curry(pi1).pi2).pi1, pi2)))
• = curry(eval.pair(eval.pair(curry(curry(pi1).pi2).pi1, pi2), eval.pair(curry(curry(pi1).pi2).pi1, pi2)))
• = curry(eval.pair(curry(pi1).pi2, curry(pi1).pi2))
• = curry(eval.pair(curry(pi1).pi1, pi2).pair(pi2, curry(pi1).pi2))
• = curry(pi1.pair(pi2, curry(pi1).pi2))
• = curry(pi2)
• = I'