あらすじ:しくぴー Exercise 2.6. で チャーチ数(Church numerals)という謎の概念が登場して、足したりかけたりできるってところまではわかって書けたものの引き算を書こうと思った途端さっぱりわからなくなって(特に wikipedia の pred ≡ λn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u) あたり)悶死したので無理やりやってみたらなんだか残念な感じになった予感がしたのでフテ寝。

参考資料

とりあえず zero を定義する。

(define zero (lambda (f) (lambda (x) x)))

これは簡単。関数 f を食うものの、引数 x を f に食わせないでそのまま返す。 zero(f, x) -> x というイメージ。で、one は one(f, x) -> f(x)、two は two(f, x) -> f(f(x)) なので

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

こうなる。これ以上はだるいので succ を

(define (succ n)
  (lambda (f) (lambda (x) (f ((n f) x)))))

こんな感じで定義すると

(define one (succ zero))
(define two (succ one))
...

と、無限に作ることが可能になる。で、チャーチ数の足し算/かけ算/m^n は

(define (plus m n)
  (lambda (f) (lambda (x) ((m f) ((n f) x)))))

(define (mult m n)
  (lambda (f) (lambda (x) ((m (n f)) x))))

(define (exp m n)
  (lambda (f) (lambda (x) (((n m) f) x))))

こんな感じになる。が、こいつは全部チャーチ数の話なので、目で見て確認できない。というわけでチャーチ数を可視化する方法を考える。

(define (ch->int n)
  *1

チャーチ数 n に"引数 x を受け取って x+1 を返す関数"を食わせて、引数として 0 を食わせることで整数にしている。手で書いて確かめてみると zero(f, 0) -> 0、one(f, 0) -> (0+1) = 1、two(f, 0) -> ((0+1)+1) = 2 となる。

次に引き算を考えてみたものの……さっぱりわからない。あまりにもわからないので チャーチ数 -> 整数 の逆、整数 -> チャーチ数 を作って無理やりやってみた。まず

(define (int->ch n)
  (if (= n 0)
      zero
      (succ (int->ch (- n 1)))))

こんなのを定義する。整数 n が 0 だったら zero を返して、そいつから目的の数まで succ で増やしていくイメージ。こんなんがあると pred も引き算も簡単で

(define (pred n)
  (int->ch (- (ch->int n) 1)))

(define (sub m n)
  (n (pred m)))

こうなる。いや、えー、あー、うん、簡単だけどさ、合ってんのこれ……? つうかこんなんできるなら

(define (plus2 m n)
  (int->ch (+ (ch->int m) (ch->int n))))

(define (mult2 m n)
  (int->ch (* (ch->int m) (ch->int n))))

(define (exp2 m n)
  (int->ch (expt (ch->int m) (ch->int n))))

(define (sub2 m n)
  (int->ch (- (ch->int m) (ch->int n))))

これでいいんじゃね?という気がしてきて非常に残念な予感。

*1:n (lambda (x) (+ x 1))) 0