ラムダ計算のpredを理解する
チャーチ数に対する前者関数predは、足し算や掛け算などの他の関数に比べ、理解がしにくく作るのが難しいように思われる。
この記事は、pred を理解することを目的とする。
定義
ラムダ計算では自然数は以下のように表現することができ、これをチャーチ数と言う。
0 = λs. λz. z 1 = λs. λz. s z 2 = λs. λz. s (s z) 3 = λs. λz. s (s (s z)) ......
チャーチ数に対する演算として、後者関数、足し算、掛け算、累乗はそれぞれ、以下のように表せる。
succ = λn. λs. λz. s (n s z) add = λn. λm. m succ n mul = λn. λm. m (add n) 0 pow = λn. λm. m (mul n) 1
このように、簡単にできる。
前者関数は以下のように表せる。
pred = λn. λs. λz. n (λx. λy. y (x s)) (λx. z) (λx. x)
これは、難しい。
なぜなら、n は2回引数を受け取る関数であるのに、n の後ろに項が3つあるからだ。
つまり、pred は2つの動作が1つの関数にまとめられており、それによって難しく感じるのだと考えられる。
predの理解
pred を理解するために関数を2つの部分に分ける。
pred = λn. erase (replace n) replace = λn. λs. λz. n (λx. λy. y (x s)) (λy. z) erase = λm. λs. λz. m s z (λx. x)
このとき replace は以下のような動作をする。
replace 0 = replace (λs. λz. z) = λs. λz. λy. z replace 1 = replace (λs. λz. s z) = λs. λz. λy. y z replace 2 = replace (λs. λz. s (s z)) = λs. λz. λy. y (s z) replace 3 = replace (λs. λz. s (s (s z))) = λs. λz. λy. y (s (s z))
つまり、replace は最も外側の s を y に置き換えるという動作をしている。
また、erase は y を消すという動作をしているということがわかる。
これで、pred の動作が理解できた。
分かってみれば、非常に単純である。
predの作成
pred を作ることを考える。
erase は恒等関数 (λx. x) を与えているだけなので、難しくない。
replace が作れれば良い。
replace = λn. λs. λz. n s' z'
として、s' と z' を求めればよい。
replace 0 = λs. λz. z' = λs. λz. λy. z
よって、z' = λy. z である。
replace 1 = λs. λz. s' z' = λs. λz. s' (λy. z) = λs. λz. λy. y z replace 2 = λs. λz. s' (s' z') = λs. λz. s' (λy. y z) = λs. λz. λy. y (s z)
したがって、s' は2回引数を受け取る関数であり、λx. λy. y (???) という形をしていることがわかる。
z' の形状から、s' = λx. λy. y (x s) とするとうまくいく。
これで pred ができる。
おまけ
pred関数を少し変形すると(チャーチ数に対する)恒等関数idや、後者関数succになる。
pred = λn. λs. λz. n (λx. λy. y (x s)) (λx. z) (λx. x) id = λn. λs. λz. n (λx. λy. y (x s)) (λx. z) s id' = λn. λs. λz. n (λx. λy. y (x s)) (λx. x z) (λx. x) succ = λn. λs. λz. n (λx. λy. y (x s)) (λx. x z) s