HelloRusk

reading and coding ...

ラムダ計算と自然数の演算

1/3/2020, 2:38:47 PM - 449 days ago

自然数の表現

基本構成子 $Z$ (zero) と $S$ (successor) を引数として受け取り、対応する値を返す関数として表現する。

\begin{aligned} 0 = \ & \lambda s. \lambda z. z \\ 1 = \ & \lambda s. \lambda z. s z \\ 2 = \ & \lambda s. \lambda z. s (s z) \\ 3 = \ & \lambda s. \lambda z. s (s (s z)) \\ ... \end{aligned}

Python での実装例:

zero  = lambda s: lambda z: z
one   = lambda s: lambda z: s(z)
two   = lambda s: lambda z: s(s(z))
three = lambda s: lambda z: s(s(s(z)))

確認用に、ラムダ式で表された自然数を int に変換して表示する関数を定義しておく。

def print_nat(nat):
    print(nat(lambda n: n+1)(0))

print_nat(zero)
# 0
print_nat(three)
# 3

足し算

自然数 $m$ と $n$ が与えられたとき、 $Z$ に $S$ を $n$ 回適用し、さらにそれに対して $S$ を $m$ 回適用すれば、 $m+n$ が得られる。

Plus = \lambda m. \lambda n. \lambda s. \lambda z. m s (n s z)

plus = lambda m: lambda n: lambda s: lambda z: m(s)(n(s)(z))

print_nat(plus(two)(three))
# 5

かけ算

自然数 $m$ と $n$ が与えられたとき、 $0$ に $Plus \ \ m$ を $n$ 回適用すれば、 $m \times n$ が得られる。

Mult = \lambda m. \lambda n. n (Plus \ m) \ 0

mult = lambda m: lambda n: n(plus(m))(zero)

print_nat(mult(two)(three))
# 6

べき乗

自然数 $m$ と $n$ が与えられたとき、 $1$ に $Mult \ \ m$ を $n$ 回適用すれば、 $m^n$ が得られる。

Exp = \lambda m. \lambda n. n (Mult \ m) \ 1

exp = lambda m: lambda n: n(mult(m))(one)

print_nat(exp(two)(three))
# 8

引き算

準備として、まずラムダ計算で「組」を表すことを考える。組は

\lambda f. f M N

このように表す。つまり、組の要素にアクセスする関数 $f$ を受け取り、 $M, N$ に適用する関数である。

組からの要素の取り出しは

Fst (P) = P (\lambda x. \lambda y. x) \\ Snd (P) = P (\lambda x. \lambda y. y)

となる。
以上を実際にプログラミング言語で実装してみよう。

fst = lambda p: p (lambda x: lambda y: x)
snd = lambda p: p (lambda x: lambda y: y)

example_pair = lambda f: f(2)(3)
fst (example_pair)
# 2
snd (example_pair)
# 3

さて、この組に対して、

Next(x, y) = (x+1, x)

というような、組を引数にとって組を返す関数 $Next$ を作る。
このとき、 $Next$ を $n$ 回合成した $Next^n$ を考え、それに $(0, 0)$ を引数として与えると、

Next^n (0, 0) = (n, n-1)

となる。よって

Pred = \lambda n. Snd (Next^n(0, 0))

とすれば、 $Pred$ は与えられた自然数から1を引く関数となる（ただし、0が与えられたら0を返す）。

$Pred$ を使うことで引き算 $Minus$ も構成できる。
自然数 $m$ と $n$ が与えられたとき、 $m$ に $Pred$ を $n$ 回適用すれば、 $m-n$ が得られる。

Minus = \lambda m. \lambda n. n \ Pred \ m

以上を実際にプログラミング言語で実装してみよう。

# next は予約語なので nex にする
nex = lambda p: lambda f: f( plus(fst(p))(one) )(fst(p))
# (0, 0)
zero_zero = lambda f: f(zero)(zero)

pred = lambda n: snd(n(nex)(zero_zero))

minus = lambda m: lambda n: n(pred)(m)

print_nat(minus(three)(one))
# 2
print_nat(minus(three)(two))
# 1