[ruby-list:35091] Re: Y Combinator

原（信）です。

>コンビネータというのは自由変数を持たない(閉じた)ラムダ式のことをいいま
>すから，結局は同じですね．

ああ、そうなんですか。何となく「結合」みたいに考えていたけど、専門
用語なんですね。

> > さて、ここで思い出したのが「Lawvere の不動点定理」という、昔、森毅
> > さんの『無限集合』（共立出版？）という本で読んだ定理です。これは、
>
>大学で使うλ計算の教科書やプログラム意味論などの教科書などでもたぶん載っ
>ています．

え？載っていますかね。多分 Y を天下りで与えて、それが不動点を与える
事を証明しているだけでは無いですか？ここでのミソは、Lawvere の定理
から、Y を導出しているって所です。Y が不動点を与えることの証明だけ
ならば、

   proc{|f| g[f[f]}[proc{|f| g[f[f]}]  …前の f に後ろの [] の中身を代入
          = g[proc{|f| g[f[f]}[proc{|f| g[f[f]}]

の１行でＯＫでしょう。

「Lawvere の不動点定理」というのは、ゲーデルの不完全性定理や、カン
トールのパラドックス、ラッセルのパラドックス、果ては生物の自己組織
化の解釈に応用されるという、実に妖しい定理なので、なかなかマトモな
教科書で使いこなすのは難しいのではないかと。(^^;


>僕が持っているものだと，同じ共立出版の「プログラミング言語意味論」「プロ
>グラミング言語のための基礎理論」のどちらかにもこのあたりにも話が載ってい
>ます．岩波の白いカバーのやつにもあったと思います．

ウチの大学の図書館にはありませんでした。しょぼいなあ。
見たいなあ。