ラムダ計算の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