Natural Number Encoding (Church Style)

church-encoding.scm

;;;;
;;;; Church encoding
;;;;
;;;; ラムダ計算で自然数を符号化する方法
;;;;
;;;; 基本的アイディア：
;;;; one(f, x) = f(x)
;;;; two(f, x) = f(f(x))
;;;; three(f, x) = f(f(f(x)))
;;;; ...
;;;; n(f, x) = f^n(x)
;;;; zero(f, x) = f^0(x) = x
;;;; (n+1)(f, x) = f(f^n(x)) = f^n(f(x))
;;;;
;;;; ラムダ計算：
;;;; f(x) = expr のとき，f は関数自体であって f = λx.expr = (lambda (x) expr)
;;;;
;;;; α変換： λx.f(x) = λ(y).f(y)
;;;; β変換： (λx.f(x))(a) = f(a)
;;;; η変換： λx.f(x) = f
;;;; 
;;;; zero  f x = x      ; zero  = λ(f,x).x = (lambda (f x) x)
;;;; one   f x = f(x)   ; one   = (lambda (f x) (f x))
;;;; two   f x = f^2(x) ; two   = (lambda (f x) (f (f x)))
;;;; three f x = f^3(x) ; three = (lambda (f x) (f (f (f x))))
;;;;
;;;; (n f x) = (f^n)(x)
;;;; (succ n) f x = f^{n+1}(x) = (f (f^n x)) = (f (n f x))
;;;;                           = (f^n (f x)) = (n f (f x))
;;;; (sunc n)     = (lambda (f x) (f (n f x)))
;;;;              = (lambda (f x) (n f (f x)))
;;;;

(define (succ church)
  (lambda (f x) (church f (f x))))

(define (zero f x) x)
(define (church-zero? f)
  (equal? f zero))

(define one   (succ zero))
(define two   (succ one))
(define three (succ two))
(define four  (succ three))
(define five  (succ four))
(define six   (succ five))
(define seven (succ six))
(define eight (succ seven))
(define nine  (succ eight))
(define ten   (succ nine))

(define (number->church n)
  (if (zero? n)
      zero
      (lambda (f x) (f ((number->church (- n 1)) f x)))))

;;;;
;;;; チャーチ符号化した結果は関数なので，プログラム上で見たり比べたりできない。
;;;; しかし f と x に具体的な値を与えることで，他の自然数モデルに変換できる。
;;;; f には後者関数 (successor) を，x には零を表すデータを与える。
;;;;
;;;; (church->number N) = (N 1+ 0)
;;;;     where (1+ x) = (+ 1 x)
;;;; (church->list N) = (N s '())
;;;;     where (s x) = (cons 's x)
;;;; (church->neumann N) = (N double-cons '())
;;;;     where (double-cons x) = (cons x x)
;;;; (church->fraction N) = (N to-1 0)
;;;;     where (to-1 x) = (x + 1) / 2


(define (1+ n) (+ 1 n))
(define (s  x) (cons 's x))
(define (double-cons x) (cons  x x))
(define (to-1 x) (* 1/2 (+ x 1)))

(define (church->number church)
  (church 1+ 0))
(define (church->list church)
  (church s '()))
(define (church->neumann church)
  (church double-cons '()))
(define (church->fraction church)
  (church to-1 0))

;;;; 
;;;; Church 符号化では f の逆関数を与えれば，前者関数を定義できる。
;;;;
;;;; N        f x = f^n(x)
;;;; (pred N) f x = f^{n-1}(x) = f^{-1}(f^n(x))
;;;; pred N       = (lambda (f x) (f-inv (N f x)))
;;;;
;;;; しかし，Scheme では lambda の入れ子が深くなるだけで，構造が簡単になることはないので，使いにくい。
;;;;