ラムダ計算で整数(負の数)を扱う
ラムダ計算において、自然数を扱う方法はよく知られている。
一方で、整数や負の数を扱う方法については、あまり知られていないように思われる。
そこで、ラムダ計算において整数を扱う方法を1から考えてみた。
この記事では、ラムダ計算とチャーチ数の知識を仮定する。
整数の定義
自然数(チャーチ数)を拡張し、整数を作ることを考える。
まず初めに思いつくのは、自然数に符号を持たせるという方法だろう。
しかし、その方法では、0の表現が唯一通りにならない。(+0と-0)
そのため、別の方法を考える必要がある。
次に思いつく方法としては、自然数のsuccをpredで置き換えるという方法がある。
この方法で、自然数を表現すると以下のようになる。
...... -2 = λp. λs. λz. p (p z) -1 = λp. λs. λz. p z 0 = λp. λs. λz. z 1 = λp. λs. λz. s z 2 = λp. λs. λz. s (s z) ......
今回は、この方法で表現された整数を扱うことにする。
真偽値の定義
二値の比較などの演算を用意するためには、まず、真偽値とその演算を用意する必要がある。
真、偽、not、and、orは以下のように定義される。
true = λt. λf. t false = λt. λf. f not = λb. b false true and = λb. λc. b c false or = λb. λc. b true c
単項論理演算の定義
整数に対して、ゼロであるか(iszero)、非正であるか(isnonpos)、非負であるか(isnonneg)、負であるか(isneg)、正であるか(ispos)を判定する関数を作ると以下のようになる。
iszero = λn. n (and false) (and false) true isnonpos = λn. n (or true) (and false) true isnonneg = λn. n (and false) (or true) true isneg = λn. n (or true) (and false) false ispos = λn. n (and false) (or true) false
このように、単項論理演算は簡単に作れることがわかる。
単項算術演算の定義
まず、符号反転invを定義する。
これは簡単にできる。
inv = λn. λp. λs. n s p
次に、succとpredを定義する。
実は、今回扱う関数の中で、難しいのはsuccとpredだけである。
そのsuccとpredも、自然数のsuccとpredを理解していれば、それほど難しくない。
まず、補助関数を用意する。
s+ = λn. λp. λs. λz. s (n p s z) p+ = λn. λp. λs. λz. p (n p s z) sp- = λn. λp. λs. λz. n (λx. λy. y (x p)) (λx. λy. y (x s)) (λy. z) (λx. x)
s+, p+はそれぞれs, pを1つ加えるという動作をする。
これは、自然数のsuccからすぐに作れる。
sp-はsまたはpを1つ除くという動作をする。
こちらも、自然数のpredから作ることができる。
それらを組み合わせれば、整数のsuccとpredができる。
succ = λn. (isnonneg n) (s+ n) (sp- n) pred = λn. (isnonpos n) (p+ n) (sp- n)
二項算術演算の定義
二項算術演算として、足し算、引き算、掛け算を作ると以下のようになる。
add = λn. λm. m pred succ n sub = λn. λm. m succ pred n mul = λn. λm. m (λx. sub x n) (add n) 0
自然数の場合と対応した非常にきれいな形で書けるので面白い。
二項論理演算の定義
単項論理演算と引き算を利用するだけなので、今までで一番簡単である。
== = λn. λm. iszero (sub n m) <= = λn. λm. isnonpos (sub n m) >= = λn. λm. isnonneg (sub n m) < = λn. λm. isneg (sub n m) > = λn. λm. ispos (sub n m)
まとめ
ラムダ計算において、整数は自然数と同じくらい扱いやすく、多くの関数が非常にきれいな形で書けることが分かった。
これだけ簡単に整数を扱うことができるのなら、ラムダ計算で整数を扱うというテーマはもっと取り上げられてもよいのではないかと思った。
ラムダ計算の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
