2013/05/20

プログラム運算

(2015/01/07修正)

 プログラム運算というのがあるらしい。
最初に見た時は、演算のtypoかと思ったけど、それとは違うらしい。
英語では、「calculational programming」というらしい。
プログラムの最適化手法の一種で、あるプログラムをプログラムの意味を変えずに、変換していくことでより効率的なプログラムに書き換える手法なのだそうです。この手法とコンパイラにおける最適化との違いは、アルゴリズム(抽象)レベルで最適化するか、変換後のコードを最適化するかという違いのようです。

エレガントで綺麗なコード(ただし遅い) → 高速なコード(ただし、汚く読みにくい)

「→」は「数学的理論(プログラム意味論)に基づいた変換」です。
速度的な面から見た、プログラム/アルゴリズムのリファクタリングってことなのかな?

例えば、関数型言語で記述された(速度を考慮していない)フィボナッチ数列を返す関数は、数学的な表現をそのまま表すこができ、非常に綺麗ですが、重たいです。それを、プログラムの意味を数学的な表現に落とし込み、数学的に変形する(もちろん、高速化されることは大前提という)ことで、数学的な等価性から、プログラムの等価性を証明するってことのようです。 (フィボナッチ数列の計算が運算によって高速化できるのかはわかりません.)
最適化すると同時に、その最適化が適切であることを証明する(保証する)ことができると。
 ちなみに、この変換自体は、基本的に人が手で行う模様…… 
(以下, 2015/01/07追記)
 ある意味では, 関数型言語の実行速度のチューニングの一種と言えるのかもしれませんね.

 基本的に手作業に勝るプログラム運算はありませんが, 自動化するシステムもいくつか開発されているようです. 日本語で読める書籍としては, 少なくとも以下の二冊があります(他にもあるかもしれませんが).
  • 関数プログラミングの楽しみ, Jeremy Gibbons & Oege de Moor(編集), 山下 伸夫 (翻訳)
  • 関数プログラミング入門 ―Haskellで学ぶ原理と技法―, Richard Bird (著), 山下伸夫 (翻訳)
 『関数プログラミング入門』については, 自動運算器の解説があります. 『関数プログラミングの楽しみ』でも, 同様に運算(融合変換)の自動化とその実装例であるMAGシステムの説明がありました.

 手作業で出来る簡単な例として, このブログでは, map分配則と, hylomorphismについて紹介しています.

 以下の文献が見つかりました。まだ、読んでないのですが。
参考文献

  • 定理証明支援系 Coq を用いたプログラム運算

  • 融合変換による関数プログラムの最適化

  • 構成的アルゴリズム論
  • 0 件のコメント :