本論文では,最大マーク付け問題という最適化問題の効率の良いアルゴリズムの自動生成を行う.最大マーク付け問題とは,「要素に重みの与えられたあるデータxが与えられたときに,性質pを満たすマーク付けの中で与えられた重み関数wの値を最大にするものを求める」という問題である.この問題は,ナップサック問題,データマイニングの分野における最適連想規則問題等,現実の問題を含む,広範囲の問題を例として含んでおり,効率の良いアルゴリズムを求める手法を与えることは重要である.

　効率の良いプログラムを正しさの明らかな仕様から導出することによって,正しくかつ効率の良いアルゴリズムを得るというプログラム導出は,プログラム構築の一つの有用な方法である.プログラム導出を用いると,仕様の変更に柔軟に対応できるという利点がある.一般にはプログラマが考えて効率の良いプログラムを作成するが,その場合,仕様が変更されると,プログラムを正しく修正することは容易でない.それに対し,プログラム導出を用いると,仕様を変更するだけで,導出を同様に行えば,効率の良いプログラムを得ることができる.

　最大マーク付け問題は,再帰的グラフ(decomposableグラフ)という,制限されたグラフ上で考えられていた,最大部分(頂点または枝)集合問題を,マークを付ける問題として一般化し,再帰データ上の問題として定式化しなおしたものである.再帰的グラフを入力とする最大部分集合問題には,性質pが正則な述語であれば,線形時間アルゴリズムが存在することがBernらによって発見された.さらに,正則な述語を,基本的な述語と,∀,∃,∧,∨,¬を用いて作り上げられる単項二階論理式によって記述し,これから,線形時間アルゴリズムを機械的に導出する方法がBorieらによって考案された.この論理式の記述力は高く,頂点被覆問題,巡回セールスマン問題等,広範囲のグラフ上の問題を記述でき,理論的には興味深いが,素朴に線形時間アルゴリズムを導出するため,非常にサイズの大きなテーブルが生成され,計算量の定数係数が非常に大きくなり,全く実用にならないという問題点があった.我々の提案する方法は,この問題点を解決し,係数の小さい線形時間アルゴリズムを機械的に導出する.具体的には,例えば,最大部分列和(maximum segment sum)問題という問題においては,上記のBorieらの方法によるアルゴリズムと我々の提示する方法によるアルゴリズムを同一の基準で計算量評価すると,計算量の係数が,Borieらの方法では(4(2(2619)))2となるのに対し,我々の提示する方法では82となる.

　我々のアプローチのポイントは,性質pを再帰関数で記述するところにあり,これにより,再帰関数上でのプログラム変換を行うことができるようになる.本論文において提案する主要な定理は,「性質pが,有限の値域を持つ,mutumorphismsという再帰関数群で表されれば,最大マーク付け問題を解く線形時間アルゴリズムが存在し,それを機械的に導出できる」という最適化定理である.有限の値域を持つ,mutumorphismsという関数群で性質pを表すという条件は非常に緩い条件であり,柔軟に広範囲の性質を記述できる.導出されるアルゴリズムはテーブルを用いるものであるが,そのサイズが多くの場合において十分小さく,実用的なアルゴリズムとなる.テーブルサイズはmutumorphisms中のそれぞれの関数の値域のサイズで決まるが,多くの性質は,少数の述語(真偽値を返す関数)からなるmutumorphismsによって記述可能であるので,テーブルサイズが小さなアルゴリズムとなる.

　例として,リスト上の,最大独立部分列和問題を考えてみる.最大独立部分列和問題とは,重みを持つ要素からなるリストを入力として受け取り,どの2つの要素も隣接していないような要素集合のうち,重み和が最大のものを求めるという問題である.性質pは,マークの付けられた要素中には隣接している要素はないという性質であり,これをリスト上の再帰関数として記述すればよい.

p[x]=True

p(x:xs)=if marked x then p1 xs else p xs

p1[x]=not (marked x)

p1(x:xs)=not (marked x) ∧ p xs

関数p,p1はリスト上の有限mutumorphismsを成しており,最適化定理により,線形時間アルゴリズムが機械的に得られ,そのテーブルサイズは8である.一方,この性質pを単項二階論理式で書くと,

p=∀v1∀v2¬Adj(v1,v2)

Adj(v1,v2)=∃e1(Inc(v1,e1)∧Inc(v2,e1))∧¬(v1=v2)

のように記述されるが,テーブルサイズは2(2142)以上となる.

　提案した最適化定理は,広範囲に渡るさまざまな最適化問題に適用することができ,簡潔な仕様から,実用的線形時間アルゴリズムが機械的に得られる.適用例は,ナップサック問題,段落構成問題,データマイニングにおける最適連想規則問題など多岐にわたる.最適連想規則問題に対しては,既存のアルゴリズムと効率は同等であるが,新たなアルゴリズムが導出された.

　また,本研究で提案する手法を,実際に仕様から線形時間アルゴリズムを生成する自動生成システムとして実現する.MAG等の既存の変換システムを用いても実現は可能であるが,戦略の記述ができない等不自由な点があるため,新たに自動生成システムを作成する.このシステムは,Calculation Carrying Programという既存の研究に基づいて作成されている.

　Bird, de Moorにより,あるクラスの最適化問題(最大マーク付け問題を含む)に対し,関係を用いた仕様記述から効率の良いアルゴリズムを導出する,Thinning Theoryという理論が提案されている.これは,非常に広範囲の問題を扱えるが,導出に人間の洞察力が必要である.本研究は,最大マーク付け問題という問題クラスに注目し,機械的に導出する手法を与えている.我々の方法では,性質pが有限の値域を持つ関数からなるmutumorphismsで記述できさえすれば,あとは機械的に線形時間アルゴリズムに変換することができる.

　我々の方法の適用範囲は広いが,入力データが再帰的グラフで書けない場合には適用できない.例えば,2次元格子は,いくらでも大きな木幅をもつものが存在し,再帰的グラフでは表すことができないので,最大部分列和問題の2次元版の問題には適用できない.再帰的グラフは確かに制限されたグラフではあるが,応用可能範囲は広い.一例として,構造的プログラムの線形時間制御フロー解析が考えられる.構造的プログラムの制御フローグラフは再帰的グラフで表されることが知られており,最大マーク付け問題で定式化できる問題であれば,我々の方法が適用可能である.

　本論文は、Generation of Efficient Algorithms for Maximum Marking Problems(邦訳:最大マーク付け問題の効率的解法の自動生成)と題し、英文で書かれ8章からなる。本論文では、最大マーク付け問題という一群の最適化問題に対する効率のよいアルゴリズムの自動生成を行なう手法を論じたものである。対象としている問題のクラスには、一定の制限下ではあるが、ナップサック問題やデータマイニングにおける最適相関規則問題等、実際的な広範囲の問題が含まれており、これらの問題に対する効率のよいアルゴリズムを求める一般的な手法を与えることは工学的見地からもきわめて重要であるといえる。

　第1章Introductionでは、本論文で対象とする「最大マーク付け問題のクラス」を明確にし、その問題を解くアルゴリズム導出のための一般的な方法論として用いるプログラム変換、およびアルゴリズム導出手法を述べている。また、従来の研究にも触れ、本研究の位置付けを明確にしている。

　第2章Preliminariesでは、再帰データを対象とする基本的関数であるcatamorphismに関する性質とその上に成り立つ融合定理、および相互再帰関数の基本形であるmutumorphismsに関して成り立つ組化定理を扱い、これらが、アルゴリズム導出の基礎となっていることを述べている。

　第3章Maximum Marking Problemsでは、「最大マーク付け問題」を「要素に重みのついたデータが与えられたときに、性質pを満たすマーク付けの中で与えられた重み関数wの値を最大にするものを求めるという問題」として定式化し、この問題が、入力データに可能なすべてのマーク付けを行なって、性質pを満たすものだけを取り出して、それらのうちで重み関数wの値が最大のものを1つ選ぶという形で解くことができることを示している。本論文では、これを、最大マーク付け問題の仕様であるとして、この問題を解くアルゴリズムを求める方法を扱うことを明示している。

　第4章Derivation of Efficient Algorithmsでは、第3章で与えた仕様から効率のよいアルゴリズムを導出する手法を与えている。ここでは、重み関数としては、各要素に関数を適用したのち、すべてを足し合わせるという形で記述されるもののみを対象としている。本論文の主要な成果である最適化定理は、性質が有限mutumorphismsで記述されているならば、線形時間アルゴリズムが得られるというものであり、多くの場合に、定数係数の小さな実用的な線形時間アルゴリズムが得られると主張している。

　第5章Examplesでは、第4章に示した最適化定理が広範囲の最適化問題に適用することができることと、簡潔な仕様から実用的な線形時間アルゴリズムが機械的に得られることを例示している。適用例はとして、ナップサック問題、段落構成問題、データマイニングにおける最適相関規則問題など多岐に及んでいる。最適相関規則問題に対しては、既存のアルゴリズムと効率が同等である新たなアルゴリズムが導出されており、一般的な手法として、アルゴリズムの開発に有用であると主張している。

　第6章Automatic Generation of Efficient Programsでは、本研究で提案している手法に基づいて、仕様から線形時間アルゴリズムを生成するシステムの実現について述べている。そこでは、Calculation Carrying Programの考え方による新たな導出戦略の記述法を採用している。

　第7章Related Workでは、本研究に関連している研究に触れている。グラフ上で最大部分集合問題に対する単項二階論理式からの線形時間アルゴリズム生成法が知られているが、それによると定数係数がきわめて大きく、この方法が実用的ではないことを示し、本研究では論理式のかわりに再帰関数を用いることによって定数係数の爆発を解決していることを述べている。また、あるクラスの最適化問題(最大マーク付け問題を含む)に対しては、関係による仕様記述から効率のよいアルゴリズムを得るThinning Theoryが知られているが、そこでは導出時に人間の洞察力が必要とされ、本研究におけるアルゴリズム生成システムのような一般性のある機械的導出には適していないことを述べ、本研究がいくらか狭い問題を対象としているが、実用性においては勝っていると主張している。

　第8章Conclusionでは、本研究の総括を行ない、今後の研究の発展方向を示している。

　以上、これを要するに、本研究は、最大マーク付け問題に対する実用的線形時間アルゴリズムの導出法を提案するとともに、その方法によってアルゴリズム導出を行なうシステムを構築して、実際に現実のさまざまな問題に対する実用的アルゴリズムが単純な仕様から自動生成できることを示したものであり、この成果は情報工学上貢献するところが多大である。よって本論文は博士(工学)の論文として合格と認められる。