XML has become widely used in computer industry, and the importance of static analysis and verification of applications manipulating XML documents is increasing. For analyzing or proving any properties on XML manipulating programs, it is essential to have some model with theoretically well-defined semantics. After a long history of researches on models of tree-to-tree translations, a recent trend is to regard macro tree transducers (mtts) as a standard model for XML manipulation. Mtts are known to cover tree translations expressible by other models such as attributed tree transducers, MSO-definable tree translations, or pebble tree transducers, and the high expressiveness allows representing a vast range of practical XML translations. Yet, they ensure various good properties such as exact typechecking, streaming, decidable emptiness, and so on. Nevertheless, mtts still lack some properties desired for modeling XML translations. In particular, (1) mtts have poor closure properties on composition and (2) computational complexities for many problems on mtts are still unknown. A consequence of the first point is that, for example, an mtt composed with even a very simple pre- or post- tree translation cannot be represented by a single mtt. The lack of the composability implies difficulty of modular modeling; even if we could construct a model for each smaller subpart of a program separately, it is in general impossible to compose them up to obtain the model for the whole program. For the second point, the decidability is proved for many problems on mtts or their compositions, while the complexities and concrete algorithms solving the problems have been left open. This makes it difficult to estimate the computational hardness of each verification problem. One example of such a case is the membership problem of output languages, i.e., the problem determining whether a tree is a valid output with respect to the translation and a given input regular type. Although the problem is essential for, e.g., verifying that a program never generates 'wrong' outputs, its complexity had not been analyzed.

The goal of the thesis is to improve these shortcomings of mtts. First, to address the composability issue, a new model of tree-to-tree translation called multi-return macro tree transducer (mr-mtt) is introduced. As its name shows, an mr-mtt is an mtt extended with the capability of returning multiple tree fragments simultaneously, in contrast to an mtt that can return only one. We show that mr-mtts are closed under pre- and post- compositions with arbitrary deterministic total top-down tree transducers, and therefore enable modular modeling of tree-translations. We also show that mr-mtts are strictly more expressive than mtts, which at the same time formally proves as a corollary the folklore conjecture that mtts are not closed under post-compositions with top-down tree transducers.

Second, the thesis investigates complexity on compositions of mtts. We show that the data-complexity of the membership problem of output languages is in the class DSPACE(n) and is NP-complete. The crucial lemma of the proof is that any composition of finite number of mtts can be transformed into so-called garbage-free forms, meaning that any subtrees of intermediate results are actually used for generating the final output. Besides the complexity of output languages, we give another application of the garbage-free form: the complexity is shown for the 'translation membership' problem which determines whether a given pair of trees is an input-output pair of the translation.

近年、情報流通の手段としてXMLが標準的なフォーマットになるにつれ、XML文書を操作するプログラムの正しさを検証することは喫緊の課題となっている。このためには、XMLを操作するプログラムに対する適切かつ厳密なモデルが必要である。XMLは木構造を表現するフォーマットであるので、XML処理プログラムのモデルとは、木構造間の変換モデルに他ならない。このようなモデルとしては、マクロ木変換器(mtt)が標準的となっている。mttは、高い表現力を有するとともに、型検査や空変換判定が可能であるといった、検証に適した性質を多く持っている。しかし、(1) mttは合成に関して良い閉包性を持たない。また、(2) mttに関連する多くの問題の計算複雑性が未知である。本論文は、これら二つの問題を解決している。

本論文の第1章では、上述したような背景と本論文の概要が述べられている。特に、mttの性質について解説されている。

第2章では、(1)の合成可能性の問題を解決するために、新しい木変換モデルであるマルチリターンmtt (mr-mtt)を導入している。mr-mttは、同時に複数の木を計算できるようにmttを拡張したモデルである。

第3章では、mr-mttが任意の全域決定性木変換器の前後からの合成に関して閉じていること、すなわち、モジュラなモデル化を可能とすることが証明され、(1)の問題が解決されている。さらに、mr-mttがmttより真に表現力の高いモデルであることが示されている。

第4章では、単一のmttに対して、与えられた二つの木が変換の入出力ペアであるかどうかを判定する変換メンバシップ問題の計算複雑性が明らかにされている。すなわち、名前呼びのmtt(OI-mtt)に対して、この問題がNP完全かつ DSPACE(n) であることが示されている。また、値呼びのmtt(IO-mtt)に対しては、この問題が多項式時間で解けることが示されている。

第5章では、mttの合成列に対して、出力言語のメンバシップ判定問題が DSPACE(n) に位置し、同時にNP完全問題であることが、具体的なアルゴリズムと共に示されている。このために、任意のmttの合成列が、ガベージフリー形式と呼ばれる合成列へと変換可能であることが示され用いられている。さらに、変換メンバシップ問題の計算複雑性についても、単一のmttと同様に、明らかにされている。

第6章では、本論文の結論と今後の課題が述べられている。

mttの合成列は、木構造間の変換モデルとして現在研究されているものの中で最も表現力が高い。第2章で導入されたmr-mttの合成列も、mttの合成列として表現することができる。したがって、特に最後の章の結果は、mttの合成列の計算複雑性を明らかにしたことにより、木構造間の変換モデルの計算複雑性に対して、一応の決着を与えたということができる。論文全体としても、木構造間の変換モデルの研究に対して多大な貢献を与えている。

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