ラムダ計算と再帰
1/2/2020, 2:43:45 PM - 384 days ago
まず、(λx.F(xx))(λx.F(xx)) という式をβ簡約してみると、
→=(λx.F(xx))(λx.F(xx))[(λx.F(xx))/x]F(xx)F((λx.F(xx))(λx.F(xx))) となる。つまり MF=(λx.F(xx))(λx.F(xx))とおくと、=β
をβ簡約を含む最小の同値関係として、
MF=βF(MF) となるから、MF は関数 F の不動点である。
次に、Y=λf.Mf=λf.(λx.f(xx))(λx.f(xx)) とすると、前の結果と同様に、
YF=βF(YF) このことから、Y は任意の関数 F を引数として受け取ってその F の不動点を返すような関数(不動点演算子)になっていることがわかる。
不動点演算子 Y を使うことで、ラムダ計算で再帰を表現することができる。
表現したい再帰関数 F がある関数 G の不動点になっていることが分かれば、YG によって F を定められるという仕組みだ。
例えば、階乗を求める fact をラムダ計算で表現したいとする。 fact は等式
f=λn. if n=0 then 1 else n⋅f(n−1) を満たす。ここで、
factgen=λf.λn. if n=0 then 1 else n⋅f(n−1) と定義してやれば、fact は f=factgen f を満たすことになるので、fact は factgen の不動点になっていることがわかる。
よって、不動点演算子を用いて fact=Y factgen と書ける。
実際にプログラミング言語で実装してみよう。ただし、不動点演算子 Y(Yコンビネータと呼ばれる)をこの形のまま乗せることはできない
(引数を評価しないまま式が再帰的に展開され、無限ループに陥ってしまうため)。そこで、η変換(M→λx.Mx)を Yコンビネータに施した、
λf.(λx.f(λy.xxy))(λx.f(λy.xxy)) を代わりに使おう(これは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)