Higher-order patterns play important role for describing concise calculation rules. Higher-order patterns are capable of checking and binding subtrees far from the root, which is useful for program manipulation. To obtain the bindings of higher-order variables, higher-order matching is used.

However, there are three major problems from the practical viewpoint. First, it is difficult to explain why a particular desired matching result cannot be obtained because of the complicated higher-order matching algorithm. Second, the general higher-order matching algorithm is of high cost, which may be exponential time at worst. Third, the （possibly infinite） nondeterministic solutions of higher-order matching prevents it from being used in a functional setting.

To resolve these problems, we impose reasonable restrictions on the form of higher-order patterns to gain predictability, efficiency and determinism. Our deterministic patterns induce the linear time algorithm.

For the nondeterministic patterns, we impose restrictions on algorithm. We define reasonable orders on solutions and only return the largest solution. As a result, algorithm becomes linear time.

We show that our deterministic higher-order patterns and deterministic higher-order matching are powerful to support concise specification and efficient implementation of various kinds of program transformations for optimizations.

本論文は"Deterministic Higher-order Matching for Program Transformation" （和訳:プログラム変換のための決定性高階マッチングに関する研究）と題し、10章よりなる。

一般に、計算機プログラムにおいてその記述の簡潔さと実行効率の高さを同時に得ることは難しいが、プログラム運算によってこれらを両立させることができる。すなわち、簡潔なプログラムを書き、プログラム運算によってこれを変換して効率のよいプログラムを得ようということである。本論文で対象とする高階パターンは、このような変換で用いられる規則を記述する際に重要な役割を担うものである。これにより、木構造パターンを照合対象である木構造の根から離れた部分木に対して検査するという形で変換規則を簡潔に記述することができる。しかし、高階パターンによる照合検査を行うための高階マッチングにはいくつかの実用上の問題が存在する。高階マッチングは、一般には複数の解を与えるが、期待するマッチングを求める方法が確立されておらず、また、この問題はプログラムの大きさに対してNP困難であり一般のアルゴリズムでは実用的でないという点である。

本論文では、2つのアプローチでこのような問題を解決している。第一のものは、パターンの形を制限して、解がたかだか1つしか存在しないようなクラスを定めようとするアプローチである。もうひとつのアプローチは、解が1つしか存在しないようにマッチングの意味づけを行うというものである。それぞれにおいて、マッチングの対象となるプログラムの大きさに対して線形の計算時間で解を求めるアルゴリズムを提案している。さらに、これらのパターンとアルゴリズムがプログラム運算に有用であることを例示している。

第1章 Introductionでは、本研究の背景や目的を述べるとともに、本論文の構成を示している。

第2章 Preliminaries では、本論文で使用する記法や基本的な概念・用語を定義し、また、既存の手法について触れている。

第3章 Deterministic Higher-order Patterns では、マッチング対象となるどのような項ともたかだか1つしか解が存在しないような高階パターンのクラスを定めている。また、このクラスに属するパターンと任意の項とのマッチングを、項の大きさに対して線形時間で求めるアルゴリズムを与え、その健全性、完全性、停止性を示している。

第4章 Second-order Linear Deterministic Higher-order Patterns では、2階線形パターンが決定性を持つための必要条件を与えている。前章のような十分条件にはいろいろなものが考えられるが、必要条件を与えることで決定性を持つパターンの拡張の理論的限界の1つを示している。

第5章は Deterministic Semantics of Higher-order Patterns と題し、高階パターンマッチングの意味づけに制限を加えて解の一意性（決定性）をもたせている。これによって、高階パターンによる表現力は低下するが、メタプログラミングにより、この高階マッチングによっては得ることができなくなった解も生成できることを示している。

第6章 Implementation では、第3章〜第5章の理論的成果をもとに、プログラム運算のための結合子ライブラリを設計し、関数型言語Haskellを用いて実装している。

第7章 Case Studyと第8章 Examples は本論文で定めたパターンのクラスと結合子ライブラリの応用について述べている。第7章では高階パターンを用いてプログラム運算を高階パターンで簡潔に記述する方法を探り、第8章では結合子ライブラリを用いて種々のプログラム運算の例を通して本論文のアプローチの有効性を示している。

第9章 Related Workでは関連研究について述べ、第10章 Conclusion では得られた結論をまとめ今後の課題について述べている。

以上を要するに、本論文では、プログラム運算における高階パターンの有用性に着目し、実用面で課題とされていた効率的な決定性を有するマッチングアルゴリズムを開発するための手法を理論的に考察するとともに、開発されたアルゴリズムによりその有効性を実証している。これらの成果は数理情報学、計算機科学の発展に大きく貢献するものである。

よって本論文は博士（情報理工学）の学位請求論文として合格と認められる。