ex2.6 Church数
ex2.6はチャーチ数の問題で、以前に取り組んだ時はweb上の情報をみてもさっぱり分からなかった問題です。
今回いろいろやってみて、何となく分かって来ました。
あと、素のラムダ計算を記述するためには、schemeは絶望的に向いていなそうです。大分慣れたと思っていた括弧の海に再び飲まれてしまいました...。
問題では、以下の２つの関数が示され、1,2の直接表現と足し算関数を定義せよとされています。
(define zero (lambda (f) (lambda (x) x))) (define (add-1 n) (lambda (f) (lambda (x) (f ((n f) x)))))
(add-1 zero)を 置き換えモデルで展開します。
add-1のnをzeroの定義でそっくり置き換えます。zeroで使用している変数をそのまま使うと混乱するので、名前は換えました。
(lambda (f) (lambda (x) (f (((lambda (f1) (lambda (x1) x1)) f) x))))
((lambda (f1) ...) f)でf1をfに置き換えますが、内部では使われていません。そのため、...の部分だけ抜き出せます。
(lambda (f) (lambda (x) (f ((lambda (x1) x1) x))))
((lambda (x1) x1) x)も、結局xに置き換えられます。その結果が、(add-1 zero)の置き換え結果、すなわちoneです。
(lambda (f) (lambda (x) (f x)))
さらに、oneに対してadd-1を適用してみます。
(add-1 (lambda (f) (lambda (x) (f x))))
add-1のnを(lambda (f1) (lambda (x1) (f1 x1)))でそっくり置き換えます。ここでもzeroで使用している変数をそのまま使うと混乱するので、名前は換えました。
(lambda (f) (lambda (x) (f (((lambda (f1) (lambda (x1) (f1 x1))) f) x))))
((lambda (f1) ...) f)は、f1をfに置き換え、lambdaを外します。
(lambda (f) (lambda (x) (f ((lambda (x1) (f x1)) x))))
同様に、((lambda (x1) (f x1) ) x)も、x1をxに置き換えられます。
(lambda (f) (lambda (x) (f (f x))))
以上の置き換えから、Church数の体系では、
- 数とは、fを引数としてとり、xを引数としてとる関数を返す関数である
- 数を1増やすとは、fの適用回数を1回増やすことである
- 数の大きさは、xに対してfを何回適用するかで示される
ということが分かります。
- 数が、xにfを一度も適用しなければ、0
- 数が、xにfを1回適用すれば、1
- 数が、xにfを2回適用すれば、2
- :
ですね。
Church数のままだと、演算結果を確認する方法がないので、表示可能な形式に変換してあげると便利です。
xに対しfが何回適用されたかをschemeの数字に変換してあげるには、xに0、fにinc、つまり(lambda (x) (+ x 1))を渡してあげればよいです。
- Church数 zeroに inc,0を渡すと 0にincが0回適用される => 0
- Church数 zeroに inc,0を渡すと 0にincが1回適用される => 1
- Church数 zeroに inc,0を渡すと 0にincが2回適用される => 2
となり、計算結果がREPLで確認可能となります。
(define (p cn) (define (inc x) (+ x 1)) ((cn inc) 0))
数 1の直接的な定義
(define one (lambda (f) (lambda (x) (f x))))
数 2の直接的な定義
(define two (lambda (f) (lambda (x) (f (f x)))))
数 3の直接的な定義
(define three (lambda (f) (lambda (x) (f (f (f x))))))
確認してみます。
;; (p zero) ;; => 0 ;; (p (add-1 zero)) ;; => 1 ;; (p one) ;; => 1 ;; (p (add-1 (add-1 zero))) ;; => 2 ;; (p two) ;; => 2 ;; (p three) ;; => 3
よさそうです。
足し算の定義
インタフェースは、
(plus-cn a b) ;; a: Church数 ;; b: Church数
とします。
まず fにaを適用(a f)します。これでxに対してfをa回適用する関数が得られます。
bも同様(b f)です。
xに対して(b f)を適用したものに対して、(a f)をさらに適用するとxにfをa+b回適用したことになります。
(define (plus-cn a b) (lambda (f) (lambda (x) ((a f) ((b f) x))))) ;; (p (plus-cn two three)) ;; => 5 ;; (p (plus-cn zero three)) ;; => 3
Church数はおもしろそうなので、もう少し掘り下げてみます。
べき乗の定義
(expt-cn a b) ;; a: Church数 ;; b: Church数
とします。
べき乗の定義は、実は「問題1.41、doubleの定義」にヒントがありました。
doubleの定義は、
(define (double f) (lambda (x) (f (f x))))
ですが、これは以下と等価です。
(define double (lambda (f) (lambda (x) (f (f x)))))
そしてこれは、Church数の2と全く同じ定義です。つまり、doubleはChurch数だったのです。
そして、問1.41では、(((double (double double) ) inc) 5)の値は何かと聞いています。
この答えは21だったのですが、解析の途中で、(double double)がfを引数にとり、xに対しfを4回適用する関数を返す関数を返すことが分かります。つまりchurch数の4ですね。
これにさらにdoubleを適用すると、4回適用する関数に4回適用する関数を適用することとなり、fを引数にとり、xに対しfを16回適用する関数を返す関数を返すことが分かりました。4*4の演算ですね。
このことから類推すると、Chuch数にChuch数を適用するとべき乗が計算できそうです。
;; (p (two two)) ;; => 4 : 2*2 ;; (p (two (two two))) ;; => 16 : (2 * 2) * (2 * 2) ;; (p (three (two two))) ;; => 64 : (2 * 2) * (2 * 2) * (2 * 2)
どうやら出来そうです。
(define (expt-cn a b) (b a)) ;; (p (expt-cn three three)) ;; => 27 ;; (p (expt-cn three (add-1 three))) ;; => 81
掛け算の定義
(mul-cn a b) ;; a: Church数 ;; b: Church数
とします。
まず fにbを適用(b f)します。これでxに対してfをb回適用する関数が得られます。
(b f)をa回適用すれば、掛け算を行ったことになります。
(define (mul-cn a b) (lambda (f) (lambda (x) ((a (b f)) x)))) ;; (p (mul-cn zero one)) ;; => 0 ;; (p (mul-cn two three)) ;; => 6 ;; (p (mul-cn three two)) ;; => 6 ;; (p (mul-cn one one)) ;; => 1
1を引く関数
これは厄介。
+1はfへnを適用した結果にfを再度適用するだけだったので(まだ)簡単でしたが、
1度だけ適用されないようにするというのをどうすればよいのでしょうか?
とりあえずWikipediaの「ラムダ計算」を参考に、答えは見ずに、途中でちらっとみえたif関数を導入してみます。
ifは、関数適用のためのカッコが多くなったので、3引数の関数としておきます。
(define true-cn (lambda (a)(lambda (b) a))) (define false-cn (lambda (a)(lambda (b) b))) (define if-cn (lambda (bool tr fl) ((bool tr) fl))) ;; (if-cn true-cn 1 2) ;; => 1 ;; (if-cn false-cn 1 2) ;; => 2
つぎにzeroかどうかを判定する関数を考えます
Chuch数では、xにfを適用するのだから、fが適用されたらfalse-cnになるようなfがあればよいです。
つまり、fは無条件でfalse-cnを返し、xをtrue-cnとすればよいことになります。
(define (is-zero-cn n) ((n (lambda (x) false-cn)) true-cn)) (define (cn->bool bool) ((bool #t) #f)) ;; (cn->bool (is-zero-cn zero)) ;; => #t ;; (cn->bool (is-zero-cn one)) ;; => #f
これらの条件式を用いて、最初の関数適用か、最後の関数適用を
skipできないかどうかを考えてみます。
(f (f (f .... (f x))))
上の形からすると、一番内側でごまかすのがよい気がします。
つまり、fとxをなんらかの関数でくるんでどうにか最初の適用を逃れ、その後は普通に適用させる作戦です。
- f'(x) = x ただし0回めの場合
- f'(x) = f(x) ただし0回目ではない場合
となるようなf'を定義できれば 1引くことができます。
0回めだけ適用しないということは、一度だけ特殊な処理をすればよいということです。
一度だけという条件を一引数で満たすために、対を定義してみます。
これは問2.4で定義したものと同じですね。
(define (cons-cn car-val cdr-val) (lambda (bool) ((bool car-val) cdr-val))) (define (car-cn pair) (pair true-cn)) (define (cdr-cn pair) (pair false-cn)) ;; (car-cn (cons-cn 1 2)) ;; => 1 ;; (cdr-cn (cons-cn 1 2)) ;; => 2
ここまでツールができれば、sub-1が書けます。
(define (sub-1 n) (lambda (f) (lambda (x) (cdr-cn ((n (lambda (pair) (if-cn (car-cn pair) (cons-cn false-cn (cdr-cn pair)) (cons-cn false-cn (f (cdr-cn pair)))))) (cons-cn true-cn x)))))) ;; (p (sub-1 one)) ;; => 0 ;; (p (sub-1 two)) ;; => 1
答えが出来たので、ここで、Wikipediaの「ラムダ計算」のPREDの定義と見比べてみます。
(define (pred n) (lambda (f) (lambda (x) (((n (lambda (g) (lambda (h) (h (g f))))) (lambda (u) x)) (lambda (u) u)))))
さすがに簡潔ですね。
原理がよく分からないので、例によってtwoに適用して置き換えてみます。
nをtwoの定義で置き換えます。twoのfはf1にxはx1に置き換えます。
(lambda (f) (lambda (x) ((((lambda (f1) (lambda (x1) (f1 (f1 x1)))) (lambda (g) (lambda (h) (h (g f))))) (lambda (u) x)) (lambda (u) u))))
f1を(lambda (g) ...)で置き換えます
ここでfがn個分展開されます。
(lambda (f) (lambda (x) (((lambda (x1) ((lambda (g) (lambda (h) (h (g f)))) ; <-f ((lambda (g) (lambda (h) (h (g f)))) ; <-f x1))) (lambda (u) x)) (lambda (u) u))))
x1を(lambda (u) x)で置き換えます
(lambda (f) (lambda (x) (((lambda (g) (lambda (h) (h (g f)))) ((lambda (g) (lambda (h) (h (g f)))) (lambda (u) x))) (lambda (u) u))))
下の段のgを(lambda (u) x)で置き換えます。
ここでfが一つ消えますね。
このgとhの折込まれたような適用が肝のようです。
最初の適用でfが一つ消えた後は、fがn-1回適用されます。
一番最後に残った(lambda (h) ...)へidを適用することで、つじつまをあわせているようです。
(lambda (f) (lambda (x) (((lambda (g) (lambda (h) (h (g f)))) (h ((lambda (u) x) f))) (lambda (u) u)))) (lambda (f) (lambda (x) (((lambda (g) (lambda (h) (h (g f)))) (lambda (h) (h x))) ; <- fが消えた (lambda (u) u))))
gを(lambda (h) ...)で置き換えます
(lambda (f) (lambda (x) ((lambda (h) (h ((lambda (h) (h x)) f))) (lambda (u) u))))
内側のhをfで置き換えます。
(lambda (f) (lambda (x) ((lambda (h) (h (f x))) (lambda (u) u))))
hをuで置き換えます。
(lambda (f) (lambda (x) ((lambda (h) (h (f x))) (lambda (u) u))))
uを置き換えます。
(lambda (f) (lambda (x) ((lambda (u) u) (f x))))
oneになりました。
(lambda (f) (lambda (x) (f x)))
原理は何となく分かりましたが、とても思いつきそうにありません。
