トップ «前の日記(2003-01-14) 最新 次の日記(2003-01-16)» 月表示 編集

日々の流転


2003-01-15 [長年日記]

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

λ. 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でEP,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'
Tags: CPL