脱関数化を実用する 6 - shiatsumat/fp-papers GitHub Wiki

6 結論と論点

レナルズの脱関数化のテクニックは高階のプログラムの世界と一階のプログラムの世界とをつなげる。この記事では、私たちは脱関数化が宣言型の状況において有用であると分かるようなさまざまな状況を考えてこのつながりを説明してきた。

高階の関数は仕様の記述とプログラムの変換を便利に支えてくれる。これまでに示したように、脱関数化は、一階の蓄積引数を使うなどしている、より具体的な仕様をもたらす。ワンドの継続ベースのプログラム変換の戦略で見たように、脱関数化はデータ型の継続を表すヒラメキを自動化できるのだ。

逆に、脱関数化はある一階のプログラムが他の高階のプログラムと対応していることをよりはっきり認識するきっかけにもなる。例えば、構文論の評価環境が継続に対応するということを見た。別の例を挙げれば、バックトラッキングのある言語に対する関数型の解釈器は、1つか2つのスタックを持つ形、あるいは1つか2つの継続を持つ形で記述することができる。しかし、継続ベースの解釈器を脱関数化すると対応するスタックベースの解釈器が生まれるので、両者の記述は関係が無いわけではない。それに関連して、継続が1つある解釈器をCPS変換すると自動的に2つの継続を持つ解釈器が生まれることがすでに知られている [[12](脱関数化を実用する 8#reference12)]。しかし私たちは、スタックベースの解釈器に対する同様の変換を知らない。

更に私たちはプログラムの正当性証明を脱関数化の前後で比較対照した。そして一階と高階のプログラミングの方法が異なる証明方法を示唆するものの、それぞれの証明が他方のバージョンのプログラムと適合させられうるということを見た。

最後に、私たちは脱関数化の型理論的基礎を指摘した。