reading and coding ...

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

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

自然数の表現

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

0= λs.λz.z1= λs.λz.sz2= λs.λz.s(sz)3= λs.λz.s(s(sz))...\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

足し算

自然数 mmnn が与えられたとき、ZZSSnn 回適用し、さらにそれに対して SSmm 回適用すれば、m+nm+n が得られる。

Plus=λm.λn.λs.λz.ms(nsz)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

かけ算

自然数 mmnn が与えられたとき、00Plus  mPlus \ \ mnn 回適用すれば、 m×nm \times n が得られる。

Mult=λm.λn.n(Plus m) 0Mult = \lambda m. \lambda n. n (Plus \ m) \ 0
mult = lambda m: lambda n: n(plus(m))(zero)

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

べき乗

自然数 mmnn が与えられたとき、11Mult  mMult \ \ mnn 回適用すれば、 mnm^n が得られる。

Exp=λm.λn.n(Mult m) 1Exp = \lambda m. \lambda n. n (Mult \ m) \ 1
exp = lambda m: lambda n: n(mult(m))(one)

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

引き算

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

λf.fMN\lambda f. f M N

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

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

Fst(P)=P(λx.λy.x)Snd(P)=P(λx.λy.y)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(x, y) = (x+1, x)

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

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

となる。よって

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

とすれば、PredPred は与えられた自然数から1を引く関数となる(ただし、0が与えられたら0を返す)。

PredPred を使うことで引き算 MinusMinus も構成できる。
自然数 mmnn が与えられたとき、mmPredPrednn 回適用すれば、mnm-n が得られる。

Minus=λm.λn.n Pred mMinus = \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