SICP問題2.6

SICP

Church数(Church numerals)の問題。
0と1を足す演算の定義

(define zero (lambda (f) (lambda (x) x)))
(define (add-1 n)
  (lambda (f) (lambda (x) (f ((n f) x)))))

ためしに実行してみる。

(add-1 zero)
; #<closure (add-1 add-1)>
(zero add-1)
; #<closure (zero zero)>

ん? 良く分からんので、ためしに guile でも動かしてみる

(add-1 zero)
; #<procedure #f (x)>
(zero add-1)
; #<procedure #f (f)>

うーん。ますます良く分からないのでChurch数をネットで調べてみると

要は、ある数は、ある関数fを何回xに適用するか、という定義にしてしまうのである。

404 Blog Not Found:TuringとChurchの狭間で

しかし、ここでの特徴は、「普通の数値に戻す」ことではなくて、「関数をそのまま数として扱う」ということにある。

404 Blog Not Found:TuringとChurchの狭間で

ということらしい。

ここで先ほどの zero について考えてみると

(lambda (f) (lambda (x) x))
; => (lambda (f) (lambda (x) x))
; => (lambda (x) x)
; => (x)

と f を一回も適用していない x を返すので、ゼロだということらしい。
次に (add-1 zero) してみる。(add-1 n) は

(lambda (f) (lambda (x) (f ((n f) x))))

なので

(add-1 zero)
; => ((lambda (f) (lambda (x) (f ((n f) x)))) zero)
; => (lambda (f) (lambda (x) (f ((zero f) x))))
; => (lambda (f) (lambda (x) (f ((lambda (x) x) x))))
; => (lambda (f) (lambda (x) (f x)))
; => (lambda (f) (f x))
; => (f x)

ということで x に f を一回適用したので one になる。

以上のことから one の定義は以下のようになる

(define one (lambda (f) (lambda (x) (f x))))

ということで確認してみる。(そもそも zero も add-1 もちゃんと確かめられていないし)
確認のために以下のような inc を定義する

(define (inc n) (+ n 1))
(define (church-to-int c) ((c inc) 0))

確認。

(church-to-int zero)
; 0
(church-to-int one)
; 1
(church-to-int (add-1 zero))
; 1
(church-to-int (add-1 one))
; 2

次は two の定義。f を x に適用した回数だからは以下のようになる

(define two (lambda (f) (lambda (x) (f (f x)))))

確認。

(church-to-int two)
; 2
(church-to-int (add-1 two))
; 3

ヨサゲ。次は加算手続き。
加算は one + two だと (f x) + (f (f x)) = (f (f (f x))) という感じになればよいはず。
ちなみにλ記法では

  zero = λfx.x 
   one = λfx.fx
   two = λfx.ffx
 three = λfx.fffx

となるので、上記の式は

 λfx.fx + λfx.ffx = λfx.fffx

となる。以下が実装。

(define (church+ m n)
  (lambda (f) (lambda (x) ((m f) ((n f) x)))))

ということでカンニングしながらなんとか完成。

(church-to-int (church+ one two))
; 3
(church-to-int (church+ one zero))
; 1
(church-to-int (church+ zero one))
; 1
(church-to-int (church+ zero two))
; 2
(church-to-int (church+ two two))
; 4

ついでにテスト用に three, four も定義

(define three (lambda (f) (lambda (x) (f (f (f x))))))
(define four (lambda (f) (lambda (x) (f (f (f (f x)))))))