1/3/2020, 2:38:47 PM - 383 days ago
基本構成子 (zero) と (successor) を引数として受け取り、対応する値を返す関数として表現する。
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
自然数 と が与えられたとき、 に を 回適用し、さらにそれに対して を 回適用すれば、 が得られる。
plus = lambda m: lambda n: lambda s: lambda z: m(s)(n(s)(z))
print_nat(plus(two)(three))
# 5
自然数 と が与えられたとき、 に を 回適用すれば、 が得られる。
mult = lambda m: lambda n: n(plus(m))(zero)
print_nat(mult(two)(three))
# 6
自然数 と が与えられたとき、 に を 回適用すれば、 が得られる。
exp = lambda m: lambda n: n(mult(m))(one)
print_nat(exp(two)(three))
# 8
準備として、まずラムダ計算で「組」を表すことを考える。組は
このように表す。つまり、組の要素にアクセスする関数 を受け取り、 に適用する関数である。
組からの要素の取り出しは
となる。
以上を実際にプログラミング言語で実装してみよう。
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
さて、この組に対して、
というような、組を引数にとって組を返す関数 を作る。
このとき、 を 回合成した を考え、それに を引数として与えると、
となる。よって
とすれば、 は与えられた自然数から1を引く関数となる(ただし、0が与えられたら0を返す)。
を使うことで引き算 も構成できる。
自然数 と が与えられたとき、 に を 回適用すれば、 が得られる。
以上を実際にプログラミング言語で実装してみよう。
# 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