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

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

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

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