Y combinator
挑戦した。解いた顛末をそのまま dump するという、まさしく (そして珍しく)「日記」な内容。
∀f, f(Yf) = Yf ←これを逆から読む。すると Y = λg.g(Yg) になることがわかる。これをさらに naïve に展開すると
Y = λg.g(Yg) = λg.g(λh.h(Yh))g = λg.g(λh.h((λi.i(Yi))h))g = …
となって、展開が終わらない。これじゃ意味ないよー。
…とか思ったのだけど、これでいいのだ。そもそも Y は「再帰の本質」を閉じ込めた操作符であって、その本質はと言えば循環参照、つまり有限回数の dereference で解決できない参照のことであるから、無限展開が生じるのは当り前。
そこで Practical Scheme のどっかに書いてあったことを思い出す。「λは遅延構文である」。まる。そっか、展開って「評価」の事なんですね。当り前か。ということは、Y は「自分を生じる S 式」を含むわけで、式を代入と展開でいじくり回して Y =
で、ここでちょっとズルをして (というか選択肢がなかった) 既に頭の片隅にあった
(λx.xx)(λx.xx)
という式を思い出してみる。こいつだ。でもこいつは quine っていうか、自分を生成はするけどそれを返さない _|_ なので、遅延が足りてない。よって、どこかをλで遅延しないといけない。とりあえず
(λx.λ_.xx)(λx.λ_.xx)
と挿入してみたけど、これだと展開結果の頭に "λ_." が出現する。というわけで元のにそれを加えて
λ_.(λx.λ_.xx)(λx.λ_.xx)
{検証: a=(λx.λ_.xx) とおくと↑の式はλ_.aa。これを適当な引数に適用すると結果は (λx.λ_.xx)a = λ_.aa。}
おお、s/_/g/g して両脇に g つけたら Y になるんではなかろか!?
Y=λg.g( (λx.λh.h(xxh)) (λx.λh.h(xxh)) g ) 検証: b := λx.λh.h(xxh) とおくと Y = λg.g(bbg) であって、 bb = (λx.λh.h(xxh))b = λh.h(bbh) = Y そこで Yf = f(bbf) = f(Yf)
でけた! しかしこの感じだと、quine なら何でもそれから出発して Y に仕立てあげられそうなんだけど、何か間違ってるんだろうか。
追記: quine というより _|_ な式か。んー?
- 自分を生成するけど
- それを返さずに _|_ る式
だな。…Y に仕立てられて当り前だ。
とか思ったら、Gauche に打ち込んでみてもうまく動かない (Y 使用時に memory を食いつぶして死ぬ)。純粋なλ算法では正しそうだから、遅延をどこか間違えてるっぽい。Haskell だと動くかしら。
追記: ああ、そういや何かどっかで "applicative-order Y" だの何だの言ってたな。上記の証明が normal-order でやってるからか。むむむ、もう一種類用意する必要があるのか。いいや、今日はここまで。
追記: んが、λ算法の適用って left-associative だった。括弧入れないと…
