読者です 読者をやめる 読者になる 読者になる

ラムダ計算で整数(負の数)を扱う

プログラミング ラムダ計算

ラムダ計算において、自然数を扱う方法はよく知られている。
一方で、整数や負の数を扱う方法については、あまり知られていないように思われる。
そこで、ラムダ計算において整数を扱う方法を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)

まとめ

ラムダ計算において、整数は自然数と同じくらい扱いやすく、多くの関数が非常にきれいな形で書けることが分かった。
これだけ簡単に整数を扱うことができるのなら、ラムダ計算で整数を扱うというテーマはもっと取り上げられてもよいのではないかと思った。