不動点コンビネータによる再帰の実現を解説する

課題

code:ml

factorial = \n ->

if n = 1 then 1

else n * factorial n-1

こういった関数定義は、再帰の構造をしている

再帰をせずに、この定義ができないか？

表現方法

code:ml

factorial_impl = \f -> \n ->

if n = 1 then 1

else n * f n-1

自分自身を表す関数を、引数fとして受け取れば、構文上の再帰が消える

当然、型が異なるので、元のfactorialをこれを使って表すなら、

code:ml

factorial = factorial_impl ???

たとえばこのような形で、正しいfactorialが欲しい

しかし、???に入るべきはなんだったかというと、\fにわたすものであり、関数自身である

code:ml

factorial = factorial_impl factorial

これでは、この記述上で、factorialが再帰してしまっている

よって、この右辺をfactorialを使わずに表現しなければ、やりたかったことにはならない

我々が欲しいのは、factorialの定義に、factorialを使わない方法である

factorial = __do_somthing_with__{factorial_impl}

天下り的、とは書いたが、「再帰を含まない形のimplを渡すと、良しなに求めたい関数に変換してくれるF」とも見れる

そのようなFが存在するとしたら、Fはどのような性質が要求されるだろうか？

このとき

code:ml

factorial = F factorial_impl //仮定

factorial = factorial_impl factorial // factorial_implの前提より

この２式より

F Factorial_impl = factorial_impl factorial

= factorial_impl (F factorial_impl)

言い換えると、「Fは、aを受けて、aの不動点を返す」という性質を持つ、といえる

逆に言えば、これを満たすようなFが存在すれば、問題は解けたことになる

さて、そのようなFが存在するのか、というと、存在するのである

このFの定義にfactorialやそのimplの関数は出てこない。一般に成立する関数として存在する

F x = x (F x)

Y = (λf. (λx. f (x x)) (λx. f (x x)))

実際, Y fを簡約すると以下のようになる

code:ml

Y f = (λx. f (x x)) (λx. f (x x))

= f ( (λx. f (x x)) (λx. f (x x)) )

//これはf (Y f)に等しい

よって、以下が求めたかった,再帰を用いないfactorialの定義である

code:ml

factorial = Y factorial_impl

実は、正格評価の場合に、これは問題がある

code:ml

Y f = (λx. f (x x)) (λx. f (x x))

= f ( (λx. f (x x)) (λx. f (x x)) )

= f (Y f) // ←ここで、正格評価の場合、(Y f)を先に評価してしまう

なので、

code:ml

Y f = f (Y f)

= f (f (Y f))

= f (f (f (Y f)))

...

となり、無限ループしてしまう

遅延評価であれば、先に左側を評価するので問題ない

関数適用のfの方を適用して、その後に内側を評価するので、必要に応じて再帰を繰り返す形になる

そこで、先にfの評価を進むためには、この(Y f)の部分を(\y Y f y)のように関数でwrapした形になっていると良い

そうすれば、引数部分は簡約できないので、こいつをfに適用するステップに進める

すなわち以下を満たすような別のコンビネータであれば良い

code:ml

Z f = f (\y Z f y)

code:ml

Z = λf. (λx. f (\y x x y)) (λx. f (\y x x y))

確認

code:ml

Z f = λx. f (\y x x y)) (λx. f (\y x x y)

Z f = f (\y ((λx. f (\y x x y)) (λx. f (\y x x y))) y)

また

f (\y Z f y) = f (\y ((λx. f (\y x x y)) (λx. f (\y x x y))) y)

となり、たしかにZ f = f (\y Z f y)

実際、factorialの例で正格評価を行うと

code:ml

factorial = Z impl

= (λf. (λx. f (\y x x y)) (λx. f (\y x x y))) impl

= (λx. impl (\y x x y)) (λx. impl (\y x x y))

(λx. impl (\y x x y))をhとして

= h h

= (λx. impl (\y x x y)) h

= impl (\y h h y)

=== ここが、factorialに相当する

implに対して引数fとして利用された際に

impl内でf nがあり、

code:ml

f n

= (\y h h y) n

= h h n

factorialを評価するとh hになったわけだが

impl内のfは、(\y (h h) y)が渡され、遅延評価されてh hと同じになる

結果的に、implの引数fにh hを渡したときと同じ形になっている

---

jsでやってる記事見つけた

評価順を無視して書いたら分かりやすいが、そうすると遅延評価する意味がわからなくなる