原です。

>正木です。

>|そして、これを Proc に当てはめます。ここからはかなりいい加減な話で
>|す。今、不動点定理で、F = V = Proc と思います。そして、a の定義を
>|
>|  a(x, y) = x[y]
>|
>|とおくと、これは定理の条件を満たします。なぜなら、任意の
>|
>|  h: Proc -> Proc
>|
>|に対して f0 = h とおけば a(f0, f) = f0[f] = h[f] だからです。
>
>ここの所で Proc の要素は同時に
>Proc**Proc={ f | f: Proc -> Proc }
>の要素になっていて、その逆も成り立つことを仮定しているように読めます:
>Proc**Proc = Proc
>これは Proc が2個以上の要素を持つ限り有り得ないことですが、
>この辺の事情はどうなっていますか?

いやあ、だからいい加減な話だって言ったでしょう?
おっしゃる通りです。(^^;

普通はこの定理は本来は圏論的に述べられるので、「全ての写像は」とい
言葉は、ほんとは「全ての射は」と言うべきですね。圏論なんてもったい
ぶらずとも、「これこれの条件を持つ全ての写像について、あれが言える
とすると、これこれの条件を持つ全ての写像には不動点がある。」という
形になる、と言えば良いかな。

しかし、この定理を「従ってそのような a(x, y)」は存在しない。」とい
うように背理法的に使うならば、その圏すなわちその写像の条件について、
厳密に設定しないといけないですが、今回のように肯定的に使う場合、不
動点がみつかってナンボの話ですから、つまり発見的推論の補助に使って
いるだけなんで、厳密さはテキトーです。実際、一度見つかればそれが不
動点である事の証明は厳密にできるわけですから。