pred

なんか最近プログラムの記事ばっかなので、今日は趣向を変えると見せかけてまたプログラムの記事。

Church 数の前者関数は、ペアを使って

let pred n = fst (n (fun (x,y) -> (y,y+1)) (0,0))

みたいにすると割と簡単に作れるものの、かなり複雑になる。機械的にλ式に変換すると、

pred = λn.n(λpx.x(p(λxy.y))(λsz.s(p(λxy.y)sz)))
            (λx.x(λsz.z)(λsz.z))
            (λxy.x)

この時点ですでに頭が痛くなってくるが、さらに Scheme でベタに書いちゃったりすると

(define (pred n)
  (((n (lambda (p) (lambda (x)
         ((x (p (lambda (x) (lambda (y) y))))
          (lambda (s) (lambda (z) (s (((p (lambda (x) (lambda (y) y))) s) z))))))))
    (lambda (x) ((x (lambda (s) (lambda (z) z))) (lambda (s) (lambda (z) z)))))
   (lambda (x) (lambda (y) x))))

ぎょぇぇー。

しかしこの pred、なんか知らんが

pred = λnsz.n(λxy.y(xs))(λx.z)(λx.x)

とするだけであっさり定義できちゃうらしい。こんなもんどうやったら思い付くんだ…？

試しに Scheme で実行してみるとこんな感じ。

gosh> (define (pred n)
  (lambda (s) (lambda (z)
    (((n (lambda (x) (lambda (y) (y (x s))))) (lambda (x) z)) (lambda (x) x)))))
pred
gosh> (define (n->c n) (lambda (s) (lambda (z)
  (let loop ((n n) (z z)) (if (< n 1) z (loop (- n 1) (s z)))))))
n->c
gosh> (define (c->n n) ((n (lambda (x) (+ x 1))) 0))
c->n
gosh> (c->n (pred (n->c 10000)))
9999

ペア版と比べて格段に高速。すげー！ でも覚えられない！