[ruby-list:35060] Re: Y Combinator

続いて、ちょっと数学っぽい解釈をします。先の

  S = proc{|x| x[x]}
  Y = proc{|g| S[proc{|f| g[proc{|z| S[f][z]}]}]}

ですが、なんとなくできちゃった感じで、もう少し理論的な見方が
無いかと考えたのですが、この問題は実は不動点問題だと気づきま
した。というのは

  fact = proc{|f| proc{|n| n == 0 ? 1 : n * f[n-1]}}

は、Proc オブジェクト f に fact[f] という Proc オブジェクト対
応させる関数 Proc -> Proc です。ここでもし

  fact[f0] = f0

となる不動点 f0 がみつかれば、これは

  proc{|n| n == 0 ? 1 : n * f0[n-1]} = f0

を意味するので、f0 が求める階乗を表す関数になるはずです。
つまり問題は

  fact : Proc -> Proc の不動点を求めよ

あるいは、

  任意の g : Proc -> Proc に対して、その不動点 Y[g] を与える
  Y を求めよ

と表現できます。

この見方は、「不動点」という言葉こそないけれど、「日々の流転」
で紹介された URL:

  http://www.itlabs.umn.edu/HyperNews/get/gopalan/courses/CSCI8980-fall-2001/classwork/2.html

にも若干見られます。（今、たまたま「論理と計算」（岩波講座・応用
数学）を見たら Y にはまさに「不動点演算子」という名前があるみた
いですね。）

さて、ここで思い出したのが「Lawvere の不動点定理」という、昔、森毅
さんの『無限集合』（共立出版？）という本で読んだ定理です。これは、
対角線論法を定式化したもので、種々のパラドックスをがこの形に表現で
きるというものですが、やさしいので、定理と証明を書いてしまいます。

  [不動点定理] F, V をものの集まりとし、写像

    a: F x F -> V

  が次の条件を満たすとする。

    「全ての写像 h: F -> V に対し、ある F の要素 f0 が存在して、

      a(f0, f) = h(f)   (f の関数として)

    がいえる」

  このとき、全ての写像 g: V -> V には不動点が存在する。

  [証明] h(f) = g(a(f, f)) に対する上の f0 を取り、

    v0 = a(f0, f0)

  とおけばよい。なぜなら　a(f0, f) = h(f) = g(a(f, f)) より、f に
  f0 を代入すれば、a(f0, f0) = g(a(f0, f0)) 。つまり v0 = g(v0)。

そして、これを Proc に当てはめます。ここからはかなりいい加減な話で
す。今、不動点定理で、F = V = Proc と思います。そして、a の定義を

  a(x, y) = x[y]

とおくと、これは定理の条件を満たします。なぜなら、任意の

  h: Proc -> Proc

に対して f0 = h とおけば a(f0, f) = f0[f] = h[f] だからです。

さて、ここで[証明]における、g: Proc -> Proc の不動点 v0 を求めて
みます。[証明]に倣うと h(f) = g(a(f, f)) = g[f[f]] と置きますが、
これは

  h = proc{|f| g[f[f]]}

と置くことです。よって、

  v0 = a(f0, f0) = a(h, h) = h[h]
     = proc{|f| g[f[f]]}[proc{|f| g[f[f]]}]

となり、これが求める g の不動点でした。

しかしこのままだと、以前と同様に、後ろの f[f] を評価した時に無限
ループになります。そこで、f[f] に遅延評価を施すと、最初の

  proc{|g|
    proc{|f|
      g[f[f]]
    }[
      proc{|f|
        g[proc{|y| f[f][y]}]
      }
    ]
  }

が得られます。


以上は「解釈」に過ぎないので、何か新しい発見があるわけではないの
ですが、「対角線論法を肯定的に使う」アリガターイ例ではないかと思
います。

最後の部分、遅延評価させる場所を特定する一般的な方法があれば、更
に面白いのですが、、、難しい。