Church Numerals と Lambda Calculus

アルゴリズムとデータ構造入門補足

後半は佐藤雅彦先生に教えてもらいました.

SICP Exercise 2.4 ～ Exercise 2.6

誤解を恐れずに大雑把にいうと, λ計算では名前つきのシンボル (名前付きの手続き) による再帰呼出しや special form が使えないところが Scheme と違うところです. そのため, λ計算を Scheme で行うためにはいろいろな工夫が必要となります. そのポイントは closure (閉包) と呼ばれる構造です.

自然数 n の Church numeral を c(n) とすると,

    c(n) f x = (f ... (f x)), ただし, f は n 回出現.

となることを利用します.

まず, c0 と successor を定義します. (SICP Ex.2.6 参照)

    (define c0 (lambda (f) (lambda (x) x)))
    (define (%succ c)
      (lambda (f) (lambda (x) (f ((c f) x)))) )

この考えは, 右図 (Lao Tsu TAO TE CHING, Vintage Book, 394-71833-X) に示した『老子』第42節の 「道 (TAO) から一が生まれ, 一から二が生まれ, 二から三が生まれ, 三から万物が生まれ, 云々」と符合するものです.
Backus 記法が導入された Algol-68 Revised Report にも上記の一節が引用されています. それ以外にも, "The TAO of Pooh" (もちろん, Pooh は Winnie the Pooh のこと) や, プログラミング言語 TAO なんていうのもあります.

今定義した c0 と successor から, 次々と Church numeral を定義していきます.

    (define c1 (%succ c0))
    (define c2 (%succ c1)) あるいは (define c2 (%succ (%succ c0)))
    (define c3 (%succ c2))
つまり
    (define c1 (lambda (f) (lambda (x) (f x))))
    (define c2 (lambda (f) (lambda (x) (f (f x)))))
    (define c3 (lambda (f) (lambda (x) (f (f (f x))))))

Church numeral を使った add (加算), multiply (乗算), power (冪乗) は次のように定義できます.

    (define (%add n m)
      (lambda (f) (lambda (x) ((m f) ((n f) x)))) )

    (define (%multiply n m)
      (lambda (f) (lambda (x) ((n (m f)) x))) )

    (define (%power n m)
      (lambda (f) (lambda (x) (((m n) f) x))) )

実際の動きを見るために, 入出力の関数を定義しましょう.

   (define (c->n c)
     ((c (lambda (x) (+ 1 x))) 0) )

   (define (n->c n)
     (if (> n 0)
         (%succ (n->c (- n 1)))
         c0 ))

上記の c->n はメモリを大量に消費し遅いので, 下記の定義を使うべき.

    (define (c->n c) ((c 1+) 0))

では実験.

   (c->n (%add (n->c 5) (n->c 3)))
   (c->n (%multiply (n->c 5) (n->c 3)))
   (c->n (%power (n->c 5) (n->c 3)))
   (c->n (%add (%power c2 c3) (%multiply c3 (n->c 4))))

ここからが本題です. 比較を名前のない (裸の)λ式で定義します.

まず, λ計算での真偽 (true, false) と条件式 (if-then-else) を定義しましょう.

   (define (%true x) (lambda (y) x))
   (define (%false x) (lambda (y) y))
   (define (%if c x y) ((c x) y))

次に, pair (対) というデータ構造を定義します. pair の constructor と selectors である cons, car, cdr は次のように定義されます. (SICP Ex.2.4 参照)

    (define (%cons x y) (lambda (p) ((p x) y)))
    (define (%car x) (x %true))
    (define (%cdr x) (x %false))

ゼロチェックは次のように定義します. ここで, c0 が %false と同じ定義であることを思い出して下さい.

    (define (%iszero? c)
      ((c (lambda (z) %false)) %true) )

大小関係は次のように定義します.

    (define (%gt a b)
      (%car
        ((b (lambda (z) (%if (%car z) (%cdr z) z)))
         ((a (lambda (z) (%cons %true z)))
          (%cons %false %false) ))))

a 個の %true の並びの後に, %false からなる次のようなリストを作成します.
```
    (%true %true %true %true %true ...  %false ・ %false)
```
Church numeral b は (if (car z) (cdr z) z) というλ式を上記のリストに b 回適用を試みます. ただし, b > a のときは, a 個の %true が尽きたところで (%false ・ %false) となるので, その時点以降は cdr down は終ります. (お分かりですか)

実例を見てみましょう.

    (%gt c0 c1)
    (%gt c2 c1)
    (%gt c2 c2)
    (%gt (n->c 10) (n->c 8))

ゼロチェックは %gt を用いて次のように定義することもできます.
```
    (define (%iszero?? c)
      (%if (%gt c 0) %false %true) )
```

1つ前のChurch Numeral を求める %pred は次のように定義します.

    (define (%predp c)
      ((c (lambda (z) ((z (lambda (x) x)) (%succ z))))
       (lambda (a) (lambda (x) c0)) ))

    (define (%pred c)
      (%if (%gt c c0) (%predp c) c0) )

では, 減算を定義しましょう. n-m は, %pred をm回適用すればよいので, 下記のようになります.

    (define (%subtract n m)
      ((m %pred) n) )

階乗は, 再帰呼出しの部分に工夫が必要です.

    (define (fact c)
      ((%if (%iszero? c)
            (lambda () c1)
            (lambda () (%multiply c (fact (%pred c)))) )))

この手続きで, 正しい答が求まります. しかし, 再帰呼出しで fact という名前つきのλ式を使っています.

まず, Y combinator を定義します.

    (define Y
      (lambda (f)
        ((lambda (x) (f (lambda (arg) ((x x) arg))))
         (lambda (x) (f (lambda (arg) ((x x) arg)))) )))

これにより, f で手続きを定義して, 再帰呼出しを行います. 具体的には, 次のように定義します.

    (define Y-fact
      (Y
       (lambda (fact)
         (lambda (n)
           ((%if (%iszero? n)
                 (lambda () c1)
                 (lambda () (%multiply n (fact (%pred n)))) ))))))

    (c->n (Y-fact c2))
    (c->n (Y-fact (n->c 10)))

このY combinator は, 不動点を求める手続きになっています.

    (Y f) = (f (Y f))

除算と剰余も定義しましょう.

    (define (%le a b) (%iszero? (%subtract a b)))
    (define (%ge a b) (%le b a))

    (define (%remainder divd divr)
      ((Y (lambda (f)
           (lambda (x)
             ((%if (%ge x divr) 
                   (lambda () (f (%subtract x divr)))
                   (lambda () x) )))
           ))
       divd ))

    (c->n (%remainder (n->c 30) c3))
    (c->n (%remainder (n->c 100) (n->c 9)))

    (define (%divide divd divr)
      ((Y (lambda (f)
           (lambda (x)
             ((%if (%ge x divr) 
                   (lambda () (%succ (f (%subtract x divr))))
                   (lambda () c0) )))
           ))
       divd ))

    (c->n (%divide (n->c 100) (n->C 9)))

上記の Y combinator は1引数しか許さないので, Y-fact はうまくに書けますが, %remainder や %divide は Y combinator にさらにもう 1つの引数を与えてやる必要があります.

2引数版の Y combinator の定義とそれを応用した %remainder2 と %divide2 を次に示します.

    (define Y2
      (lambda (f)
        ((lambda (x) (f (lambda (a b) ((x x) a b))))
         (lambda (x) (f (lambda (a b) ((x x) a b)))))))

    (define %remainder2
      (Y2 (lambda (f)
            (lambda (divd divr)
              ((%if (%ge divd divr) 
                    (lambda () (f (%subtract divd divr) divr))
                    (lambda () divd) ))))))


    (define %divide2
      (Y2 (lambda (f)
            (lambda (divd divr)
              ((%if (%ge divd divr) 
                    (lambda () (%succ (f (%subtract divd divr) divr)))
                    (lambda () c0) ))))))

終りに

これで, 型なしλ計算が Scheme の上で自由にできることになりました. コードも公開します.
型付きλ計算では, 上記のような処理がもっとやさしくなります.
詳しくは, 佐藤先生の「計算と論理」で学んで下さい. 講義のページ
参考情報: λ計算 (佐藤先生からの情報)

Back to アルゴリズムとデータ構造入門　　講義関係のページ　　 2004年度データ構造

Copyleft (C) 2004-2005. All wrongs reserved.
Last modified: Mon Jan 3 17:10:56 2005
奥乃博

Church Numerals と Lambda Calculus

アルゴリズムとデータ構造入門 補足

アルゴリズムとデータ構造入門補足