ラムダ計算で整数(負の数)を扱う
ラムダ計算において、自然数を扱う方法はよく知られている。
一方で、整数や負の数を扱う方法については、あまり知られていないように思われる。
そこで、ラムダ計算において整数を扱う方法を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)
まとめ
ラムダ計算において、整数は自然数と同じくらい扱いやすく、多くの関数が非常にきれいな形で書けることが分かった。
これだけ簡単に整数を扱うことができるのなら、ラムダ計算で整数を扱うというテーマはもっと取り上げられてもよいのではないかと思った。
