reading and coding ...

ラムダ計算と再帰

1/2/2020, 2:43:45 PM - 198 days ago

まず、(λx.F(xx))(λx.F(xx))(\lambda x. F(x x)) (\lambda x. F(x x)) という式をβ簡約してみると、

(λx.F(xx))(λx.F(xx))[(λx.F(xx))/x]F(xx)=F((λx.F(xx))(λx.F(xx)))\begin{aligned} & (\lambda x. F(x x)) (\lambda x. F(x x)) \\ \to &[(\lambda x. F(x x)) / x] F(x x) \\ = & F ((\lambda x. F(x x)) (\lambda x. F(x x))) \end{aligned}

となる。つまり MF=(λx.F(xx))(λx.F(xx))M_F = (\lambda x. F(x x)) (\lambda x. F(x x))とおくと、=β=_{\beta} をβ簡約を含む最小の同値関係として、

MF=βF(MF)M_F =_{\beta} F (M_F)

となるから、MFM_F は関数 FF の不動点である。

次に、Y=λf.Mf=λf.(λx.f(xx))(λx.f(xx))Y = \lambda f. M_f = \lambda f. (\lambda x. f(x x)) (\lambda x. f(x x)) とすると、前の結果と同様に、

YF=βF(YF)Y F =_{\beta} F (Y F)

このことから、YY は任意の関数 FF を引数として受け取ってその FF の不動点を返すような関数(不動点演算子)になっていることがわかる。


不動点演算子 YY を使うことで、ラムダ計算で再帰を表現することができる。
表現したい再帰関数 FF がある関数 GG の不動点になっていることが分かれば、YGY G によって FF を定められるという仕組みだ。

例えば、階乗を求める factfact をラムダ計算で表現したいとする。 factfact は等式

f=λn. if n=0 then 1 else nf(n1)f = \lambda n. \ \mathrm{if} \ n = 0 \ \mathrm{then} \ 1 \ \mathrm{else} \ n \cdot f (n - 1)

を満たす。ここで、

factgen=λf.λn. if n=0 then 1 else nf(n1)factgen = \lambda f. \lambda n. \ \mathrm{if} \ n = 0 \ \mathrm{then} \ 1 \ \mathrm{else} \ n \cdot f (n - 1)

と定義してやれば、factfactf=factgen ff = factgen \ f を満たすことになるので、factfactfactgenfactgen の不動点になっていることがわかる。
よって、不動点演算子を用いて fact=Y factgenfact = Y \ factgen と書ける。


実際にプログラミング言語で実装してみよう。ただし、不動点演算子 YY(Yコンビネータと呼ばれる)をこの形のまま乗せることはできない (引数を評価しないまま式が再帰的に展開され、無限ループに陥ってしまうため)。そこで、η変換(Mλx.MxM \to \lambda x. M x)を Yコンビネータに施した、

λf.(λx.f(λy.xxy))(λx.f(λy.xxy))\lambda f. (\lambda x. f(\lambda y. x x y)) (\lambda x. f(\lambda y.x x y))

を代わりに使おう(これはZコンビネータと呼ばれる)。

Python での実装例:

Z = lambda f: (lambda x: f (lambda y: x(x)(y)))(lambda x: f (lambda y: x(x)(y)))

factgen = lambda f: (lambda n: 1 if (n == 0) else n * f (n - 1))

fact = Z (factgen)

fact(10)
# 3628800