等価変換型プログラムをかじる
ETの理論が示したパラダイムシフト
ETの枠組みの画期的な点は、仕様と手続きの理論を分けて、その間の関係性(仕様に対する正当性関係)とそれに基づくプログラム合成を中心に考えた理論であることです。
明確に仕様と手続きが分かれており、仕様をプログラムとして実際に動作させる必要が無いので、仕様は無限の確定節による記述なども許される、非常に広範囲の問題を表現できる宣言的記述となっています。また、従来のプログラムの最適化は、プログラム自体の意味を変えない最適化に限定されていましたが、ETの枠組みは仕様に対して正当な手続きという概念をよりどころとしているため、拡張されたより広い手続きの空間で効率的なプログラムを探索できるようになります。
つまり、ETの枠組みでは、本当に重要なのは仕様に対する正当性と位置付けられているので、正当性関係を満たしている限り、どんな手続きでも許されます。ETの枠組みから見ると、従来の意味での最適化という概念はナンセンスなものにさえ思えます。
例えるならば、国の法律が変わったのに、会社内の仕事のやり方(プログラム)は昔のままで、そのルールの中で競争を行い(最適化し)、成果を挙げようと頑張っているようなものです。重要なのは、大本の法律(仕様)であり、法律が変わったならば、仕事のやり方(プログラム)自体も変える必要があります。そこで法律の範囲内でさらにうまいやり方を考え、組織自体をダイナミックに変えていくことによって競争力を生み出す、というのが自然な発想ではないでしょうか?この発想の転換が、プログラミングにおいても本質的に重要だと思われます。
現在の状況と今後の展望
現在のETの研究は、大きく分けると次の3つに分けられます(図3)。
1.問題をどのようにして確定節でモデル化するか?(仕様記述手法)
2.確定節仕様記述から、いかにしてより効率的なルールを生成するか?(ルール生成)
3.現実のハードウエアの上で生成したルールをいかに効率的に実行するか?(具体プログラム変換)
仕様記述に関しては、確定節の持つ、処理順を規定しない(手続きではなく、性質や制約の記述)という利点を生かし、GUIやWebアプリケーションなどの動的でインタラクティブなシステムをモデル化する研究が進められています。例えば、北海道大学のプログラミング言語の講義用のe-lerningシステムは、この技術を用いて仕様を記述し、生成されたルールをETルールインタプリタ(ETI)(http://assam.cims.hokudai.ac.jp/et/indexj.html)によるCGIで実行することにより運営されています。
仕様からのルール生成は、ETパラダイムのコア部分であり、今までも、そして現在でも最もホットな部分です。次々と新しい成果が生まれ、より広いクラスのルールを仕様から生成するための理論が着々と研究されています。
具体プログラム生成の部分は、筆者が大学院時代に直接かかわっていた部分であり、主に決定的なアルゴリズムを記述するET D(Deterministic)ルールから、Cやアセンブリー言語などで記述される具体命令型プログラムを生成するような研究をしてきました。ほかにも、非決定的なアルゴリズムを記述するET N(Non-Deterministic)ルールから、並列実行プログラムやハードウエア記述を生成するような研究も進められています。並列計算というクラスは、非決定的計算というクラスの一部として位置付けられるため、Nルールは並列プログラムやハードウエア、そしてインタラクティブなシステムの記述言語としても優れていることがわかってきています。
なお、本稿の執筆にあたって、以下を参考にしました。より深く ET パラダイムについて知りたい方は、以下に示す資料や論文が参考になるかと思います。
等価変換理論集中セミナー(http://www.slideshare.net/alohakun/e-tsemi2008-presentation)(アクセス:2008年11月)
一般公開されている論文のリスト(http://assam.cims.hokudai.ac.jp/akama/j/papers.html)(アクセス:2008年11月)
ET SITE(http://assam.cims.hokudai.ac.jp/et/indexj.html)(アクセス:2008年11月)