等価変換型プログラムをかじる

2008年11月26日(水)
若槻 俊宏

基礎理論からわかること

 いつの間にかねじれてしまった宣言型プログラミングの本質をあらためて考えてみると、本当にやりたかったことは、問題の定義とその解法を分離して、それぞれを独立して理論化していくことだったと考えられます。

 宣言型プログラミングは、仕様と実装を同一視するため、問題の定義に解法が深く侵入してしまい、分離不可能なものとなっています。そのため、問題ドメインごとに、効率化のためのさまざまなデータ構造と、それを扱うための手続き(制約ソルバー)が拡張された、多くの言語が次々と開発されるようになりました。結果として、命令型プログラミングと同様に、まとまりに欠ける混迷状態となってしまっています。

 プログラミングという概念が、より広く、より複雑なものになってきているのですから、どこが一番上のレイヤーで、どこが一番下なのかということは一意に決まりませんし、決めるべきではありません。また、問題ドメインが多様化してきているのですから、プログラミングの基礎となる理論は、特定の問題ドメインに依存しない一般的なものであることが望ましいと言えます(図1)。

等価変換型プログラミング

 さて、そのような理論的枠組みを構築するためには、プログラミングをどのように位置付けて考えれば良いのでしょうか?

 ここで1つの可能性として、等価変換(Equivalent Transformation;ET)に基づく問題解決の枠組みを紹介します。もちろん、これが絶対的な答えというつもりはありませんし、より良い枠組みがありましたら、ぜひ筆者に教えていただきたいところです。

 ETパラダイムはまだ歴史が浅く、入門書や教科書などは整備されていません。論文はたくさん出ていますが、研究者以外の方々にそれを読めというのは乱暴ですし、ハードルが高いのではないかと思います。正直なところ、今回の連載のような一般のメディアに紹介するのはまだ時期尚早なのではないかとも悩みました。しかし、この理論からは多くの示唆が得られると考え、何らかの参考になることを願い紹介させていただきます。

 とはいえ筆者自身は一介の学生にすぎないので、フォローできている理論の範囲はとても限定されたものです。また、間違いや誤解、理解不足な点も多く存在すると思います。以下は完ぺきな解説ではなく、あくまでも現時点での私なりの理解だということをあらかじめお断りさせていただきます。

 ETパラダイムは、もともとは90年代初頭に北海道大学で行われていた、コンピュータに自然言語を処理させるための基礎研究に端を発しています。本質的にあいまいである自然言語をコンピュータに理解させるためには、具体例からのルール抽出、ルールの最適化やそこからのプログラム生成、制約充足問題の並列処理などが複雑に絡み合った、極めて広範囲にまたがる高度なプログラム構築技術が必要とされたからです。

 人間が話す自然言語は、形式的に文法が定義された人工言語(プログラミング言語が代表例です)とは異なり、解釈が一意には定まらないあいまいなものです。そのため、(コンパイラの用語で言うところの)字句解析、構文解析、意味解析などの各工程をきれいに分割することが難しく、すべてを並列に行い、ありえない可能性をそのつど枝刈りしながら進めなくては、あっという間に可能性が爆発的に増えてしまいます。

 人間の知能という極めて高度なシステムを研究するAI(人工知能)分野では、常により強力なプログラミング技術が求められ、その発展を後押ししてきました。例えば「第3回:宣言型プログラミングの可能性と限界(http://www.thinkit.co.jp/article/157/3/)」に紹介したPrologも、もともとは自然言語処理研究から生まれた言語です。また、なじみ深い方が多いと思われるオブジェクト指向プログラミングも、もともとはAIの階層型の知識表現(フレーム理論)研究の影響があります。

議論の枠組みとしてのETパラダイム

 ETパラダイムには、さまざまなプログラミングモデルを統一的に議論したいというモチベーションもあります。そのためETの理論体系は、まずはETのプログラミングモデルに限定されない、より汎用的な仕様とプログラムの枠組みを定め、その上で確定節によるET仕様記述と、ETルールという書き換え規則によって定義されるETプログラムの枠組みを構築しています(図2)。

 これにより、同じ枠組みの上で、関数プログラミングや論理プログラミングなどの、ほかのプログラミングモデルを議論することが可能となります。当然、プログラミングモデルが異なれば、扱うデータ構造や手続きも異なってきます。そこでETの理論は、特殊化システム(Specialization System)という枠組みを定め、それらの違いを統一的に議論できる理論を構築しました。

 少し専門的になってしまいますが、特殊化システムによって、例えば関数プログラミングにおける遅延評価や論理プログラミングの単一化、それらの複合パラダイムである関数論理プログラミングのナローイングなど、さまざまな概念を統一的に議論できることがわかっています。

 ETパラダイムは、等価変換という一般的な原理に基づいて、形式的仕様記述から具体プログラム生成までの一貫した理論化を進めているので、その名が付いています。理論の肝となる「等価変換」とは、宣言的記述(確定節の集合)の意味を保存する変換という意味です。意味と言うと、何やら哲学的で難しい感じがしますが、要するに仕様(宣言的記述)よって定義される集合のことです。

 例えば、Prologの説明の際に出てきたappendという述語は、1番目のリストと2番目のリストを連結したリストが3番目の引数である、という関係を満たす集合の定義と考えることができます。この集合は無限集合で、例えばappend([], [], []),append([1], [], [1]), append([1], [2], [1, 2])のような形をしたアトムの具体例がその要素となります。

 そしてその集合において、どのようなデータ構造がアトムの引数に許されるのかということ、つまりプログラムが扱うデータ構造の種類は、特殊化システムの定義によって決まります。

仕様とプログラム、正当性関係

 ETの枠組みにおける仕様は、問題ドメインとそのドメインに含まれる具体的な問題の解(問題ドメインの背景知識)を確定節の集合で定義します。そしてETの枠組みにおけるプログラムは、解を得るための手続きをETルールの集合によって定義します。ETの計算の枠組みでは、状態を確定節の集合で表現します。そしてETルールは、確定節の集合を書き換えます。その際、変換前後での確定節集合の意味が等しいという、正当性関係を満たさなければなりません。

 プログラム合成のための枠組みを考えたとき、仕様に対する正当性という概念が厳密に定義されていることと、プログラムがルールによって記述されることが本質的に重要なのだと考えられています。ETルールは、単体で仕様に対する正当性を議論できるので、仕様からのプログラム生成を考えたとき、とても扱いやすい部品となるのです。

 ETの枠組みは、ETルールを仕様から自動生成するための理論的な枠組みを持っていますし、人間のひらめきによって記述したルールがETルールであることを証明する枠組みも持っています。これにより、機械による推論と、人間のひらめきを総動員し、効率的なプログラムを体系的に得るための理論が構築されています。

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月)

北海道大学大学院
北海道大学大学院 情報科学研究科 博士後期課程(D1)。当初はAI研究に興味を持っていたのだが、現在のプログラミング技術の水準では不十分だと考え、いつの間にかプログラミングの基礎理論を研究する道に。大学院時代は、等価変換に基づく問題解決、特にルール型プログラムから命令型プログラムを合成するための理論について研究。2008年11月21日付けで、京都マイクロコンピュータ株式会社に入社予定。今後はデバッガ技術に基づきソフトウエアとハードウエアの本質を突き詰めて行くつもりである。http://alohakun.blog7.fc2.com/

Think ITメルマガ会員登録受付中

Think ITでは、技術情報が詰まったメールマガジン「Think IT Weekly」の配信サービスを提供しています。メルマガ会員登録を済ませれば、メルマガだけでなく、さまざまな限定特典を入手できるようになります。

Think ITメルマガ会員のサービス内容を見る

他にもこの記事が読まれています