脳ざらし紀行

_ [ネット] 不動点演算子Yの何が嬉しいか

専門じゃないんで適当に書きますが。というか、今日調べたことなんですが。研究もせずに何やってんだかという感じですが。

不動点演算子Yの何が嬉しいか。define やletrecを使わずにラムダ式だけで再帰的な関数を定義できるとかじゃないでしょうか。

(let ((fact (lambda (n)
                 (if (= n 0)
                     1
                     (* n (fact (- n 1)))))))
  (print (fact 10)))

これはエラー。

(letrec ((fact (lambda (n)
                 (if (= n 0)
                     1
                     (* n (fact (- n 1)))))))
  (fact 10)) ;=> 3628800

letrecを使えば、OK。letrecを使わなくても、Yを使えば、

(let ((fact (Y (lambda (fact)
                (lambda (n)
                  (if (= n 0)
                      1
                      (* n (fact (- n 1)))))))))
  (fact 10)) ;=> 3628800

Yを定義するのにdefineを使っていますが、式を短くするためだけに使っているのでOKです。

(define  Y
  (lambda (F)
    ((lambda (s)
       (F (lambda (x) ((s s) x))))
     (lambda (s)
       (F (lambda (x) ((s s) x)))))))

Yを良くみて下さい。Yの定義には再帰を使っていません。自分に自分を適用している (s s) の部分が非常に怪しいですが、これは再帰ではありません。Yを使えば、再帰のないところから再帰をつくり出すことができます。

さて、再帰といえば思い出すのが再帰的関数です。だからYもそこら辺と関係しているのではないかと見当がつきます。実際その通りのようです。今日調べてきました。

再帰的関数であることとTuring機械で計算可能であることは同値であることが良く知られています。

同じように再帰的関数であることとラムダ定義可能であることは同値だそうです。今日調べてきました。

で、同値であることを証明するのに不動点演算子Yが使われるようです。

どうでもいいですが、ラムダ計算の世界では始めはラムダ式と変数しかない(リストさえない)ので、帰納的関数を作るには数字を定義する必要があって、

まずこれが0です。λxy.y

(lambda (x)
  (lambda (y)
    y))

1はこれです。λxy.xy

(lambda (x)
  (lambda (y)
    (x y)))

2です。λxy.x(xy)

 (lambda (x)
  (lambda (y)
    (x (x y))))

以下続く。という本当にラムダしかない世界のようです。

詳しいことは「Expressiveness of the Lambda Calculus」をどうぞ。

_ [ネット] ラムダ式な数字

ラムダ式で数字を表すのつづき。

ラムダ式で表された数字を1増やす。

(define S
  (lambda (z)
    (lambda (x)
      (lambda (y)
        (x ((z x) y))))))

これを使って、Schemeの型としての数字からラムダ式な数字に変換する。

(define num2lambda
  (lambda (num)
    (if (= num 0)
        (lambda (x)
          (lambda (y)
            y))
        (S (num2lambda (- num 1))))))

ラムダ式な数字をSchemeの型としての数字になおす。

(define lambda2num
  (lambda (lm)
    ((lm (lambda (y) (+ y 1))) 0)))

ラムダ式な数字同士を足します。

(define sum
  (lambda (x)
    (lambda (y)
      (lambda (a)
        (lambda (b)
          ((x a) ((y a) b)))))))

(lambda2num ((sum (num2lambda 2))
             (num2lambda 3))) ; => 5

こんな感じです。