β簡約(beta.ml)

 

いきなり例ですが、たとえばlet x = y in x + yのような式があったら、xyが等しいことは明らかですから、x + yy + yと置き換えてしまうことができます。このような変換をK正規形のβ簡約といいます(λ計算という理論でもβ簡約という言葉がありますが、それの特殊な場合になっています)。普通のプログラムだと、あまり必要な処理でもないのですが、他の最適化等をした後のプログラムでは効果がある場合もあります。

 

MinCamlでは、関数Beta.gがβ簡約の処理をしている本体です。ある変数からそれに等しい変数への写像envと、式eとを受け取り、eをβ簡約した式を返します。やはりポイントはlet x = e1 in e2の場合で、e1をβ簡約した結果が変数yだったら、xからyへの対応をenvに追加して、e2をβ簡約します。そして、変数xが出てきたら、envを引いて、変数yに置き換えてしまいます。ただしK正規形では、ありとあらゆる式に変数が出てくるので、この置換のための関数findを定義・使用しています。

 

次へ進む