λ計算の乱択評価
さて、いわゆる関数型言語の基礎となっているλ計算ですが、一部の言語(eg. Haskell)では厳しく副作用を禁止することでパワフルでありながら参照透過性を維持し、非正格な評価を可能にしています。*1
こうするとうまく評価戦略を選べば*2、λ抽象でない正規形を持つ式は必ず有限時間で評価できて、無限データ構造が使えたりして大変嬉しい訳です。しかし、このような遅延評価を行う言語にはスペースリークの問題があって、例えばfoldl (+) 0 [1..n]等がO(n)のメモリを消費してしまったりします。大量のデータを扱うようなアプリケーションではこれは非常に深刻な問題で、「一行コード追加したらメモリ使いすぎで動かなくなった」みたいなことが発生します。
そこでこのような問題を回避できる(かもしれない)評価戦略として、ランダムにひとつapplicationを選んできてβ簡約することを繰り返す手順を考えてみます。大体の場合うまく行きそうな気がしますが、無限に成長する二分木のようなものがあると、どんどん役に立たない項を選ぶ確率が増えて収束しない場合がありえます。
つまり実際的にはlim_{t->∞}P(E-> ...t... ->NF)>0じゃなくて、lim_{t->∞}P(E-> ...t... ->NF)=1になって欲しいわけですね。無限に大きくなり得る構造を書くとき、それは有限で打ち切られることを期待しているわけですが、そうでなくても積極的に実行して欲しくないなぁというλにはフラグをつけられるような仕組みを考えてみましょう。
そして
- フラグの付いてないλがあればランダムにβ簡約
- なければ正規形 or 一番外側をβ簡約
なんとなくデフォルトで正格でlazinessを明示的に指定する方法(eg. OCaml)と似ている気がしますが、こっちは何も指定しなくても動く(可能性は0ではない)し、消費メモリが少ない時は全部outermost reductionで、増えてきたら先程の戦略に切り替える等、いろいろいじればちょうどいい感じになるパラメータがあるかもしれません。
どうなんでしょう？
