近年、計算機は非常に身近なものとなった。計算機の能力は格段に向上し、また安価で手に入るようにもなった。そのため、最近では多くの人が自分のための計算機を各々の目的のために用いるようになっている。しかし、計算機の能力を十分に活かすのはそれほど簡単なことではない。なぜなら、計算機が処理を行う速度はその処理手順に大きく依存するからである。良い手順を用いることができれば、計算機は非常に大きな問題すらもあっという間に処理することができる。しかし、処理手順が悪ければ、計算機は間違った結果を返したり、または処理を終えることができなかったりする。すなわち、計算機を利用するためには良い手順を用意することが不可欠である。「良い手順」はアルゴリズムと呼ばれ、様々な問題に対して効率の良いアルゴリズムが考案されてきた。しかし、近年の計算機の普及はさらに多くのアルゴリズムが必要となる状況を生んでいる。なぜなら、各人が各々の問題のためのアルゴリズムを必要としているからである。しかし、特に専門家以外にとって、効率の良いアルゴリズムを考案することは非常に難しい。そのため、アルゴリズム構成のための良い方法論が求められている。

プログラム運算は効率の良いプログラムの系統的な構成のための手法のひとつである。プログラム運算では、効率の良いプログラムを以下の二段階で構成する。まず、効率を気にすることなく明らかに正しいプログラムを構成する。次に、得られたプログラムに対し運算規則と呼ばれるプログラム変換規則を繰り返し適用することでその効率を向上する。プログラム運算では、明らかに正しいプログラムから正しさの証明された変換規則を用いて効率の良いプログラムを導出するため、得られたプログラムの正しさはその構成から保証されるという長所がある。また、アルゴリズム類型を表現するプログラムを考えることにより、アルゴリズムの構成も同様に議論できる点も長所である。

本論文ではプログラム運算に基づいたアルゴリズムの自動構成に取り組む。効率の良いアルゴリズムの導出の際には、プログラムに陽には現れていない性質を発見・証明する必要があることが多いが、そのような性質を自動的に確認するのは一般に困難である。そのため、プログラム運算によるアルゴリズムの自動構成は十分には達成されていなかった。本論文では、プログラム変換器に対して適切な情報を与える手段を提供することでこの問題の解決を試みる。具体的にはまず、プログラム変換器に対して適切な情報を与えることのできる運算規則を用意する。さらに、それらの運算規則を有効活用するためのプログラミング言語を設計する。提案した運算規則及びプログラミング言語によって、効率の良いアルゴリズムのための情報はプログラム変換器にも確認できる形で提示され、自動的なアルゴリズム構成が達成される。

本論文では大きく分けて二種類のアルゴリズム類型の自動構成に取り組む。ひとつは動的計画法アルゴリズムの構成であり、もうひとつは分割統治アルゴリズムの構成である。その両方について、アルゴリズム導出のための運算規則を用意し、運算規則を活用するためのプログラミング言語を設計し、それらに基づいたアルゴリズムの自動構成器を構成する。

本論文の前半では組合せ最適化問題について議論する。組合せ最適化問題とは、離散的な解候補から最適なものを発見する問題であり、アルゴリズム構成における重要な問題のひとつである。組合せ最適化問題に対するプログラム運算によるアルゴリズム構成に関しては、Bird、de Moor、Curtisらによる「貪欲定理」に関するものが挙げられる。貪欲定理は組合せ最適化問題に対する効率の良いアルゴリズムの導出をプログラム運算の立場から定式化したものである。しかし、この定理はアルゴリズムの自動導出には不向きであった。自動的なアルゴリズム構成の立場からは、Sasanoらによる最大マーク付け問題の統一解法が挙げられる。これは、最大マーク付け問題と呼ばれるある種の組合せ最適化問題に対し、その効率的な解法を問題の仕様記述から自動的に導出するものである。しかし、この手法ではグラフを扱う問題など多くの興味深い問題を扱うことができなかった。

組合せ最適化問題に対する効率の良いアルゴリズムを構成するため、本論文では最適解を定める順序関係に着目する。特に、効率の良いアルゴリズムに必要な「適切な場合分け」を特徴づけることにより、動的計画法アルゴリズムの導出のための運算規則を提案する。この運算規則は最大マーク付け問題に関する既知の結果の一般化にあたる。かつ、この運算規則は広い範囲の問題を対象にしており、例えばグラフを扱う問題に対しても適用できる。提案した運算規則の効果は最短路問題及びその亜種に対する効率の良いアルゴリズムの導出を通して確認する。

さらに、前述の成果に基づき、最適経路問題に対する統一的な枠組みを提案する。最適経路問題とはグラフ中の最適な経路を求める問題である。本論文では最適経路問題のための領域特化言語を提案し、その言語で特定された最適経路を効率よく求める最適経路問合せ器の実現を示す。本論文で提案する領域特化言語は、再帰関数による最適経路の柔軟な記述が可能であるだけでなく、その記述から効率良い最適経路問合せアルゴリズムが自動的に得られるよう設計されている。さらに、提案する最適経路問合せアルゴリズムは既知の効率の良いいくつかのアルゴリズムの一般化になっている。最適経路問合せ器の実装及験結果についても報告する。

本論文の後半では、分割統治アルゴリズムの導出について議論する。分割統治アルゴリズムは複数の演算器による並列実行に適しているため、近年特にその重要性が増している。

本論文では「第三準同型定理」と呼ばれる関数プログラミングの分野で知られている定理に着目する。第三準同型定理は、特定の形式の二種類の逐次プログラムによってある計算が記述できれば、分割統治アルゴリズムによってもその計算を行うことができる、ということを示している。この定理の特徴的な点は、二種類の逐次プログラムが分割統治アルゴリズム導出に十分な情報を保持していることを指摘している点にある。そのため、二種類の逐次プログラムからであれば、分割統治アルゴリズムの自動構成を比較的容易に達成できることが期待できる。

本論文ではまず、列から値を計算する問題について、第三準同型定理が確かに分割統治アルゴリズムを導出する際に効果的であることを確認する。次に、二分木の上での第三準同型定理を提案する。二分木に対する効率的な並列アルゴリズムの系統的な構成法としては、並列木縮約手法に基づいたものが知られていた。これをふまえ、並列木縮約手法と列上の第三準同型定理の関係を示し、二分木を扱う計算に対する第三準同型定理を提案する。手法の要点は木上の経路に着目することにより列の上での結果を活用する点にある。さらに、これらの結果を一般化し、子の数が高々定数の木に対する一般的な議論を行う。具体的には、子の数が高々定数の木に対する並列木縮約アルゴリズムおよび第三準同型定理を与え、これらが列の上の既知の結果の一般化となっていることを確認する。

本論文ではさらに第三準同型定理に基づいた自動並列化手法を提案する。まず、自動並列化のための領域特化言語を設計する。この言語は第三準同型定理と定理自動証明手法を活用できるよう設計されている。この言語に基づき二種類の自動並列化手法について議論を行う。ひとつは自動逆化に基づく手法であり、もうひとつは生成検査に基づく手法である。本論文では特に後者の手法についてその実装と実験の結果を報告する。これらの手法は共に非自明ないくつかの問題に対して現実的な時間で並列プログラムを生成する。また、これら二種類の手法の長短についても議論を行う。

本論文は運算手法に基づいたアルゴリズムの自動構成について、運算規則の構成から自動化まで、一貫した立場からの議論を行う試みである。今後の課題としては、別のアルゴリズム類型についての議論、他のアルゴリズム自動構成手法との連携、定理自動証明手法のより積極的な利用、などが挙げられる。

これまでにもさまざまな問題に対するアルゴリズムが考案されてきているが、近年はさらに多くのアルゴリズムが求められている。しかし、一般利用者が効率のよいアルゴリズムを考案して実現することはきわめて難しく、個々の問題のためのアルゴリズムを簡便に得るための方法論が求められている。このような課題に対して系統的にアルゴリズムを導出する手法であるプログラム運算の枠組みでアルゴリズムを構成することが考えられる。

本論文は "Calculational Approach to Automatic Algorithm Construction (運算手法によるアルゴリズムの自動構成に関する研究)" と題し、英文で書かれ全8章から成る。本論文では、動的計画法アルゴリズムと分割統治アルゴリズムとの2種類のアルゴリズム類型を対象に、具体的な問題解決のためのアルゴリズムを自動的に構成する手法を論じている。いずれに対しても、アルゴリズム導出のための運算規則を用意し、運算規則を活用するための領域向けの記述言語を設計し、それらに基づいてアルゴリズムを自動的に構成するシステムを実現している。

第1章 Introduction では、本研究の背景とプログラム運算(Program Calculation)の概要を述べ、アルゴリズムの自動的な構築と記述言語の関係を説明している。また、本論文の貢献と論文の構成を示した後で関連研究に触れている。

第2章 Basis of Program Calculation では基本的な記法と概念を説明している。多くはBirdとde Moorによる著書Algebra of Programmingに従うものとしている。

第3章 Calculational Laws for Combinatorial Optimization Problems では、組合せ最適化問題におけるアルゴリズムの導出について従来の研究成果を紹介し、アルゴリズムの自動構成の観点からそれらの特徴を述べている。種々の離散構造の上で効率のよいアルゴリズムを導出するには、Bird、de Moor、Curtisらによる「貪欲定理」があるが、この定理は一般的ではあるものの自動構成には適していないとしている。また、ある種の組合せ最適化問題に対して問題の仕様記述から効率的な解法を導出するSasanoらによる最大マーク付け問題はアルゴリズムの自動導出には適しているが、グラフなど多くの興味深い問題を扱うことができていないと述べている。このような考察から、これら両者の長所を兼ね備えたプログラム運算規則の構築が必要であると結論づけている。

第4章 Compositional Approach to Monotonicity では、組合せ最適化問題に対する効率のよいアルゴリズムを構成するための枝刈りの順序関係に着目して論じている。具体的には、問題を特徴づける解候補の生成と許容解が満たすべき制約条件と最適化を行うための順序関係のそれぞれについて、アルゴリズム中の枝刈りを運算規則の形で定式化して「適切な場合分け」を特徴づけ、動的計画法アルゴリズムの導出のための運算規則を示している。これは最大マーク付け問題に関する既知の結果の一般化になっており、グラフを扱う問題に対しても適用できるもので、貪欲定理よりもはるかに自動化が容易であると主張している。ここで提案した運算規則の効果は最短路問題等に対する効率のよいアルゴリズムの導出を通して確認している。

第5章 A General Framework for Optimal Path Querying では、グラフ中の最適経路を求める問題に対する統一的な枠組みを提案している。そこでは、この領域向けに効率的アルゴリズムの自動構成に適した最適基準記述用言語を設計し、その言語による記述から最適解を求める最適経路問合せ器の実現法を与えている。この最適経路問合せアルゴリズムが効率のよい既知のものの一般化になっていることも示している。また、実現した最適経路問合せ器を用いた実験により、その実行時間が個別に人手で開発された既知のものに比べても数倍程度しか遅くないことを確認して、人手を介することなく自動的に実用的なプログラムを構成できることを実証している。

第6章 Calculational Laws for Parallel Programming では分割統治アルゴリズムの導出を扱っている。そこでは、同一の問題を解く特定の形の2種類の逐次的アルゴリズムの記述が存在するならば、その問題に対する分割統治アルゴリズムが存在するという、列に対する「第3準同型定理」に着目し、それを拡張して二分木の上の第3準同型定理を提案し、同時に分割統治アルゴリズムの導出法を与えている。この考え方の要点は、二分木上の経路に着目して列に対する定理を活用する点にある。さらに、部分木の個数が定数であるような木に対する第3準同型定理を与え、これが列に対する既知の結果の一般化となっていることを述べている。

第7章 Automatic Parallelization via the Third Homomorphism Theoremでは、第6章で扱った第3準同型定理に基づいた分割統治アルゴリズムによる逐次プログラムの自動並列化手法を扱っている。そこでは、第3準同型定理と限定記号除去による自動証明を活用できるように設計した自動並列化のための領域向け言語を提案している。そこでは、自動並列化に際して、可能性のあるプログラム候補を生成してそこから適切なものを選択するという生成-検査に基づく手法を詳述し、それを実現して実験結果を報告して有効性を主張している。

第8章 Conclusion では本論文の成果を取りまとめている。各章で論じているように、本論文では、動的計画法によるアルゴリズムと分割統治アルゴリズムに関して、特定の領域向けに設計された言語による問題の記述から自動的にアルゴリズムを構成するための数理的な基盤構築を行ったと述べている。これらの成果をもとに、別のアルゴリズム類型をも対象とするとともに、他のアルゴリズム自動構成手法との連携や定理自動証明手法の積極的な利用などがあることをあげて、今後の研究への展望を与えている。

以上を要するに、本論文はアルゴリズムの自動構成に関して新たな方法論を理論的に展開するとともに、システムを実現してその手法の有効性を実証したもので、数理情報学、計算機科学の発展に寄与するところが大きい。よって本論文は博士(情報理工学)の学位請求論文として合格と認められる。